Changed constructor of ParameterRegion to take a valuation.

Use ParameterRegion.create_from_string() to initialize a region from string.

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

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)

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)

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)