From 8589e9be9c7d7e99be61c7bd7c01dd630cded5f2 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Mon, 2 Dec 2019 18:03:11 +0100
Subject: [PATCH] Added missing file that illustrates some ways to explore
 parametric models

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

diff --git a/examples/parametric_models/03-parametric-models.py b/examples/parametric_models/03-parametric-models.py
new file mode 100644
index 0000000..15bc8dc
--- /dev/null
+++ b/examples/parametric_models/03-parametric-models.py
@@ -0,0 +1,59 @@
+import time
+
+import stormpy
+import stormpy.core
+
+import stormpy.examples
+import stormpy.examples.files
+
+def example_parametric_models_03():
+    path = stormpy.examples.files.prism_dtmc_brp
+    prism_program = stormpy.parse_prism_program(path)
+
+    formula_str = "P=? [F \"target\"]"
+    properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program)
+    model = stormpy.build_parametric_model(prism_program, properties)
+
+    print(model.model_type)
+    start = time.time()
+    t = 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 transition.value().constant_part() == 1:
+                    t += 1
+                    #print("From state {}, with probability {}, go to state {}".format(state, transition.value(), transition.column))
+    print(time.time() - start)
+    print(t)
+
+
+    t2 = 0
+    start = time.time()
+    for row_group in range(model.nr_states):
+        for row in range(model.transition_matrix.get_row_group_start(row_group), model.transition_matrix.get_row_group_end(row_group)):
+            for entry in model.transition_matrix.get_row(row):
+                if entry.value().constant_part() == 1:
+                    t2 += 1
+    print(time.time() - start)
+    print(t2)
+
+    states_and_transitions = []
+    for row_group in range(model.nr_states):
+        states_and_transitions.append([])
+        for row in range(model.transition_matrix.get_row_group_start(row_group), model.transition_matrix.get_row_group_end(row_group)):
+            for entry in model.transition_matrix.get_row(row):
+                states_and_transitions[-1].append((entry.value(), entry.column))
+    t3 = 0
+    start = time.time()
+    for s in states_and_transitions:
+        for (v,c) in s:
+            if v.constant_part() == 1:
+                t3 += 1
+    print(time.time() - start)
+    print(t3)
+
+
+if __name__ == '__main__':
+    example_parametric_models_03()
\ No newline at end of file