Merge branch 'master' into wrap_highlevel

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

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

@@ -25,3 +25,5 @@ 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"""
+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,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<double>(m, "Double");
+    define_distribution<double>(m, "Double");
 }

src/storage/distribution.cpp

@@ -0,0 +1,17 @@
+#include "distribution.h"
+#include "src/helpers.h"
+
+#include "storm/storage/Distribution.h"
+
+template<typename ValueType>
+void define_distribution(py::module& m, std::string vt_suffix) {
+    using Distrib = storm::storage::Distribution<ValueType, uint32_t>;
+
+    std::string distributionClassName = std::string("Distribution") + vt_suffix;
+    py::class_<Distrib> distribution(m, distributionClassName.c_str(), "Finite Support Distribution");
+    distribution
+            .def("__str__", &streamToString<Distrib>);
+}
+
+
+template void define_distribution<double>(py::module&, std::string vt_suffix);

src/storage/distribution.h

@@ -0,0 +1,6 @@
+#pragma once
+
+#include "common.h"
+
+template<typename ValueType>
+void define_distribution(py::module& m, std::string vt_suffix);

src/storage/scheduler.cpp

@@ -0,0 +1,37 @@
+#include "scheduler.h"
+#include "src/helpers.h"
+
+#include "storm/storage/Scheduler.h"
+
+template<typename ValueType>
+void define_scheduler(py::module& m, std::string vt_suffix) {
+    using Scheduler = storm::storage::Scheduler<ValueType>;
+    using SchedulerChoice = storm::storage::SchedulerChoice<ValueType>;
+
+    std::string schedulerClassName = std::string("Scheduler") + vt_suffix;
+    py::class_<Scheduler, std::shared_ptr<storm::storage::Scheduler<ValueType>>> 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> 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<SchedulerChoice>);
+
+}
+
+
+template void define_scheduler<double>(py::module& m, std::string vt_suffix);

src/storage/scheduler.h

@@ -0,0 +1,7 @@
+#pragma once
+
+#include "common.h"
+
+
+template<typename ValueType>
+void define_scheduler(py::module& m, std::string vt_suffix);

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