From 9da3bc8053aef4deede09663e51a772e5fdf8501 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 28 Mar 2018 17:01:44 +0200 Subject: [PATCH 1/3] Test case for MDP model checking --- tests/core/test_modelchecking.py | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 70b6ae5..fef445d 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -18,6 +18,18 @@ class TestModelChecking: result = stormpy.model_checking(model, formulas[0]) assert math.isclose(result.at(initial_state), 0.16666666666666663) + def test_model_checking_prism_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]) + assert math.isclose(result.at(initial_state), 0.3828117384) + def test_model_checking_jani_dtmc(self): jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) formula = properties["Probability to throw a six"] From 11b2a219a74a40ffccfd53aa0631d5c5e99a9f24 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 28 Mar 2018 17:17:41 +0200 Subject: [PATCH 2/3] support for extraction of schedulers --- examples/schedulers/01-schedulers.py | 25 +++++++++++++++++++++++++ lib/stormpy/__init__.py | 5 ++++- lib/stormpy/examples/files.py | 4 +++- src/core/modelchecking.cpp | 2 ++ src/core/result.cpp | 2 ++ src/mod_storage.cpp | 2 ++ src/storage/scheduler.cpp | 18 ++++++++++++++++++ src/storage/scheduler.h | 6 ++++++ tests/core/test_modelchecking.py | 1 + 9 files changed, 63 insertions(+), 2 deletions(-) create mode 100644 examples/schedulers/01-schedulers.py create mode 100644 src/storage/scheduler.cpp create mode 100644 src/storage/scheduler.h diff --git a/examples/schedulers/01-schedulers.py b/examples/schedulers/01-schedulers.py new file mode 100644 index 0000000..75a8cc7 --- /dev/null +++ b/examples/schedulers/01-schedulers.py @@ -0,0 +1,25 @@ +import stormpy +import stormpy.core + +import stormpy.examples +import stormpy.examples.files + + +def example_schedulers_01(): + path = stormpy.examples.files.prism_mdp_coin_2_2 + + formula_str = "Pmin=? [F \"finished\" & \"all_coins_equal_1\"]" + + program = stormpy.parse_prism_program(path) + formulas = stormpy.parse_properties_for_prism_program(formula_str, program) + model = stormpy.build_model(program, formulas) + initial_state = model.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0], extract_scheduler = True) + assert result.has_scheduler + print(result.scheduler) + + + +if __name__ == '__main__': + example_schedulers_01() diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 8ffd318..f1ee516 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -137,13 +137,14 @@ def perform_bisimulation(model, properties, bisimulation_type): return core._perform_bisimulation(model, formulae, bisimulation_type) -def model_checking(model, property, only_initial_states=False): +def model_checking(model, property, only_initial_states=False, extract_scheduler=False): """ Perform model checking on model for property. :param model: Model. :param property: Property to check for. :param only_initial_states: If True, only results for initial states are computed. If False, results for all states are computed. + :param extract_scheduler: If True, try to extract a scheduler :return: Model checking result. :rtype: CheckResult """ @@ -154,9 +155,11 @@ def model_checking(model, property, only_initial_states=False): if model.supports_parameters: task = core.ParametricCheckTask(formula, only_initial_states) + task.set_produce_schedulers(extract_scheduler) return core._parametric_model_checking_sparse_engine(model, task) else: task = core.CheckTask(formula, only_initial_states) + task.set_produce_schedulers(extract_scheduler) return core._model_checking_sparse_engine(model, task) diff --git a/lib/stormpy/examples/files.py b/lib/stormpy/examples/files.py index bfc6f13..61d9fdb 100644 --- a/lib/stormpy/examples/files.py +++ b/lib/stormpy/examples/files.py @@ -24,4 +24,6 @@ drn_ctmc_dft = _path("ctmc", "dft.drn") drn_pdtmc_die = _path("pdtmc", "die.drn") """DRN format for a pDTMC for the KY-Die""" jani_dtmc_die = _path("dtmc", "die.jani") -"""Jani Version of Knuth Yao Die Example""" \ No newline at end of file +"""Jani Version of Knuth Yao Die Example""" +prism_mdp_coin_2_2 = _path("mdp", "coin2-2.nm") +"""Prism example for coin MDP""" \ No newline at end of file diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp index f7d9d5e..703e53c 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -33,10 +33,12 @@ void define_modelchecking(py::module& m) { py::class_, std::shared_ptr>>(m, "CheckTask", "Task for model checking") //m.def("create_check_task", &storm::api::createTask, "Create task for verification", py::arg("formula"), py::arg("only_initial_states") = false); .def(py::init(), py::arg("formula"), py::arg("only_initial_states") = false) + .def("set_produce_schedulers", &CheckTask::setProduceSchedulers, "Set whether schedulers should be produced (if possible)", py::arg("produce_schedulers") = true) ; py::class_, std::shared_ptr>>(m, "ParametricCheckTask", "Task for parametric model checking") //m.def("create_check_task", &storm::api::createTask, "Create task for verification", py::arg("formula"), py::arg("only_initial_states") = false); .def(py::init(), py::arg("formula"), py::arg("only_initial_states") = false) + .def("set_produce_schedulers", &CheckTask::setProduceSchedulers, "Set whether schedulers should be produced (if possible)", py::arg("produce_schedulers") = true) ; // Model checking diff --git a/src/core/result.cpp b/src/core/result.cpp index 33f6bce..b564e3c 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -23,6 +23,7 @@ void define_result(py::module& m) { .def_property_readonly("_hybrid_quantitative", &storm::modelchecker::CheckResult::isHybridQuantitativeCheckResult, "Flag if result is hybrid quantitative") .def_property_readonly("_pareto_curve", &storm::modelchecker::CheckResult::isParetoCurveCheckResult, "Flag if result is a pareto curve") .def_property_readonly("result_for_all_states", &storm::modelchecker::CheckResult::isResultForAllStates, "Flag if result is for all states") + .def_property_readonly("has_scheduler", &storm::modelchecker::CheckResult::hasScheduler, "Flag if a scheduler is present") .def("as_explicit_qualitative", [](storm::modelchecker::CheckResult const& result) { return result.asExplicitQualitativeCheckResult(); @@ -56,6 +57,7 @@ void define_result(py::module& m) { return result[state]; }, py::arg("state"), "Get result for given state") .def("get_values", &getValues, "Get model checking result values for all states") + .def_property_readonly("scheduler", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& res) {return res.getScheduler();}, "get scheduler") ; py::class_, std::shared_ptr>> parametricQuantitativeCheckResult(m, "_ParametricQuantitativeCheckResult", "Abstract class for parametric quantitative model checking results", checkResult); py::class_, std::shared_ptr>>(m, "ExplicitParametricQuantitativeCheckResult", "Explicit parametric quantitative model checking result", parametricQuantitativeCheckResult) diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 62ced7d..2e0c3e1 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -3,6 +3,7 @@ #include "storage/bitvector.h" #include "storage/model.h" #include "storage/matrix.h" +#include "storage/scheduler.h" #include "storage/prism.h" #include "storage/state.h" #include "storage/labeling.h" @@ -23,4 +24,5 @@ PYBIND11_MODULE(storage, m) { define_prism(m); define_labeling(m); define_expressions(m); + define_scheduler(m); } diff --git a/src/storage/scheduler.cpp b/src/storage/scheduler.cpp new file mode 100644 index 0000000..065e888 --- /dev/null +++ b/src/storage/scheduler.cpp @@ -0,0 +1,18 @@ +#include "scheduler.h" +#include "src/helpers.h" + +#include "storm/storage/Scheduler.h" + +void define_scheduler(py::module& m) { + using Scheduler = storm::storage::Scheduler; + + py::class_>> scheduler(m, "Scheduler", "A Finite Memory Scheduler"); + scheduler + .def("__str__", [](Scheduler const& s) { + std::stringstream str; + s.printToStream(str); + return str.str(); + }) + ; + +} \ No newline at end of file diff --git a/src/storage/scheduler.h b/src/storage/scheduler.h new file mode 100644 index 0000000..b66000d --- /dev/null +++ b/src/storage/scheduler.h @@ -0,0 +1,6 @@ +#pragma once + +#include "common.h" + + +void define_scheduler(py::module& m); diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index fef445d..e4df9eb 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -30,6 +30,7 @@ class TestModelChecking: result = stormpy.model_checking(model, formulas[0]) assert math.isclose(result.at(initial_state), 0.3828117384) + def test_model_checking_jani_dtmc(self): jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) formula = properties["Probability to throw a six"] From a7191e24ba38fc316cd1f92438fcce9e7668f27c Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 28 Mar 2018 18:15:20 +0200 Subject: [PATCH 3/3] support for queries on schedulers --- examples/schedulers/01-schedulers.py | 5 +++++ src/mod_storage.cpp | 4 +++- src/storage/distribution.cpp | 17 +++++++++++++++++ src/storage/distribution.h | 6 ++++++ src/storage/scheduler.cpp | 27 +++++++++++++++++++++++---- src/storage/scheduler.h | 3 ++- 6 files changed, 56 insertions(+), 6 deletions(-) create mode 100644 src/storage/distribution.cpp create mode 100644 src/storage/distribution.h diff --git a/examples/schedulers/01-schedulers.py b/examples/schedulers/01-schedulers.py index 75a8cc7..6a0b2bd 100644 --- a/examples/schedulers/01-schedulers.py +++ b/examples/schedulers/01-schedulers.py @@ -18,6 +18,11 @@ def example_schedulers_01(): result = stormpy.model_checking(model, formulas[0], extract_scheduler = True) assert result.has_scheduler print(result.scheduler) + assert result.scheduler.memoryless + assert result.scheduler.deterministic + + for i in range(0,model.nr_states): + print("In state {} choose action {}".format(i,result.scheduler.get_choice(i).get_deterministic_choice())) diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 2e0c3e1..4fd3cbd 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -3,6 +3,7 @@ #include "storage/bitvector.h" #include "storage/model.h" #include "storage/matrix.h" +#include "storage/distribution.h" #include "storage/scheduler.h" #include "storage/prism.h" #include "storage/state.h" @@ -24,5 +25,6 @@ PYBIND11_MODULE(storage, m) { define_prism(m); define_labeling(m); define_expressions(m); - define_scheduler(m); + define_scheduler(m, "Double"); + define_distribution(m, "Double"); } diff --git a/src/storage/distribution.cpp b/src/storage/distribution.cpp new file mode 100644 index 0000000..79a03a2 --- /dev/null +++ b/src/storage/distribution.cpp @@ -0,0 +1,17 @@ +#include "distribution.h" +#include "src/helpers.h" + +#include "storm/storage/Distribution.h" + +template +void define_distribution(py::module& m, std::string vt_suffix) { + using Distrib = storm::storage::Distribution; + + std::string distributionClassName = std::string("Distribution") + vt_suffix; + py::class_ distribution(m, distributionClassName.c_str(), "Finite Support Distribution"); + distribution + .def("__str__", &streamToString); +} + + +template void define_distribution(py::module&, std::string vt_suffix); \ No newline at end of file diff --git a/src/storage/distribution.h b/src/storage/distribution.h new file mode 100644 index 0000000..3396827 --- /dev/null +++ b/src/storage/distribution.h @@ -0,0 +1,6 @@ +#pragma once + +#include "common.h" + +template +void define_distribution(py::module& m, std::string vt_suffix); \ No newline at end of file diff --git a/src/storage/scheduler.cpp b/src/storage/scheduler.cpp index 065e888..5d79f09 100644 --- a/src/storage/scheduler.cpp +++ b/src/storage/scheduler.cpp @@ -3,16 +3,35 @@ #include "storm/storage/Scheduler.h" -void define_scheduler(py::module& m) { - using Scheduler = storm::storage::Scheduler; +template +void define_scheduler(py::module& m, std::string vt_suffix) { + using Scheduler = storm::storage::Scheduler; + using SchedulerChoice = storm::storage::SchedulerChoice; - py::class_>> scheduler(m, "Scheduler", "A Finite Memory Scheduler"); + std::string schedulerClassName = std::string("Scheduler") + vt_suffix; + py::class_>> scheduler(m, schedulerClassName.c_str(), "A Finite Memory Scheduler"); scheduler .def("__str__", [](Scheduler const& s) { std::stringstream str; s.printToStream(str); return str.str(); }) + .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("get_choice", &Scheduler::getChoice, py::arg("state_index"), py::arg("memory_index") = 0) ; -} \ No newline at end of file + std::string schedulerChoiceClassName = std::string("SchedulerChoice") + vt_suffix; + py::class_ schedulerChoice(m, schedulerChoiceClassName.c_str(), "A choice of a finite memory scheduler"); + schedulerChoice + .def_property_readonly("defined", &SchedulerChoice::isDefined, "Is the choice defined by the scheduler?") + .def_property_readonly("deterministic", &SchedulerChoice::isDeterministic, "Is the choice deterministic (given by a Dirac distribution)?") + .def("get_deterministic_choice", &SchedulerChoice::getDeterministicChoice, "Get the deterministic choice") + .def("get_choice", &SchedulerChoice::getChoiceAsDistribution, "Get the distribution over the actions") + .def("__str__", &streamToString); + +} + + +template void define_scheduler(py::module& m, std::string vt_suffix); \ No newline at end of file diff --git a/src/storage/scheduler.h b/src/storage/scheduler.h index b66000d..24cd4cf 100644 --- a/src/storage/scheduler.h +++ b/src/storage/scheduler.h @@ -3,4 +3,5 @@ #include "common.h" -void define_scheduler(py::module& m); +template +void define_scheduler(py::module& m, std::string vt_suffix);