From dff5e65b9373a176a6f12ba5258b250eca2a3438 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 2 Dec 2019 17:53:25 +0100 Subject: [PATCH] new information on using different model checking techniques --- doc/source/doc/analysis.rst | 38 ++++++++++++++++++++++++-------- examples/analysis/02-analysis.py | 13 +++++------ examples/analysis/03-analysis.py | 32 +++++++++++++++++++++++++++ 3 files changed, 67 insertions(+), 16 deletions(-) create mode 100644 examples/analysis/03-analysis.py diff --git a/doc/source/doc/analysis.rst b/doc/source/doc/analysis.rst index 0df7693..493c2f5 100644 --- a/doc/source/doc/analysis.rst +++ b/doc/source/doc/analysis.rst @@ -12,24 +12,43 @@ 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 `_ +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 `_ + 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) + >>> model = stormpy.build_model(prism_program, properties) >>> result = stormpy.model_checking(model, properties[0]) We can also vary the model checking algorithm:: @@ -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. diff --git a/examples/analysis/02-analysis.py b/examples/analysis/02-analysis.py index 49ea931..4cee8d2 100644 --- a/examples/analysis/02-analysis.py +++ b/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() \ No newline at end of file diff --git a/examples/analysis/03-analysis.py b/examples/analysis/03-analysis.py new file mode 100644 index 0000000..a43638e --- /dev/null +++ b/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() \ No newline at end of file