Merge branch 'pla_bindings'

src/core/pla.cpp

@@ -0,0 +1,60 @@
+#include "pla.h"
+#include "src/helpers.h"
+
+typedef storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> SparseDtmcRegionChecker;
+typedef storm::storage::ParameterRegion<storm::RationalFunction> Region;
+
+// Thin wrappers
+void specifyFormula(std::shared_ptr<SparseDtmcRegionChecker>& checker, std::shared_ptr<const storm::logic::Formula> const& formula) {
+    checker->specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formula, true));
+}
+storm::modelchecker::parametric::RegionCheckResult checkRegion(std::shared_ptr<SparseDtmcRegionChecker>& checker, Region& region, storm::modelchecker::parametric::RegionCheckResult initialResult, bool sampleVertices) {
+    return checker->analyzeRegion(region, initialResult, sampleVertices);
+}
+
+std::set<storm::Polynomial> gatherDerivatives(storm::models::sparse::Dtmc<storm::RationalFunction> const& model, carl::Variable const& var) {
+    std::set<storm::Polynomial> derivatives;
+    for (auto it : model.getTransitionMatrix()) {
+        storm::Polynomial pol = it.getValue().derivative(var, 1).nominator();
+        if (!pol.isConstant()) {
+            derivatives.insert(pol);
+        }
+    }
+    return derivatives;
+}
+
+// Define python bindings
+void define_pla(py::module& m) {
+    
+    // RegionCheckResult 
+    py::enum_<storm::modelchecker::parametric::RegionCheckResult>(m, "RegionCheckResult", "Types of region check results")
+        .value("EXISTSSAT", storm::modelchecker::parametric::RegionCheckResult::ExistsSat)
+        .value("EXISTSVIOLATED", storm::modelchecker::parametric::RegionCheckResult::ExistsViolated)
+        .value("EXISTSBOTH", storm::modelchecker::parametric::RegionCheckResult::ExistsBoth)
+        .value("CENTERSAT", storm::modelchecker::parametric::RegionCheckResult::CenterSat)
+        .value("CENTERVIOLATED", storm::modelchecker::parametric::RegionCheckResult::CenterViolated)
+        .value("ALLSAT", storm::modelchecker::parametric::RegionCheckResult::AllSat)
+        .value("ALLVIOLATED", storm::modelchecker::parametric::RegionCheckResult::AllViolated)
+        .value("UNKNOWN", storm::modelchecker::parametric::RegionCheckResult::Unknown)
+        .def("__str__", &streamToString<storm::modelchecker::parametric::RegionCheckResult>)
+    ;
+
+    // Region
+    py::class_<Region, std::shared_ptr<Region>>(m, "ParameterRegion", "Parameter region")
+       .def("__init__", [](Region &instance, std::string const& regionString, std::set<Region::VariableType> const& variables) -> void {
+                new (&instance) Region(Region::parseRegion(regionString, variables));
+            })
+        //.def(py::init<Region::VariableSubstitutionType &, Region::VariableSubstitutionType &>(), py::arg("lowerBounds"), py::arg("upperBounds"))
+    ;
+
+    // RegionChecker
+    py::class_<SparseDtmcRegionChecker, std::shared_ptr<SparseDtmcRegionChecker>>(m, "SparseDtmcRegionChecker", "Region model checker for sparse DTMCs")
+        .def("__init__", [](SparseDtmcRegionChecker& instance, std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model) -> void {
+                new (&instance) SparseDtmcRegionChecker(*model);
+            })
+        .def("specify_formula", &specifyFormula, "Specify formula", py::arg("formula"))
+        .def("check_region", &checkRegion, "Check region", py::arg("region"), py::arg("initialResult") = storm::modelchecker::parametric::RegionCheckResult::Unknown, py::arg("sampleVertices") = false)
+    ;
+
+    m.def("gather_derivatives", &gatherDerivatives, "Gather all derivatives of transition probabilities", py::arg("model"), py::arg("var"));
+}

src/core/pla.h

@@ -0,0 +1,8 @@
+#ifndef PYTHON_CORE_PLA_H_
+#define PYTHON_CORE_PLA_H_
+
+#include "common.h"
+
+void define_pla(py::module& m);
+
+#endif /* PYTHON_CORE_PLA_H_ */

src/core/result.cpp

@@ -1,5 +1,11 @@
 #include "result.h"
 
