diff --git a/CHANGELOG.md b/CHANGELOG.md index 8ecc145..8b0f444 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,10 +1,15 @@ Changelog ============== -Version 1.1 ------------ +Version 1.1.x +------------- -### Version 1.1.0 +### Version 1.1.1 + +- Bindings for simplification of parametric models + + +### Version 1.1.0 (2017/08) - Bindings for storm-pars - Bindings for graph constraints @@ -15,19 +20,19 @@ Version 1.1 - Updated pybind version -Version 1.0 ------------ +Version 1.0.x +------------- Skipped, to keep on par with storm -Version 0.9 ------------ +Version 0.9.x +------------- -### Version 0.9.1 (2017/4) +### Version 0.9.1 (2017/04) - Bindings for DFTs - Bindings for PLA - Updated to pycarl v2 (support for both cln and gmp) - Improved building system, read flags from storm build system -### Version 0.9 (2017/3) +### Version 0.9 (2017/03) Start of this changelog diff --git a/lib/stormpy/pars/__init__.py b/lib/stormpy/pars/__init__.py index 8ea02d4..fa1becf 100644 --- a/lib/stormpy/pars/__init__.py +++ b/lib/stormpy/pars/__init__.py @@ -6,4 +6,24 @@ if not _config.storm_with_pars: from . import pars from .pars import * +from stormpy import ModelType, StormError + pars._set_up() + + +def simplify_model(model, formula): + """ + Simplify parametric model preserving the given formula by eliminating states with constant outgoing probabilities. + :param model: Model. + :param formula: Formula. + :return: Tuple of simplified model and simplified formula. + """ + if model.model_type == ModelType.DTMC: + simplifier = pars._SparseParametricDtmcSimplifier(model) + elif model.model_type == ModelType.MDP: + simplifier = pars._SparseParametricMdpSimplifier(model) + else: + raise StormError("Model type {} cannot be simplified.".format(model.model_type)) + if not simplifier.simplify(formula): + raise StormError("Model could not be simplified") + return simplifier.simplified_model, simplifier.simplified_formula diff --git a/src/pars/pars.cpp b/src/pars/pars.cpp index 662735c..cb6cc74 100644 --- a/src/pars/pars.cpp +++ b/src/pars/pars.cpp @@ -2,10 +2,48 @@ #include "storm/settings/SettingsManager.h" #include "storm-pars/settings/modules/ParametricSettings.h" #include "storm-pars/settings/modules/RegionSettings.h" +#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" +#include "storm-pars/transformer/SparseParametricMdpSimplifier.h" + +typedef storm::models::sparse::Dtmc Dtmc; +typedef storm::models::sparse::Mdp Mdp; +typedef storm::transformer::SparseParametricDtmcSimplifier SparseParametricDtmcSimplifier; +typedef storm::transformer::SparseParametricMdpSimplifier SparseParametricMdpSimplifier; void define_pars(py::module& m) { m.def("_set_up", []() { storm::settings::addModule(); storm::settings::addModule(); }, "Initialize Storm-pars"); + + py::class_>(m, "_SparseParametricDtmcSimplifier", "Model simplifier for parametric DTMCs") + .def("__init__", [](SparseParametricDtmcSimplifier &instance, Dtmc const& dtmc) -> void { + new (&instance) SparseParametricDtmcSimplifier(dtmc); + }, py::arg("dtmc")) + .def("simplify", [](SparseParametricDtmcSimplifier &simplifier, storm::logic::Formula const& formula) -> bool { + return simplifier.simplify(formula); + }, "Simplify model", py::arg("formula")) + .def_property_readonly("simplified_model", [](SparseParametricDtmcSimplifier const& simplifier) { + return simplifier.getSimplifiedModel(); + }, "Return simplified model") + .def_property_readonly("simplified_formula", [](SparseParametricDtmcSimplifier const& simplifier) { + return simplifier.getSimplifiedFormula(); + }, "Return simplified formula") + ; + + py::class_>(m, "_SparseParametricMdpSimplifier", "Model simplifier for parametric MDPs") + .def("__init__", [](SparseParametricMdpSimplifier &instance, Mdp const& mdp) -> void { + new (&instance) SparseParametricMdpSimplifier(mdp); + }, py::arg("mdp")) + .def("simplify", [](SparseParametricMdpSimplifier &simplifier, storm::logic::Formula const& formula) -> bool { + return simplifier.simplify(formula); + }, "Simplify model", py::arg("formula")) + .def_property_readonly("simplified_model", [](SparseParametricMdpSimplifier const& simplifier) { + return simplifier.getSimplifiedModel(); + }, "Return simplified model") + .def_property_readonly("simplified_formula", [](SparseParametricMdpSimplifier const& simplifier) { + return simplifier.getSimplifiedFormula(); + }, "Return simplified formula") + ; + } diff --git a/tests/pars/test_parametric.py b/tests/pars/test_parametric.py index 6e14570..4b74b3a 100644 --- a/tests/pars/test_parametric.py +++ b/tests/pars/test_parametric.py @@ -43,3 +43,26 @@ class TestParametric: assert len(parameters) == 2 derivatives = stormpy.pars.gather_derivatives(model, list(parameters)[0]) assert len(derivatives) == 0 + + def test_dtmc_simplification(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) + formula = formulas[0].raw_formula + model = stormpy.build_parametric_model(program, formulas) + assert model.nr_states == 613 + assert model.nr_transitions == 803 + model, formula = stormpy.pars.simplify_model(model, formula) + assert model.nr_states == 193 + assert model.nr_transitions == 383 + + def test_mdp_simplification(self): + program = stormpy.parse_prism_program(get_example_path("pmdp", "two_dice.nm")) + formulas = stormpy.parse_properties_for_prism_program("Pmin=? [ F \"two\" ]", program) + formula = formulas[0].raw_formula + model = stormpy.build_parametric_model(program, formulas) + assert model.nr_states == 169 + assert model.nr_transitions == 435 + model, formula = stormpy.pars.simplify_model(model, formula) + assert model.nr_states == 17 + assert model.nr_transitions == 50