Merge branch 'master' into wrap_highlevel

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

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

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 <http://www.stormchecker.org/documentation/usage/engines.html>`_.
+
+
+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))
+    <class 'stormpy.storage.storage.SparseDtmc'>
+    >>> 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))
+    <class 'stormpy.storage.storage.SymbolicSylvanDtmc'>
+    >>> 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))
+    <class 'stormpy.storage.storage.SymbolicSylvanDtmc'>
+    >>> transformed_model = stormpy.transform_to_sparse_model(symbolic_model)
+    >>> print(type(transformed_model))
+    <class 'stormpy.storage.storage.SparseDtmc'>
+
+
+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))
+    <class 'stormpy.storage.storage.SymbolicSylvanDtmc'>
+    >>> 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

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)
 

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:

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)
 

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 <https://github.com/moves-rwth/stormpy/blob/master/examples/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:

src/core/result.cpp

@@ -8,6 +8,17 @@
 
 #include "storm/models/symbolic/StandardRewardModel.h"
 
+template<typename ValueType>
+std::shared_ptr<storm::modelchecker::QualitativeCheckResult> createFilterInitialStatesSparse(std::shared_ptr<storm::models::sparse::Model<ValueType>> model) {
+    return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->getInitialStates());
+}
+
+template<storm::dd::DdType DdType, typename ValueType>
+std::shared_ptr<storm::modelchecker::QualitativeCheckResult> createFilterInitialStatesSymbolic(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> model) {
+   return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<DdType>>(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<storm::RationalFunction>();
             }, "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_<storm::modelchecker::QualitativeCheckResult, std::shared_ptr<storm::modelchecker::QualitativeCheckResult>> qualitativeCheckResult(m, "_QualitativeCheckResult", "Abstract class for qualitative model checking results", checkResult);
     py::class_<storm::modelchecker::ExplicitQualitativeCheckResult, std::shared_ptr<storm::modelchecker::ExplicitQualitativeCheckResult>>(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_<storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>, std::shared_ptr<storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>>>(m, "SymbolicQualitativeCheckResult", "Symbolic qualitative model checking result", qualitativeCheckResult)
     ;
 
     // QuantitativeCheckResult
     py::class_<storm::modelchecker::QuantitativeCheckResult<double>, std::shared_ptr<storm::modelchecker::QuantitativeCheckResult<double>>> quantitativeCheckResult(m, "_QuantitativeCheckResult", "Abstract class for quantitative model checking results", checkResult);
+    quantitativeCheckResult.def_property_readonly("min", &storm::modelchecker::QuantitativeCheckResult<double>::getMin, "Minimal value")
+        .def_property_readonly("max", &storm::modelchecker::QuantitativeCheckResult<double>::getMax, "Maximal value")
+    ;
+
     py::class_<storm::modelchecker::ExplicitQuantitativeCheckResult<double>, std::shared_ptr<storm::modelchecker::ExplicitQuantitativeCheckResult<double>>>(m, "ExplicitQuantitativeCheckResult", "Explicit quantitative model checking result", quantitativeCheckResult)
         .def("at", [](storm::modelchecker::ExplicitQuantitativeCheckResult<double> 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<storm::dd::DdType::Sylvan, storm::RationalFunction>::getExplicitValueVector, "Get model checking result values for all states")
     ;
 
+
+    m.def("create_filter_initial_states_sparse", &createFilterInitialStatesSparse<double>, "Create a filter for the initial states on a sparse model", py::arg("model"));
+    m.def("create_filter_initial_states_symbolic", &createFilterInitialStatesSymbolic<storm::dd::DdType::Sylvan, double>, "Create a filter for the initial states on a symbolic model", py::arg("model"));
+
 }
 

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

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