diff --git a/doc/source/doc/models/building_ctmcs.ipynb b/doc/source/doc/models/building_ctmcs.ipynb index ff3222952..50a0e180d 100644 --- a/doc/source/doc/models/building_ctmcs.ipynb +++ b/doc/source/doc/models/building_ctmcs.ipynb @@ -14,7 +14,7 @@ "## Background\n", "\n", "In this section, we explain how Stormpy can be used to build a simple CTMC.\n", - "Building CTMCs works similar to building DTMCs as in [Discrete-time Markov chains (DTMCs)](building_dtmcs.ipynb), but additionally every state is equipped with an exit rate.\n", + "Building CTMCs works similar to building DTMCs as in [Discrete-time Markov chains (DTMCs)](building_dtmcs.ipynb), however instead of transition probabilities we use transition rates.\n", "\n", "[01-building-ctmcs.py](https://github.com/moves-rwth/stormpy/blob/master/examples/building_ctmcs/01-building-ctmcs.py)\n", "\n", @@ -100,33 +100,13 @@ ">>> state_labeling.add_label_to_state('full', 3)" ] }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Exit Rates\n", - "\n", - "Lastly, we initialize a list to equip every state with an exit rate:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> exit_rates = [1.5, 4.5, 4.5, 3.0]" - ] - }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Building the Model\n", "\n", - "Now, we can collect all components, including the choice labeling and the exit rates.\n", + "Now, we can collect all components, including the choice labeling.\n", "To let the transition values be interpreted as rates we set rate_transitions to True:" ] }, @@ -138,8 +118,7 @@ }, "outputs": [], "source": [ - ">>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, rate_transitions=True)\n", - ">>> components.exit_rates = exit_rates" + ">>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, rate_transitions=True)\n" ] }, { diff --git a/doc/source/doc/models/building_mas.ipynb b/doc/source/doc/models/building_mas.ipynb index b4f177fb3..5d0a2377e 100644 --- a/doc/source/doc/models/building_mas.ipynb +++ b/doc/source/doc/models/building_mas.ipynb @@ -18,7 +18,7 @@ "Markov automata use states that are probabilistic, i.e. like the states of an MDP, or Markovian, i.e. like the states of a CTMC.\n", "\n", "In this section, we build a small MA with five states from which the first four are Markovian.\n", - "Since we covered labeling and exit rates already in the previous examples we omit the description of these components.\n", + "Since we covered the labeling already in the previous examples we omit the description here.\n", "The full example can be found here:\n", "\n", "[01-building-mas.py](https://github.com/moves-rwth/stormpy/blob/master/examples/building_mas/01-building-mas.py)\n", @@ -92,7 +92,7 @@ "nbsphinx": "hidden" }, "source": [ - "## Labeling and Exit Rates" + "## Labeling" ] }, { @@ -115,9 +115,7 @@ ">>> for label in choice_labels:\n", "... choice_labeling.add_label(label)\n", ">>> choice_labeling.add_label_to_choice('alpha', 0)\n", - ">>> choice_labeling.add_label_to_choice('beta', 1)\n", - "\n", - ">>> exit_rates = [0.0, 10.0, 12.0, 1.0, 1.0]" + ">>> choice_labeling.add_label_to_choice('beta', 1)\n" ] }, { @@ -141,6 +139,29 @@ ">>> markovian_states = stormpy.BitVector(5, [1, 2, 3, 4])" ] }, + { + "cell_type": "markdown", + "metadata": { + "nbsphinx": "hidden" + }, + "source": [ + "## Exit Rates\n", + "\n", + "Lastly, we initialize a list to equip every (Markovian) state with an exit rate > 0:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": { + "nbsphinx": "hidden" + }, + "outputs": [], + "source": [ + "\n", + ">>> exit_rates = [0.0, 10.0, 12.0, 1.0, 1.0]" + ] + }, { "cell_type": "markdown", "metadata": {}, diff --git a/examples/building_ctmcs/01-building-ctmcs.py b/examples/building_ctmcs/01-building-ctmcs.py index 0fd0702d0..c2603a1c1 100644 --- a/examples/building_ctmcs/01-building-ctmcs.py +++ b/examples/building_ctmcs/01-building-ctmcs.py @@ -35,13 +35,9 @@ def example_building_ctmcs_01(): state_labeling.add_label_to_state('empty', 0) state_labeling.add_label_to_state('full', 3) - # Exit rate for each state - exit_rates = [1.5, 4.5, 4.5, 3.0] - # Collect components # rate_transitions = True, because the transition values are interpreted as rates components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, rate_transitions=True) - components.exit_rates = exit_rates # Build the model ctmc = stormpy.storage.SparseCtmc(components) diff --git a/examples/building_mas/01-building-mas.py b/examples/building_mas/01-building-mas.py index d68374179..a7e4bcc27 100644 --- a/examples/building_mas/01-building-mas.py +++ b/examples/building_mas/01-building-mas.py @@ -46,6 +46,7 @@ def example_building_mas_01(): choice_labeling.add_label_to_choice('alpha', 0) choice_labeling.add_label_to_choice('beta', 1) + # Provide exit rates (for Markovian states) exit_rates = [0.0, 10.0, 12.0, 1.0, 1.0] markovian_states = stormpy.BitVector(5, [1, 2, 3, 4]) diff --git a/tests/storage/test_model_components.py b/tests/storage/test_model_components.py index 40e12618c..223402d5e 100644 --- a/tests/storage/test_model_components.py +++ b/tests/storage/test_model_components.py @@ -357,9 +357,6 @@ def test_build_ctmc(self): choice_labeling.set_choices('loop2b', stormpy.BitVector(nr_choices, [6, 9])) choice_labeling.set_choices('serve2', stormpy.BitVector(nr_choices, [10, 11])) - # state exit rates - exit_rates = [201.0, 200.5, 200.5, 201.0, 200.0, 1.5, 200.5, 200.5, 1.0, 200.0, 1.5, 1.0] - # state valuations manager = stormpy.ExpressionManager() var_s = manager.create_integer_variable(name='s') @@ -391,7 +388,7 @@ def test_build_ctmc(self): components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models, rate_transitions=True) components.choice_labeling = choice_labeling - components.exit_rates = exit_rates + # exit_rates are not required due to using a rate matrix components.state_valuations = state_valuations # Build CTMC