Transformation from CTMCs to DTMCs

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

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<VT> constructSubsystem(storm::mod
     return storm::transformer::buildSubsystem(originalModel, subsystemStates, subsystemActions, keepUnreachableStates, options);
 }
 
+template<typename ValueType>
+std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> 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<storm::dd::DdType::Sylvan, double>, "Transform symbolic model into sparse model", py::arg("model"), py::arg("formulae") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
     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>>());
+
     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")
             .def_readonly("new_to_old_state_mapping", &storm::transformer::SubsystemBuilderReturnType<double>::newToOldStateIndexMapping, "for each state in result, the state index in the original model")

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)