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_>(m, "ParameterRegion", "Parameter region") - .def("__init__", [](Region &instance, std::string const& regionString, std::set const& variables) -> void { - new (&instance) Region(storm::api::parseRegion(regionString, variables)); - }) + .def("__init__", [](Region &instance, std::map> 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 const& variables) -> Region { + return storm::api::parseRegion(regionString, variables); + }, "Create region from string", py::arg("region_string"), py::arg("variables")) + .def_property_readonly("area", &Region::area, "Get area") + .def("__str__", &streamToString) ; // RegionModelChecker - 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) 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)