From fd1c9a586e60863bff317fd4811e76cc1f930646 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 4 Apr 2017 17:58:09 +0200 Subject: [PATCH] Add PLA support --- src/core/pla.cpp | 49 ++++++++++++++++++++++++++++++++++++++++++ src/core/pla.h | 8 +++++++ src/mod_core.cpp | 2 ++ tests/core/test_pla.py | 45 ++++++++++++++++++++++++++++++++++++++ 4 files changed, 104 insertions(+) create mode 100644 src/core/pla.cpp create mode 100644 src/core/pla.h create mode 100644 tests/core/test_pla.py diff --git a/src/core/pla.cpp b/src/core/pla.cpp new file mode 100644 index 0000000..7124427 --- /dev/null +++ b/src/core/pla.cpp @@ -0,0 +1,49 @@ +#include "pla.h" +#include "src/helpers.h" + +typedef storm::modelchecker::parametric::SparseDtmcParameterLifting, double> PLAChecker; +typedef storm::storage::ParameterRegion Region; + +// Thin wrappers +void specifyFormula(std::shared_ptr& checker, std::shared_ptr const& formula) { + checker->specifyFormula(storm::modelchecker::CheckTask(*formula, true)); +} +storm::modelchecker::parametric::RegionCheckResult checkRegion(std::shared_ptr& checker, Region& region) { + return checker->analyzeRegion(region, storm::modelchecker::parametric::RegionCheckResult::Unknown, true); +} + +// Define python bindings +void define_pla(py::module& m) { + + // PLAChecker + py::class_>(m, "SparseDtmcRegionModelChecker", "Region model checker for sparse DTMCs") + .def("__init__", [](PLAChecker& instance, std::shared_ptr> model) -> void { + new (&instance) PLAChecker(*model); + }) + //.def(py::init>) + .def("specify_formula", &specifyFormula, "Specify formula", py::arg("formula")) + .def("check_region", &checkRegion, "Check region", py::arg("region")) + ; + + // Region + py::class_>(m, "ParameterRegion", "Parameter region") + .def("__init__", [](Region &instance, std::string const& regionString, std::set const& variables) -> void { + new (&instance) Region(Region::parseRegion(regionString, variables)); + }) + //.def(py::init(), py::arg("lowerBounds"), py::arg("upperBounds")) + //.def("result", &Region::getCheckResult, "Get check result") + ; + + // RegionCheckResult + py::enum_(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) + ; +} diff --git a/src/core/pla.h b/src/core/pla.h new file mode 100644 index 0000000..7ca587a --- /dev/null +++ b/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_ */ diff --git a/src/mod_core.cpp b/src/mod_core.cpp index f394ab1..8e7e507 100644 --- a/src/mod_core.cpp +++ b/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(); } diff --git a/tests/core/test_pla.py b/tests/core/test_pla.py new file mode 100644 index 0000000..2884b1a --- /dev/null +++ b/tests/core/test_pla.py @@ -0,0 +1,45 @@ +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.SparseDtmcRegionModelChecker(model) + checker.specify_formula(formulas[0].raw_formula) + parameters = model.collect_probability_parameters() + assert len(parameters) == 2 + #if str(parameters[0]) == "pL": + # pL = parameters[0] + # pK = parameters[1] + #else: + # pK = parameters[0] + # pL = parameters[1] + #assert str(pL) == "pL" + #assert str(pK) == "pK" + #lowerBounds = {pL: 0.7, pK: 0.75} + #upperBounds = {pL: 0.9, pK: 0.95} + #region = stormpy.ParameterRegion(lowerBounds, upperBounds) + region = stormpy.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters) + result = checker.check_region(region) + assert result == stormpy.RegionCheckResult.ALLSAT + #lowerBounds = {pL: 0.4, pK: 0.75} + #upperBounds = {pL: 0.65, pK: 0.95} + #region = stormpy.ParameterRegion(lowerBounds, upperBounds) + region = stormpy.ParameterRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", parameters) + result = checker.check_region(region) + assert result == stormpy.RegionCheckResult.EXISTSBOTH + #lowerBounds = {pL: 0.1, pK: 0.2} + #upperBounds = {pL: 0.73, pK: 0.715} + #region = stormpy.ParameterRegion(lowerBounds, upperBounds) + region = stormpy.ParameterRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", parameters) + result = checker.check_region(region) + assert result == stormpy.RegionCheckResult.ALLVIOLATED