new information on using different model checking techniques

doc/source/doc/analysis.rst

@@ -12,23 +12,42 @@ As always::
     >>>	import stormpy
     >>> import stormpy.examples
 	>>> import stormpy.examples.files
+    >>> path = stormpy.examples.files.prism_dtmc_die
+	>>> prism_program = stormpy.parse_prism_program(path)
+	>>> formula_str = "P=? [F s=7 & d=2]"
+    >>> properties = stormpy.parse_properties(formula_str, prism_program)
 
 
 Qualitative Analysis
 ======================
 
 
-More to come...
-
-Model checking algorithms
-=========================
+Adapting the model checking engine
+==================================
 .. seealso:: `02-analysis.py <https://github.com/moves-rwth/stormpy/blob/master/examples/analysis/02-analysis.py>`_
 
+Instead of using the sparse representation, models can also be built symbolically::
+
+    >>> model = stormpy.build_symbolic_model(prism_program, properties)
+    >>> result = stormpy.model_checking(model, properties[0])
+
+To access the result, the result has to be filtered::
+
+    >>> filter = stormpy.create_filter_initial_states_symbolic(model)
+    >>> result.filter(filter)
+    >>> assert result.min == result.max
+
+Then, result.min (or result.max) contains the result. Notice that if there are multiple initial states, result.min will not be equal to result.max.
+
+Besides this analysis on the DD, there are approaches that combine both representation.
+Stormpy does support them, but we have not yet documented them.
+
+Adapting model checking algorithms
+==================================
+.. seealso:: `03-analysis.py <https://github.com/moves-rwth/stormpy/blob/master/examples/analysis/03-analysis.py>`_
+
 Reconsider the model checking example from the getting started guide::
 
-	>>> path = stormpy.examples.files.prism_dtmc_die
-	>>> prism_program = stormpy.parse_prism_program(path)
-    >>> properties = stormpy.parse_properties(formula_str, prism_program)
 	>>> model = stormpy.build_model(prism_program, properties)
     >>> result = stormpy.model_checking(model, properties[0])
 
@@ -42,8 +61,9 @@ We can also vary the model checking algorithm::
 Finally, we allow to change some parameters of the algorithms. E.g., in iterative approaches,
 we allow to change the number of iterations::
 
-    >>> env.solver_environment.maximum_iterations = 3
+    >>> env.solver_environment.native_solver_environment.maximum_iterations = 3
     >>> result = stormpy.model_checking(model, properties[0])
 
 Notice that by setting such parameters, the result may be off from the actual model checking algorithm.
 
+Environments can be used likewise for symbolic model checking. See the example for more information.

examples/analysis/02-analysis.py

@@ -11,13 +11,12 @@ def example_analysis_02():
 
     formula_str = "P=? [F s=7 & d=2]"
     properties = stormpy.parse_properties(formula_str, prism_program)
-    model = stormpy.build_model(prism_program, properties)
-    env = stormpy.Environment()
-    env.solver_environment.set_linear_equation_solver_type(stormpy.EquationSolverType.native)
-    env.solver_environment.native_solver_environment.method = stormpy.NativeLinearEquationSolverMethod.power_iteration
-    env.solver_environment.native_solver_environment.maximum_iterations = 2
-    result = stormpy.model_checking(model, properties[0], environment=env)
-
+    model = stormpy.build_symbolic_model(prism_program, properties)
+    result = stormpy.model_checking(model, properties[0])
+    filter = stormpy.create_filter_initial_states_symbolic(model)
+    result.filter(filter)
+    assert result.min == result.max
+    print(result.min)
 
 if __name__ == '__main__':
     example_analysis_02()

examples/analysis/03-analysis.py

@@ -0,0 +1,32 @@
+import stormpy
+import stormpy.core
+
+import stormpy.examples
+import stormpy.examples.files
+
+
+def example_analysis_03():
+    path = stormpy.examples.files.prism_dtmc_die
+    prism_program = stormpy.parse_prism_program(path)
+
+    formula_str = "P=? [F s=7 & d=2]"
+    properties = stormpy.parse_properties(formula_str, prism_program)
+    model = stormpy.build_model(prism_program, properties)
+    env = stormpy.Environment()
+    env.solver_environment.set_linear_equation_solver_type(stormpy.EquationSolverType.native)
+    env.solver_environment.native_solver_environment.method = stormpy.NativeLinearEquationSolverMethod.power_iteration
+    env.solver_environment.native_solver_environment.maximum_iterations = 2
+    result = stormpy.model_checking(model, properties[0], environment=env)
+    print(result.at(model.initial_states[0]))
+
+    dd_model = stormpy.build_symbolic_model(prism_program, properties)
+    result = stormpy.model_checking(dd_model, properties[0], environment=env)
+    filter = stormpy.create_filter_initial_states_symbolic(dd_model)
+    result.filter(filter)
+    assert result.min == result.max
+    print(result.min)
+
+
+
+if __name__ == '__main__':
+    example_analysis_03()