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/src/mod_storage.cpp b/src/mod_storage.cpp index 94acd6d0a..97e7a9287 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -57,6 +57,7 @@ PYBIND11_MODULE(storage, m) { define_distribution(m, "Double"); define_sparse_model_components(m, ""); define_sparse_model_components(m, "Exact"); + define_sparse_model_components(m, "Parametric"); define_geometry(m, "Double"); define_geometry(m, "Exact"); diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 48e1814e2..2e5c99533 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -360,6 +360,9 @@ void define_sparse_parametric_model(py::module& m) { ; py::class_>(m, "SparseParametricRewardModel", "Reward structure for parametric sparse models") + .def(py::init> const&, std::optional> const&, + std::optional> 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::hasStateRewards) .def_property_readonly("has_state_action_rewards", &SparseRewardModel::hasStateActionRewards) .def_property_readonly("has_transition_rewards", &SparseRewardModel::hasTransitionRewards) diff --git a/tests/storage/test_model_components.py b/tests/storage/test_model_components.py index a7a08f99c..223402d5e 100644 --- a/tests/storage/test_model_components.py +++ b/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()