support for extraction of schedulers

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()

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)
 
 

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"""
+"""Jani Version of Knuth Yao Die Example"""
+prism_mdp_coin_2_2 = _path("mdp", "coin2-2.nm")
+"""Prism example for coin MDP"""

src/core/modelchecking.cpp

@@ -33,10 +33,12 @@ void define_modelchecking(py::module& m) {
     py::class_<CheckTask<double>, std::shared_ptr<CheckTask<double>>>(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<storm::logic::Formula const&, bool>(), py::arg("formula"), py::arg("only_initial_states") = false)
+        .def("set_produce_schedulers", &CheckTask<double>::setProduceSchedulers, "Set whether schedulers should be produced (if possible)", py::arg("produce_schedulers") = true)
     ;
     py::class_<CheckTask<storm::RationalFunction>, std::shared_ptr<CheckTask<storm::RationalFunction>>>(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<storm::logic::Formula const&, bool>(), py::arg("formula"), py::arg("only_initial_states") = false)
+        .def("set_produce_schedulers", &CheckTask<storm::RationalFunction>::setProduceSchedulers, "Set whether schedulers should be produced (if possible)", py::arg("produce_schedulers") = true)
     ;
 
     // Model checking

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<double>, "Get model checking result values for all states")
+        .def_property_readonly("scheduler", [](storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& res) {return res.getScheduler();}, "get scheduler")
     ;
     py::class_<storm::modelchecker::QuantitativeCheckResult<storm::RationalFunction>, std::shared_ptr<storm::modelchecker::QuantitativeCheckResult<storm::RationalFunction>>> parametricQuantitativeCheckResult(m, "_ParametricQuantitativeCheckResult", "Abstract class for parametric quantitative model checking results", checkResult);
     py::class_<storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>, std::shared_ptr<storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>>>(m, "ExplicitParametricQuantitativeCheckResult", "Explicit parametric quantitative model checking result", parametricQuantitativeCheckResult)

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);
 }

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<double>;
+
+    py::class_<Scheduler, std::shared_ptr<storm::storage::Scheduler<double>>> scheduler(m, "Scheduler", "A Finite Memory Scheduler");
+    scheduler
+            .def("__str__", [](Scheduler const& s) {
+                std::stringstream str;
+                s.printToStream(str);
+                return str.str();
+            })
+    ;
+
+}

src/storage/scheduler.h

@@ -0,0 +1,6 @@
+#pragma once
+
+#include "common.h"
+
+
+void define_scheduler(py::module& m);

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"]