diff --git a/doc/source/advanced_topics.rst b/doc/source/advanced_topics.rst index 2ed8d80..bc32885 100644 --- a/doc/source/advanced_topics.rst +++ b/doc/source/advanced_topics.rst @@ -9,6 +9,7 @@ This guide is a collection of examples meant to bridge the gap between the getti :caption: Contents: doc/building_models + doc/engines doc/exploration doc/reward_models doc/shortest_paths diff --git a/doc/source/doc/building_models.rst b/doc/source/doc/building_models.rst index 690e491..02229b3 100644 --- a/doc/source/doc/building_models.rst +++ b/doc/source/doc/building_models.rst @@ -17,7 +17,7 @@ We use some standard examples:: >>> import stormpy.examples >>> import stormpy.examples.files -Storm supports the DRN format. +Storm supports the explicit DRN format. From this, models can be built directly:: >>> path = stormpy.examples.files.drn_ctmc_dft diff --git a/doc/source/doc/engines.rst b/doc/source/doc/engines.rst new file mode 100644 index 0000000..f145e5b --- /dev/null +++ b/doc/source/doc/engines.rst @@ -0,0 +1,82 @@ +*************** +Engines +*************** + +Background +===================== + +Storm supports different engines for building and checking a model. A detailed comparison of the different engines provided in Storm can be found on the `Storm website `_. + + +Sparse engine +=============================== + +In all of the examples so far we used the default sparse engine: + + >>> import stormpy.examples + >>> import stormpy.examples.files + >>> prism_program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die) + >>> properties = stormpy.parse_properties_for_prism_program('P=? [F "one"]', prism_program) + >>> sparse_model = stormpy.build_sparse_model(prism_program, properties) + >>> print(type(sparse_model)) + + >>> print("Number of states: {}".format(sparse_model.nr_states)) + Number of states: 13 + >>> print("Number of transitions: {}".format(sparse_model.nr_transitions)) + Number of transitions: 20 + +The model checking was also done in the sparse engine: + + >>> sparse_result = stormpy.check_model_sparse(sparse_model, properties[0]) + >>> initial_state = sparse_model.initial_states[0] + >>> print(sparse_result.at(initial_state)) + 0.16666666666666666 + + +Symbolic engine +=============================== + +Instead of using the sparse engine, one can also use a symbolic representation in terms of `binary decision diagrams (BDDs)`. +To use the symbolic (dd) engine, we use the symbolic versions for the building and model checking: + + >>> symbolic_model = stormpy.build_symbolic_model(prism_program, properties) + >>> print(type(symbolic_model)) + + >>> print("Number of states: {}".format(symbolic_model.nr_states)) + Number of states: 13 + >>> print("Number of transitions: {}".format(symbolic_model.nr_transitions)) + Number of transitions: 20 + >>> symbolic_result = stormpy.check_model_dd(symbolic_model, properties[0]) + >>> print(symbolic_result) + [0, 1] (range) + +We can also filter the computed results and only consider the initial states: + + >>> filter = stormpy.create_filter_initial_states_symbolic(symbolic_model) + >>> symbolic_result.filter(filter) + >>> print(symbolic_result.min) + 0.16666650772094727 + +It is also possible to first build the model symbolically and then transform it into a sparse model: + + >>> print(type(symbolic_model)) + + >>> transformed_model = stormpy.transform_to_sparse_model(symbolic_model) + >>> print(type(transformed_model)) + + + +Hybrid engine +=============================== + +A third possibility is to use the hybrid engine, a combination of sparse and dd engines. +It first builds the model symbolically. +The actual model checking is then performed with the engine which is deemed most suitable for the given task. + + >>> print(type(symbolic_model)) + + >>> hybrid_result = stormpy.check_model_hybrid(symbolic_model, properties[0]) + >>> filter = stormpy.create_filter_initial_states_symbolic(symbolic_model) + >>> hybrid_result.filter(filter) + >>> print(hybrid_result) + 0.166667 diff --git a/doc/source/doc/exploration.rst b/doc/source/doc/exploration.rst index 5285b2a..383d4f2 100644 --- a/doc/source/doc/exploration.rst +++ b/doc/source/doc/exploration.rst @@ -37,7 +37,7 @@ The iteration over the model is as before, but now, for every action, we can hav ... print("From state {} by action {}, with probability {}, go to state {}".format(state, action, transition.value(), transition.column)) -etc- -The output (omitted for brievety) contains sentences like: +The output (omitted for brievety) contains sentences like:: From state 1 by action 0, with probability 1.0, go to state 2 From state 1 by action 1, with probability 1.0, go to state 1 @@ -48,7 +48,7 @@ Internally, storm can hold hints to the origin of the actions, which may be help As the availability and the encoding of this data depends on the input model, we discuss these features in :doc:`highlevel_models`. -Storm currently supports deterministic rewards on states or actions. More information can be found in that :doc:`reward_models`. +Storm currently supports deterministic rewards on states or actions. More information can be found in :doc:`reward_models`. Reading POMDPs @@ -63,7 +63,6 @@ Internally, POMDPs extend MDPs. Thus, iterating over the MDP is done as before. >>> import stormpy.examples.files >>> program = stormpy.parse_prism_program(stormpy.examples.files.prism_pomdp_maze) >>> prop = "R=? [F \"goal\"]" - >>> properties = stormpy.parse_properties_for_prism_program(prop, program, None) >>> model = stormpy.build_model(program, properties) diff --git a/doc/source/doc/parametric_models.rst b/doc/source/doc/parametric_models.rst index c4376c4..d16b597 100644 --- a/doc/source/doc/parametric_models.rst +++ b/doc/source/doc/parametric_models.rst @@ -18,7 +18,6 @@ If the constants only influence the probabilities or rates, but not the topology >>> prism_program = stormpy.parse_prism_program(path) >>> formula_str = "P=? [F s=7 & d=2]" >>> properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program) - >>> model = stormpy.build_parametric_model(prism_program, properties) >>> parameters = model.collect_probability_parameters() >>> for x in parameters: diff --git a/doc/source/doc/shortest_paths.rst b/doc/source/doc/shortest_paths.rst index aca96fa..a727950 100644 --- a/doc/source/doc/shortest_paths.rst +++ b/doc/source/doc/shortest_paths.rst @@ -29,7 +29,7 @@ As in :doc:`../getting_started`, we import some required modules and build a mod >>> model = stormpy.build_model(prism_program) -We also import the `ShortestPathsGenerator`:: +We also import the ``ShortestPathsGenerator``:: >>> from stormpy.utility import ShortestPathsGenerator @@ -40,7 +40,7 @@ and choose a target state (by its ID) to which we want to compute the shortest p It is also possible to specify a set of target states (as a list, e.g., ``[8, 10, 11]``) or a label in the model if applicable (e.g., ``"observe0Greater1"``). For simplicity, we will stick to using a single state for now. -We initialize a `ShortestPathsGenerator` instance:: +We initialize a ``ShortestPathsGenerator`` instance:: >>> spg = ShortestPathsGenerator(model, state_id) diff --git a/doc/source/getting_started.rst b/doc/source/getting_started.rst index abf1c57..e35acc1 100644 --- a/doc/source/getting_started.rst +++ b/doc/source/getting_started.rst @@ -41,7 +41,7 @@ With this, we can now import the path of our prism file:: >>> path = stormpy.examples.files.prism_dtmc_die >>> prism_program = stormpy.parse_prism_program(path) -The `prism_program` can be translated into Markov chains:: +The ``prism_program`` can be translated into a Markov chain:: >>> model = stormpy.build_model(prism_program) >>> print("Number of states: {}".format(model.nr_states)) @@ -56,7 +56,7 @@ Moreover, initial states and deadlocks are indicated with a labelling function. >>> print("Labels: {}".format(model.labeling.get_labels())) Labels: ... -We will investigate ways to examine the model in more detail in :ref:`getting-started-investigating-the-model`. +We will investigate ways to examine the model in more detail later in :ref:`getting-started-investigating-the-model`. .. _getting-started-building-properties: @@ -65,7 +65,7 @@ Building properties .. seealso:: `02-getting-started.py `_ Storm takes properties in the prism-property format. -To express that one is interested in the reachability of any state where the prism program variable s is 2, one would formulate:: +To express that one is interested in the reachability of any state where the prism program variable ``s`` is 2, one would formulate:: P=? [F s=2] @@ -76,7 +76,7 @@ Stormpy can be used to parse this. As the variables in the property refer to a p Notice that properties is now a list of properties containing a single element. -However, if we build the model as before, then the appropriate information that the variable s=2 in some states is not present. +However, if we build the model as before, then the appropriate information that the variable ``s=2`` in some states is not present. In order to label the states accordingly, we should notify Storm upon building the model that we would like to preserve given properties. Storm will then add the labels accordingly:: @@ -85,7 +85,7 @@ Storm will then add the labels accordingly:: Labels in the model: ['(s = 2)', 'deadlock', 'init'] Model building however now behaves slightly different: Only the properties passed are preserved, which means that model building might skip parts of the model. -In particular, to check the probability of eventually reaching a state x where s=2, successor states of x are not relevant:: +In particular, to check the probability of eventually reaching a state ``x`` where ``s=2``, successor states of ``x`` are not relevant:: >>> print("Number of states: {}".format(model.nr_states)) Number of states: 8 @@ -94,7 +94,7 @@ If we consider another property, however, such as:: P=? [F s=7 & d=2] -then Storm is only skipping exploration of successors of the particular state y where s=7 and d=2. In this model, state y has a self-loop, so effectively, the whole model is explored. +then Storm is only skipping exploration of successors of the particular state ``y`` where ``s=7`` and ``d=2``. In this model, state ``y`` has a self-loop, so effectively, the whole model is explored. .. _getting-started-checking-properties: @@ -180,7 +180,7 @@ Thus:: ... assert len(state.actions) <= 1 -We can also check if a state is indeed an initial state. Notice that model.initial_states contains state ids, not states.:: +We can also check if a state is indeed an initial state. Notice that ``model.initial_states`` contains state ids, not states.:: >>> for state in model.states: ... if state.id in model.initial_states: diff --git a/src/core/result.cpp b/src/core/result.cpp index 4e6728d..9827950 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -8,6 +8,17 @@ #include "storm/models/symbolic/StandardRewardModel.h" +template +std::shared_ptr createFilterInitialStatesSparse(std::shared_ptr> model) { + return std::make_unique(model->getInitialStates()); +} + +template +std::shared_ptr createFilterInitialStatesSymbolic(std::shared_ptr> model) { + return std::make_unique>(model->getReachableStates(), model->getInitialStates()); +} + + // Define python bindings void define_result(py::module& m) { @@ -35,6 +46,7 @@ void define_result(py::module& m) { .def("as_explicit_parametric_quantitative", [](storm::modelchecker::CheckResult const& result) { return result.asExplicitQuantitativeCheckResult(); }, "Convert into explicit quantitative result") + .def("filter", &storm::modelchecker::CheckResult::filter, py::arg("filter"), "Filter the result") .def("__str__", [](storm::modelchecker::CheckResult const& result) { std::stringstream stream; result.writeToStream(stream); @@ -45,16 +57,20 @@ void define_result(py::module& m) { // QualitativeCheckResult py::class_> qualitativeCheckResult(m, "_QualitativeCheckResult", "Abstract class for qualitative model checking results", checkResult); py::class_>(m, "ExplicitQualitativeCheckResult", "Explicit qualitative model checking result", qualitativeCheckResult) - .def("at", [](storm::modelchecker::ExplicitQualitativeCheckResult const& result, storm::storage::sparse::state_type state) { + .def("at", [](storm::modelchecker::ExplicitQualitativeCheckResult const& result, storm::storage::sparse::state_type state) { return result[state]; }, py::arg("state"), "Get result for given state") - .def("get_truth_values", &storm::modelchecker::ExplicitQualitativeCheckResult::getTruthValuesVector, "Get BitVector representing the truth values") + .def("get_truth_values", &storm::modelchecker::ExplicitQualitativeCheckResult::getTruthValuesVector, "Get BitVector representing the truth values") ; py::class_, std::shared_ptr>>(m, "SymbolicQualitativeCheckResult", "Symbolic qualitative model checking result", qualitativeCheckResult) ; // QuantitativeCheckResult py::class_, std::shared_ptr>> quantitativeCheckResult(m, "_QuantitativeCheckResult", "Abstract class for quantitative model checking results", checkResult); + quantitativeCheckResult.def_property_readonly("min", &storm::modelchecker::QuantitativeCheckResult::getMin, "Minimal value") + .def_property_readonly("max", &storm::modelchecker::QuantitativeCheckResult::getMax, "Maximal value") + ; + py::class_, std::shared_ptr>>(m, "ExplicitQuantitativeCheckResult", "Explicit quantitative model checking result", quantitativeCheckResult) .def("at", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& result, storm::storage::sparse::state_type state) { return result[state]; @@ -81,5 +97,9 @@ void define_result(py::module& m) { .def("get_values", &storm::modelchecker::HybridQuantitativeCheckResult::getExplicitValueVector, "Get model checking result values for all states") ; + + m.def("create_filter_initial_states_sparse", &createFilterInitialStatesSparse, "Create a filter for the initial states on a sparse model", py::arg("model")); + m.def("create_filter_initial_states_symbolic", &createFilterInitialStatesSymbolic, "Create a filter for the initial states on a symbolic model", py::arg("model")); + } diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 1d4b15f..2868953 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -118,6 +118,22 @@ class TestModelChecking: result = stormpy.model_checking(model, formulas[0]) assert math.isclose(result.at(initial_state), 4.166666667) + def test_filter(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + model = stormpy.build_model(program, formulas) + assert model.nr_states == 13 + assert model.nr_transitions == 20 + assert len(model.initial_states) == 1 + initial_state = model.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0]) + assert math.isclose(result.at(initial_state), 1 / 6) + filter = stormpy.create_filter_initial_states_sparse(model) + result.filter(filter) + assert result.min == result.max + assert math.isclose(result.min, 1 / 6) + def test_model_checking_prism_dd_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) @@ -126,6 +142,10 @@ class TestModelChecking: assert model.nr_transitions == 20 result = stormpy.check_model_dd(model, formulas[0]) assert type(result) is stormpy.SymbolicQuantitativeCheckResult + filter = stormpy.create_filter_initial_states_symbolic(model) + result.filter(filter) + assert result.min == result.max + assert math.isclose(result.min, 1 / 6, rel_tol=1e-6) def test_model_checking_prism_hybrid_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) diff --git a/tests/core/test_transformation.py b/tests/core/test_transformation.py index 562f85f..e1a322e 100644 --- a/tests/core/test_transformation.py +++ b/tests/core/test_transformation.py @@ -6,18 +6,18 @@ from helpers.helper import get_example_path class TestTransformation: def test_transform_symbolic_dtmc_to_sparse(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds5_5.pm")) - model = stormpy.build_symbolic_model(program) - assert model.nr_states == 8607 - assert model.nr_transitions == 15113 - assert model.model_type == stormpy.ModelType.DTMC - assert not model.supports_parameters - assert type(model) is stormpy.SymbolicSylvanDtmc - symbolic_model = stormpy.transform_to_sparse_model(model) + symbolic_model = stormpy.build_symbolic_model(program) assert symbolic_model.nr_states == 8607 assert symbolic_model.nr_transitions == 15113 assert symbolic_model.model_type == stormpy.ModelType.DTMC assert not symbolic_model.supports_parameters - assert type(symbolic_model) is stormpy.SparseDtmc + assert type(symbolic_model) is stormpy.SymbolicSylvanDtmc + sparse_model = stormpy.transform_to_sparse_model(symbolic_model) + assert sparse_model.nr_states == 8607 + assert sparse_model.nr_transitions == 15113 + assert sparse_model.model_type == stormpy.ModelType.DTMC + assert not sparse_model.supports_parameters + assert type(sparse_model) is stormpy.SparseDtmc def test_transform_symbolic_parametric_dtmc_to_sparse(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "parametric_die.pm"))