From afc8af220e927122e3c0256cee15ee4aee061b1a Mon Sep 17 00:00:00 2001
From: hannah <hannah.mertens@rwth-aachen.de>
Date: Sat, 27 Jun 2020 17:39:29 +0200
Subject: [PATCH] doc ctmcs example

---
 examples/building_ctmcs/01-building-ctmcs.py | 77 ++++++++++++++++++++
 examples/building_dtmcs/01-building-dtmcs.py |  1 -
 2 files changed, 77 insertions(+), 1 deletion(-)
 create mode 100644 examples/building_ctmcs/01-building-ctmcs.py

diff --git a/examples/building_ctmcs/01-building-ctmcs.py b/examples/building_ctmcs/01-building-ctmcs.py
new file mode 100644
index 0000000..07df0e4
--- /dev/null
+++ b/examples/building_ctmcs/01-building-ctmcs.py
@@ -0,0 +1,77 @@
+import stormpy
+import numpy as np
+
+# polling example [IT90]
+# gxn/dxp 26/01/00
+def example_building_ctmcs_01():
+
+    # Building the transition matrix using numpy
+    transitions = np.array([
+        [0, 0.5, 0.5, 200, 0, 0, 0, 0, 0, 0, 0, 0],
+        [0, 0, 0, 0, 0.5, 200, 0, 0, 0, 0, 0, 0],
+        [0, 0, 0, 0, 0.5, 0, 200, 0, 0, 0, 0, 0],
+        [200, 0, 0, 0, 0, 0, 0.5, 0.5, 0, 0, 0, 0],
+        [0, 0, 0, 0, 0, 0, 0, 0, 200, 0, 0, 0],
+        [0, 0, 0, 1, 0, 0, 0, 0, 0.5, 0, 0, 0],
+        [0, 0, 0, 0, 0, 0, 0, 0, 0, 0.5, 200, 0],
+        [0, 200, 0, 0, 0, 0, 0, 0, 0, 0.5, 0, 0],
+        [0, 0, 0, 0, 0, 0, 1, 0, 0, 0 ,0, 0],
+        [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 200],
+        [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0.5	],
+        [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
+    ], dtype='float64')
+
+    # Default row groups: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]
+    transition_matrix = stormpy.build_sparse_matrix(transitions)
+
+
+    # State labeling
+    state_labeling = stormpy.storage.StateLabeling(12)
+    state_labels = {'init', 'deadlock', 'target'}
+    for label in state_labels:
+        state_labeling.add_label(label)
+
+    # Adding label to states
+    state_labeling.add_label_to_state('init', 0)
+    # Sets the labeling of states given in a BitVector (length: nr_states)
+    state_labeling.set_states('target', stormpy.BitVector(12, [5, 8]))
+
+    # Choice labeling
+    nr_choices = 12
+    choice_labeling = stormpy.storage.ChoiceLabeling(nr_choices)
+    choice_labels = {'loop1a', 'loop1b', 'serve1', 'loop2a', 'loop2b', 'serve2'}
+    for label in choice_labels:
+        choice_labeling.add_label(label)
+    # Sets the labeling of states given in a bit vector (length: nr_choices)
+    choice_labeling.set_choices('loop1a', stormpy.BitVector(nr_choices, [0, 2]))
+    choice_labeling.set_choices('loop1b', stormpy.BitVector(nr_choices, [1, 4]))
+    choice_labeling.set_choices('serve1', stormpy.BitVector(nr_choices, [5, 8]))
+    choice_labeling.set_choices('loop2a', stormpy.BitVector(nr_choices, [3, 7]))
+    choice_labeling.set_choices('loop2b', stormpy.BitVector(nr_choices, [6, 9]))
+    choice_labeling.set_choices('serve2', stormpy.BitVector(nr_choices, [10, 11]))
+
+    # Reward models:
+    reward_models = {}
+    # Create a vector representing the state-action rewards
+    action_reward = [0.0, 0.0, 0.0, 0.0, 0.0, 2/3, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0]
+    reward_models['served'] = stormpy.SparseRewardModel(optional_state_action_reward_vector = action_reward)
+
+    ## Create a vector representing the state rewards
+    state_reward = [0.0, 1.0, 0.0, 0.0, 1.0, 0.0, 0.0, 1.0, 0.0, 1.0, 0.0, 1.0]
+    reward_models['waiting'] = stormpy.SparseRewardModel(optional_state_reward_vector = state_reward)
+
+    # Exit rate for each state
+    exit_rates =  [201.0, 200.5, 200.5, 201.0, 200.0, 1.5, 200.5, 200.5, 1.0, 200.0, 1.5, 1.0]
+
+    # Collect components, rate_transitions = True, because the transition values are interpreted as rates (CTMC specific)
+    components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models, rate_transitions = True)
+    components.choice_labeling = choice_labeling
+    components.exit_rates = exit_rates
+
+    # Build the model
+    ctmc = stormpy.storage.SparseCtmc(components)
+
+    print(ctmc)
+
+if __name__ == '__main__':
+    example_building_ctmcs_01()
\ No newline at end of file
diff --git a/examples/building_dtmcs/01-building-dtmcs.py b/examples/building_dtmcs/01-building-dtmcs.py
index 18cdafb..58e8e94 100644
--- a/examples/building_dtmcs/01-building-dtmcs.py
+++ b/examples/building_dtmcs/01-building-dtmcs.py
@@ -1,5 +1,4 @@
 import stormpy
-import numpy as np
 
 
 def example_building_dtmcs_01():