Parametric model components (#129)

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

src/mod_storage.cpp

@@ -57,6 +57,7 @@ PYBIND11_MODULE(storage, m) {
  define_distribution<double>(m, "Double");
  define_sparse_model_components<double>(m, "");
  define_sparse_model_components<storm::RationalNumber>(m, "Exact");
+ define_sparse_model_components<storm::RationalFunction>(m, "Parametric");
  define_geometry<double>(m, "Double");
  define_geometry<storm::RationalNumber>(m, "Exact");
 

src/storage/model.cpp

@@ -360,6 +360,9 @@ void define_sparse_parametric_model(py::module& m) {
  ;
 
  py::class_<SparseRewardModel<RationalFunction>>(m, "SparseParametricRewardModel", "Reward structure for parametric sparse models")
+ .def(py::init<std::optional<std::vector<RationalFunction>> const&, std::optional<std::vector<RationalFunction>> const&,
+ std::optional<storm::storage::SparseMatrix<RationalFunction>> const&>(), py::arg("optional_state_reward_vector") = std::nullopt,
+ py::arg("optional_state_action_reward_vector") = std::nullopt, py::arg("optional_transition_reward_matrix") = std::nullopt)
  .def_property_readonly("has_state_rewards", &SparseRewardModel<RationalFunction>::hasStateRewards)
  .def_property_readonly("has_state_action_rewards", &SparseRewardModel<RationalFunction>::hasStateActionRewards)
  .def_property_readonly("has_transition_rewards", &SparseRewardModel<RationalFunction>::hasTransitionRewards)

tests/storage/test_model_components.py

@@ -1,6 +1,6 @@
 import stormpy
 from helpers.helper import get_example_path
-from configurations import numpy_avail
+from configurations import numpy_avail, pars
 
 
 class TestSparseModelComponents:
@@ -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
@@ -771,3 +768,110 @@ def test_build_pomdp(self):
  assert not pomdp.has_choice_origins()
 
  assert pomdp.observations == [1, 0, 0, 0, 0, 0, 0, 0, 0, 2]
+
+ @pars
+ def test_build_parametric_dtmc(self):
+ import stormpy.info
+ import stormpy.pars
+ if stormpy.info.storm_ratfunc_use_cln():
+ import pycarl.cln as pc
+ else:
+ import pycarl.gmp as pc
+
+ def create_polynomial(pol):
+ num = pc.create_factorized_polynomial(pc.Polynomial(pol))
+ return pc.FactorizedRationalFunction(num)
+
+ def create_number(num):
+ num = pc.FactorizedPolynomial(pc.Rational(num))
+ return pc.FactorizedRationalFunction(num)
+
+ from pycarl import Variable
+ nr_states = 13
+ nr_choices = 13
+
+ # transition_matrix
+ builder = stormpy.ParametricSparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False,
+ has_custom_row_grouping=False, row_groups=0)
+
+ # Create variables
+ var_p = create_polynomial(Variable("p"))
+ var_q = create_polynomial(Variable("q"))
+ one = create_number(1)
+ zero = create_number(0)
+
+ # Add transitions
+ builder.add_next_value(0, 1, var_p)
+ builder.add_next_value(0, 2, one - var_p)
+ builder.add_next_value(1, 3, var_q)
+ builder.add_next_value(1, 4, one - var_q)
+ builder.add_next_value(2, 5, var_q)
+ builder.add_next_value(2, 6, one - var_q)
+ builder.add_next_value(3, 7, create_number(0.5))
+ builder.add_next_value(3, 1, create_number(0.5))
+ builder.add_next_value(4, 8, var_p * var_q)
+ builder.add_next_value(4, 9, one - var_p * var_q)
+ builder.add_next_value(5, 10, create_number(0.2) * var_p * var_q)
+ builder.add_next_value(5, 11, one - create_number(0.2) * var_p * var_q)
+ builder.add_next_value(6, 2, var_p + var_q)
+ builder.add_next_value(6, 12, one - var_p - var_q)
+ for s in range(7, 13):
+ builder.add_next_value(s, s, one)
+ # Build transition matrix, update number of rows and columns
+ transition_matrix = builder.build(nr_states, nr_states)
+
+ # state labeling
+ state_labeling = stormpy.storage.StateLabeling(nr_states)
+ state_labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'}
+ for label in state_labels:
+ state_labeling.add_label(label)
+ # Add label to one state
+ state_labeling.add_label_to_state('init', 0)
+ state_labeling.add_label_to_state('one', 7)
+ state_labeling.add_label_to_state('two', 8)
+ state_labeling.add_label_to_state('three', 9)
+ state_labeling.add_label_to_state('four', 10)
+ state_labeling.add_label_to_state('five', 11)
+ state_labeling.add_label_to_state('six', 12)
+
+ state_labeling.set_states('done', stormpy.BitVector(nr_states, [7, 8, 9, 10, 11, 12]))
+
+ # reward_models
+ reward_models = {}
+ # Create a vector representing the state-action rewards
+ action_reward = [one, one, one, one, one, one, one, zero, zero, zero, zero, zero, zero]
+ reward_models['coin_flips'] = stormpy.SparseParametricRewardModel(optional_state_action_reward_vector=action_reward)
+
+ # Construct components
+ components = stormpy.SparseParametricModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling,
+ reward_models=reward_models)
+ # Build parametric DTMC
+ dtmc = stormpy.storage.SparseParametricDtmc(components)
+
+ assert type(dtmc) is stormpy.SparseParametricDtmc
+ assert dtmc.supports_parameters
+ assert dtmc.has_parameters
+
+ # Test transition matrix
+ assert dtmc.nr_choices == nr_choices
+ assert dtmc.nr_states == nr_states
+ assert dtmc.nr_transitions == 20
+ assert dtmc.transition_matrix.nr_entries == dtmc.nr_transitions
+ for e in dtmc.transition_matrix:
+ assert type(e.value()) is pc.FactorizedRationalFunction
+ for state in dtmc.states:
+ assert len(state.actions) <= 1
+
+ # Test state labeling
+ assert dtmc.labeling.get_labels() == {'init', 'deadlock', 'done', 'one', 'two', 'three', 'four', 'five', 'six'}
+
+ # Test reward_models
+ assert len(dtmc.reward_models) == 1
+ assert not dtmc.reward_models["coin_flips"].has_state_rewards
+ assert dtmc.reward_models["coin_flips"].has_state_action_rewards
+ for reward in dtmc.reward_models["coin_flips"].state_action_rewards:
+ assert reward == one or reward == zero
+ assert not dtmc.reward_models["coin_flips"].has_transition_rewards
+
+ # Test choice labeling
+ assert not dtmc.has_choice_labeling()