diff --git a/examples/schedulers/01-schedulers.py b/examples/schedulers/01-schedulers.py new file mode 100644 index 0000000..6a0b2bd --- /dev/null +++ b/examples/schedulers/01-schedulers.py @@ -0,0 +1,30 @@ +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) + 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())) + + + +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 55a62a2..7514c9f 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..4fd3cbd 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -3,6 +3,8 @@ #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" #include "storage/labeling.h" @@ -23,4 +25,6 @@ PYBIND11_MODULE(storage, m) { define_prism(m); define_labeling(m); define_expressions(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 new file mode 100644 index 0000000..5d79f09 --- /dev/null +++ b/src/storage/scheduler.cpp @@ -0,0 +1,37 @@ +#include "scheduler.h" +#include "src/helpers.h" + +#include "storm/storage/Scheduler.h" + +template +void define_scheduler(py::module& m, std::string vt_suffix) { + using Scheduler = storm::storage::Scheduler; + using SchedulerChoice = storm::storage::SchedulerChoice; + + 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) + ; + + 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 new file mode 100644 index 0000000..24cd4cf --- /dev/null +++ b/src/storage/scheduler.h @@ -0,0 +1,7 @@ +#pragma once + +#include "common.h" + + +template +void define_scheduler(py::module& m, std::string vt_suffix); diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 70b6ae5..e4df9eb 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -18,6 +18,19 @@ 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"]