Browse Source

A new example showing that one can change the analysis method

refactoring
Sebastian Junges 5 years ago
parent
commit
52b88c3710
  1. 1
      doc/source/advanced_topics.rst
  2. 20
      doc/source/doc/analysis.rst
  3. 23
      examples/analysis/02-analysis.py

1
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 :maxdepth: 2
:caption: Contents: :caption: Contents:
doc/analysis
doc/building_models doc/building_models
doc/engines doc/engines
doc/exploration doc/exploration

20
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...

23
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()
Loading…
Cancel
Save