From 3f06963172c73536276465b505061521cdfec21f Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Mon, 2 Dec 2019 16:14:50 +0100
Subject: [PATCH] extended description of changing model checking environments

---
 doc/source/doc/analysis.rst | 35 ++++++++++++++++++++++++++++++++---
 1 file changed, 32 insertions(+), 3 deletions(-)

diff --git a/doc/source/doc/analysis.rst b/doc/source/doc/analysis.rst
index 5acd8c4..0df7693 100644
--- a/doc/source/doc/analysis.rst
+++ b/doc/source/doc/analysis.rst
@@ -1,5 +1,5 @@
 ***************
-Building Models
+Analysis
 ***************
 
 Background
@@ -7,14 +7,43 @@ Background
 
 Storm supports various model checking approaches that we consider in this section on analysis.
 
+As always::
+
+    >>>	import stormpy
+    >>> import stormpy.examples
+	>>> import stormpy.examples.files
+
+
 Qualitative Analysis
 ======================
 
+
 More to come...
 
 Model checking algorithms
 =========================
+.. seealso:: `02-analysis.py <https://github.com/moves-rwth/stormpy/blob/master/examples/analysis/02-analysis.py>`_
 
-We can also vary the model checking algorithm.
+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])
+
+We can also vary the model checking algorithm::
+
+    >>> 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
+    >>> result = stormpy.model_checking(model, properties[0], environment=env)
+
+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
+    >>> result = stormpy.model_checking(model, properties[0])
+
+Notice that by setting such parameters, the result may be off from the actual model checking algorithm.
 
-More to come...