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, "Transform symbolic model into sparse model", py::arg("model")); + m.def("_transform_to_sparse_parametric_model", &storm::api::transformSymbolicToSparseModel, "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