diff --git a/doc/source/doc/building_ctmcs.rst b/doc/source/doc/building_ctmcs.rst index aea3d4a..27ecc0b 100644 --- a/doc/source/doc/building_ctmcs.rst +++ b/doc/source/doc/building_ctmcs.rst @@ -6,7 +6,7 @@ Continuous-time Markov chains (CTMCs) Background ===================== -In this section, we explain how Stormpy can be used to build a CTMC representing a cyclic server polling system. +In this section, we explain how Stormpy can be used to build a simple CTMC. Building CTMCs works similar to building DTMCs as in :doc:`building_dtmcs`, but additionally every state is equipped with an exit rate. .. seealso:: `01-building-ctmcs.py ` @@ -17,75 +17,50 @@ First, we import Stormpy:: Transition Matrix ===================== -We build the transition matrix using numpy. As an alternative, the SparseMatrixBuilder can be used here:: +In this example, we build the transition matrix using a numpy array:: >>> import numpy as np >>> 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') - -We do not specify the row_group_indices. Thus, the following function call returns a sparse matrix with default row groups.:: + ... [0, 1.5, 0, 0], + ... [3, 0, 1.5, 0], + ... [0, 3, 0, 1.5], + ... [0, 0, 3, 0], ], dtype='float64') + +The following function call returns a sparse matrix with default row groups:: >>> transition_matrix = stormpy.build_sparse_matrix(transitions) + >>> print(transition_matrix)< + + 0 1 2 3 + ---- group 0/3 ---- + 0 ( 0 1.5 0 0 ) 0 + ---- group 1/3 ---- + 1 ( 3 0 1.5 0 ) 1 + ---- group 2/3 ---- + 2 ( 0 3 0 1.5 ) 2 + ---- group 3/3 ---- + 3 ( 0 0 3 0 ) 3 + 0 1 2 3 + Labeling ================ -Next, we create the state labeling:: +The state labeling is created analogously to the previous example:: - >>> state_labeling = stormpy.storage.StateLabeling(12) - >>> state_labels = {'init', 'deadlock', 'target'} + >>> state_labeling = stormpy.storage.StateLabeling(4) + >>> state_labels = {'empty', 'init', 'deadlock', 'full'} >>> for label in state_labels: ... state_labeling.add_label(label) >>> state_labeling.add_label_to_state('init', 0) - >>> state_labeling.set_states('target', stormpy.BitVector(12, [5, 8])) - -For the choice labeling this works similar:: - - >>> 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) - -To set the same label for multiple choices, we can use a BitVector:: - - >>> 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 -================== - -Now, we create the reward models, beginning with the reward model named 'served' which has state-action rewards:: - - >>> reward_models = {} - >>> 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) - -In the same way we can create a second reward model. This time we consider 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) + >>> state_labeling.add_label_to_state('empty', 0) + >>> state_labeling.add_label_to_state('full', 3) Exit Rates ==================== Lastly, we equip every state with an exit rate:: - >>> 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] + >>> exit_rates = [1.5, 4.5, 4.5, 3.0] Building the Model ==================== @@ -93,9 +68,8 @@ Building the Model Now, we can collect all components, including the choice labeling and the exit rates. To let the transition values be interpreted as rates we set rate_transitions to True:: - >>> 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 + components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, rate_transitions=True) + components.exit_rates = exit_rates And finally, we can build the model:: @@ -103,20 +77,15 @@ And finally, we can build the model:: >>> print(ctmc) -------------------------------------------------------------- Model type: CTMC (sparse) - States: 12 - Transitions: 22 - Reward Models: waiting, served - State Labels: 3 labels + States: 4 + Transitions: 6 + Reward Models: none + State Labels: 4 labels * init -> 1 item(s) + * empty -> 1 item(s) * deadlock -> 0 item(s) - * target -> 2 item(s) - Choice Labels: 6 labels - * loop2a -> 2 item(s) - * serve1 -> 2 item(s) - * serve2 -> 2 item(s) - * loop2b -> 2 item(s) - * loop1b -> 2 item(s) - * loop1a -> 2 item(s) + * full -> 1 item(s) + Choice Labels: none -------------------------------------------------------------- diff --git a/doc/source/doc/building_dtmcs.rst b/doc/source/doc/building_dtmcs.rst index f5493ac..9def2f1 100644 --- a/doc/source/doc/building_dtmcs.rst +++ b/doc/source/doc/building_dtmcs.rst @@ -75,9 +75,13 @@ In order to specify the state labeling we create an empty labeling for the given >>> for label in labels: ... state_labeling.add_label(label) -Next, we set teh associations between the labels and the respective states.:: +Labels can be asociated with states. As an example, we label the state 0 with 'init':: >>> state_labeling.add_label_to_state('init', 0) + >>> print(state_labeling.get_states('init')) + bit vector(1/13) [0] +Next, we set the associations between the remaining labels and states.:: + >>> state_labeling.add_label_to_state('one', 7) >>> state_labeling.add_label_to_state('two', 8) >>> state_labeling.add_label_to_state('three', 9) @@ -88,8 +92,19 @@ Next, we set teh associations between the labels and the respective states.:: To set the same label for multiple states, we can use a BitVector representation for the set of states:: >>> state_labeling.set_states('done', stormpy.BitVector(13, [7, 8, 9, 10, 11, 12])) + >>> print(state_labeling) + 9 labels + * one -> 1 item(s) + * four -> 1 item(s) + * done -> 6 item(s) + * three -> 1 item(s) + * init -> 1 item(s) + * two -> 1 item(s) + * six -> 1 item(s) + * deadlock -> 0 item(s) + * five -> 1 item(s) -In addition, it is possible to define a choice labeling, which is described in :doc:`building_ctmcs`. +Defining a choice labeling is possible in a similar way. Reward Models ==================== diff --git a/doc/source/doc/building_mas.rst b/doc/source/doc/building_mas.rst index e770038..cdc3034 100644 --- a/doc/source/doc/building_mas.rst +++ b/doc/source/doc/building_mas.rst @@ -8,6 +8,7 @@ Background ... works similar as explained in as in :doc:`building_dtmcs` +Build simple ma example .. seealso:: `01-building-mas.py ` First, we import Stormpy:: @@ -15,7 +16,8 @@ First, we import Stormpy:: >>> import stormpy Transition Matrix -===================== +================== + Labeling diff --git a/doc/source/doc/building_mdps.rst b/doc/source/doc/building_mdps.rst index d1a5505..eefd770 100644 --- a/doc/source/doc/building_mdps.rst +++ b/doc/source/doc/building_mdps.rst @@ -5,7 +5,7 @@ Discrete-time Markov decision processes (MDPs) Background ===================== - +Same example of die knuth as in dtmc but mdp (model with nondeterminsm) .. seealso:: `01-building-mdps.py ` @@ -15,6 +15,7 @@ First, we import Stormpy:: Transition Matrix ===================== +more choices than states! Labeling @@ -31,3 +32,8 @@ Exit Rates Building the Model ==================== + +POMDPS +==================== +Give +observations as .. \ No newline at end of file