From 06ec360c86ec813cc19fac0035b445498ccc94bf Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 26 Nov 2017 16:04:35 +0100 Subject: [PATCH 1/2] Bindings for storm environments --- src/core/environment.cpp | 10 ++++++++++ src/core/environment.h | 8 ++++++++ src/mod_core.cpp | 2 ++ tests/core/test_environment.py | 6 ++++++ 4 files changed, 26 insertions(+) create mode 100644 src/core/environment.cpp create mode 100644 src/core/environment.h create mode 100644 tests/core/test_environment.py diff --git a/src/core/environment.cpp b/src/core/environment.cpp new file mode 100644 index 0000000..23ad447 --- /dev/null +++ b/src/core/environment.cpp @@ -0,0 +1,10 @@ +#include "environment.h" +#include "src/helpers.h" +#include "storm/environment/Environment.h" + +void define_environment(py::module& m) { + py::class_(m, "Environment", "Environment") + .def(py::init<>(), "Construct default environment") + ; +} + diff --git a/src/core/environment.h b/src/core/environment.h new file mode 100644 index 0000000..63783c1 --- /dev/null +++ b/src/core/environment.h @@ -0,0 +1,8 @@ +#ifndef PYTHON_CORE_ENVIRONMENT_H_ +#define PYTHON_CORE_ENVIRONMENT_H_ + +#include "common.h" + +void define_environment(py::module& m); + +#endif /* PYTHON_CORE_ENVIRONMENT_H_ */ diff --git a/src/mod_core.cpp b/src/mod_core.cpp index d98d603..583eff6 100644 --- a/src/mod_core.cpp +++ b/src/mod_core.cpp @@ -6,6 +6,7 @@ #include "core/bisimulation.h" #include "core/input.h" #include "core/analysis.h" +#include "core/environment.h" PYBIND11_MODULE(core, m) { m.doc() = "core"; @@ -25,4 +26,5 @@ PYBIND11_MODULE(core, m) { define_bisimulation(m); define_input(m); define_graph_constraints(m); + define_environment(m); } diff --git a/tests/core/test_environment.py b/tests/core/test_environment.py new file mode 100644 index 0000000..fa6b0ea --- /dev/null +++ b/tests/core/test_environment.py @@ -0,0 +1,6 @@ +import stormpy +from helpers.helper import get_example_path + +class TestEnvironment: + def test_environment(self): + env = stormpy.Environment() From a7e623d29be2da4b60f65b47a0ed41811112cbca Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 26 Nov 2017 16:05:07 +0100 Subject: [PATCH 2/2] Updated bindings for PLA after environment change --- src/pars/pla.cpp | 19 ++++++++++--------- tests/pars/test_pla.py | 9 +++++---- 2 files changed, 15 insertions(+), 13 deletions(-) diff --git a/src/pars/pla.cpp b/src/pars/pla.cpp index 0ecd192..92ab461 100644 --- a/src/pars/pla.cpp +++ b/src/pars/pla.cpp @@ -2,21 +2,22 @@ #include "src/helpers.h" #include "storm/api/storm.h" + typedef storm::modelchecker::SparseDtmcParameterLiftingModelChecker, double> SparseDtmcRegionChecker; typedef storm::modelchecker::RegionModelChecker RegionModelChecker; typedef storm::storage::ParameterRegion Region; // Thin wrappers -std::shared_ptr createRegionChecker(std::shared_ptr> const& model, std::shared_ptr const& formula) { - return storm::api::initializeParameterLiftingRegionModelChecker(model, storm::api::createTask(formula, true)); +std::shared_ptr createRegionChecker(storm::Environment const& env, std::shared_ptr> const& model, std::shared_ptr const& formula) { + return storm::api::initializeParameterLiftingRegionModelChecker(env, model, storm::api::createTask(formula, true)); } -storm::modelchecker::RegionResult checkRegion(std::shared_ptr& checker, Region const& region, storm::modelchecker::RegionResultHypothesis const& hypothesis, storm::modelchecker::RegionResult const& initialResult, bool sampleVertices) { - return checker->analyzeRegion(region, hypothesis, initialResult, sampleVertices); +storm::modelchecker::RegionResult checkRegion(std::shared_ptr& checker, storm::Environment const& env, Region const& region, storm::modelchecker::RegionResultHypothesis const& hypothesis, storm::modelchecker::RegionResult const& initialResult, bool sampleVertices) { + return checker->analyzeRegion(env, region, hypothesis, initialResult, sampleVertices); } -storm::RationalFunction getBound(std::shared_ptr& checker, Region const& region, bool maximise) { - return checker->getBoundAtInitState(region, maximise ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize); +storm::RationalFunction getBound(std::shared_ptr& checker, storm::Environment const& env, Region const& region, bool maximise) { + return checker->getBoundAtInitState(env, region, maximise ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize); } @@ -74,11 +75,11 @@ void define_pla(py::module& m) { auto tmp = storm::api::initializeParameterLiftingRegionModelChecker(model, task); new (&instance) std::unique_ptr(tmp); }, py::arg("model"), py::arg("task")*/ - .def("check_region", &checkRegion, "Check region", py::arg("region"), py::arg("hypothesis") = storm::modelchecker::RegionResultHypothesis::Unknown, py::arg("initialResult") = storm::modelchecker::RegionResult::Unknown, py::arg("sampleVertices") = false) - .def("get_bound", &getBound, "Get bound", py::arg("region"), py::arg("maximise")= true); + .def("check_region", &checkRegion, "Check region", py::arg("environment"), py::arg("region"), py::arg("hypothesis") = storm::modelchecker::RegionResultHypothesis::Unknown, py::arg("initialResult") = storm::modelchecker::RegionResult::Unknown, py::arg("sampleVertices") = false) + .def("get_bound", &getBound, "Get bound", py::arg("environment"), py::arg("region"), py::arg("maximise")= true); ; - m.def("create_region_checker", &createRegionChecker, "Create region checker", py::arg("model"), py::arg("formula")); + m.def("create_region_checker", &createRegionChecker, "Create region checker", py::arg("environment"), py::arg("model"), py::arg("formula")); //m.def("is_parameter_lifting_sound", &storm::utility::parameterlifting::validateParameterLiftingSound, "Check if parameter lifting is sound", py::arg("model"), py::arg("formula")); m.def("gather_derivatives", &gatherDerivatives, "Gather all derivatives of transition probabilities", py::arg("model"), py::arg("var")); } diff --git a/tests/pars/test_pla.py b/tests/pars/test_pla.py index 314ce14..6336527 100644 --- a/tests/pars/test_pla.py +++ b/tests/pars/test_pla.py @@ -16,16 +16,17 @@ class TestPLA: assert model.nr_transitions == 803 assert model.model_type == stormpy.ModelType.DTMC assert model.has_parameters - checker = stormpy.pars.create_region_checker(model, formulas[0].raw_formula) + env = stormpy.Environment() + checker = stormpy.pars.create_region_checker(env, model, formulas[0].raw_formula) parameters = model.collect_probability_parameters() assert len(parameters) == 2 region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters) - result = checker.check_region(region) + result = checker.check_region(env, region) assert result == stormpy.pars.RegionResult.ALLSAT region = stormpy.pars.ParameterRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", parameters) - result = checker.check_region(region, stormpy.pars.RegionResultHypothesis.UNKNOWN, + result = checker.check_region(env, region, stormpy.pars.RegionResultHypothesis.UNKNOWN, stormpy.pars.RegionResult.UNKNOWN, True) assert result == stormpy.pars.RegionResult.EXISTSBOTH region = stormpy.pars.ParameterRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", parameters) - result = checker.check_region(region) + result = checker.check_region(env, region) assert result == stormpy.pars.RegionResult.ALLVIOLATED