diff --git a/doc/source/advanced_topics.rst b/doc/source/advanced_topics.rst index 62142be..55de824 100644 --- a/doc/source/advanced_topics.rst +++ b/doc/source/advanced_topics.rst @@ -8,6 +8,7 @@ This guide is a collection of examples meant to bridge the gap between the getti :maxdepth: 2 :caption: Contents: + doc/analysis doc/building_models doc/engines doc/exploration diff --git a/doc/source/doc/analysis.rst b/doc/source/doc/analysis.rst new file mode 100644 index 0000000..5acd8c4 --- /dev/null +++ b/doc/source/doc/analysis.rst @@ -0,0 +1,20 @@ +*************** +Building Models +*************** + +Background +===================== + +Storm supports various model checking approaches that we consider in this section on analysis. + +Qualitative Analysis +====================== + +More to come... + +Model checking algorithms +========================= + +We can also vary the model checking algorithm. + +More to come... diff --git a/examples/analysis/02-analysis.py b/examples/analysis/02-analysis.py new file mode 100644 index 0000000..49ea931 --- /dev/null +++ b/examples/analysis/02-analysis.py @@ -0,0 +1,23 @@ +import stormpy +import stormpy.core + +import stormpy.examples +import stormpy.examples.files + + +def example_analysis_02(): + 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) + + +if __name__ == '__main__': + example_analysis_02() \ No newline at end of file