From 106e1146b6402b73e7b5a3d075202eb5e7b8f3e9 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 22 Jan 2020 16:32:42 +0100 Subject: [PATCH] Bindings for elimination of chains of non-Markovian states --- lib/stormpy/__init__.py | 24 ++++++++++++--- src/core/transformation.cpp | 12 +++++++- tests/core/test_transformation.py | 50 +++++++++++++++++++++++++++++++ 3 files changed, 81 insertions(+), 5 deletions(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 8445b17..376a941 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -264,13 +264,13 @@ def model_checking(model, property, only_initial_states=False, extract_scheduler """ if model.is_sparse_model: return check_model_sparse(model, property, only_initial_states=only_initial_states, - extract_scheduler=extract_scheduler, environment=environment) + extract_scheduler=extract_scheduler, environment=environment) else: - assert(model.is_symbolic_model) + assert (model.is_symbolic_model) if extract_scheduler: raise StormError("Model checking based on dd engine does not support extracting schedulers right now.") return check_model_dd(model, property, only_initial_states=only_initial_states, - environment=environment) + environment=environment) def check_model_sparse(model, property, only_initial_states=False, extract_scheduler=False, environment=Environment()): @@ -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,7 +466,8 @@ def construct_submodel(model, states, actions, keep_unreachable_states=True, opt else: raise NotImplementedError() -def parse_properties(properties, context = None, filters = None): + +def parse_properties(properties, context=None, filters=None): """ :param properties: A string with the pctl properties diff --git a/src/core/transformation.cpp b/src/core/transformation.cpp index a852563..ff36aeb 100644 --- a/src/core/transformation.cpp +++ b/src/core/transformation.cpp @@ -20,7 +20,7 @@ void define_transformation(py::module& m) { m.def("_transform_to_sparse_parametric_model", &storm::api::transformSymbolicToSparseModel, "Transform symbolic parametric model into sparse parametric model", py::arg("model"), py::arg("formulae") = std::vector>()); m.def("_transform_to_discrete_time_model", &transformContinuousToDiscreteTimeSparseModel, "Transform continuous time model to discrete time model", py::arg("model"), py::arg("formulae") = std::vector>()); - m.def("_transform_to_discrete_time_parametric_model", &transformContinuousToDiscreteTimeSparseModel, "Transform continuous time model to discrete time model", py::arg("model"), py::arg("formulae") = std::vector>()); + m.def("_transform_to_discrete_time_parametric_model", &transformContinuousToDiscreteTimeSparseModel, "Transform parametric continuous time model to parametric discrete time model", py::arg("model"), py::arg("formulae") = std::vector>()); py::class_>(m, "SubsystemBuilderReturnTypeDouble", "Result of the construction of a subsystem") .def_readonly("model", &storm::transformer::SubsystemBuilderReturnType::model, "the submodel") @@ -40,4 +40,14 @@ void define_transformation(py::module& m) { m.def("_construct_subsystem_double", &constructSubsystem, "build a subsystem of a sparse model"); + // Non-Markovian chain elimination + py::enum_(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, "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, "Eliminate chains of non-Markovian states in Markov automaton.", py::arg("ma"), py::arg("formulae"), py::arg("label_behavior")); + } \ No newline at end of file diff --git a/tests/core/test_transformation.py b/tests/core/test_transformation.py index b1ffe99..2377371 100644 --- a/tests/core/test_transformation.py +++ b/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)