Tests for scheduler application and MA->CTMC translation

lib/stormpy/examples/files/ma/ctmc.ma

@@ -0,0 +1,14 @@
+
+ma
+
+module simple
+	
+	s : [0..4];
+	
+	
+	<> (s=0) -> 0.8 : (s'=1) + 0.2 : (s'=2);
+	<> (s=1) -> 9 : (s'=0) + 1 : (s'=3);
+	<> (s=2) -> 12 : (s'=4);
+	<> (s>2) -> 1 : true;
+	
+endmodule

src/storage/model.cpp

@@ -206,7 +206,11 @@ void define_sparse_model(py::module& m) {
     ;
     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_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)
+        .def_property_readonly("convertible_to_ctmc", &SparseMarkovAutomaton<double>::isConvertibleToCtmc, "Check whether the MA can be converted into a CTMC.")
+        .def("convert_to_ctmc", &SparseMarkovAutomaton<double>::convertToCtmc, "Convert the MA into a CTMC.")
     ;
 
     py::class_<SparseRewardModel<double>>(m, "SparseRewardModel", "Reward structure for sparse models")
@@ -256,6 +260,8 @@ void define_sparse_model(py::module& m) {
         .def("__str__", &getModelInfoPrinter)
     ;
     py::class_<SparseMarkovAutomaton<RationalFunction>, std::shared_ptr<SparseMarkovAutomaton<RationalFunction>>>(m, "SparseParametricMA", "pMA in sparse representation", modelRatFunc)
+        .def_property_readonly("nondeterministic_choice_indices", [](SparseMarkovAutomaton<RationalFunction> const& ma) { return ma.getNondeterministicChoiceIndices(); })
+        .def("apply_scheduler", [](SparseMarkovAutomaton<RationalFunction> const& ma, storm::storage::Scheduler<RationalFunction> const& scheduler, bool dropUnreachableStates) { return ma.applyScheduler(scheduler, dropUnreachableStates); } , "apply scheduler", "scheduler"_a, "drop_unreachable_states"_a = true)
         .def("__str__", &getModelInfoPrinter)
     ;
 

src/storage/scheduler.cpp

@@ -19,6 +19,7 @@ void define_scheduler(py::module& m, std::string vt_suffix) {
             .def_property_readonly("memoryless", &Scheduler::isMemorylessScheduler, "Is the scheduler memoryless?")
             .def_property_readonly("memory_size", &Scheduler::getNumberOfMemoryStates, "How much memory does the scheduler take?")
             .def_property_readonly("deterministic", &Scheduler::isDeterministicScheduler, "Is the scheduler deterministic?")
+            .def_property_readonly("partial", &Scheduler::isPartialScheduler, "Is the scheduler partial?")
             .def("get_choice", &Scheduler::getChoice, py::arg("state_index"), py::arg("memory_index") = 0)
             .def("compute_action_support", &Scheduler::computeActionSupport, "nondeterministic_choice_indices"_a)
     ;

tests/storage/test_model.py

@@ -119,7 +119,6 @@ class TestSparseModel:
         assert model.nr_states == 16
         assert model.nr_observations == 8
 
-
     def test_build_ma(self):
         program = stormpy.parse_prism_program(get_example_path("ma", "simple.ma"), False, True)
         formulas = stormpy.parse_properties_for_prism_program("Pmax=? [ F<=2 s=2 ]", program)
@@ -130,6 +129,22 @@ class TestSparseModel:
         assert not model.supports_parameters
         assert type(model) is stormpy.SparseMA
 
+    def test_convert_ma_to_ctmc(self):
+        program = stormpy.parse_prism_program(get_example_path("ma", "ctmc.ma"), True)
+        formulas = stormpy.parse_properties_for_prism_program("P=? [ F<=3 s=2 ]", program)
+        model = stormpy.build_model(program, formulas)
+        assert model.nr_states == 4
+        assert model.nr_transitions == 6
+        assert model.model_type == stormpy.ModelType.MA
+        assert type(model) is stormpy.SparseMA
+
+        assert model.convertible_to_ctmc
+        ctmc = model.convert_to_ctmc()
+        assert ctmc.nr_states == 4
+        assert ctmc.nr_transitions == 6
+        assert ctmc.model_type == stormpy.ModelType.CTMC
+        assert type(ctmc) is stormpy.SparseCtmc
+
     def test_initial_states(self):
         program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
         formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program)

tests/storage/test_scheduler.py

@@ -63,3 +63,50 @@ class TestScheduler:
                 assert action == 1
             else:
                 assert action == 0
+
+    def test_apply_scheduler_mdp(self):
+        program = stormpy.parse_prism_program(get_example_path("mdp", "coin2-2.nm"))
+        formulas = stormpy.parse_properties_for_prism_program("Pmin=? [ F \"finished\" & \"all_coins_equal_1\"]", program)
+        model = stormpy.build_model(program, formulas)
+        assert model.nr_states == 272
+        assert model.nr_transitions == 492
+        assert len(model.initial_states) == 1
+        initial_state = model.initial_states[0]
+        assert initial_state == 0
+        result = stormpy.model_checking(model, formulas[0], extract_scheduler=True)
+        assert result.has_scheduler
+        scheduler = result.scheduler
+        assert scheduler.memoryless
+        assert scheduler.memory_size == 1
+        assert scheduler.deterministic
+        assert not scheduler.partial
+        intermediate = model.apply_scheduler(scheduler, True)
+        assert intermediate.model_type == stormpy.ModelType.MDP
+        assert intermediate.nr_states == 126
+        assert intermediate.nr_transitions == 156
+        for state in intermediate.states:
+            assert len(state.actions) == 1
+
+    def test_apply_scheduler_ma(self):
+        program = stormpy.parse_prism_program(get_example_path("ma", "simple.ma"), False, True)
+        formulas = stormpy.parse_properties_for_prism_program("Tmin=? [ F s=4 ]", program)
+        ma = stormpy.build_model(program, formulas)
+        assert ma.nr_states == 5
+        assert ma.nr_transitions == 8
+        assert ma.model_type == stormpy.ModelType.MA
+        initial_state = ma.initial_states[0]
+        assert initial_state == 0
+
+        result = stormpy.model_checking(ma, formulas[0], extract_scheduler=True)
+        assert math.isclose(result.at(initial_state), 0.08333333333)
+        assert result.has_scheduler
+        scheduler = result.scheduler
+        assert scheduler.memoryless
+        assert scheduler.memory_size == 1
+        assert scheduler.deterministic
+        intermediate = ma.apply_scheduler(scheduler)
+        assert intermediate.model_type == stormpy.ModelType.MA
+        assert intermediate.nr_states == 3
+        assert intermediate.nr_transitions == 4
+        for state in intermediate.states:
+            assert len(state.actions) == 1