diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 32e577b..7893c6f 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -10,10 +10,12 @@ core._set_up("") def build_model(program, properties = None): """ - Build a model from a symbolic description + Build a model from a symbolic description. :param PrismProgram program: Prism program to translate into a model. :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. + :return: Model in sparse representation. + :rtype: SparseDtmc or SparseMdp """ if properties: formulae = [prop.raw_formula for prop in properties] @@ -30,9 +32,12 @@ def build_model(program, properties = None): def build_parametric_model(program, properties = None): """ + Build a parametric model from a symbolic description. :param PrismProgram program: Prism program with open constants to translate into a parametric model. :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. + :return: Parametric model in sparse representation. + :rtype: SparseParametricDtmc or SparseParametricMdp """ if properties: formulae = [prop.raw_formula for prop in properties] @@ -47,6 +52,48 @@ def build_parametric_model(program, properties = None): else: raise RuntimeError("Not supported parametric model constructed") +def build_model_from_drn(file): + """ + Build a model from the explicit DRN representation. + + :param String file: DRN file containing the model. + :return: Model in sparse representation. + :rtype: SparseDtmc or SparseMdp or SparseCTMC or SparseMA + """ + intermediate = core._build_sparse_model_from_drn(file) + assert not intermediate.supports_parameters + if intermediate.model_type == ModelType.DTMC: + return intermediate._as_dtmc() + elif intermediate.model_type == ModelType.MDP: + return intermediate._as_mdp() + elif intermediate.model_type == ModelType.CTMC: + return intermediate._as_ctmc() + elif intermediate.model_type == ModelType.MA: + return intermediate._as_ma() + else: + raise RuntimeError("Not supported non-parametric model constructed") + +def build_parametric_model_from_drn(file): + """ + Build a parametric model from the explicit DRN representation. + + :param String file: DRN file containing the model. + :return: Parametric model in sparse representation. + :rtype: SparseParametricDtmc or SparseParametricMdp or SparseParametricCTMC or SparseParametricMA + """ + intermediate = core._build_sparse_parametric_model_from_drn(file) + assert intermediate.supports_parameters + if intermediate.model_type == ModelType.DTMC: + return intermediate._as_pdtmc() + elif intermediate.model_type == ModelType.MDP: + return intermediate._as_pmdp() + elif intermediate.model_type == ModelType.CTMC: + return intermediate._as_pctmc() + elif intermediate.model_type == ModelType.MA: + return intermediate._as_pma() + else: + raise RuntimeError("Not supported parametric model constructed") + def perform_bisimulation(model, property, bisimulation_type): if model.supports_parameters: return core._perform_parametric_bisimulation(model, property.raw_formula, bisimulation_type) diff --git a/lib/stormpy/examples/files/ctmc/dft.drn b/lib/stormpy/examples/files/ctmc/dft.drn new file mode 100644 index 0000000..1f1f317 --- /dev/null +++ b/lib/stormpy/examples/files/ctmc/dft.drn @@ -0,0 +1,73 @@ +// Exported by storm +// Original model type: CTMC +@type: CTMC +@parameters + +@nr_states +16 +@model +state 0 init + action 0 + 1 : 0.5 + 2 : 0.5 + 3 : 0.5 + 4 : 0.5 +state 1 + action 0 + 5 : 0.5 + 9 : 0.5 + 11 : 0.5 +state 2 + action 0 + 5 : 0.5 + 14 : 0.5 + 15 : 0.5 +state 3 + action 0 + 9 : 0.5 + 12 : 0.5 + 15 : 0.5 +state 4 + action 0 + 11 : 0.5 + 12 : 0.5 + 14 : 0.5 +state 5 + action 0 + 6 : 0.5 + 8 : 0.5 +state 6 + action 0 + 7 : 0.5 +state 7 failed + action 0 + 7 : 1 +state 8 + action 0 + 7 : 0.5 +state 9 + action 0 + 8 : 0.5 + 10 : 0.5 +state 10 + action 0 + 7 : 0.5 +state 11 + action 0 + 6 : 0.5 + 10 : 0.5 +state 12 + action 0 + 10 : 0.5 + 13 : 0.5 +state 13 + action 0 + 7 : 0.5 +state 14 + action 0 + 6 : 0.5 + 13 : 0.5 +state 15 + action 0 + 8 : 0.5 + 13 : 0.5 diff --git a/src/core/core.cpp b/src/core/core.cpp index b766017..0458165 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -58,5 +58,7 @@ void define_build(py::module& m) { // Build model m.def("_build_sparse_model_from_prism_program", &storm::buildSparseModel, "Build the model", py::arg("program"), py::arg("formulas") = std::vector>()); m.def("_build_sparse_parametric_model_from_prism_program", &storm::buildSparseModel, "Build the parametric model", py::arg("program"), py::arg("formulas")); + m.def("_build_sparse_model_from_drn", &storm::buildExplicitDRNModel, "Build the model from DRN", py::arg("file")); + m.def("_build_sparse_parametric_model_from_drn", &storm::buildExplicitDRNModel, "Build the parametric model from DRN", py::arg("file")); } diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 0f79fe0..290e077 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -53,6 +53,10 @@ void define_model(py::module& m) { .def("_as_pdtmc", &storm::models::ModelBase::as>, "Get model as pDTMC") .def("_as_mdp", &storm::models::ModelBase::as>, "Get model as MDP") .def("_as_pmdp", &storm::models::ModelBase::as>, "Get model as pMDP") + .def("_as_ctmc", &storm::models::ModelBase::as>, "Get model as CTMC") + .def("_as_pctmc", &storm::models::ModelBase::as>, "Get model as pCTMC") + .def("_as_ma", &storm::models::ModelBase::as>, "Get model as MA") + .def("_as_pma", &storm::models::ModelBase::as>, "Get model as pMA") ; // Models @@ -70,6 +74,10 @@ void define_model(py::module& m) { ; py::class_, std::shared_ptr>>(m, "SparseMdp", "MDP in sparse representation", model) ; + py::class_, std::shared_ptr>>(m, "SparseCtmc", "CTMC in sparse representation", model) + ; + py::class_, std::shared_ptr>>(m, "SparseMA", "MA in sparse representation", model) + ; py::class_, std::shared_ptr>> modelRatFunc(m, "_SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix", modelBase); modelRatFunc.def("collect_probability_parameters", &probabilityVariables, "Collect parameters") @@ -85,6 +93,10 @@ void define_model(py::module& m) { ; py::class_, std::shared_ptr>>(m, "SparseParametricMdp", "pMDP in sparse representation", modelRatFunc) ; + py::class_, std::shared_ptr>>(m, "SparseParametricCtmc", "pCTMC in sparse representation", modelRatFunc) + ; + py::class_, std::shared_ptr>>(m, "SparseParametricMA", "pMA in sparse representation", modelRatFunc) + ; } diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 017b156..f44b81c 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -73,3 +73,14 @@ class TestModelChecking: labelprop = stormpy.core.Property("cora", formulaPsi.raw_formula) result = stormpy.model_checking(model, labelprop) assert result.get_truth_values().number_of_set_bits() == 1 + + def test_model_checking_ctmc(self): + model = stormpy.build_model_from_drn(get_example_path("ctmc", "dft.drn")) + formulas = stormpy.parse_properties("T=? [ F \"failed\" ]") + assert model.nr_states == 16 + assert model.nr_transitions == 33 + assert len(model.initial_states) == 1 + initial_state = model.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0]) + assert math.isclose(result.at(initial_state), 4.166666667) diff --git a/tests/core/test_parse.py b/tests/core/test_parse.py index 56e6bc6..743eca7 100644 --- a/tests/core/test_parse.py +++ b/tests/core/test_parse.py @@ -30,3 +30,12 @@ class TestParse: assert model.model_type == stormpy.ModelType.MDP assert not model.supports_parameters assert type(model) is stormpy.SparseMdp + + def test_parse_drn_dtmc(self): + model = stormpy.build_model_from_drn(get_example_path("ctmc", "dft.drn")) + assert model.nr_states == 16 + assert model.nr_transitions == 33 + assert model.model_type == stormpy.ModelType.CTMC + assert not model.supports_parameters + assert type(model) is stormpy.SparseCtmc +