From d9ff33a9e06a4df0db0ac9ce85847ca98b3f8ba3 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 12 Jan 2018 23:38:58 +0100 Subject: [PATCH] extended pla bindings for latest additions in PLA and to build PLA checker directly --- src/pars/pla.cpp | 47 +++++++++++++++++++++++++++++++---------------- 1 file changed, 31 insertions(+), 16 deletions(-) diff --git a/src/pars/pla.cpp b/src/pars/pla.cpp index 92ab461..54c1d0a 100644 --- a/src/pars/pla.cpp +++ b/src/pars/pla.cpp @@ -3,23 +3,36 @@ #include "storm/api/storm.h" -typedef storm::modelchecker::SparseDtmcParameterLiftingModelChecker, double> SparseDtmcRegionChecker; +typedef storm::modelchecker::SparseDtmcParameterLiftingModelChecker, double> DtmcParameterLiftingModelChecker; +typedef storm::modelchecker::SparseMdpParameterLiftingModelChecker, double> MdpParameterLiftingModelChecker; + typedef storm::modelchecker::RegionModelChecker RegionModelChecker; typedef storm::storage::ParameterRegion Region; // Thin wrappers -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)); +std::shared_ptr createRegionChecker(storm::Environment const& env, std::shared_ptr> const& model, std::shared_ptr const& formula, bool generateSplittingEstimate, bool allowModelSimplifications) { + return storm::api::initializeParameterLiftingRegionModelChecker(env, model, storm::api::createTask(formula, true), generateSplittingEstimate, allowModelSimplifications); +} + +void specify(std::shared_ptr& checker, storm::Environment const& env, std::shared_ptr> const& model, std::shared_ptr const& formula, bool generateSplittingEstimate, bool allowModelSimplifications) { + return checker->specify(env, model, storm::api::createTask(formula, true), generateSplittingEstimate, allowModelSimplifications); } 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, storm::Environment const& env, Region const& region, bool maximise) { +storm::RationalFunction getBoundAtInit(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); } +storm::modelchecker::ExplicitQuantitativeCheckResult getBound_dtmc(std::shared_ptr& checker, storm::Environment const& env, Region const& region, bool maximise) { + return res = checker->getBound(env, region, maximise ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize)->asExplicitQuantitativeCheckResult(); +} + +std::unique_ptr> getBound_mdp(std::shared_ptr& checker, storm::Environment const& env, Region const& region, bool maximise) { + return checker->getBound(env, region, maximise ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize)->asExplicitQuantitativeCheckResult(); +} std::set gatherDerivatives(storm::models::sparse::Model const& model, carl::Variable const& var) { std::set derivatives; @@ -66,20 +79,22 @@ void define_pla(py::module& m) { ; // RegionModelChecker - //py::class_>(m, "SparseDtmcRegionChecker", "Region model checker for sparse DTMCs") - py::class_>(m, "RegionModelChecker", "Region model checker via paramater lifting") -/* .def("__init__", [](std::unique_ptr& instance, std::shared_ptr> model, storm::modelchecker::CheckTask const& task) -> void { - // Better use storm::api::initializeParameterLiftingRegionModelChecker(model, task); - //SparseDtmcRegionChecker tmp; - //tmp.specify(model, task); - 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("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); + + py::class_> regionModelChecker(m, "RegionModelChecker", "Region model checker via paramater lifting"); + regionModelChecker.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", &getBoundAtInit, "Get bound", py::arg("environment"), py::arg("region"), py::arg("maximise")= true) + .def("specify", &specify, "specify arguments",py::arg("environment"), py::arg("model"), py::arg("formula"), py::arg("generate_splitting_estimate") = false, py::arg("allow_model_simplification") = true); ; - m.def("create_region_checker", &createRegionChecker, "Create region checker", py::arg("environment"), py::arg("model"), py::arg("formula")); + + py::class_>(m, "DtmcParameterLiftingModelChecker", "Region model checker for DTMCs", regionModelChecker) + .def(py::init<>()) + .def("get_bound_all_states", &getBound_dtmc, "Get bound", py::arg("environment"), py::arg("region"), py::arg("maximise")= true); + py::class_>(m, "MdpParameterLiftingModelChecker", "Region model checker for MPDs", regionModelChecker) + .def(py::init<>()) + .def("get_bound_all_states", &getBound_mdp, "Get bound", py::arg("environment"), py::arg("region"), py::arg("maximise")= true); + + m.def("create_region_checker", &createRegionChecker, "Create region checker", py::arg("environment"), py::arg("model"), py::arg("formula"), py::arg("generate_splitting_estimate") = false, py::arg("allow_model_simplification") = true); //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")); }