Transformation from symbolic model to sparse model

lib/stormpy/__init__.py

@@ -332,6 +332,17 @@ def check_model_hybrid(model, property, only_initial_states=False):
         task = core.CheckTask(formula, only_initial_states)
         return core._model_checking_hybrid_engine(model, task)
 
+def transform_to_sparse_model(model):
+    """
+    Transform model in symbolic representation into model in sparse representation.
+    :param model: Symbolic model.
+    :return: Sparse model.
+    """
+    if model.supports_parameters:
+        return core._transform_to_sparse_parametric_model(model)
+    else:
+        return core._transform_to_sparse_model(model)
+
 
 def prob01min_states(model, eventually_formula):
     assert type(eventually_formula) == logic.EventuallyFormula

src/core/transformation.cpp

@@ -0,0 +1,7 @@
+#include "transformation.h"
+
+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"));
+    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"));
+}

src/core/transformation.h

@@ -0,0 +1,5 @@
+#pragma once
+
+#include "common.h"
+
+void define_transformation(py::module& m);

src/mod_core.cpp

@@ -7,6 +7,7 @@
 #include "core/input.h"
 #include "core/analysis.h"
 #include "core/environment.h"
+#include "core/transformation.h"
 
 PYBIND11_MODULE(core, m) {
     m.doc() = "core";
@@ -28,4 +29,5 @@ PYBIND11_MODULE(core, m) {
     define_input(m);
     define_graph_constraints(m);
     define_environment(m);
+    define_transformation(m);
 }

tests/core/test_transformation.py

@@ -0,0 +1,35 @@
+import stormpy
+import stormpy.logic
+from helpers.helper import get_example_path
+
+
+class TestTransformation:
+    def test_transform_symbolic_dtmc_to_sparse(self):
+        program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds5_5.pm"))
+        model = stormpy.build_symbolic_model(program)
+        assert model.nr_states == 8607
+        assert model.nr_transitions == 15113
+        assert model.model_type == stormpy.ModelType.DTMC
+        assert not model.supports_parameters
+        assert type(model) is stormpy.SymbolicSylvanDtmc
+        symbolic_model = stormpy.transform_to_sparse_model(model)
+        assert symbolic_model.nr_states == 8607
+        assert symbolic_model.nr_transitions == 15113
+        assert symbolic_model.model_type == stormpy.ModelType.DTMC
+        assert not symbolic_model.supports_parameters
+        assert type(symbolic_model) is stormpy.SparseDtmc
+
+    def test_transform_symbolic_parametric_dtmc_to_sparse(self):
+        program = stormpy.parse_prism_program(get_example_path("pdtmc", "parametric_die.pm"))
+        model = stormpy.build_symbolic_parametric_model(program)
+        assert model.nr_states == 13
+        assert model.nr_transitions == 20
+        assert model.model_type == stormpy.ModelType.DTMC
+        assert model.supports_parameters
+        assert type(model) is stormpy.SymbolicSylvanParametricDtmc
+        symbolic_model = stormpy.transform_to_sparse_model(model)
+        assert symbolic_model.nr_states == 13
+        assert symbolic_model.nr_transitions == 20
+        assert symbolic_model.model_type == stormpy.ModelType.DTMC
+        assert symbolic_model.supports_parameters
+        assert type(symbolic_model) is stormpy.SparseParametricDtmc