From 3bf516f08e8e9fa17f16f8efe149a3949d74e6b7 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 13 Aug 2019 14:48:51 +0200
Subject: [PATCH] Changed constructor of ParameterRegion to take a valuation.
Use ParameterRegion.create_from_string() to initialize a region from string.
---
CHANGELOG.md | 5 ++++
src/pars/pla.cpp | 18 +++++++++---
tests/pars/test_parametric.py | 21 ++++++++++++++
tests/pars/test_pla.py | 53 +++++++++++++++++++++++++++++------
4 files changed, 84 insertions(+), 13 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 347b676..e4c805a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,11 @@ Changelog
Version 1.3.x
-------------
+### Version 1.3.1 (under development)
+- Changed constructor of `ParameterRegion` to take a valuation instead of string.
+ Use `ParameterRegion.create_from_string()` to create a region from string.
+
+
### Version 1.3.0 (2019/01)
Requires storm version >= 1.3.0 and pycarl version >= 2.0.3
- Adaptions to changes in Storm
diff --git a/src/pars/pla.cpp b/src/pars/pla.cpp
index 64de4f4..9389978 100644
--- a/src/pars/pla.cpp
+++ b/src/pars/pla.cpp
@@ -73,13 +73,23 @@ void define_pla(py::module& m) {
// 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(storm::api::parseRegion<storm::RationalFunction>(regionString, variables));
- })
+ .def("__init__", [](Region &instance, std::map<Region::VariableType, std::pair<Region::CoefficientType, Region::CoefficientType>> valuation) -> void {
+ Region::Valuation lowerValuation;
+ Region::Valuation upperValuation;
+ for (auto const& val : valuation) {
+ lowerValuation[val.first] = val.second.first;
+ upperValuation[val.first] = val.second.second;
+ }
+ new (&instance) Region(lowerValuation, upperValuation);
+ }, "Create region from valuation of var -> (lower_bound, upper_bound)", py::arg("valuation"))
+ .def_static("create_from_string", [](std::string const& regionString, std::set<Region::VariableType> const& variables) -> Region {
+ return storm::api::parseRegion<storm::RationalFunction>(regionString, variables);
+ }, "Create region from string", py::arg("region_string"), py::arg("variables"))
+ .def_property_readonly("area", &Region::area, "Get area")
+ .def("__str__", &streamToString<Region>)
;
// RegionModelChecker
-
py::class_<RegionModelChecker, std::shared_ptr<RegionModelChecker>> 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)
diff --git a/tests/pars/test_parametric.py b/tests/pars/test_parametric.py
index 77f1fc2..4edb95e 100644
--- a/tests/pars/test_parametric.py
+++ b/tests/pars/test_parametric.py
@@ -135,3 +135,24 @@ class TestParametric:
model, formula = stormpy.pars.simplify_model(model, formula)
assert model.nr_states == 17
assert model.nr_transitions == 50
+
+ def test_region(self):
+ 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)
+ parameters = model.collect_probability_parameters()
+ assert len(parameters) == 2
+ region = stormpy.pars.ParameterRegion.create_from_string("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters)
+ assert region.area == stormpy.RationalRF(1) / stormpy.RationalRF(25)
+ for par in parameters:
+ if par.name == "pL":
+ pL = par
+ elif par.name == "pK":
+ pK = par
+ else:
+ assert False
+ dec = stormpy.RationalRF(100)
+ region_valuation = {pL: (stormpy.RationalRF(70) / dec, stormpy.RationalRF(90) / dec), pK: (stormpy.RationalRF(75) / dec, stormpy.RationalRF(95) / dec)}
+ region = stormpy.pars.ParameterRegion(region_valuation)
+ assert region.area == stormpy.RationalRF(1) / stormpy.RationalRF(25)
diff --git a/tests/pars/test_pla.py b/tests/pars/test_pla.py
index 80a585f..bb12352 100644
--- a/tests/pars/test_pla.py
+++ b/tests/pars/test_pla.py
@@ -21,14 +21,49 @@ class TestPLA:
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)
+ region = stormpy.pars.ParameterRegion.create_from_string("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters)
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(env, region, stormpy.pars.RegionResultHypothesis.UNKNOWN,
- stormpy.pars.RegionResult.UNKNOWN, True)
+ region = stormpy.pars.ParameterRegion.create_from_string("0.4<=pL<=0.65,0.75<=pK<=0.95", parameters)
+ 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)
+ region = stormpy.pars.ParameterRegion.create_from_string("0.1<=pL<=0.73,0.2<=pK<=0.715", parameters)
+ result = checker.check_region(env, region)
+ assert result == stormpy.pars.RegionResult.ALLVIOLATED
+
+ def test_pla_region_valuation(self):
+ 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
+ env = stormpy.Environment()
+ checker = stormpy.pars.create_region_checker(env, model, formulas[0].raw_formula)
+ parameters = model.collect_probability_parameters()
+ assert len(parameters) == 2
+ for par in parameters:
+ if par.name == "pL":
+ pL = par
+ elif par.name == "pK":
+ pK = par
+ else:
+ assert False
+ region_valuation = dict()
+ region_valuation[pL] = (stormpy.RationalRF(0.7), stormpy.RationalRF(0.9))
+ region_valuation[pK] = (stormpy.RationalRF(0.75), stormpy.RationalRF(0.95))
+ region = stormpy.pars.ParameterRegion(region_valuation)
+ result = checker.check_region(env, region)
+ assert result == stormpy.pars.RegionResult.ALLSAT
+ region_valuation[pL] = (stormpy.RationalRF(0.4), stormpy.RationalRF(0.65))
+ region = stormpy.pars.ParameterRegion(region_valuation)
+ result = checker.check_region(env, region, stormpy.pars.RegionResultHypothesis.UNKNOWN, stormpy.pars.RegionResult.UNKNOWN, True)
+ assert result == stormpy.pars.RegionResult.EXISTSBOTH
+ region_valuation[pK] = (stormpy.RationalRF(0.2), stormpy.RationalRF(0.715))
+ region_valuation[pL] = (stormpy.RationalRF(0.1), stormpy.RationalRF(0.73))
+ region = stormpy.pars.ParameterRegion(region_valuation)
result = checker.check_region(env, region)
assert result == stormpy.pars.RegionResult.ALLVIOLATED
@@ -42,7 +77,7 @@ class TestPLA:
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)
+ region = stormpy.pars.ParameterRegion.create_from_string("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters)
result = checker.get_bound(env, region, True)
assert math.isclose(float(result.constant_part()), 0.8369631383670559, rel_tol=1e-6)
result_vec = checker.get_bound_all_states(env, region, True)
@@ -60,7 +95,7 @@ class TestPLA:
checker.specify(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)
+ region = stormpy.pars.ParameterRegion.create_from_string("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters)
result = checker.get_bound(env, region, True)
assert math.isclose(float(result.constant_part()), 0.8369631383670559, rel_tol=1e-6)
@@ -75,7 +110,7 @@ class TestPLA:
checker.specify(env, model, formulas[0].raw_formula, allow_model_simplification=False)
parameters = model.collect_probability_parameters()
assert len(parameters) == 2
- region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters)
+ region = stormpy.pars.ParameterRegion.create_from_string("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters)
result = checker.get_bound(env, region, True)
assert math.isclose(float(result.constant_part()), 0.836963056082918, rel_tol=1e-6)
@@ -90,7 +125,7 @@ class TestPLA:
checker.specify(env, model, formulas[0].raw_formula, allow_model_simplification=False)
parameters = model.collect_probability_parameters()
assert len(parameters) == 2
- region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters)
+ region = stormpy.pars.ParameterRegion.create_from_string("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters)
result_vec = checker.get_bound_all_states(env, region, True)
assert len(result_vec.get_values()) == model.nr_states
assert math.isclose(result_vec.at(model.initial_states[0]), 0.836963056082918, rel_tol=1e-6)