diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 25f841e..6c356ec 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -1,11 +1,6 @@ name: Docs -on: - # Runs on pushes targeting the default branch and pull requests. - push: - branches: [main] - pull_request: - types: [opened, reopened] +on: [push] concurrency: group: ${{ github.workflow }}-${{ github.ref_name }} @@ -60,22 +55,25 @@ jobs: files: | docs/**/*.ipynb - # - name: Run documentation notebooks - # run: | - # poetry run jupyter nbconvert --execute --to notebook --inplace ${{ steps.glob.outputs.paths }} + # - name: Run documentation notebooks + # run: | + # poetry run jupyter nbconvert --execute --to notebook --inplace ${{ steps.glob.outputs.paths }} --ExecutePreprocessor.kernel_name=python3 - name: Generate docs working-directory: docs/ run: make html - name: Setup Pages + if: github.ref == 'refs/heads/main' uses: actions/configure-pages@v5 - name: Upload artifact + if: github.ref == 'refs/heads/main' uses: actions/upload-pages-artifact@v3 with: path: "docs/_build/html/" - name: Deploy to GitHub Pages + if: github.ref == 'refs/heads/main' id: deployment uses: actions/deploy-pages@v4 diff --git a/Untitled.ipynb b/Untitled.ipynb deleted file mode 100644 index dba60c4..0000000 --- a/Untitled.ipynb +++ /dev/null @@ -1,43 +0,0 @@ -{ - "cells": [ - { - "cell_type": "code", - "execution_count": 1, - "id": "c4d32ada-47ed-412e-95dd-3f16880fa568", - "metadata": {}, - "outputs": [], - "source": [ - "import examples" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "1935eab3-9731-4cd3-9fde-cbd22a25eea3", - "metadata": {}, - "outputs": [], - "source": [] - } - ], - "metadata": { - "kernelspec": { - "display_name": "Python 3 (ipykernel)", - "language": "python", - "name": "python3" - }, - "language_info": { - "codemirror_mode": { - "name": "ipython", - "version": 3 - }, - "file_extension": ".py", - "mimetype": "text/x-python", - "name": "python", - "nbconvert_exporter": "python", - "pygments_lexer": "ipython3", - "version": "3.12.7" - } - }, - "nbformat": 4, - "nbformat_minor": 5 -} diff --git a/docs/getting_started/mdp.ipynb b/docs/getting_started/mdp.ipynb index 9a6402d..931d68b 100644 --- a/docs/getting_started/mdp.ipynb +++ b/docs/getting_started/mdp.ipynb @@ -1,5 +1,12 @@ { "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Example MDP" + ] + }, { "cell_type": "code", "execution_count": 1, @@ -18,7 +25,7 @@ { "data": { "text/plain": [ - "" + "" ] }, "execution_count": 2, @@ -275,7 +282,7 @@ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "997d4600f467461ea1373a3ada686982", + "model_id": "f113a3bb73e541179bb0eb95c0cacbb4", "version_major": 2, "version_minor": 0 }, @@ -285,44 +292,6 @@ }, "metadata": {}, "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "text/html": [ - "" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "data": { - "application/vnd.jupyter.widget-view+json": { - "model_id": "f45b2ef528d34e9fadcd1202511779a3", - "version_major": 2, - "version_minor": 0 - }, - "text/plain": [ - "HBox(children=(Output(), Output()))" - ] - }, - "metadata": {}, - "output_type": "display_data" } ], "source": [ @@ -347,341 +316,13 @@ "outputs": [ { "data": { - "text/html": [ - "\n", - "\n", - "\n", - " \n", - " Network\n", - " \n", - " \n", - " \n", - " \n", - "
\n", - " \n", - " \n", - "\n" - ], + "application/vnd.jupyter.widget-view+json": { + "model_id": "8d832d9188a642f0aeb3b4b740eb1006", + "version_major": 2, + "version_minor": 0 + }, "text/plain": [ - "" + "Output()" ] }, "metadata": {}, @@ -716,9 +357,9 @@ ], "metadata": { "kernelspec": { - "display_name": "Python (stormvogel)", + "display_name": ".venv", "language": "python", - "name": "stormvogel-env" + "name": "python3" }, "language_info": { "codemirror_mode": { @@ -730,7 +371,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.12.7" + "version": "3.12.6" } }, { diff --git a/docs/getting_started/model.html b/docs/getting_started/model.html new file mode 100644 index 0000000..9ea6fd0 --- /dev/null +++ b/docs/getting_started/model.html @@ -0,0 +1,196 @@ + + diff --git a/docs/getting_started/simulator.ipynb b/docs/getting_started/simulator.ipynb index 0dbb8d1..f7fafbe 100644 --- a/docs/getting_started/simulator.ipynb +++ b/docs/getting_started/simulator.ipynb @@ -1,19 +1,27 @@ { "cells": [ + { + "cell_type": "markdown", + "id": "a7245ed2", + "metadata": {}, + "source": [ + "# The simulator" + ] + }, { "cell_type": "code", - "execution_count": null, + "execution_count": 7, "id": "a8ddc37c-66d2-43e4-8162-6be19a1d70a1", "metadata": {}, "outputs": [], "source": [ - "from stormvogel import visualization, show, simulator\n", + "from stormvogel import show\n", "import stormvogel.model" ] }, { "cell_type": "code", - "execution_count": null, + "execution_count": 8, "id": "cab40f99-3460-4497-8b9f-3d669eee1e11", "metadata": {}, "outputs": [], @@ -86,10 +94,31 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 9, "id": "eb0fadc0-7bb6-4c1d-ae3e-9e16527726ab", "metadata": {}, - "outputs": [], + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "ModelType.MDP with name None\n", + "\n", + "States:\n", + "State 0 with labels ['init'] and features {}\n", + "State 1 with labels ['carchosen'] and features {}\n", + "State 2 with labels ['open'] and features {}\n", + "State 3 with labels ['goatrevealed'] and features {}\n", + "State 4 with labels ['done', 'target'] and features {}\n", + "\n", + "Transitions:\n", + "0.3333333333333333 -> State 1 with labels ['carchosen'] and features {}\n", + "1.0 -> State 2 with labels ['open'] and features {}\n", + "1.0 -> State 3 with labels ['goatrevealed'] and features {}\n", + "1.0 -> State 4 with labels ['done', 'target'] and features {}\n" + ] + } + ], "source": [ "#we want to simulate this model. That is, we start at the initial state and then\n", "#we walk through the model according to transition probabilities.\n", @@ -109,12 +138,33 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 10, "id": "59ac1e34-866c-42c4-b19b-c2a15c830e2e", "metadata": { "scrolled": true }, - "outputs": [], + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "ModelType.MDP with name None\n", + "\n", + "States:\n", + "State 0 with labels ['init'] and features {}\n", + "State 1 with labels ['carchosen'] and features {}\n", + "State 2 with labels ['open'] and features {}\n", + "State 3 with labels ['goatrevealed'] and features {}\n", + "State 4 with labels ['done'] and features {}\n", + "\n", + "Transitions:\n", + "0.3333333333333333 -> State 1 with labels ['carchosen'] and features {}\n", + "1.0 -> State 2 with labels ['open'] and features {}\n", + "1.0 -> State 3 with labels ['goatrevealed'] and features {}\n", + "1.0 -> State 4 with labels ['done'] and features {}\n" + ] + } + ], "source": [ "#it still chooses random actions but we can prevent this by providing a scheduler:\n", "taken_actions = {}\n", @@ -128,21 +178,237 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 11, "id": "22871288-755c-463f-9150-f207c2f5c211", "metadata": {}, - "outputs": [], + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " " + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], "source": [ "#we can also visualize the partial model that we get from the simulator:\n", - "show.show(partial_model)\n" + "vis = show.show(partial_model, save_and_embed=True)" ] }, { "cell_type": "code", - "execution_count": null, + "execution_count": 12, "id": "34d0c293-d090-4e3d-9e80-4351f5fcba62", "metadata": {}, - "outputs": [], + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "initial state --(action: empty)--> state: 2 --(action: open0)--> state: 7 --(action: empty)--> state: 17 --(action: stay)--> state: 33\n" + ] + } + ], "source": [ "#we can also use another simulator function that returns a path instead of a partial model:\n", "path = stormvogel.simulator.simulate_path(mdp, steps=4, scheduler=scheduler, seed=123456)\n", @@ -161,9 +427,9 @@ ], "metadata": { "kernelspec": { - "display_name": "Python (stormvogel)", + "display_name": ".venv", "language": "python", - "name": "stormvogel-env" + "name": "python3" }, "language_info": { "codemirror_mode": { @@ -175,7 +441,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.12.7" + "version": "3.12.6" } }, "nbformat": 4, diff --git a/examples/simple_ma.py b/examples/simple_ma.py index e64dc03..5e43d6e 100644 --- a/examples/simple_ma.py +++ b/examples/simple_ma.py @@ -7,7 +7,7 @@ def create_simple_ma(): init = ma.get_initial_state() - # We have 2 actions + # We have 5 actions init.set_transitions( [ ( @@ -29,9 +29,6 @@ def create_simple_ma(): # we add self loops to all states with no outgoing transitions ma.add_self_loops() - # we delete a state - ma.remove_state(ma.get_state_by_id(3), True) - return ma diff --git a/notebooks/die.ipynb b/notebooks/die.ipynb index d9c9650..ad2e2c6 100644 --- a/notebooks/die.ipynb +++ b/notebooks/die.ipynb @@ -29,7 +29,7 @@ { "data": { "application/vnd.jupyter.widget-view+json": { - "model_id": "e474efd2c4d741d7bb54ae89c3fbc78c", + "model_id": "697dcf595c434725965c4c078e4190c3", "version_major": 2, "version_minor": 0 }, @@ -67,9 +67,9 @@ ], "metadata": { "kernelspec": { - "display_name": "Python (stormvogel)", + "display_name": ".venv", "language": "python", - "name": "stormvogel-env" + "name": "python3" }, "language_info": { "codemirror_mode": { @@ -81,7 +81,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.11.2" + "version": "3.12.6" } }, "nbformat": 4, diff --git a/stormvogel/mapping.py b/stormvogel/mapping.py index 110db3a..565670c 100644 --- a/stormvogel/mapping.py +++ b/stormvogel/mapping.py @@ -324,6 +324,7 @@ def add_states( """ helper function to add the states from the sparsemodel to the model """ + model.new_state() for state in sparsemodel.states: if state.id == 0: for label in state.labels: @@ -357,7 +358,7 @@ def map_dtmc(sparsedtmc: stormpy.storage.SparseDtmc) -> stormvogel.model.Model: """ # we create the model (it seems names are not stored in sparsedtmcs) - model = stormvogel.model.new_dtmc(name=None) + model = stormvogel.model.new_dtmc(name=None, create_initial_state=False) # we add the states add_states(model, sparsedtmc) @@ -388,7 +389,7 @@ def map_mdp(sparsemdp: stormpy.storage.SparseDtmc) -> stormvogel.model.Model: """ # we create the model - model = stormvogel.model.new_mdp(name=None) + model = stormvogel.model.new_mdp(name=None, create_initial_state=False) # we add the states add_states(model, sparsemdp) @@ -430,7 +431,7 @@ def map_ctmc(sparsectmc: stormpy.storage.SparseCtmc) -> stormvogel.model.Model: """ # we create the model (it seems names are not stored in sparsectmcs) - model = stormvogel.model.new_ctmc(name=None) + model = stormvogel.model.new_ctmc(name=None, create_initial_state=False) # we add the states add_states(model, sparsectmc) @@ -465,7 +466,7 @@ def map_pomdp(sparsepomdp: stormpy.storage.SparsePomdp) -> stormvogel.model.Mode """ # we create the model (it seems names are not stored in sparsepomdps) - model = stormvogel.model.new_pomdp(name=None) + model = stormvogel.model.new_pomdp(name=None, create_initial_state=False) # we add the states add_states(model, sparsepomdp) @@ -511,7 +512,7 @@ def map_ma(sparsema: stormpy.storage.SparseMA) -> stormvogel.model.Model: """ # we create the model (it seems names are not stored in sparsemas) - model = stormvogel.model.new_ma(name=None) + model = stormvogel.model.new_ma(name=None, create_initial_state=False) # we add the states add_states(model, sparsema) diff --git a/stormvogel/model.py b/stormvogel/model.py index 1f7da00..4476195 100644 --- a/stormvogel/model.py +++ b/stormvogel/model.py @@ -79,8 +79,8 @@ def __init__( "There is already a state with this id. Make sure the id is unique." ) - names = [state.name for state in self.model.states.values()] - if name in names: + used_names = [state.name for state in self.model.states.values()] + if name in used_names: raise RuntimeError( "There is already a state with this name. Make sure the name is unique." ) @@ -142,16 +142,28 @@ def available_actions(self) -> list["Action"]: def get_outgoing_transitions( self, action: "Action | None" = None - ) -> list[tuple[Number, "State"]]: + ) -> list[tuple[Number, "State"]] | None: """gets the outgoing transitions""" if action and self.model.supports_actions(): - branch = self.model.transitions[self.id].transition[action] + if self.id in self.model.transitions.keys(): + branch = self.model.transitions[self.id].transition[action] + return branch.branch elif self.model.supports_actions() and not action: raise RuntimeError("You need to provide a specific action") else: - branch = self.model.transitions[self.id].transition[EmptyAction] - - return branch.branch + if self.id in self.model.transitions.keys(): + branch = self.model.transitions[self.id].transition[EmptyAction] + return branch.branch + return None + + def is_absorbing(self, action: "Action | None" = None) -> bool: + """returns if the state has a nonzero transition going to another state or not""" + transitions = self.get_outgoing_transitions(action) + if transitions is not None: + for transition in transitions: + if float(transition[0]) > 0 and transition[1] != self: + return False + return True def __str__(self): res = f"State {self.id} with labels {self.labels} and features {self.features}" @@ -162,8 +174,6 @@ def __str__(self): def __eq__(self, other): if isinstance(other, State): if self.id == other.id: - self.labels.sort() - other.labels.sort() if self.model.supports_observations(): if self.observation is not None and other.observation is not None: observations_equal = self.observation == other.observation @@ -171,7 +181,9 @@ def __eq__(self, other): observations_equal = True else: observations_equal = True - return self.labels == other.labels and observations_equal + return ( + sorted(self.labels) == sorted(other.labels) and observations_equal + ) return False return False @@ -222,9 +234,7 @@ def __str__(self): def __eq__(self, other): if isinstance(other, Branch): - self.branch.sort() - other.branch.sort() - return self.branch == other.branch + return sorted(self.branch) == sorted(other.branch) return False def __add__(self, other): @@ -261,11 +271,9 @@ def __str__(self): def __eq__(self, other): if isinstance(other, Transition): - self_values = list(self.transition.values()) - other_values = list(other.transition.values()) - self_values.sort() - other_values.sort() - return self_values == other_values + return sorted(list(self.transition.values())) == sorted( + list(other.transition.values()) + ) return False def has_empty_action(self) -> bool: @@ -309,7 +317,6 @@ def transition_from_shorthand(shorthand: TransitionShorthand) -> Transition: @dataclass(order=True) class RewardModel: """Represents a state-exit reward model. - dtmc.delete_state(dtmc.get_state_by_id(1), True, True) Args: name: Name of the reward model. rewards: The rewards, the keys are the state's ids (or state action pair ids). @@ -340,10 +347,10 @@ class Model: name: An optional name for this model. type: The model type. states: The states of the model. The keys are the state's ids. + transitions: The transitions of this model. actions: The actions of the model, if this is a model that supports actions. rewards: The rewardsmodels of this model. exit_rates: The exit rates of the model, optional if this model supports rates. - transitions: The transitions of this model. markovian_states: list of markovian states in the case of a ma. """ @@ -359,7 +366,9 @@ class Model: # In ma's we keep track of markovian states markovian_states: list[State] | None - def __init__(self, name: str | None, model_type: ModelType): + def __init__( + self, name: str | None, model_type: ModelType, create_initial_state: bool = True + ): self.name = name self.type = model_type self.transitions = {} @@ -390,8 +399,9 @@ def __init__(self, name: str | None, model_type: ModelType): else: self.markovian_states = None - # Add the initial state - self.new_state(["init"]) + # Add the initial state if specified to do so + if create_initial_state: + self.new_state(["init"]) def supports_actions(self): """Returns whether this model supports actions.""" @@ -405,14 +415,18 @@ def supports_observations(self): """Returns whether this model supports observations.""" return self.type == ModelType.POMDP - def is_well_defined(self) -> bool: - """Checks if all sums of outgoing transition probabilities for all states equal 1""" + def is_stochastic(self) -> bool: + """For discrete models: Checks if all sums of outgoing transition probabilities for all states equal 1 + For continuous models: Checks if all sums of outgoing rates sum to 0 + """ - if self.get_type() in (ModelType.DTMC, ModelType.MDP, ModelType.POMDP): + if not self.supports_rates(): for state in self.states.values(): for action in state.available_actions(): sum_prob = 0 - for transition in state.get_outgoing_transitions(action): + transitions = state.get_outgoing_transitions(action) + assert transitions is not None + for transition in transitions: if ( isinstance(transition[0], float) or isinstance(transition[0], Fraction) @@ -421,23 +435,34 @@ def is_well_defined(self) -> bool: sum_prob += transition[0] if sum_prob != 1: return False - elif self.get_type() in ( - ModelType.CTMC, - ModelType.MA, - ): - # TODO make it work for these models - raise RuntimeError("Not implemented") + else: + for state in self.states.values(): + for action in state.available_actions(): + sum_rates = 0 + transitions = state.get_outgoing_transitions(action) + assert transitions is not None + for transition in transitions: + if ( + isinstance(transition[0], float) + or isinstance(transition[0], Fraction) + or isinstance(transition[0], int) + ): + sum_rates += transition[0] + if sum_rates != 0: + return False return True def normalize(self): """Normalizes a model (for states where outgoing transition probabilities don't sum to 1, we divide each probability by the sum)""" - if self.get_type() in (ModelType.DTMC, ModelType.POMDP, ModelType.MDP): + if not self.supports_rates(): self.add_self_loops() for state in self.states.values(): for action in state.available_actions(): sum_prob = 0 - for tuple in state.get_outgoing_transitions(action): + transitions = state.get_outgoing_transitions(action) + assert transitions is not None + for tuple in transitions: if ( isinstance(tuple[0], float) or isinstance(tuple[0], Fraction) @@ -446,7 +471,7 @@ def normalize(self): sum_prob += tuple[0] new_transitions = [] - for tuple in state.get_outgoing_transitions(action): + for tuple in transitions: if ( isinstance(tuple[0], float) or isinstance(tuple[0], Fraction) @@ -460,11 +485,8 @@ def normalize(self): self.transitions[state.id].transition[ action ].branch = new_transitions - elif self.get_type() in ( - ModelType.CTMC, - ModelType.MA, - ): - # TODO: As of now, for the CTMCs and MAs we only add self loops + else: + # for ctmcs and mas we currently only add self loops self.add_self_loops() def __free_state_id(self): @@ -479,15 +501,16 @@ def add_self_loops(self): """adds self loops to all states that do not have an outgoing transition""" for id, state in self.states.items(): if self.transitions.get(id) is None: - self.set_transitions(state, [(float(1), state)]) + self.set_transitions( + state, [(float(0) if self.supports_rates() else float(1), state)] + ) def all_states_outgoing_transition(self) -> bool: """checks if all states have an outgoing transition""" - all_states_outgoing_transition = True for state in self.states.items(): if self.transitions.get(state[0]) is None: - all_states_outgoing_transition = False - return all_states_outgoing_transition + return False + return True def add_markovian_state(self, markovian_state: State): """Adds a state to the markovian states.""" @@ -578,27 +601,51 @@ def new_action(self, name: str, labels: frozenset[str] | None = None) -> Action: self.actions[name] = action return action - def remove_state(self, state: State, normalize_and_reassign_ids: bool = True): + def reassign_ids(self): + """reassigns the ids of states, transitions and rates to be in order again""" + self.states = { + new_id: value + for new_id, (old_id, value) in enumerate(sorted(self.states.items())) + } + + self.transitions = { + new_id: value + for new_id, (old_id, value) in enumerate(sorted(self.transitions.items())) + } + + if self.supports_rates and self.exit_rates is not None: + self.exit_rates = { + new_id: value + for new_id, (old_id, value) in enumerate( + sorted(self.exit_rates.items()) + ) + } + + def remove_state( + self, state: State, normalize: bool = True, reassign_ids: bool = True + ): """properly removes a state, it can optionally normalize the model and reassign ids automatically""" if state in self.states.values(): # we remove the state from the transitions # first we remove transitions that go into the state remove_actions_index = [] for index, transition in self.transitions.items(): - for action in transition.transition.items(): - for index_tuple, tuple in enumerate(action[1].branch): + for action, branch in transition.transition.items(): + for index_tuple, tuple in enumerate(branch.branch): + # remove the tuple if it goes to the state if tuple[1].id == state.id: - self.transitions[index].transition[action[0]].branch.pop( + self.transitions[index].transition[action].branch.pop( index_tuple ) - # if we have empty objects we need to remove those as well - if self.transitions[index].transition[action[0]].branch == []: - remove_actions_index.append((action[0], index)) - # here we remove those empty objects + # if we have empty actions we need to remove those as well (later) + if branch.branch == []: + remove_actions_index.append((action, index)) + # here we remove those empty actions (this needs to happen after the other for loops) for action, index in remove_actions_index: self.transitions[index].transition.pop(action) - if self.transitions[index].transition == {}: + # if we have no actions at all anymore, delete the transition + if self.transitions[index].transition == {} and not index == state.id: self.transitions.pop(index) # we remove transitions that come out of the state @@ -617,33 +664,16 @@ def remove_state(self, state: State, normalize_and_reassign_ids: bool = True): self.markovian_states.remove(state) # we normalize the model if specified to do so - if normalize_and_reassign_ids: + if normalize: self.normalize() - self.states = { - new_id: value - for new_id, (old_id, value) in enumerate( - sorted(self.states.items()) - ) - } + # we reassign the ids if specified to do so + if reassign_ids: + self.reassign_ids() for other_state in self.states.values(): if other_state.id > state.id: other_state.id -= 1 - self.transitions = { - new_id: value - for new_id, (old_id, value) in enumerate( - sorted(self.transitions.items()) - ) - } - if self.supports_rates and self.exit_rates is not None: - self.exit_rates = { - new_id: value - for new_id, (old_id, value) in enumerate( - sorted(self.exit_rates.items()) - ) - } - def remove_transitions_between_states( self, state0: State, state1: State, normalize: bool = True ): @@ -853,31 +883,33 @@ def __eq__(self, other): return False -def new_dtmc(name: str | None = None): +def new_dtmc(name: str | None = None, create_initial_state: bool = True): """Creates a DTMC.""" - return Model(name, ModelType.DTMC) + return Model(name, ModelType.DTMC, create_initial_state) -def new_mdp(name: str | None = None): +def new_mdp(name: str | None = None, create_initial_state: bool = True): """Creates an MDP.""" - return Model(name, ModelType.MDP) + return Model(name, ModelType.MDP, create_initial_state) -def new_ctmc(name: str | None = None): +def new_ctmc(name: str | None = None, create_initial_state: bool = True): """Creates a CTMC.""" - return Model(name, ModelType.CTMC) + return Model(name, ModelType.CTMC, create_initial_state) -def new_pomdp(name: str | None = None): +def new_pomdp(name: str | None = None, create_initial_state: bool = True): """Creates a POMDP.""" - return Model(name, ModelType.POMDP) + return Model(name, ModelType.POMDP, create_initial_state) -def new_ma(name: str | None = None): +def new_ma(name: str | None = None, create_initial_state: bool = True): """Creates a MA.""" - return Model(name, ModelType.MA) + return Model(name, ModelType.MA, create_initial_state) -def new_model(modeltype: ModelType, name: str | None = None): +def new_model( + modeltype: ModelType, name: str | None = None, create_initial_state: bool = True +): """More general model creation function""" - return Model(name, modeltype) + return Model(name, modeltype, create_initial_state) diff --git a/stormvogel/simulator.py b/stormvogel/simulator.py index 408d33e..3b2e500 100644 --- a/stormvogel/simulator.py +++ b/stormvogel/simulator.py @@ -131,19 +131,18 @@ def get_range_index(stateid: int): assert simulator is not None # we start adding states or state action pairs to the path + state = 0 + path = {} + simulator.restart() if not model.supports_actions(): - path = {} - simulator.restart() for i in range(steps): # for each step we add a state to the path - state, reward, labels = simulator.step() - path[i + 1] = model.states[state] - if simulator.is_done(): + if not model.states[state].is_absorbing() and not simulator.is_done(): + state, reward, labels = simulator.step() + path[i + 1] = model.states[state] + else: break else: - state = 0 - path = {} - simulator.restart() for i in range(steps): # we first choose an action (randomly or according to scheduler) actions = simulator.available_actions() @@ -155,10 +154,14 @@ def get_range_index(stateid: int): # we add the state action pair to the path stormvogel_action = model.states[state].available_actions()[select_action] - next_step = simulator.step(actions[select_action]) - state, reward, labels = next_step - path[i + 1] = (stormvogel_action, model.states[state]) - if simulator.is_done(): + + if ( + not model.states[state].is_absorbing(stormvogel_action) + and not simulator.is_done() + ): + state, reward, labels = simulator.step(actions[select_action]) + path[i + 1] = (stormvogel_action, model.states[state]) + else: break path_object = Path(path, model) diff --git a/tests/test_mapping.py b/tests/test_mapping.py index 847178f..b2a70e0 100644 --- a/tests/test_mapping.py +++ b/tests/test_mapping.py @@ -102,8 +102,6 @@ def test_stormpy_to_stormvogel_and_back_dtmc(): new_stormpy_dtmc = stormvogel.mapping.stormvogel_to_stormpy(stormvogel_dtmc) # print(new_stormpy_dtmc.transition_matrix) - # TODO also compare other parts than the matrix (e.g. state labels) - assert sparse_equal(stormpy_dtmc, new_stormpy_dtmc) @@ -138,7 +136,6 @@ def test_stormpy_to_stormvogel_and_back_mdp(): new_stormpy_mdp = stormvogel.mapping.stormvogel_to_stormpy(stormvogel_mdp) # print(new_stormpy_mdp) - # TODO also compare other parts than the matrix (e.g. choice labels) assert sparse_equal(stormpy_mdp, new_stormpy_mdp) diff --git a/tests/test_model_methods.py b/tests/test_model_methods.py index ca51655..380ecc8 100644 --- a/tests/test_model_methods.py +++ b/tests/test_model_methods.py @@ -34,6 +34,22 @@ def test_get_outgoing_transitions(): ] +def test_is_absorbing(): + # one example of a ctmc state that is absorbing and one that isn't + ctmc = examples.nuclear_fusion_ctmc.create_nuclear_fusion_ctmc() + state0 = ctmc.get_state_by_id(4) + state1 = ctmc.get_state_by_id(3) + assert state0.is_absorbing() + assert not state1.is_absorbing() + + # one example of a dtmc state that is absorbing and one that isn't + dtmc = examples.die.create_die_dtmc() + state0 = dtmc.get_initial_state() + state1 = dtmc.get_state_by_id(1) + assert state1.is_absorbing() + assert not state0.is_absorbing() + + def test_transition_from_shorthand(): # First we test it for a model without actions dtmc = stormvogel.model.new_dtmc() @@ -79,8 +95,8 @@ def test_transition_from_shorthand(): ) -def test_is_well_defined(): - # we check for an instance where it is not well defined +def test_is_stochastic(): + # we check for an instance where it is not stochastic dtmc = stormvogel.model.new_dtmc() state = dtmc.new_state() dtmc.set_transitions( @@ -88,9 +104,9 @@ def test_is_well_defined(): [(1 / 2, state)], ) - assert not dtmc.is_well_defined() + assert not dtmc.is_stochastic() - # we check for an instance where it is well defined + # we check for an instance where it is stochastic dtmc.set_transitions( dtmc.get_initial_state(), [(1 / 2, state), (1 / 2, state)], @@ -98,7 +114,15 @@ def test_is_well_defined(): dtmc.add_self_loops() - assert dtmc.is_well_defined() + assert dtmc.is_stochastic() + + # we check it for a continuous time model + ctmc = stormvogel.model.new_ctmc() + ctmc.set_transitions(ctmc.get_initial_state(), [(1, ctmc.new_state())]) + + ctmc.add_self_loops() + + assert not ctmc.is_stochastic() def test_normalize(): @@ -127,7 +151,7 @@ def test_normalize(): def test_remove_state(): # we make a normal ctmc and remove a state ctmc = examples.nuclear_fusion_ctmc.create_nuclear_fusion_ctmc() - ctmc.remove_state(ctmc.get_state_by_id(3), True) + ctmc.remove_state(ctmc.get_state_by_id(3)) # we make a ctmc with the state already missing new_ctmc = stormvogel.model.new_ctmc("Nuclear fusion") @@ -143,6 +167,38 @@ def test_remove_state(): assert ctmc == new_ctmc + # we also test if it works for a model that has nontrivial actions: + mdp = stormvogel.model.new_mdp() + state1 = mdp.new_state() + state2 = mdp.new_state() + action0 = mdp.new_action("0") + action1 = mdp.new_action("1") + branch0 = stormvogel.model.Branch( + cast( + list[tuple[stormvogel.model.Number, stormvogel.model.State]], + [(1 / 2, state1), (1 / 2, state2)], + ) + ) + branch1 = stormvogel.model.Branch( + cast( + list[tuple[stormvogel.model.Number, stormvogel.model.State]], + [(1 / 4, state1), (3 / 4, state2)], + ) + ) + transition = stormvogel.model.Transition({action0: branch0, action1: branch1}) + mdp.set_transitions(mdp.get_initial_state(), transition) + + # we remove a state + mdp.remove_state(mdp.get_state_by_id(0)) + + # we make the mdp with the state already missing + new_mdp = stormvogel.model.new_mdp(create_initial_state=False) + new_mdp.new_state() + new_mdp.new_state() + new_mdp.add_self_loops() + + assert mdp == new_mdp + def test_remove_transitions_between_states(): # we make a model and remove transitions between two states