+// Thin wrapper
+template<typename ValueType>
+std::vector<ValueType> getValues(storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType> const& result) {
+    return result.getValueVector();
+}
+
 // Define python bindings
 void define_result(py::module& m) {
 
@@ -53,14 +59,14 @@ void define_result(py::module& m) {
         .def("at", [](storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& result, storm::storage::sparse::state_type state) {
             return result[state];
         }, py::arg("state"), "Get result for given state")
-        .def("get_values", &storm::modelchecker::ExplicitQuantitativeCheckResult<double>::getValueVector, "Get model checking result values for all states")
+        .def("get_values", &getValues<double>, "Get model checking result values for all states")
     ;
     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)
         .def("at", [](storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction> const& result, storm::storage::sparse::state_type state) {
             return result[state];
         }, py::arg("state"), "Get result for given state")
-        .def("get_values", &storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>::getValueVector, "Get model checking result values for all states")
+        .def("get_values", &getValues<storm::RationalFunction>, "Get model checking result values for all states")
     ;
 
 }

src/mod_core.cpp

@@ -5,6 +5,7 @@
 #include "core/modelchecking.h"
 #include "core/bisimulation.h"
 #include "core/input.h"
+#include "core/pla.h"
 
 PYBIND11_PLUGIN(core) {
     py::module m("core");
@@ -22,5 +23,6 @@ PYBIND11_PLUGIN(core) {
     define_modelchecking(m);
     define_bisimulation(m);
     define_input(m);
+    define_pla(m);
     return m.ptr();
 }

src/utility/shortestPaths.cpp

@@ -36,7 +36,7 @@ void define_ksp(py::module& m) {
 
         .def(py::self == py::self, "Compares predecessor node and index, ignoring distance")
 
-        .def("__str__", &streamToString<Path>)
+        //.def("__str__", &streamToString<Path>)
 
         .def_readwrite("predecessorNode", &Path::predecessorNode) // TODO (un-)wrap boost::optional so it's usable
         .def_readwrite("predecessorK", &Path::predecessorK)
@@ -60,4 +60,4 @@ void define_ksp(py::module& m) {
         .def("get_states", &ShortestPathsGenerator::getStates, "k"_a)
         .def("get_path_as_list", &ShortestPathsGenerator::getPathAsList, "k"_a)
     ;
-}
+}

tests/core/test_pla.py

@@ -0,0 +1,43 @@
+import stormpy
+import stormpy.logic
+from helpers.helper import get_example_path
+
+class TestModelChecking:
+    def test_pla(self):
+        import pycarl
+        program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
+        prop = "P<=0.84 [F s=5 ]"
+        formulas = stormpy.parse_properties_for_prism_program(prop, program)
+        model = stormpy.build_parametric_model(program, formulas)
+        assert model.nr_states == 613
+        assert model.nr_transitions == 803
+        assert model.model_type == stormpy.ModelType.DTMC
+        assert model.has_parameters
+        checker = stormpy.SparseDtmcRegionChecker(model)
+        checker.specify_formula(formulas[0].raw_formula)
+        parameters = model.collect_probability_parameters()
+        assert len(parameters) == 2
+        region = stormpy.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters)
+        result = checker.check_region(region)
+        assert result == stormpy.RegionCheckResult.ALLSAT
+        region = stormpy.ParameterRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", parameters)
+        result = checker.check_region(region, stormpy.RegionCheckResult.UNKNOWN, True)
+        assert result == stormpy.RegionCheckResult.EXISTSBOTH
+        region = stormpy.ParameterRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", parameters)
+        result = checker.check_region(region)
+        assert result == stormpy.RegionCheckResult.ALLVIOLATED
+    
+    def test_derivatives(self):
+        import pycarl
+        program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
+        prop = "P<=0.84 [F s=5 ]"
+        formulas = stormpy.parse_properties_for_prism_program(prop, program)
+        model = stormpy.build_parametric_model(program, formulas)
+        assert model.nr_states == 613
+        assert model.nr_transitions == 803
+        assert model.model_type == stormpy.ModelType.DTMC
+        assert model.has_parameters
+        parameters = model.collect_probability_parameters()
+        assert len(parameters) == 2
+        derivatives = stormpy.gather_derivatives(model, list(parameters)[0])
+        assert len(derivatives) == 0