completed ctmc tests

tests/storage/test_model_components.py

@@ -1,7 +1,7 @@
 import stormpy
 import stormpy.logic
 from helpers.helper import get_example_path
-import pytest
+from configurations import numpy_avail
 
 
 class TestSparseModelComponents:
@@ -25,7 +25,7 @@ class TestSparseModelComponents:
         nr_states = 13
         nr_choices = 13
 
-        # TransitionMatrix
+        # transition_matrix
         builder = stormpy.SparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False,
                                               has_custom_row_grouping=False, row_groups=0)
 
@@ -49,7 +49,7 @@ class TestSparseModelComponents:
         # Build transition matrix, update number of rows and columns
         transition_matrix = builder.build(nr_states, nr_states)
 
-        # StateLabeling
+        # state_labeling
         state_labeling = stormpy.storage.StateLabeling(nr_states)
         state_labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'}
         for label in state_labels:
@@ -62,16 +62,16 @@ class TestSparseModelComponents:
         state_labeling.add_label_to_state('four', 10)
         state_labeling.add_label_to_state('five', 11)
         state_labeling.add_label_to_state('six', 12)
-        # Set the labeling of states given in a bit vector, where length = nr_states
+
         state_labeling.set_states('done', stormpy.BitVector(nr_states, [7, 8, 9, 10, 11, 12]))
 
-        # RewardModels
+        # reward_models
         reward_models = {}
         # Create a vector representing the state-action rewards
         action_reward = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
         reward_models['coin_flips'] = stormpy.SparseRewardModel(optional_state_action_reward_vector=action_reward)
 
-        # StateValuations
+        # state_valuations
         manager = stormpy.ExpressionManager()
         var_s = manager.create_integer_variable(name='s')
         var_d = manager.create_integer_variable(name='d')
@@ -87,29 +87,29 @@ class TestSparseModelComponents:
 
         state_valuations = v_builder.build(13)
 
-        # todo choice origins:
+        # choice origins
         prism_program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
         index_to_identifier_mapping = [1, 2, 3, 4, 5, 6, 7, 8, 8, 8, 8, 8, 8]
         id_to_command_set_mapping = [stormpy.FlatSet() for _ in range(9)]
         for i in range(1, 8):  # 0: no origin
             id_to_command_set_mapping[i].insert(i - 1)
         id_to_command_set_mapping[8].insert(7)
-        #
         choice_origins = stormpy.PrismChoiceOrigins(prism_program, index_to_identifier_mapping,
                                                     id_to_command_set_mapping)
 
+        # Construct Components
         components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling,
                                                    reward_models=reward_models)
         components.choice_origins = choice_origins
-
         components.state_valuations = state_valuations
 
+        # Build DTMC
         dtmc = stormpy.storage.SparseDtmc(components)
 
         assert type(dtmc) is stormpy.SparseDtmc
         assert not dtmc.supports_parameters
 
-        # test transition matrix
+        # Test transition matrix
         assert dtmc.nr_choices == nr_choices
         assert dtmc.nr_states == nr_states
         assert dtmc.nr_transitions == 20
@@ -119,10 +119,10 @@ class TestSparseModelComponents:
         for state in dtmc.states:
             assert len(state.actions) <= 1
 
-        # test state_labeling
+        # Test state_labeling
         assert dtmc.labeling.get_labels() == {'init', 'deadlock', 'done', 'one', 'two', 'three', 'four', 'five', 'six'}
 
-        # test reward_models
+        # Test reward_models
         assert len(dtmc.reward_models) == 1
         assert not dtmc.reward_models["coin_flips"].has_state_rewards
         assert dtmc.reward_models["coin_flips"].has_state_action_rewards
@@ -130,10 +130,10 @@ class TestSparseModelComponents:
             assert reward == 1.0 or reward == 0.0
         assert not dtmc.reward_models["coin_flips"].has_transition_rewards
 
-        # test choice_labeling
+        # Test choice_labeling
         assert not dtmc.has_choice_labeling()
 
-        # test state_valuations
+        # Test state_valuations
         assert dtmc.has_state_valuations()
         assert dtmc.state_valuations
         value_s = [None] * nr_states
@@ -144,7 +144,162 @@ class TestSparseModelComponents:
         assert value_s == [0, 1, 2, 3, 4, 5, 6, 7, 7, 7, 7, 7, 7]
         assert value_d == [0, 0, 0, 0, 0, 0, 0, 1, 2, 3, 4, 5, 6]
 
-        # todo choice_origins more tests
+        # Test choice_origins
         assert dtmc.has_choice_origins()
         assert dtmc.choice_origins is components.choice_origins
         assert dtmc.choice_origins.get_number_of_identifiers() == 9
