From 054df185c0f49f96052217ea02582745dbc5ca7c Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 18 May 2018 18:33:29 +0200
Subject: [PATCH] Transformation from symbolic model to sparse model

---
 lib/stormpy/__init__.py           | 11 ++++++++++
 src/core/transformation.cpp       |  7 +++++++
 src/core/transformation.h         |  5 +++++
 src/mod_core.cpp                  |  2 ++
 tests/core/test_transformation.py | 35 +++++++++++++++++++++++++++++++
 5 files changed, 60 insertions(+)
 create mode 100644 src/core/transformation.cpp
 create mode 100644 src/core/transformation.h
 create mode 100644 tests/core/test_transformation.py

diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py
index 7d76643..9d3829c 100644
--- a/lib/stormpy/__init__.py
+++ b/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
diff --git a/src/core/transformation.cpp b/src/core/transformation.cpp
new file mode 100644
index 0000000..984c0e8
--- /dev/null
+++ b/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"));
+}
\ No newline at end of file
diff --git a/src/core/transformation.h b/src/core/transformation.h
new file mode 100644
index 0000000..d098346
--- /dev/null
+++ b/src/core/transformation.h
@@ -0,0 +1,5 @@
+#pragma once
+
+#include "common.h"
+
+void define_transformation(py::module& m);
diff --git a/src/mod_core.cpp b/src/mod_core.cpp
index 615a7ef..5a84f58 100644
--- a/src/mod_core.cpp
+++ b/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);
 }
diff --git a/tests/core/test_transformation.py b/tests/core/test_transformation.py
new file mode 100644
index 0000000..562f85f
--- /dev/null
+++ b/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