From d1c3be5dba5b6cd0a7bfad4d685da7c4d8a9cd59 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Mon, 2 Dec 2019 18:31:53 +0100
Subject: [PATCH] slightly awkward example to change probabilities

---
 .../parametric_models/04-parametric-models.py | 54 +++++++++++++++++++
 1 file changed, 54 insertions(+)
 create mode 100644 examples/parametric_models/04-parametric-models.py

diff --git a/examples/parametric_models/04-parametric-models.py b/examples/parametric_models/04-parametric-models.py
new file mode 100644
index 0000000..7fbf8a0
--- /dev/null
+++ b/examples/parametric_models/04-parametric-models.py
@@ -0,0 +1,54 @@
+import stormpy
+import stormpy.core
+
+import pycarl
+import pycarl.core
+
+import stormpy.examples
+import stormpy.examples.files
+import stormpy._config as config
+
+
+
+def example_parametric_models_04():
+    # Check support for parameters
+    if not config.storm_with_pars:
+        print("Support parameters is missing. Try building storm-pars.")
+        return
+
+    import stormpy.pars
+    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(formula_str, prism_program)
+    model = stormpy.build_parametric_model(prism_program, properties)
+
+    # Modify
+    i = 0
+    for state in model.states:
+        if state.id in model.initial_states:
+            print(state)
+        for action in state.actions:
+            for transition in action.transitions:
+                if len(transition.value().gather_variables()) > 0:
+
+                    new_var = pycarl.Variable("p{}".format(i))
+                    i += 1
+                    new_pol = stormpy.Polynomial(new_var)
+                    pol_in_right_format = stormpy.FactorizedPolynomial(new_pol, transition.value().numerator.cache())
+
+                    new_factorized_ratfunc = stormpy.FactorizedRationalFunction(pol_in_right_format)
+                    transition.set_value(new_factorized_ratfunc)
+
+    # Display
+    for state in model.states:
+        if state.id in model.initial_states:
+            print(state)
+        for action in state.actions:
+            for transition in action.transitions:
+                print("From state {}, with probability {}, go to state {}".format(state, transition.value(), transition.column))
+
+
+if __name__ == '__main__':
+    example_parametric_models_04()