diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index bf19d5a..368fbcb 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -334,6 +334,7 @@ def check_model_hybrid(model, property, only_initial_states=False, environment=E task = core.CheckTask(formula, only_initial_states) return core._model_checking_hybrid_engine(model, task, environment=environment) + def transform_to_sparse_model(model): """ Transform model in symbolic representation into model in sparse representation. @@ -346,6 +347,20 @@ def transform_to_sparse_model(model): return core._transform_to_sparse_model(model) +def transform_to_discrete_time_model(model, properties): + """ + Transform continuous-time model to discrete time model. + :param model: Continuous-time model. + :param properties: List of properties to transform as well. + :return: Tuple (Discrete-time model, converted properties). + """ + formulae = [(prop.raw_formula if isinstance(prop, Property) else prop) for prop in properties] + if model.supports_parameters: + return core._transform_to_discrete_time_parametric_model(model, formulae) + else: + return core._transform_to_discrete_time_model(model, formulae) + + def prob01min_states(model, eventually_formula): assert type(eventually_formula) == logic.EventuallyFormula labelform = eventually_formula.subformula @@ -398,6 +413,7 @@ def compute_prob01max_states(model, phi_states, psi_states): else: return core._compute_prob01states_max_double(model, phi_states, psi_states) + def topological_sort(model, forward=True, initial=[]): """ @@ -413,7 +429,8 @@ def topological_sort(model, forward=True, initial=[]): else: raise StormError("Unknown kind of model.") -def construct_submodel(model, states, actions, keep_unreachable_states = True, options = SubsystemBuilderOptions()): + +def construct_submodel(model, states, actions, keep_unreachable_states=True, options=SubsystemBuilderOptions()): """ :param model: The model diff --git a/src/core/transformation.cpp b/src/core/transformation.cpp index 59541cf..a852563 100644 --- a/src/core/transformation.cpp +++ b/src/core/transformation.cpp @@ -1,4 +1,5 @@ #include "transformation.h" +#include "storm/api/transformation.h" #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/transformer/SubsystemBuilder.h" @@ -8,11 +9,19 @@ storm::transformer::SubsystemBuilderReturnType constructSubsystem(storm::mod return storm::transformer::buildSubsystem(originalModel, subsystemStates, subsystemActions, keepUnreachableStates, options); } +template +std::pair>, std::vector>> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr> const& model, std::vector> const& formulas) { + return storm::api::transformContinuousToDiscreteTimeSparseModel(model, formulas); +} + void define_transformation(py::module& m) { // Transform model m.def("_transform_to_sparse_model", &storm::api::transformSymbolicToSparseModel, "Transform symbolic model into sparse model", py::arg("model"), py::arg("formulae") = std::vector>()); 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>()); + py::class_>(m, "SubsystemBuilderReturnTypeDouble", "Result of the construction of a subsystem") .def_readonly("model", &storm::transformer::SubsystemBuilderReturnType::model, "the submodel") .def_readonly("new_to_old_state_mapping", &storm::transformer::SubsystemBuilderReturnType::newToOldStateIndexMapping, "for each state in result, the state index in the original model") diff --git a/tests/core/test_transformation.py b/tests/core/test_transformation.py index e1a322e..803c57e 100644 --- a/tests/core/test_transformation.py +++ b/tests/core/test_transformation.py @@ -2,6 +2,8 @@ import stormpy import stormpy.logic from helpers.helper import get_example_path +import math + class TestTransformation: def test_transform_symbolic_dtmc_to_sparse(self): @@ -33,3 +35,25 @@ class TestTransformation: assert symbolic_model.model_type == stormpy.ModelType.DTMC assert symbolic_model.supports_parameters assert type(symbolic_model) is stormpy.SparseParametricDtmc + + def test_transform_continuous_to_discrete_time_model(self): + ctmc = stormpy.build_model_from_drn(get_example_path("ctmc", "dft.drn")) + formulas = stormpy.parse_properties("T=? [ F \"failed\" ]") + print(formulas) + assert ctmc.nr_states == 16 + assert ctmc.nr_transitions == 33 + assert len(ctmc.initial_states) == 1 + initial_state = ctmc.initial_states[0] + assert initial_state == 1 + result = stormpy.model_checking(ctmc, formulas[0]) + assert math.isclose(result.at(initial_state), 4.166666667) + + dtmc, dtmc_formulas = stormpy.transform_to_discrete_time_model(ctmc, formulas) + print(dtmc_formulas) + assert dtmc.nr_states == 16 + assert dtmc.nr_transitions == 33 + assert len(dtmc.initial_states) == 1 + initial_state = dtmc.initial_states[0] + assert initial_state == 1 + result = stormpy.model_checking(dtmc, dtmc_formulas[0]) + assert math.isclose(result.at(initial_state), 4.166666667)