completed dtmc tests

lib/stormpy/examples/files/pomdp/3x3grid.prism

@@ -0,0 +1,59 @@
+
+
+// 3x3 grid
+// based on Littman, Cassandra and Kaelbling
+// Learning policies for partially observable environments: Scaling up  
+// Technical Report CS, Brown University
+
+pomdp
+
+
+
+// only the target is observable which is in the south east corner
+observables
+	o
+endobservables
+
+module grid
+	
+	x : [0..2]; // x coordinate
+	y : [0..2]; // y coordinate
+	o : [0..2]; // observables
+	// 0 - initial observation
+	// 1 - in the grid (not target)
+	// 2 - observe target
+	
+	// initially randomly placed within the grid (not at the target)
+	[] o=0 -> 1/8 : (o'=1) & (x'=0) & (y'=0)
+			+ 1/8 : (o'=1) & (x'=0) & (y'=1)
+			+ 1/8 : (o'=1) & (x'=0) & (y'=2)
+			+ 1/8 : (o'=1) & (x'=1) & (y'=0)
+			+ 1/8 : (o'=1) & (x'=1) & (y'=1)
+			+ 1/8 : (o'=1) & (x'=1) & (y'=2)
+			// + 1/8 : (o'=1) & (x'=2) & (y'=0) the target
+			+ 1/8 : (o'=1) & (x'=2) & (y'=1)
+			+ 1/8 : (o'=1) & (x'=2) & (y'=2);
+			
+	// move around the grid
+	[east] o=1 & !(x=1 & y=0) -> (x'=min(x+1,2)); // not reached target
+	[east] o=1 & x=1 & y=0 -> (x'=min(x+1,2)) & (o'=2);
+	[west] o=1 -> (x'=max(x-1,0)); // not reached target
+	[north] o=1 -> (y'=min(y+1,2)); // reached target
+	[south] o=1 & !(x=2 & y=1) -> (y'=max(y-1,0)); // not reached target
+	[south] o=1 & x=2 & y=1 -> (y'=max(y-1,0)) & (o'=2); // reached target
+	
+	// reached target
+	[done] o=2 -> true;
+	
+endmodule
+
+// reward structure for number of steps to reach the target
+rewards
+        [east] true : 1;
+        [west] true : 1;
+        [north] true : 1;
+        [south] true : 1;
+endrewards
+
+// target observation
+label "goal" = o=2;

src/storage/labeling.cpp

@@ -21,20 +21,26 @@ void define_labeling(py::module& m) {
 
     // StateLabeling
     py::class_<storm::models::sparse::StateLabeling, std::shared_ptr<storm::models::sparse::StateLabeling>>(m, "StateLabeling", "Labeling for states", labeling)
-        .def(py::init<uint_fast64_t>(), "state_count"_a)  // todo tests
+        .def(py::init<uint_fast64_t>(), "state_count"_a)
         .def("get_labels_of_state", &storm::models::sparse::StateLabeling::getLabelsOfState, "Get labels of given state", py::arg("state"))
         .def("add_label_to_state", &storm::models::sparse::StateLabeling::addLabelToState, "Add label to state", py::arg("label"), py::arg("state"))
         .def("has_state_label", &storm::models::sparse::StateLabeling::getStateHasLabel, "Check if the given state has the given label", py::arg("label"), py::arg("state"))
         .def("get_states", &storm::models::sparse::StateLabeling::getStates, "Get all states which have the given label", py::arg("label"))
         .def("set_states", [](storm::models::sparse::StateLabeling& labeling, std::string const& label, storm::storage::BitVector const& states) {
                 labeling.setStates(label, states);
-            }, "Set all states which have the given label", py::arg("label"), py::arg("states"))
+            }, "Add a label to the given states", py::arg("label"), py::arg("states"))
         .def("__str__", &streamToString<storm::models::sparse::StateLabeling>)
     ;
 
 
     py::class_<storm::models::sparse::ChoiceLabeling>(m, "ChoiceLabeling", "Labeling for choices", labeling)
-            .def(py::init<uint_fast64_t>(), "choice_count"_a)  // todo tests
-            .def("get_labels_of_choice", &storm::models::sparse::ChoiceLabeling::getLabelsOfChoice, py::arg("choice"), "get labels of a choice")
+            .def(py::init<uint_fast64_t>(), "choice_count"_a)
+            .def("get_labels_of_choice", &storm::models::sparse::ChoiceLabeling::getLabelsOfChoice, py::arg("choice"),  "Get labels of the given choice")
+            .def("add_label_to_choice", &storm::models::sparse::ChoiceLabeling::addLabelToChoice, "Adds a label to a given choice", py::arg("label"), py::arg("state"))
+            .def("get_choices", &storm::models::sparse::ChoiceLabeling::getChoices, py::arg("label"),  "Get all choices which have the given label")
+            .def("set_choices", [](storm::models::sparse::ChoiceLabeling& labeling, std::string const& label, storm::storage::BitVector const& choices) {
+                labeling.setChoices(label, choices);
+            },  "Add a label to a the given choices", py::arg("label"), py::arg("choices"))
+            .def("__str__", &streamToString<storm::models::sparse::ChoiceLabeling>)
     ;
 }

src/storage/model.cpp

@@ -221,14 +221,14 @@ void define_sparse_model(py::module& m) {
     py::class_<SparseCtmc<double>, std::shared_ptr<SparseCtmc<double>>>(m, "SparseCtmc", "CTMC in sparse representation", model)
         .def(py::init<SparseCtmc<double>>(), py::arg("other_model"))
         .def(py::init<ModelComponents<double> const&>(), py::arg("components"))
-        .def_property_readonly("exit_rates", [](SparseCtmc<double> const& ctmc) { return ctmc.getExitRateVector(); }) //todo new: tests
+        .def_property_readonly("exit_rates", [](SparseCtmc<double> const& ctmc) { return ctmc.getExitRateVector(); })
         .def("__str__", &getModelInfoPrinter)
     ;
     py::class_<SparseMarkovAutomaton<double>, std::shared_ptr<SparseMarkovAutomaton<double>>>(m, "SparseMA", "MA in sparse representation", model)
         .def(py::init<SparseMarkovAutomaton<double>>(), py::arg("other_model"))
         .def(py::init<ModelComponents<double> const&>(), py::arg("components"))
         .def_property_readonly("exit_rates", [](SparseMarkovAutomaton<double> const& ma) { return ma.getExitRates(); })
-        .def_property_readonly("markovian_states", [](SparseMarkovAutomaton<double> const& ma) { return ma.getMarkovianStates(); }) //todo new: tests
+        .def_property_readonly("markovian_states", [](SparseMarkovAutomaton<double> const& ma) { return ma.getMarkovianStates(); })
         .def_property_readonly("nondeterministic_choice_indices", [](SparseMarkovAutomaton<double> const& ma) { return ma.getNondeterministicChoiceIndices(); })
         .def("apply_scheduler", [](SparseMarkovAutomaton<double> const& ma, storm::storage::Scheduler<double> const& scheduler, bool dropUnreachableStates) { return ma.applyScheduler(scheduler, dropUnreachableStates); } , "apply scheduler", "scheduler"_a, "drop_unreachable_states"_a = true)
         .def("__str__", &getModelInfoPrinter)
@@ -239,7 +239,7 @@ void define_sparse_model(py::module& m) {
     py::class_<SparseRewardModel<double>>(m, "SparseRewardModel", "Reward structure for sparse models")
         .def(py::init<boost::optional<std::vector<double>> const&, boost::optional<std::vector<double>> const&,
                 boost::optional<storm::storage::SparseMatrix<double>> const&>(), py::arg("optional_state_reward_vector") = boost::none,
-                py::arg("optional_state_action_reward_vector") = boost::none,  py::arg("optional_transition_reward_matrix") = boost::none) // todo tests
+                py::arg("optional_state_action_reward_vector") = boost::none,  py::arg("optional_transition_reward_matrix") = boost::none)
         .def_property_readonly("has_state_rewards", &SparseRewardModel<double>::hasStateRewards)
         .def_property_readonly("has_state_action_rewards", &SparseRewardModel<double>::hasStateActionRewards)
         .def_property_readonly("has_transition_rewards", &SparseRewardModel<double>::hasTransitionRewards)

tests/storage/test_model_components.py

@@ -16,8 +16,14 @@ class TestSparseModelComponents:
         assert components.player1_matrix is None
         assert not components.rate_transitions
 
+    # todo: ctmc
+    # todo: ma
+    # todo mdp
+    # todo pomdp?
+
     def test_build_dtmc_from_model_components(self):
         nr_states = 13
+        nr_choices = 13
 
         # TransitionMatrix
         builder = stormpy.SparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False,
@@ -45,8 +51,8 @@ class TestSparseModelComponents:
 
         # StateLabeling
         state_labeling = stormpy.storage.StateLabeling(nr_states)
-        labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'}
-        for label in labels:
+        state_labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'}
+        for label in state_labels:
             state_labeling.add_label(label)
         # Add label to one state
         state_labeling.add_label_to_state('init', 0)
@@ -65,8 +71,8 @@ class TestSparseModelComponents:
         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)
 
-        # todo state valuations
-        manager = stormpy.ExpressionManager() # todo correct?
+        # StateValuations
+        manager = stormpy.ExpressionManager()
         var_s = manager.create_integer_variable(name='s')
         var_d = manager.create_integer_variable(name='d')
         v_builder = stormpy.StateValuationsBuilder()
@@ -74,11 +80,10 @@ class TestSparseModelComponents:
         v_builder.add_variable(var_s)
         v_builder.add_variable(var_d)
 
-
         for s in range(7):
-            v_builder.add_state(state=s,integer_values=[s,0])
-        for s in range(7,13):
-            v_builder.add_state(state=s,integer_values=[7,s-6])
+            v_builder.add_state(state=s, integer_values=[s, 0])
+        for s in range(7, 13):
+            v_builder.add_state(state=s, integer_values=[7, s - 6])
 
         state_valuations = v_builder.build(13)
 
@@ -88,8 +93,7 @@ class TestSparseModelComponents:
         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)
-        for i in range(8, 14):
-            id_to_command_set_mapping[8].insert(7)
+        id_to_command_set_mapping[8].insert(7)
         #
         choice_origins = stormpy.PrismChoiceOrigins(prism_program, index_to_identifier_mapping,
                                                     id_to_command_set_mapping)
@@ -106,8 +110,8 @@ class TestSparseModelComponents:
         assert not dtmc.supports_parameters
 
         # test transition matrix
-        assert dtmc.nr_choices == 13
-        assert dtmc.nr_states == 13
+        assert dtmc.nr_choices == nr_choices
+        assert dtmc.nr_states == nr_states
         assert dtmc.nr_transitions == 20
         assert dtmc.transition_matrix.nr_entries == dtmc.nr_transitions
         for e in dtmc.transition_matrix:
@@ -126,10 +130,21 @@ class TestSparseModelComponents:
             assert reward == 1.0 or reward == 0.0
         assert not dtmc.reward_models["coin_flips"].has_transition_rewards
 
-        # choice_labeling
+        # test choice_labeling
         assert not dtmc.has_choice_labeling()
-        # todo state_valuations
-        assert dtmc.has_state_valuations() # todo  more tests
-        # todo choice_origins
-        assert dtmc.has_choice_origins() #todo more tests
+
+        # test state_valuations
+        assert dtmc.has_state_valuations()
+        assert dtmc.state_valuations
+        value_s = [None] * nr_states
+        value_d = [None] * nr_states
+        for s in range(0, dtmc.nr_states):
+            value_s[s] = dtmc.state_valuations.get_integer_value(s, var_s)
+            value_d[s] = dtmc.state_valuations.get_integer_value(s, var_d)
+        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
+        assert dtmc.has_choice_origins()
         assert dtmc.choice_origins is components.choice_origins
+        assert dtmc.choice_origins.get_number_of_identifiers() == 9