From 52b88c3710a6f29971c721c676f44d8430be2fc6 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Mon, 2 Dec 2019 16:01:50 +0100
Subject: [PATCH] A new example showing that one can change the analysis method

---
 doc/source/advanced_topics.rst   |  1 +
 doc/source/doc/analysis.rst      | 20 ++++++++++++++++++++
 examples/analysis/02-analysis.py | 23 +++++++++++++++++++++++
 3 files changed, 44 insertions(+)
 create mode 100644 doc/source/doc/analysis.rst
 create mode 100644 examples/analysis/02-analysis.py

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