Exit rates are not needed for CTMCs

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"
  ]
  },
  {

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": {},

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)

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])

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