Bindings for elimination of chains of non-Markovian states

lib/stormpy/__init__.py

@@ -368,6 +368,21 @@ def transform_to_discrete_time_model(model, properties):
         return core._transform_to_discrete_time_model(model, formulae)
 
 
+def eliminate_non_markovian_chains(ma, properties, label_behavior):
+    """
+    Eliminate chains of non-Markovian states if possible.
+    :param ma: Markov automaton.
+    :param properties: List of properties to transform as well.
+    :param label_behavior: Behavior of labels while elimination.
+    :return: Tuple (converted MA, converted properties).
+    """
+    formulae = [(prop.raw_formula if isinstance(prop, Property) else prop) for prop in properties]
+    if ma.supports_parameters:
+        return core._eliminate_non_markovian_chains_parametric(ma, formulae, label_behavior)
+    else:
+        return core._eliminate_non_markovian_chains(ma, formulae, label_behavior)
+
+
 def prob01min_states(model, eventually_formula):
     assert type(eventually_formula) == logic.EventuallyFormula
     labelform = eventually_formula.subformula
@@ -451,6 +466,7 @@ def construct_submodel(model, states, actions, keep_unreachable_states=True, opt
     else:
         raise NotImplementedError()
 
+
 def parse_properties(properties, context=None, filters=None):
     """
 

src/core/transformation.cpp

@@ -20,7 +20,7 @@ void define_transformation(py::module& m) {
     m.def("_transform_to_sparse_parametric_model", &storm::api::transformSymbolicToSparseModel<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Transform symbolic parametric model into sparse parametric model", py::arg("model"), py::arg("formulae") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
 
     m.def("_transform_to_discrete_time_model", &transformContinuousToDiscreteTimeSparseModel<double>, "Transform continuous time model to discrete time model", py::arg("model"), py::arg("formulae") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
-    m.def("_transform_to_discrete_time_parametric_model", &transformContinuousToDiscreteTimeSparseModel<storm::RationalFunction>, "Transform continuous time model to discrete time model", py::arg("model"), py::arg("formulae") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
+    m.def("_transform_to_discrete_time_parametric_model", &transformContinuousToDiscreteTimeSparseModel<storm::RationalFunction>, "Transform parametric continuous time model to parametric discrete time model", py::arg("model"), py::arg("formulae") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
 
     py::class_<storm::transformer::SubsystemBuilderReturnType<double>>(m, "SubsystemBuilderReturnTypeDouble", "Result of the construction of a subsystem")
             .def_readonly("model", &storm::transformer::SubsystemBuilderReturnType<double>::model, "the submodel")
@@ -40,4 +40,14 @@ void define_transformation(py::module& m) {
 
     m.def("_construct_subsystem_double", &constructSubsystem<double>, "build a subsystem of a sparse model");
 
+    // Non-Markovian chain elimination
+    py::enum_<storm::transformer::EliminationLabelBehavior>(m, "EliminationLabelBehavior", "Behavior of labels while eliminating non-Markovian chains")
+        .value("KEEP_LABELS", storm::transformer::EliminationLabelBehavior::KeepLabels)
+        .value("MERGE_LABELS", storm::transformer::EliminationLabelBehavior::MergeLabels)
+        .value("DELETE_LABELS", storm::transformer::EliminationLabelBehavior::DeleteLabels)
+    ;
+
+    m.def("_eliminate_non_markovian_chains", &storm::api::eliminateNonMarkovianChains<double>, "Eliminate chains of non-Markovian states in Markov automaton.", py::arg("ma"), py::arg("formulae"), py::arg("label_behavior"));
+    m.def("_eliminate_non_markovian_chains_parametric", &storm::api::eliminateNonMarkovianChains<storm::RationalFunction>, "Eliminate chains of non-Markovian states in Markov automaton.", py::arg("ma"), py::arg("formulae"), py::arg("label_behavior"));
+
 }

tests/core/test_transformation.py

@@ -79,3 +79,53 @@ class TestTransformation:
         assert initial_state == 0
         result = stormpy.model_checking(mdp, mdp_formulas[0])
         assert math.isclose(result.at(initial_state), 0.08333333333)
+
+    def test_eliminate_non_markovian_chains(self):
+        program = stormpy.parse_prism_program(get_example_path("ma", "stream2.ma"), False, True)
+        formulas = stormpy.parse_properties_for_prism_program("Pmin=? [ F \"done\"];Tmin=? [ F \"done\" ]", program)
+        ma = stormpy.build_model(program, formulas)
+        assert ma.nr_states == 12
+        assert ma.nr_transitions == 14
+        assert ma.model_type == stormpy.ModelType.MA
+        assert len(ma.initial_states) == 1
+        initial_state = ma.initial_states[0]
+        assert initial_state == 0
+        assert len(formulas) == 2
+        result = stormpy.model_checking(ma, formulas[0])
+        assert math.isclose(result.at(initial_state), 1)
+
+        # Keep labels
+        ma_elim, ma_formulas_elim = stormpy.eliminate_non_markovian_chains(ma, formulas, stormpy.EliminationLabelBehavior.KEEP_LABELS)
+        assert ma_elim.nr_states == 9
+        assert ma_elim.nr_transitions == 11
+        assert ma_elim.model_type == stormpy.ModelType.MA
+        assert len(ma_elim.initial_states) == 1
+        initial_state = ma_elim.initial_states[0]
+        assert initial_state == 0
+        assert len(ma_formulas_elim) == 1
+        result = stormpy.model_checking(ma_elim, ma_formulas_elim[0])
+        assert math.isclose(result.at(initial_state), 1)
+
+        # Merge labels
+        ma_elim, ma_formulas_elim = stormpy.eliminate_non_markovian_chains(ma, formulas, stormpy.EliminationLabelBehavior.MERGE_LABELS)
+        assert ma_elim.nr_states == 8
+        assert ma_elim.nr_transitions == 10
+        assert ma_elim.model_type == stormpy.ModelType.MA
+        assert len(ma_elim.initial_states) == 1
+        initial_state = ma_elim.initial_states[0]
+        assert initial_state == 0
+        assert len(ma_formulas_elim) == 1
+        result = stormpy.model_checking(ma_elim, ma_formulas_elim[0])
+        assert math.isclose(result.at(initial_state), 1)
+
+        # Delete labels
+        ma_elim, ma_formulas_elim = stormpy.eliminate_non_markovian_chains(ma, formulas, stormpy.EliminationLabelBehavior.DELETE_LABELS)
+        assert ma_elim.nr_states == 8
+        assert ma_elim.nr_transitions == 10
+        assert ma_elim.model_type == stormpy.ModelType.MA
+        assert len(ma_elim.initial_states) == 1
+        initial_state = ma_elim.initial_states[0]
+        assert initial_state == 0
+        assert len(ma_formulas_elim) == 1
+        result = stormpy.model_checking(ma_elim, ma_formulas_elim[0])
+        assert math.isclose(result.at(initial_state), 1)