From 5a61c88b6dc1605e0621544dde47e87a39d24d1d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 21 Jan 2020 23:33:48 +0100 Subject: [PATCH] Tests for scheduler application and MA->CTMC translation --- lib/stormpy/examples/files/ma/ctmc.ma | 14 ++++++++ src/storage/model.cpp | 6 ++++ src/storage/scheduler.cpp | 1 + tests/storage/test_model.py | 17 +++++++++- tests/storage/test_scheduler.py | 47 +++++++++++++++++++++++++++ 5 files changed, 84 insertions(+), 1 deletion(-) create mode 100644 lib/stormpy/examples/files/ma/ctmc.ma diff --git a/lib/stormpy/examples/files/ma/ctmc.ma b/lib/stormpy/examples/files/ma/ctmc.ma new file mode 100644 index 0000000..f683441 --- /dev/null +++ b/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 diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 5c1ef5a..357a857 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -206,7 +206,11 @@ void define_sparse_model(py::module& m) { ; py::class_, std::shared_ptr>>(m, "SparseMA", "MA in sparse representation", model) .def(py::init>(), py::arg("other_model")) + .def_property_readonly("nondeterministic_choice_indices", [](SparseMarkovAutomaton const& ma) { return ma.getNondeterministicChoiceIndices(); }) + .def("apply_scheduler", [](SparseMarkovAutomaton const& ma, storm::storage::Scheduler 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::isConvertibleToCtmc, "Check whether the MA can be converted into a CTMC.") + .def("convert_to_ctmc", &SparseMarkovAutomaton::convertToCtmc, "Convert the MA into a CTMC.") ; py::class_>(m, "SparseRewardModel", "Reward structure for sparse models") @@ -256,6 +260,8 @@ void define_sparse_model(py::module& m) { .def("__str__", &getModelInfoPrinter) ; py::class_, std::shared_ptr>>(m, "SparseParametricMA", "pMA in sparse representation", modelRatFunc) + .def_property_readonly("nondeterministic_choice_indices", [](SparseMarkovAutomaton const& ma) { return ma.getNondeterministicChoiceIndices(); }) + .def("apply_scheduler", [](SparseMarkovAutomaton const& ma, storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) { return ma.applyScheduler(scheduler, dropUnreachableStates); } , "apply scheduler", "scheduler"_a, "drop_unreachable_states"_a = true) .def("__str__", &getModelInfoPrinter) ; diff --git a/src/storage/scheduler.cpp b/src/storage/scheduler.cpp index a553c83..97151c3 100644 --- a/src/storage/scheduler.cpp +++ b/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) ; diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index bca8d35..6345e05 100644 --- a/tests/storage/test_model.py +++ b/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) diff --git a/tests/storage/test_scheduler.py b/tests/storage/test_scheduler.py index c1ec7c8..8cb9cfb 100644 --- a/tests/storage/test_scheduler.py +++ b/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