Bindings for simplification of parametric models

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

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

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<storm::RationalFunction> Dtmc;
+typedef storm::models::sparse::Mdp<storm::RationalFunction> Mdp;
+typedef storm::transformer::SparseParametricDtmcSimplifier<Dtmc> SparseParametricDtmcSimplifier;
+typedef storm::transformer::SparseParametricMdpSimplifier<Mdp> SparseParametricMdpSimplifier;
 
 void define_pars(py::module& m) {
     m.def("_set_up", []() {
             storm::settings::addModule<storm::settings::modules::ParametricSettings>();
             storm::settings::addModule<storm::settings::modules::RegionSettings>();
         }, "Initialize Storm-pars");
+
+    py::class_<SparseParametricDtmcSimplifier, std::shared_ptr<SparseParametricDtmcSimplifier>>(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_<SparseParametricMdpSimplifier, std::shared_ptr<SparseParametricMdpSimplifier>>(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")
+    ;
+
 }

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