From 11b2a219a74a40ffccfd53aa0631d5c5e99a9f24 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 28 Mar 2018 17:17:41 +0200 Subject: [PATCH] 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"]