+
+    @numpy_avail
+    def test_build_ctmc_from_model_components(self):
+        import numpy as np
+
+        nr_states = 12
+        nr_choices = 12
+
+        # Build transition_matrix
+        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')
+
+        transition_matrix = stormpy.build_sparse_matrix(transitions)
+
+        # state_labeling
+        state_labeling = stormpy.storage.StateLabeling(nr_states)
+        # Add labels
+        state_labels = {'init', 'deadlock', 'target'}
+        for label in state_labels:
+            state_labeling.add_label(label)
+
+        # Add labels to states
+        state_labeling.add_label_to_state('init', 0)
+        state_labeling.set_states('target', stormpy.BitVector(nr_states, [5, 8]))
+
+        # reward_models
+        reward_models = {}
+        # vector representing 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)
+
+        # vector representing 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)
+
+        # choice_labeling
+        choice_labeling = stormpy.storage.ChoiceLabeling(nr_choices)
+        choice_labels = {'loop1a', 'loop1b', 'serve1', 'loop2a', 'loop2b', 'serve2'}
+        # Add labels
+        for label in choice_labels:
+            choice_labeling.add_label(label)
+
+        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]))
+
+        # state exit rates
+        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]
+
+        # state_valuations
+        manager = stormpy.ExpressionManager()
+        var_s = manager.create_integer_variable(name='s')
+        var_a = manager.create_integer_variable(name='a')
+        var_s1 = manager.create_integer_variable(name='s1')
+        var_s2 = manager.create_integer_variable(name='s2')
+        v_builder = stormpy.StateValuationsBuilder()
+        v_builder.add_variable(var_s)
+        v_builder.add_variable(var_a)
+        v_builder.add_variable(var_s1)
+        v_builder.add_variable(var_s2)
+
+        v_builder.add_state(state=0, boolean_values=[], integer_values=[1, 0, 0, 0], rational_values=[])
+        v_builder.add_state(state=1, boolean_values=[], integer_values=[1, 0, 1, 0], rational_values=[])
+        v_builder.add_state(state=2, boolean_values=[], integer_values=[1, 0, 0, 1], rational_values=[])
+        v_builder.add_state(state=3, boolean_values=[], integer_values=[2, 0, 0, 0], rational_values=[])
+        v_builder.add_state(state=4, boolean_values=[], integer_values=[1, 0, 1, 1], rational_values=[])
+        v_builder.add_state(state=5, boolean_values=[], integer_values=[1, 1, 1, 0], rational_values=[])
+        v_builder.add_state(state=6, boolean_values=[], integer_values=[2, 0, 0, 1], rational_values=[])
+        v_builder.add_state(state=7, boolean_values=[], integer_values=[2, 0, 1, 0], rational_values=[])
+        v_builder.add_state(state=8, boolean_values=[], integer_values=[1, 1, 1, 1], rational_values=[])
+        v_builder.add_state(state=9, boolean_values=[], integer_values=[2, 0, 1, 1], rational_values=[])
+        v_builder.add_state(state=10, boolean_values=[], integer_values=[2, 1, 0, 1], rational_values=[])
+        v_builder.add_state(state=11, boolean_values=[], integer_values=[2, 1, 1, 1], rational_values=[])
+
+        state_valuations = v_builder.build(nr_states)
+
+        # set rate_transitions to True: the transition values are interpreted as rates
+        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.state_valuations = state_valuations
+
+        ctmc = stormpy.storage.SparseCtmc(components)
+        assert type(ctmc) is stormpy.SparseCtmc
+        assert not ctmc.supports_parameters
+
+        # Test transition matrix
+        assert ctmc.nr_choices == nr_choices
+        assert ctmc.nr_states == nr_states
+        assert ctmc.nr_transitions == 22
+        assert ctmc.transition_matrix.nr_columns == nr_choices
+        assert ctmc.transition_matrix.nr_rows == nr_states
+        for e in ctmc.transition_matrix:
+            assert e.value() == 0.5 or e.value() == 0 or e.value() == 200 or e.value() == 1.0
+        for state in ctmc.states:
+            assert len(state.actions) <= 3
+
+        # Test state_labeling
+        assert ctmc.labeling.get_labels() == {'target', 'init', 'deadlock'}
+
+        # Test reward_models
+        assert len(ctmc.reward_models) == 2
+        assert not ctmc.reward_models["served"].has_state_rewards
+        assert ctmc.reward_models["served"].has_state_action_rewards
+        assert ctmc.reward_models["served"].state_action_rewards == [0.0, 0.0, 0.0, 0.0, 0.0, 0.6666666666666666, 0.0, 0.0, 1.0, 0.0,
+                                                                     0.0, 0.0]
+        assert not ctmc.reward_models["served"].has_transition_rewards
+
+        assert ctmc.reward_models["waiting"].has_state_rewards
+        assert not ctmc.reward_models["waiting"].has_state_action_rewards
+        assert ctmc.reward_models["waiting"].state_rewards == [0.0, 1.0, 0.0, 0.0, 1.0, 0.0, 0.0, 1.0, 0.0, 1.0, 0.0, 1.0]
+        assert not ctmc.reward_models["waiting"].has_transition_rewards
+
+        # Test choice_labeling
+        assert ctmc.has_choice_labeling()
+        assert ctmc.choice_labeling.get_labels() == {'loop1a', 'loop1b', 'serve1', 'loop2a', 'loop2b', 'serve2'}
+
+        # Test state_valuations
+        assert ctmc.has_state_valuations()
+        assert ctmc.state_valuations
+        value_s = [None] * nr_states
+        value_a = [None] * nr_states
+        value_s1 = [None] * nr_states
+        value_s2 = [None] * nr_states
+        for s in range(0, ctmc.nr_states):
+            value_s[s] = ctmc.state_valuations.get_integer_value(s, var_s)
+            value_a[s] = ctmc.state_valuations.get_integer_value(s, var_a)
+            value_s1[s] = ctmc.state_valuations.get_integer_value(s, var_s1)
+            value_s2[s] = ctmc.state_valuations.get_integer_value(s, var_s2)
+        assert value_s == [1,1,1,2,1,1,2,2,1,2,2,2]
+        assert value_a == [0,0,0,0,0,1,0,0,1,0,1,1]
+        assert value_s1 == [0,1,0,0,1,1,0,1,1,1,0,1]
+        assert value_s2 == [0,0,1,0,1,0,1,0,1,1,1,1]
+
+        # Test choice_origins
+        assert not ctmc.has_choice_origins()
+
+        # Test exit_rates
+        assert ctmc.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]
+