From 4dae2007d61bcdec3e2fb2e57329772163d061df Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 12 Oct 2017 17:13:16 +0200
Subject: [PATCH] Added 05-getting-started

---
 doc/source/getting_started.rst | 15 +++++++++--
 examples/05-getting-started.py | 48 ++++++++++++++++++++++++++++++++++
 2 files changed, 61 insertions(+), 2 deletions(-)
 create mode 100644 examples/05-getting-started.py

diff --git a/doc/source/getting_started.rst b/doc/source/getting_started.rst
index 3f2505b..fcb48ee 100644
--- a/doc/source/getting_started.rst
+++ b/doc/source/getting_started.rst
@@ -93,7 +93,7 @@ If we consider another property, however, such as::
 
 then Storm is only skipping exploration of successors of the particular state y where s=7 and d=2. In this model, state y has a self-loop, so effectively, the whole model is explored.
 
-
+.. _getting-started-checking-properties:
 Checking properties
 ------------------------------------
 .. seealso:: `03-getting-started.py <https://github.com/moves-rwth/stormpy/blob/master/examples/03-getting-started.py>`_
@@ -152,10 +152,21 @@ Before we obtain an instantiated model, we need to map parameters to values: We
 
 Checking parametric models
 ------------------------------------
-.. seealso:: ``05-getting-started.py``
+.. seealso:: `05-getting-started.py <https://github.com/moves-rwth/stormpy/blob/master/examples/05-getting-started.py>`_
+
+It is also possible to check the parametric model directly, similar as before in :ref:` _getting-started-checking-properties`::
 
+    >>> result = stormpy.model_checking(model, properties[0])
+    >>> initial_state = model.initial_states[0]
+    >>> func = result.at(initial_state)
 
+We collect the constraints ensuring that underlying model is well-formed and the graph structure does not change.
 
+    >>> collector = stormpy.ConstraintCollector(model)
+    >>> for formula in collector.wellformed_constraints:
+    ...     print(formula)
+    >>> for formula in collector.graph_preserving_constraints:
+    ...     print(formula)
 
 .. _getting-started-investigating-the-model:
 
diff --git a/examples/05-getting-started.py b/examples/05-getting-started.py
new file mode 100644
index 0000000..29403f6
--- /dev/null
+++ b/examples/05-getting-started.py
@@ -0,0 +1,48 @@
+import stormpy
+import stormpy.core
+import stormpy.info
+
+import pycarl
+import pycarl.core
+
+import stormpy.examples
+import stormpy.examples.files
+
+import stormpy._config as config
+
+
+def example_getting_started_05():
+    # Check support for parameters
+    if not config.storm_with_pars:
+        print("Support parameters is missing. Try building storm-pars.")
+        return
+
+    import stormpy.pars
+    from pycarl.formula import FormulaType, Relation
+    if stormpy.info.storm_ratfunc_use_cln():
+        import pycarl.cln.formula
+    else:
+        import pycarl.gmp.formula
+
+    path = stormpy.examples.files.prism_pdtmc_die
+    prism_program = stormpy.parse_prism_program(path)
+
+    formula_str = "P=? [F s=7 & d=2]"
+    properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program)
+    model = stormpy.build_parametric_model(prism_program, properties)
+
+    initial_state = model.initial_states[0]
+    result = stormpy.model_checking(model, properties[0])
+    print("Result: {}".format(result.at(initial_state)))
+
+    collector = stormpy.ConstraintCollector(model)
+    print("Well formed constraints:")
+    for formula in collector.wellformed_constraints:
+        print(formula.get_constraint())
+    print("Graph preserving constraints:")
+    for formula in collector.graph_preserving_constraints:
+        print(formula.get_constraint())
+
+
+if __name__ == '__main__':
+    example_getting_started_05()