From 505594dbba4ad54eb6d1fa839c9f0f022f1e325f Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 1 Mar 2017 18:01:34 +0100 Subject: [PATCH 01/11] Small comment --- src/core/core.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/core/core.cpp b/src/core/core.cpp index a191403..b766017 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -17,6 +17,7 @@ void define_parse(py::module& m) { :param str formula_str: A string of formulas :param str property_filter: A filter + :return: A list of properties )dox", py::arg("formula_string"), py::arg("property_filter") = boost::none); m.def("parse_properties_for_prism_program", &storm::parsePropertiesForPrismProgram, R"dox( From db86de94437445cf19c6c27d99c2a13aed6d1796 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 2 Mar 2017 13:25:38 +0100 Subject: [PATCH 02/11] Bindings for importing DRN files --- lib/stormpy/__init__.py | 49 ++++++++++++++++- lib/stormpy/examples/files/ctmc/dft.drn | 73 +++++++++++++++++++++++++ src/core/core.cpp | 2 + src/storage/model.cpp | 12 ++++ tests/core/test_modelchecking.py | 11 ++++ tests/core/test_parse.py | 9 +++ 6 files changed, 155 insertions(+), 1 deletion(-) create mode 100644 lib/stormpy/examples/files/ctmc/dft.drn 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 + From 0b290d782f283014fb51946e69486244bff7da76 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 2 Mar 2017 23:26:24 +0100 Subject: [PATCH 03/11] ModelInstantiator for CTMC and MA as well --- lib/stormpy/storage/__init__.py | 8 ++++++-- src/storage/model.cpp | 16 ++++++++++++---- 2 files changed, 18 insertions(+), 6 deletions(-) diff --git a/lib/stormpy/storage/__init__.py b/lib/stormpy/storage/__init__.py index 2eda405..0d3e560 100644 --- a/lib/stormpy/storage/__init__.py +++ b/lib/stormpy/storage/__init__.py @@ -8,8 +8,12 @@ class ModelInstantiator: self._instantiator = PmdpInstantiator(model) elif model.model_type == ModelType.DTMC: self._instantiator = PdtmcInstantiator(model) + elif model.model_type == ModelType.CTMC: + self._instantiator = PctmcInstantiator(model) + elif model.model_type == ModelType.MA: + self._instantiator = PmaInstantiator(model) else: - raise ValueError("Only DTMCs and MDPs supported") + raise ValueError("Model type {} not supported".format(model.model_type)) def instantiate(self, point): - return self._instantiator.instantiate(point) \ No newline at end of file + return self._instantiator.instantiate(point) diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 290e077..f3bfd31 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -103,10 +103,18 @@ void define_model(py::module& m) { // Model instantiator void define_model_instantiator(py::module& m) { py::class_,storm::models::sparse::Dtmc>>(m, "PdtmcInstantiator", "Instantiate PDTMCs to DTMCs") - .def(py::init>(), "parametric model"_a) - .def("instantiate", &storm::utility::ModelInstantiator, storm::models::sparse::Dtmc>::instantiate, "Instantiate model with given parameter values"); + .def(py::init>(), "parametric model"_a) + .def("instantiate", &storm::utility::ModelInstantiator, storm::models::sparse::Dtmc>::instantiate, "Instantiate model with given parameter values"); py::class_,storm::models::sparse::Mdp>>(m, "PmdpInstantiator", "Instantiate PMDPs to MDPs") - .def(py::init>(), "parametric model"_a) - .def("instantiate", &storm::utility::ModelInstantiator, storm::models::sparse::Mdp>::instantiate, "Instantiate model with given parameter values"); + .def(py::init>(), "parametric model"_a) + .def("instantiate", &storm::utility::ModelInstantiator, storm::models::sparse::Mdp>::instantiate, "Instantiate model with given parameter values"); + + py::class_,storm::models::sparse::Ctmc>>(m, "PctmcInstantiator", "Instantiate PCTMCs to CTMCs") + .def(py::init>(), "parametric model"_a) + .def("instantiate", &storm::utility::ModelInstantiator, storm::models::sparse::Ctmc>::instantiate, "Instantiate model with given parameter values"); + + py::class_,storm::models::sparse::MarkovAutomaton>>(m, "PmaInstantiator", "Instantiate PMAs to MAs") + .def(py::init>(), "parametric model"_a) + .def("instantiate", &storm::utility::ModelInstantiator, storm::models::sparse::MarkovAutomaton>::instantiate, "Instantiate model with given parameter values"); } From 64c663a809100c489296e335abba56a995232b2c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 6 Mar 2017 16:57:26 +0100 Subject: [PATCH 04/11] Started with Python bindings for storm-dft --- CMakeLists.txt | 5 +- lib/stormpy/dft/__init__.py | 4 ++ lib/stormpy/examples/files/dft/and.json | 71 +++++++++++++++++++++++++ setup.py | 5 +- src/dft/common.h | 1 + src/dft/dft.cpp | 29 ++++++++++ src/dft/dft.h | 8 +++ src/mod_dft.cpp | 15 ++++++ tests/dft/test_build.py | 19 +++++++ 9 files changed, 153 insertions(+), 4 deletions(-) create mode 100644 lib/stormpy/dft/__init__.py create mode 100644 lib/stormpy/examples/files/dft/and.json create mode 100644 src/dft/common.h create mode 100644 src/dft/dft.cpp create mode 100644 src/dft/dft.h create mode 100644 src/mod_dft.cpp create mode 100644 tests/dft/test_build.py diff --git a/CMakeLists.txt b/CMakeLists.txt index 1ec1761..3183182 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -23,8 +23,8 @@ function(stormpy_module NAME) file(GLOB_RECURSE "STORM_${NAME}_SOURCES" "${CMAKE_CURRENT_SOURCE_DIR}/src/${NAME}/*.cpp") pybind11_add_module(${NAME} "${CMAKE_CURRENT_SOURCE_DIR}/src/mod_${NAME}.cpp" ${STORM_${NAME}_SOURCES}) - target_include_directories(${NAME} PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${storm_INCLUDE_DIR} ${CMAKE_CURRENT_BINARY_DIR}/src/generated) - target_link_libraries(${NAME} PRIVATE storm) + target_include_directories(${NAME} PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${storm_INCLUDE_DIR} ${storm-dft_INCLUDE_DIR} ${CMAKE_CURRENT_BINARY_DIR}/src/generated) + target_link_libraries(${NAME} PRIVATE storm storm-dft) # setup.py will override this (because pip may want a different install # path), but also specifying it here has the advantage that invoking cmake @@ -40,3 +40,4 @@ stormpy_module(expressions) stormpy_module(logic) stormpy_module(storage) stormpy_module(utility) +stormpy_module(dft) diff --git a/lib/stormpy/dft/__init__.py b/lib/stormpy/dft/__init__.py new file mode 100644 index 0000000..ae53cc2 --- /dev/null +++ b/lib/stormpy/dft/__init__.py @@ -0,0 +1,4 @@ +from . import dft +from .dft import * + +dft._set_up() diff --git a/lib/stormpy/examples/files/dft/and.json b/lib/stormpy/examples/files/dft/and.json new file mode 100644 index 0000000..ce62b7f --- /dev/null +++ b/lib/stormpy/examples/files/dft/and.json @@ -0,0 +1,71 @@ +{ + "toplevel": "2", + "parameters": {}, + "nodes": [ + { + "data": { + "id": "0", + "name": "B", + "type": "be", + "rate": "0.5", + "dorm": "1", + "label": "B (0.5)" + }, + "position": { + "x": 426, + "y": 142 + }, + "group": "nodes", + "removed": false, + "selected": false, + "selectable": true, + "locked": false, + "grabbable": true, + "classes": "be" + }, + { + "data": { + "id": "1", + "name": "C", + "type": "be", + "rate": "0.5", + "dorm": "1", + "label": "C (0.5)" + }, + "position": { + "x": 598, + "y": 139 + }, + "group": "nodes", + "removed": false, + "selected": false, + "selectable": true, + "locked": false, + "grabbable": true, + "classes": "be" + }, + { + "data": { + "id": "2", + "name": "A", + "type": "and", + "children": [ + "0", + "1" + ], + "label": "A" + }, + "position": { + "x": 503, + "y": 42 + }, + "group": "nodes", + "removed": false, + "selected": false, + "selectable": true, + "locked": false, + "grabbable": true, + "classes": "and toplevel" + } + ] +} \ No newline at end of file diff --git a/setup.py b/setup.py index 5ab038a..2188718 100755 --- a/setup.py +++ b/setup.py @@ -81,7 +81,7 @@ setup( maintainer_email="sebastian.junges@cs.rwth-aachen.de", url="http://moves.rwth-aachen.de", description="stormpy - Python Bindings for Storm", - packages=['stormpy', 'stormpy.info', 'stormpy.expressions', 'stormpy.logic', 'stormpy.storage', 'stormpy.utility'], + packages=['stormpy', 'stormpy.info', 'stormpy.expressions', 'stormpy.logic', 'stormpy.storage', 'stormpy.utility', 'stormpy.dft'], package_dir={'': 'lib'}, ext_package='stormpy', ext_modules=[CMakeExtension('core', subdir=''), @@ -89,7 +89,8 @@ setup( CMakeExtension('expressions', subdir='expressions'), CMakeExtension('logic', subdir='logic'), CMakeExtension('storage', subdir='storage'), - CMakeExtension('utility', subdir='utility') + CMakeExtension('utility', subdir='utility'), + CMakeExtension('dft', subdir='dft') ], cmdclass=dict(build_ext=CMakeBuild, test=PyTest), zip_safe=False, diff --git a/src/dft/common.h b/src/dft/common.h new file mode 100644 index 0000000..c9b9b0c --- /dev/null +++ b/src/dft/common.h @@ -0,0 +1 @@ +#include "src/common.h" diff --git a/src/dft/dft.cpp b/src/dft/dft.cpp new file mode 100644 index 0000000..4c2ca64 --- /dev/null +++ b/src/dft/dft.cpp @@ -0,0 +1,29 @@ +#include "dft.h" +#include "storm-dft/parser/DFTJsonParser.h" +#include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h" +#include "storm/settings/SettingsManager.h" +#include "storm-dft/settings/modules/DFTSettings.h" + +// Thin wrapper for model building using one formula as argument +template +std::shared_ptr> buildModelFromJsonDft(std::string const& jsonDft) { + // Build DFT + storm::parser::DFTJsonParser parser; + storm::storage::DFT dft = parser.parseJson(jsonDft); + // Build model + std::map>> emptySymmetry; + storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); + storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, true); + typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions({}, true); + builder.buildModel(labeloptions, 0, 0.0); + return builder.getModel(); +} + +void define_dft(py::module& m) { + m.def("_set_up", []() { + storm::settings::addModule(); + }, "Initialize Storm-dft"); + // Build model + m.def("build_sparse_model_from_json_dft", &buildModelFromJsonDft, "Build the model", py::arg("jsonDft")); + m.def("build_sparse_parametric_model_from_json_dft", &buildModelFromJsonDft, "Build the parametric model", py::arg("jsonDft")); +} diff --git a/src/dft/dft.h b/src/dft/dft.h new file mode 100644 index 0000000..2dc129a --- /dev/null +++ b/src/dft/dft.h @@ -0,0 +1,8 @@ +#ifndef PYTHON_DFT_DFT_H_ +#define PYTHON_DFT_DFT_H_ + +#include "common.h" + +void define_dft(py::module& m); + +#endif /* PYTHON_DFT_DFT_H_ */ diff --git a/src/mod_dft.cpp b/src/mod_dft.cpp new file mode 100644 index 0000000..b6a8d41 --- /dev/null +++ b/src/mod_dft.cpp @@ -0,0 +1,15 @@ +#include "common.h" + +#include "dft/dft.h" + +PYBIND11_PLUGIN(dft) { + py::module m("dft", "Functionality for DFT analysis"); + +#ifdef STORMPY_DISABLE_SIGNATURE_DOC + py::options options; + options.disable_function_signatures(); +#endif + + define_dft(m); + return m.ptr(); +} diff --git a/tests/dft/test_build.py b/tests/dft/test_build.py new file mode 100644 index 0000000..059b027 --- /dev/null +++ b/tests/dft/test_build.py @@ -0,0 +1,19 @@ +import stormpy +import stormpy.dft +import stormpy.logic +from helpers.helper import get_example_path + +import math + +class TestBuild: + def test_build_dft(self): + model = stormpy.dft.build_sparse_model_from_json_dft(get_example_path("dft", "and.json")) + formulas = stormpy.parse_properties("T=? [ F \"failed\" ]") + assert model.nr_states == 4 + assert model.nr_transitions == 5 + 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), 3) + From 26d2b90f442a3687c9bc3e8dd6b153044f36a9e0 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 7 Mar 2017 19:09:01 +0100 Subject: [PATCH 05/11] Bindings for state labeling --- src/mod_storage.cpp | 2 ++ src/storage/bitvector.cpp | 7 ++++- src/storage/labeling.cpp | 29 ++++++++++++++++++++ src/storage/labeling.h | 8 ++++++ src/storage/model.cpp | 13 ++++----- tests/storage/test_labeling.py | 49 ++++++++++++++++++++++++++++++++++ tests/storage/test_model.py | 26 ------------------ 7 files changed, 101 insertions(+), 33 deletions(-) create mode 100644 src/storage/labeling.cpp create mode 100644 src/storage/labeling.h create mode 100644 tests/storage/test_labeling.py diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 003646b..658043c 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -3,6 +3,7 @@ #include "storage/bitvector.h" #include "storage/model.h" #include "storage/matrix.h" +#include "storage/labeling.h" PYBIND11_PLUGIN(storage) { py::module m("storage"); @@ -16,5 +17,6 @@ PYBIND11_PLUGIN(storage) { define_model(m); define_sparse_matrix(m); define_model_instantiator(m); + define_labeling(m); return m.ptr(); } diff --git a/src/storage/bitvector.cpp b/src/storage/bitvector.cpp index dc24960..c40e211 100644 --- a/src/storage/bitvector.cpp +++ b/src/storage/bitvector.cpp @@ -16,7 +16,12 @@ void define_bitvector(py::module& m) { .def("size", &BitVector::size) .def("number_of_set_bits", &BitVector::getNumberOfSetBits) //.def("get", &BitVector::get, "index"_a) // no idea why this does not work - .def("get", [](BitVector const& b, uint_fast64_t i) { return b.get(i); }, "index"_a) + .def("get", [](BitVector const& b, uint_fast64_t i) { + return b.get(i); + }, "index"_a) + .def("set", [](BitVector& b, uint_fast64_t i, bool v) { + b.set(i, v); + }, py::arg("index"), py::arg("value") = true, "Set") .def(py::self == py::self) .def(py::self != py::self) diff --git a/src/storage/labeling.cpp b/src/storage/labeling.cpp new file mode 100644 index 0000000..f0217e6 --- /dev/null +++ b/src/storage/labeling.cpp @@ -0,0 +1,29 @@ +#include "labeling.h" + +#include "storm/models/sparse/StateLabeling.h" + +// Define python bindings +void define_labeling(py::module& m) { + + // StateLabeling + py::class_>(m, "StateLabeling", "Labeling for states") + .def("add_label", [](storm::models::sparse::StateLabeling& labeling, std::string label) { + labeling.addLabel(label); + }, py::arg("label"), "Add label") + .def("get_labels", &storm::models::sparse::StateLabeling::getLabels, "Get all labels") + .def("get_labels_of_state", &storm::models::sparse::StateLabeling::getLabelsOfState, "Get labels of given state", py::arg("state")) + .def("contains_label", &storm::models::sparse::StateLabeling::containsLabel, "Check if the given label is contained in the labeling", py::arg("label")) + .def("add_label_to_state", &storm::models::sparse::StateLabeling::addLabelToState, "Add label to state", py::arg("label"), py::arg("state")) + .def("has_state_label", &storm::models::sparse::StateLabeling::getStateHasLabel, "Check if the given state has the given label", py::arg("label"), py::arg("state")) + .def("get_states", &storm::models::sparse::StateLabeling::getStates, "Get all states which have the given label", py::arg("label")) + .def("set_states", [](storm::models::sparse::StateLabeling& labeling, std::string const& label, storm::storage::BitVector const& states) { + labeling.setStates(label, states); + }, "Set all states which have the given label", py::arg("label"), py::arg("states")) + .def("__str__", [](storm::models::sparse::StateLabeling const& labeling) { + std::ostringstream oss; + oss << labeling; + return oss.str(); + }) + ; + +} diff --git a/src/storage/labeling.h b/src/storage/labeling.h new file mode 100644 index 0000000..1a4e420 --- /dev/null +++ b/src/storage/labeling.h @@ -0,0 +1,8 @@ +#ifndef PYTHON_STORAGE_LABELING_H_ +#define PYTHON_STORAGE_LABELING_H_ + +#include "common.h" + +void define_labeling(py::module& m); + +#endif /* PYTHON_STORAGE_LABELING_H_ */ diff --git a/src/storage/model.cpp b/src/storage/model.cpp index f3bfd31..17c71ec 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -30,6 +30,11 @@ std::set rewardVariables(storm::models::sparse: return storm::models::sparse::getRewardParameters(model); } +template +storm::models::sparse::StateLabeling& getLabeling(storm::models::sparse::Model& model) { + return model.getStateLabeling(); +} + // Define python bindings void define_model(py::module& m) { @@ -63,9 +68,7 @@ void define_model(py::module& m) { //storm::models::sparse::Model > py::class_, std::shared_ptr>> model(m, "_SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix", modelBase); - model.def_property_readonly("labels", [](storm::models::sparse::Model& model) { - return model.getStateLabeling().getLabels(); - }, "Labels") + model.def_property_readonly("labeling", &getLabeling, "Labels") .def("labels_state", &storm::models::sparse::Model::getLabelsOfState, py::arg("state"), "Get labels of state") .def_property_readonly("initial_states", &getInitialStates, "Initial states") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") @@ -82,9 +85,7 @@ void define_model(py::module& m) { 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") .def("collect_reward_parameters", &rewardVariables, "Collect reward parameters") - .def_property_readonly("labels", [](storm::models::sparse::Model& model) { - return model.getStateLabeling().getLabels(); - }, "Labels") + .def_property_readonly("labeling", &getLabeling, "Labels") .def("labels_state", &storm::models::sparse::Model::getLabelsOfState, py::arg("state"), "Get labels of state") .def_property_readonly("initial_states", &getInitialStates, "Initial states") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") diff --git a/tests/storage/test_labeling.py b/tests/storage/test_labeling.py new file mode 100644 index 0000000..190a53e --- /dev/null +++ b/tests/storage/test_labeling.py @@ -0,0 +1,49 @@ +import stormpy +import stormpy.logic +from helpers.helper import get_example_path + +class TestLabeling: + def test_set_labeling(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + model = stormpy.build_model(program) + labeling = model.labeling + assert "tmp" not in labeling.get_labels() + assert not labeling.contains_label("tmp") + labeling.add_label("tmp") + assert labeling.contains_label("tmp") + labeling.add_label_to_state("tmp", 0) + assert labeling.has_state_label("tmp", 0) + states = labeling.get_states("tmp") + assert states.get(0) + states.set(3) + labeling.set_states("tmp", states) + assert labeling.has_state_label("tmp", 3) + + def test_label(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + model = stormpy.build_model(program, formulas) + labeling = model.labeling + labels = labeling.get_labels() + assert len(labels) == 3 + assert "init" in labels + assert "one" in labels + assert "init" in model.labels_state(0) + assert "init" in labeling.get_labels_of_state(0) + assert "one" in model.labels_state(7) + assert "one" in labeling.get_labels_of_state(7) + + def test_label_parametric(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F s=5 ]", program) + model = stormpy.build_parametric_model(program, formulas) + labels = model.labeling.get_labels() + assert len(labels) == 3 + assert "init" in labels + assert "(s = 5)" in labels + assert "init" in model.labels_state(0) + assert "(s = 5)" in model.labels_state(28) + assert "(s = 5)" in model.labels_state(611) + initial_states = model.initial_states + assert len(initial_states) == 1 + assert 0 in initial_states diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 8ca25f4..df17d89 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -70,17 +70,6 @@ class TestModel: assert not model.has_parameters assert type(model) is stormpy.SparseParametricDtmc - def test_label(self): - program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) - model = stormpy.build_model(program, formulas) - labels = model.labels - assert len(labels) == 3 - assert "init" in labels - assert "one" in labels - assert "init" in model.labels_state(0) - assert "one" in model.labels_state(7) - def test_initial_states(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) @@ -88,18 +77,3 @@ class TestModel: initial_states = model.initial_states assert len(initial_states) == 1 assert 0 in initial_states - - def test_label_parametric(self): - program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F s=5 ]", program) - model = stormpy.build_parametric_model(program, formulas) - labels = model.labels - assert len(labels) == 3 - assert "init" in labels - assert "(s = 5)" in labels - assert "init" in model.labels_state(0) - assert "(s = 5)" in model.labels_state(28) - assert "(s = 5)" in model.labels_state(611) - initial_states = model.initial_states - assert len(initial_states) == 1 - assert 0 in initial_states From c017949d0c3e73adcd25d5af06fea6531423407d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 8 Mar 2017 17:44:38 +0100 Subject: [PATCH 06/11] Use matrix instead of model for iterators --- lib/stormpy/storage/action.py | 8 ++++---- lib/stormpy/storage/state.py | 14 +++++++------- src/storage/matrix.cpp | 2 ++ src/storage/model.cpp | 7 +++++++ tests/storage/test_matrix.py | 12 +++++++++++- tests/storage/test_model_iterators.py | 26 +++++++++++++------------- 6 files changed, 44 insertions(+), 25 deletions(-) diff --git a/lib/stormpy/storage/action.py b/lib/stormpy/storage/action.py index 420f5b3..ad6f68e 100644 --- a/lib/stormpy/storage/action.py +++ b/lib/stormpy/storage/action.py @@ -1,17 +1,17 @@ class Action: """ Represents an action in the model """ - def __init__(self, row_group_start, row_group_end, row, model): + def __init__(self, row_group_start, row_group_end, row, matrix): """ Initialize :param row_group_start: Start index of the row group in the matrix :param row_group_end: End index of the row group in the matrix :param row: Index of the corresponding row in the matrix - :param model: Corresponding model + :param matrix: Corresponding matrix """ self.row_group_start = row_group_start self.row_group_end = row_group_end self.row = row - 1 - self.model = model + self.matrix = matrix assert row >= -1 and row + row_group_start <= row_group_end def __iter__(self): @@ -33,4 +33,4 @@ class Action: """ row = self.row_group_start + self.row #return self.model.transition_matrix().get_row(self.row_group_start + self.row) - return self.model.transition_matrix.row_iter(row, row) + return self.matrix.row_iter(row, row) diff --git a/lib/stormpy/storage/state.py b/lib/stormpy/storage/state.py index 6a315e7..613316e 100644 --- a/lib/stormpy/storage/state.py +++ b/lib/stormpy/storage/state.py @@ -1,21 +1,21 @@ from . import action class State: - """ Represents a state in the model """ + """ Represents a state in the matrix """ - def __init__(self, id, model): + def __init__(self, id, matrix): """ Initialize :param id: Id of the state - :param model: Corresponding model + :param matrix: Corresponding matrix """ self.id = id - 1 - self.model = model + self.matrix = matrix def __iter__(self): return self def __next__(self): - if self.id >= self.model.nr_states - 1: + if self.id >= self.matrix.nr_row_groups - 1: raise StopIteration else: self.id += 1 @@ -28,7 +28,7 @@ class State: """ Get actions associated with the state :return List of actions """ - row_group_indices = self.model.transition_matrix._row_group_indices + row_group_indices = self.matrix._row_group_indices start = row_group_indices[self.id] end = row_group_indices[self.id+1] - return action.Action(start, end, 0, self.model) + return action.Action(start, end, 0, self.matrix) diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp index 887a866..567cbdf 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -44,6 +44,7 @@ void define_sparse_matrix(py::module& m) { return stream.str(); }) .def_property_readonly("nr_rows", &storm::storage::SparseMatrix::getRowCount, "Number of rows") + .def_property_readonly("nr_row_groups", &storm::storage::SparseMatrix::getRowGroupCount, "Number of row groups") .def_property_readonly("nr_columns", &storm::storage::SparseMatrix::getColumnCount, "Number of columns") .def_property_readonly("nr_entries", &storm::storage::SparseMatrix::getEntryCount, "Number of non-zero entries") .def_property_readonly("_row_group_indices", &storm::storage::SparseMatrix::getRowGroupIndices, "Starting rows of row groups") @@ -77,6 +78,7 @@ void define_sparse_matrix(py::module& m) { return stream.str(); }) .def_property_readonly("nr_rows", &storm::storage::SparseMatrix::getRowCount, "Number of rows") + .def_property_readonly("nr_row_groups", &storm::storage::SparseMatrix::getRowGroupCount, "Number of row groups") .def_property_readonly("nr_columns", &storm::storage::SparseMatrix::getColumnCount, "Number of columns") .def_property_readonly("nr_entries", &storm::storage::SparseMatrix::getEntryCount, "Number of non-zero entries") .def_property_readonly("_row_group_indices", &storm::storage::SparseMatrix::getRowGroupIndices, "Starting rows of row groups") diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 17c71ec..839ee4e 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -22,6 +22,11 @@ storm::storage::SparseMatrix& getTransitionMatrix(storm::models::spar return model.getTransitionMatrix(); } +template +storm::storage::SparseMatrix getBackwardTransitionMatrix(storm::models::sparse::Model& model) { + return model.getBackwardTransitions(); +} + std::set probabilityVariables(storm::models::sparse::Model const& model) { return storm::models::sparse::getProbabilityParameters(model); } @@ -72,6 +77,7 @@ void define_model(py::module& m) { .def("labels_state", &storm::models::sparse::Model::getLabelsOfState, py::arg("state"), "Get labels of state") .def_property_readonly("initial_states", &getInitialStates, "Initial states") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") + .def_property_readonly("backward_transition_matrix", &getBackwardTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") ; py::class_, std::shared_ptr>>(m, "SparseDtmc", "DTMC in sparse representation", model) ; @@ -89,6 +95,7 @@ void define_model(py::module& m) { .def("labels_state", &storm::models::sparse::Model::getLabelsOfState, py::arg("state"), "Get labels of state") .def_property_readonly("initial_states", &getInitialStates, "Initial states") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") + .def_property_readonly("backward_transition_matrix", &getBackwardTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") ; py::class_, std::shared_ptr>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", modelRatFunc) ; diff --git a/tests/storage/test_matrix.py b/tests/storage/test_matrix.py index 4ca2faf..53fdc91 100644 --- a/tests/storage/test_matrix.py +++ b/tests/storage/test_matrix.py @@ -14,6 +14,16 @@ class TestMatrix: for e in matrix: assert e.value() == 0.5 or e.value() == 0 or (e.value() == 1 and e.column > 6) + def test_backward_matrix(self): + model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) + matrix = model.backward_transition_matrix + assert type(matrix) is stormpy.storage.SparseMatrix + assert matrix.nr_rows == model.nr_states + assert matrix.nr_columns == model.nr_states + assert matrix.nr_entries == 20 #model.nr_transitions + for e in matrix: + assert e.value() == 0.5 or e.value() == 0 or (e.value() == 1 and e.column > 6) + def test_change_sparse_matrix(self): model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) matrix = model.transition_matrix @@ -58,7 +68,7 @@ class TestMatrix: assert math.isclose(resValue, 0.06923076923076932) # Change probabilities again - for state in stormpy.state.State(0, model): + for state in stormpy.state.State(0, model.transition_matrix): for action in state.actions(): for transition in action.transitions(): if transition.value() == 0.3: diff --git a/tests/storage/test_model_iterators.py b/tests/storage/test_model_iterators.py index 8023b86..1f80e97 100644 --- a/tests/storage/test_model_iterators.py +++ b/tests/storage/test_model_iterators.py @@ -4,33 +4,33 @@ from helpers.helper import get_example_path class TestModelIterators: def test_states_dtmc(self): model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) - s = stormpy.state.State(0, model) + s = stormpy.state.State(0, model.transition_matrix) i = 0 - for state in stormpy.state.State(0, model): + for state in stormpy.state.State(0, model.transition_matrix): assert state.id == i i += 1 assert i == model.nr_states def test_states_mdp(self): model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab")) - s = stormpy.state.State(0, model) + s = stormpy.state.State(0, model.transition_matrix) i = 0 - for state in stormpy.state.State(0, model): + for state in stormpy.state.State(0, model.transition_matrix): assert state.id == i i += 1 assert i == model.nr_states def test_actions_dtmc(self): model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) - s = stormpy.state.State(0, model) - for state in stormpy.state.State(0, model): + s = stormpy.state.State(0, model.transition_matrix) + for state in stormpy.state.State(0, model.transition_matrix): for action in state.actions(): assert action.row == 0 def test_actions_mdp(self): model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab")) - s = stormpy.state.State(0, model) - for state in stormpy.state.State(0, model): + s = stormpy.state.State(0, model.transition_matrix) + for state in stormpy.state.State(0, model.transition_matrix): for action in state.actions(): assert action.row == 0 or action.row == 1 @@ -42,9 +42,9 @@ class TestModelIterators: (9, 9, 1), (10, 10, 1), (11, 11, 1), (12, 12, 1) ] model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) - s = stormpy.state.State(0, model) + s = stormpy.state.State(0, model.transition_matrix) i = 0 - for state in stormpy.state.State(0, model): + for state in stormpy.state.State(0, model.transition_matrix): for action in state.actions(): for transition in action.transitions(): transition_orig = transitions_orig[i] @@ -55,8 +55,8 @@ class TestModelIterators: def test_transitions_mdp(self): model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab")) - s = stormpy.state.State(0, model) - for state in stormpy.state.State(0, model): + s = stormpy.state.State(0, model.transition_matrix) + for state in stormpy.state.State(0, model.transition_matrix): i = 0 for action in state.actions(): i += 1 @@ -73,7 +73,7 @@ class TestModelIterators: ] model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) i = 0 - for state in stormpy.state.State(0, model): + for state in stormpy.state.State(0, model.transition_matrix): for transition in model.transition_matrix.row_iter(state.id, state.id): transition_orig = transitions_orig[i] i += 1 From f646a70186daf0f0be0d1321396321c278ae9fff Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 10 Mar 2017 16:24:24 +0100 Subject: [PATCH 07/11] Added symred support --- src/dft/dft.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/dft/dft.cpp b/src/dft/dft.cpp index 4c2ca64..587d8c3 100644 --- a/src/dft/dft.cpp +++ b/src/dft/dft.cpp @@ -3,16 +3,21 @@ #include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h" #include "storm/settings/SettingsManager.h" #include "storm-dft/settings/modules/DFTSettings.h" +#include "storm-dft/storage/dft/DFTIsomorphism.h" // Thin wrapper for model building using one formula as argument template -std::shared_ptr> buildModelFromJsonDft(std::string const& jsonDft) { +std::shared_ptr> buildModelFromJsonDft(std::string const& jsonDft, bool symred) { // Build DFT storm::parser::DFTJsonParser parser; storm::storage::DFT dft = parser.parseJson(jsonDft); // Build model std::map>> emptySymmetry; storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry); + if (symred) { + auto colouring = dft.colourDFT(); + symmetries = dft.findSymmetries(colouring); + } storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, true); typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions({}, true); builder.buildModel(labeloptions, 0, 0.0); @@ -24,6 +29,6 @@ void define_dft(py::module& m) { storm::settings::addModule(); }, "Initialize Storm-dft"); // Build model - m.def("build_sparse_model_from_json_dft", &buildModelFromJsonDft, "Build the model", py::arg("jsonDft")); - m.def("build_sparse_parametric_model_from_json_dft", &buildModelFromJsonDft, "Build the parametric model", py::arg("jsonDft")); + m.def("build_sparse_model_from_json_dft", &buildModelFromJsonDft, "Build the model", py::arg("jsonDft"), py::arg("symred") = false); + m.def("build_sparse_parametric_model_from_json_dft", &buildModelFromJsonDft, "Build the parametric model", py::arg("jsonDft"), py::arg("symred") = false); } From ed2875eb7da17dd5e589eefcd28000b309673369 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 16 Mar 2017 13:41:33 +0100 Subject: [PATCH 08/11] Changed state and action for models --- lib/stormpy/storage/__init__.py | 1 - lib/stormpy/storage/action.py | 36 ------ lib/stormpy/storage/state.py | 34 ----- src/mod_storage.cpp | 2 + src/storage/matrix.cpp | 6 +- src/storage/model.cpp | 10 +- src/storage/state.cpp | 45 +++++++ src/storage/state.h | 122 ++++++++++++++++++ tests/storage/test_matrix.py | 6 +- ...{test_model_iterators.py => test_state.py} | 76 +++++++---- 10 files changed, 238 insertions(+), 100 deletions(-) delete mode 100644 lib/stormpy/storage/action.py delete mode 100644 lib/stormpy/storage/state.py create mode 100644 src/storage/state.cpp create mode 100644 src/storage/state.h rename tests/storage/{test_model_iterators.py => test_state.py} (59%) diff --git a/lib/stormpy/storage/__init__.py b/lib/stormpy/storage/__init__.py index 0d3e560..08aeb77 100644 --- a/lib/stormpy/storage/__init__.py +++ b/lib/stormpy/storage/__init__.py @@ -1,6 +1,5 @@ from . import storage from .storage import * -from . import state,action class ModelInstantiator: def __init__(self, model): diff --git a/lib/stormpy/storage/action.py b/lib/stormpy/storage/action.py deleted file mode 100644 index ad6f68e..0000000 --- a/lib/stormpy/storage/action.py +++ /dev/null @@ -1,36 +0,0 @@ -class Action: - """ Represents an action in the model """ - - def __init__(self, row_group_start, row_group_end, row, matrix): - """ Initialize - :param row_group_start: Start index of the row group in the matrix - :param row_group_end: End index of the row group in the matrix - :param row: Index of the corresponding row in the matrix - :param matrix: Corresponding matrix - """ - self.row_group_start = row_group_start - self.row_group_end = row_group_end - self.row = row - 1 - self.matrix = matrix - assert row >= -1 and row + row_group_start <= row_group_end - - def __iter__(self): - return self - - def __next__(self): - if self.row + self.row_group_start >= self.row_group_end - 1: - raise StopIteration - else: - self.row += 1 - return self - - def __str__(self): - return "{}".format(self.row) - - def transitions(self): - """ Get transitions associated with the action - :return List of tranistions - """ - row = self.row_group_start + self.row - #return self.model.transition_matrix().get_row(self.row_group_start + self.row) - return self.matrix.row_iter(row, row) diff --git a/lib/stormpy/storage/state.py b/lib/stormpy/storage/state.py deleted file mode 100644 index 613316e..0000000 --- a/lib/stormpy/storage/state.py +++ /dev/null @@ -1,34 +0,0 @@ -from . import action - -class State: - """ Represents a state in the matrix """ - - def __init__(self, id, matrix): - """ Initialize - :param id: Id of the state - :param matrix: Corresponding matrix - """ - self.id = id - 1 - self.matrix = matrix - - def __iter__(self): - return self - - def __next__(self): - if self.id >= self.matrix.nr_row_groups - 1: - raise StopIteration - else: - self.id += 1 - return self - - def __str__(self): - return "{}".format(self.id) - - def actions(self): - """ Get actions associated with the state - :return List of actions - """ - row_group_indices = self.matrix._row_group_indices - start = row_group_indices[self.id] - end = row_group_indices[self.id+1] - return action.Action(start, end, 0, self.matrix) diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 658043c..2755911 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -3,6 +3,7 @@ #include "storage/bitvector.h" #include "storage/model.h" #include "storage/matrix.h" +#include "storage/state.h" #include "storage/labeling.h" PYBIND11_PLUGIN(storage) { @@ -16,6 +17,7 @@ PYBIND11_PLUGIN(storage) { define_bitvector(m); define_model(m); define_sparse_matrix(m); + define_state(m); define_model_instantiator(m); define_labeling(m); return m.ptr(); diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp index 567cbdf..5073c42 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -15,7 +15,7 @@ void define_sparse_matrix(py::module& m) { stream << entry; return stream.str(); }) - //def_property threw "pointer being freed not allocated" after exiting + //Note: def_property threw "pointer being freed not allocated" after exiting .def("value", &storm::storage::MatrixEntry::getValue, "Value") .def("set_value", &storm::storage::MatrixEntry::setValue, py::arg("value"), "Set value") .def_property_readonly("column", &storm::storage::MatrixEntry::getColumn, "Column") @@ -27,7 +27,7 @@ void define_sparse_matrix(py::module& m) { stream << entry; return stream.str(); }) - //def_property threw "pointer being freed not allocated" after exiting + //Note: def_property threw "pointer being freed not allocated" after exiting .def("value", &storm::storage::MatrixEntry::getValue, "Value") .def("set_value", &storm::storage::MatrixEntry::setValue, py::arg("value"), "Set value") .def_property_readonly("column", &storm::storage::MatrixEntry::getColumn, "Column") @@ -61,7 +61,7 @@ void define_sparse_matrix(py::module& m) { stream << transition << ", "; } return stream.str(); - }, py::arg("row"), "Print row") + }, py::arg("row"), "Print rows from start to end") // Entry_index lead to problems .def("row_iter", [](storm::storage::SparseMatrix& matrix, row_index start, row_index end) { return py::make_iterator(matrix.begin(start), matrix.end(end)); diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 839ee4e..dc091e1 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -1,4 +1,6 @@ #include "model.h" +#include "state.h" + #include "storm/models/ModelBase.h" #include "storm/models/sparse/Model.h" #include "storm/models/sparse/Dtmc.h" @@ -78,6 +80,9 @@ void define_model(py::module& m) { .def_property_readonly("initial_states", &getInitialStates, "Initial states") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") .def_property_readonly("backward_transition_matrix", &getBackwardTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") + .def_property_readonly("states", [](storm::models::sparse::Model& model) { + return SparseModelStates(model); + }, "Get states") ; py::class_, std::shared_ptr>>(m, "SparseDtmc", "DTMC in sparse representation", model) ; @@ -90,12 +95,15 @@ void define_model(py::module& m) { 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") - .def("collect_reward_parameters", &rewardVariables, "Collect reward parameters") + .def("collect_reward_parameters", &rewardVariables, "Collect reward parameters") .def_property_readonly("labeling", &getLabeling, "Labels") .def("labels_state", &storm::models::sparse::Model::getLabelsOfState, py::arg("state"), "Get labels of state") .def_property_readonly("initial_states", &getInitialStates, "Initial states") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") .def_property_readonly("backward_transition_matrix", &getBackwardTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") + .def_property_readonly("states", [](storm::models::sparse::Model& model) { + return SparseModelStates(model); + }, "Get states") ; py::class_, std::shared_ptr>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", modelRatFunc) ; diff --git a/src/storage/state.cpp b/src/storage/state.cpp new file mode 100644 index 0000000..d3724c1 --- /dev/null +++ b/src/storage/state.cpp @@ -0,0 +1,45 @@ +#include "state.h" + +void define_state(py::module& m) { + + // SparseModelStates + py::class_>(m, "SparseModelStates", "States in sparse model") + .def("__getitem__", &SparseModelStates::getState) + ; + py::class_>(m, "SparseParametricModelStates", "States in sparse parametric model") + .def("__getitem__", &SparseModelStates::getState) + ; + // SparseModelState + py::class_>(m, "SparseModelState", "State in sparse model") + .def("__str__", &SparseModelState::toString) + .def_property_readonly("id", &SparseModelState::getIndex, "Id") + .def_property_readonly("labels", &SparseModelState::getLabels, "Labels") + .def_property_readonly("actions", &SparseModelState::getActions, "Get actions") + ; + py::class_>(m, "SparseParametricModelState", "State in sparse parametric model") + .def("__str__", &SparseModelState::toString) + .def_property_readonly("id", &SparseModelState::getIndex, "Id") + .def_property_readonly("labels", &SparseModelState::getLabels, "Labels") + .def_property_readonly("actions", &SparseModelState::getActions, "Get actions") + ; + + // SparseModelActions + py::class_>(m, "SparseModelActions", "Actions for state in sparse model") + .def("__getitem__", &SparseModelActions::getAction) + ; + py::class_>(m, "SparseParametricModelActions", "Actions for state in sparse parametric model") + .def("__getitem__", &SparseModelActions::getAction) + ; + // SparseModelAction + py::class_>(m, "SparseModelAction", "Action for state in sparse model") + .def("__str__", &SparseModelAction::toString) + .def_property_readonly("id", &SparseModelAction::getIndex, "Id") + .def_property_readonly("transitions", &SparseModelAction::getTransitions, "Get transitions") + ; + py::class_>(m, "SparseParametricModelAction", "Action for state in sparse parametric model") + .def("__str__", &SparseModelAction::toString) + .def_property_readonly("id", &SparseModelAction::getIndex, "Id") + .def_property_readonly("transitions", &SparseModelAction::getTransitions, "Get transitions") + ; + +} diff --git a/src/storage/state.h b/src/storage/state.h new file mode 100644 index 0000000..a2db40e --- /dev/null +++ b/src/storage/state.h @@ -0,0 +1,122 @@ +#ifndef PYTHON_STORAGE_STATE_H_ +#define PYTHON_STORAGE_STATE_H_ + +#include "common.h" + +#include "storm/storage/SparseMatrix.h" +#include "storm/models/sparse/Model.h" + +// Forward declaration +template +class SparseModelActions; + +// State definition +template +class SparseModelState { + using s_index = typename storm::storage::SparseMatrix::index_type; + + public: + SparseModelState(storm::models::sparse::Model& model, s_index stateIndex) : model(model), stateIndex(stateIndex) { + } + + s_index getIndex() const { + return this->stateIndex; + } + + std::set getLabels() { + return this->model.getStateLabeling().getLabelsOfState(this->stateIndex); + } + + SparseModelActions getActions() { + return SparseModelActions(this->model, stateIndex); + } + + std::string toString() { + std::stringstream stream; + stream << this->getIndex(); + return stream.str(); + } + + private: + s_index stateIndex; + storm::models::sparse::Model& model; +}; + +template +class SparseModelStates { + using s_index = typename storm::storage::SparseMatrix::index_type; + + public: + SparseModelStates(storm::models::sparse::Model& model) : model(model) { + length = model.getNumberOfStates(); + } + + SparseModelState getState(s_index index) { + if (index < length) { + return SparseModelState(model, index); + } else { + throw py::index_error(); + } + } + + private: + s_index length; + storm::models::sparse::Model& model; +}; + +// Action definition +template +class SparseModelAction { + using s_index = typename storm::storage::SparseMatrix::index_type; + + public: + SparseModelAction(storm::models::sparse::Model& model, s_index stateIndex, s_index actionIndex) : model(model), stateIndex(stateIndex), actionIndex(actionIndex) { + } + + s_index getIndex() const { + return this->actionIndex; + } + + typename storm::storage::SparseMatrix::rows getTransitions() { + return model.getTransitionMatrix().getRow(stateIndex, actionIndex); + } + + std::string toString() { + std::stringstream stream; + stream << this->getIndex(); + return stream.str(); + } + + + private: + s_index stateIndex; + s_index actionIndex; + storm::models::sparse::Model& model; +}; + +template +class SparseModelActions { + using s_index = typename storm::storage::SparseMatrix::index_type; + + public: + SparseModelActions(storm::models::sparse::Model& model, s_index stateIndex) : model(model), stateIndex(stateIndex) { + length = model.getTransitionMatrix().getRowGroupSize(stateIndex); + } + + SparseModelAction getAction(size_t index) { + if (index < length) { + return SparseModelAction(model, stateIndex, index); + } else { + throw py::index_error(); + } + } + + private: + s_index stateIndex; + s_index length; + storm::models::sparse::Model& model; +}; + +void define_state(py::module& m); + +#endif /* PYTHON_STORAGE_STATE_H_ */ diff --git a/tests/storage/test_matrix.py b/tests/storage/test_matrix.py index 53fdc91..8d9fb65 100644 --- a/tests/storage/test_matrix.py +++ b/tests/storage/test_matrix.py @@ -68,9 +68,9 @@ class TestMatrix: assert math.isclose(resValue, 0.06923076923076932) # Change probabilities again - for state in stormpy.state.State(0, model.transition_matrix): - for action in state.actions(): - for transition in action.transitions(): + for state in model.states: + for action in state.actions: + for transition in action.transitions: if transition.value() == 0.3: transition.set_value(0.8) elif transition.value() == 0.7: diff --git a/tests/storage/test_model_iterators.py b/tests/storage/test_state.py similarity index 59% rename from tests/storage/test_model_iterators.py rename to tests/storage/test_state.py index 1f80e97..add9dcd 100644 --- a/tests/storage/test_model_iterators.py +++ b/tests/storage/test_state.py @@ -1,38 +1,54 @@ import stormpy from helpers.helper import get_example_path -class TestModelIterators: +class TestState: def test_states_dtmc(self): model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) - s = stormpy.state.State(0, model.transition_matrix) i = 0 - for state in stormpy.state.State(0, model.transition_matrix): + states = model.states + for state in states: assert state.id == i i += 1 assert i == model.nr_states + state = model.states[2] + assert state.id == 2 + state = states[5] + assert state.id == 5 def test_states_mdp(self): model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab")) - s = stormpy.state.State(0, model.transition_matrix) i = 0 - for state in stormpy.state.State(0, model.transition_matrix): + for state in model.states: assert state.id == i i += 1 assert i == model.nr_states + states = model.states + state = model.states[6] + assert state.id == 6 + state = states[1] + assert state.id == 1 + + def test_labels_dtmc(self): + model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) + labelsOrig = [["init"], [], [], [], [], [], [], ["one", "done"], ["two", "done"], ["three", "done"], ["four", "done"], ["five", "done"], ["six", "done"]] + i = 0 + for state in model.states: + labels = state.labels + for label in labelsOrig[i]: + assert label in labels + i += 1 def test_actions_dtmc(self): model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) - s = stormpy.state.State(0, model.transition_matrix) - for state in stormpy.state.State(0, model.transition_matrix): - for action in state.actions(): - assert action.row == 0 + for state in model.states: + for action in state.actions: + assert action.id == 0 def test_actions_mdp(self): model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab")) - s = stormpy.state.State(0, model.transition_matrix) - for state in stormpy.state.State(0, model.transition_matrix): - for action in state.actions(): - assert action.row == 0 or action.row == 1 + for state in model.states: + for action in state.actions: + assert action.id == 0 or action.id == 1 def test_transitions_dtmc(self): transitions_orig = [(0, 0, 0), (0, 1, 0.5), (0, 2, 0.5), (1, 1, 0), (1, 3, 0.5), (1, 4, 0.5), @@ -42,11 +58,10 @@ class TestModelIterators: (9, 9, 1), (10, 10, 1), (11, 11, 1), (12, 12, 1) ] model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) - s = stormpy.state.State(0, model.transition_matrix) i = 0 - for state in stormpy.state.State(0, model.transition_matrix): - for action in state.actions(): - for transition in action.transitions(): + for state in model.states: + for action in state.actions: + for transition in action.transitions: transition_orig = transitions_orig[i] i += 1 assert state.id == transition_orig[0] @@ -55,12 +70,12 @@ class TestModelIterators: def test_transitions_mdp(self): model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab")) - s = stormpy.state.State(0, model.transition_matrix) - for state in stormpy.state.State(0, model.transition_matrix): + assert model.states[1].id == 1 + for state in model.states: i = 0 - for action in state.actions(): + for action in state.actions: i += 1 - for transition in action.transitions(): + for transition in action.transitions: assert transition.value() == 0.5 or transition.value() == 1 assert i == 1 or i == 2 @@ -73,10 +88,27 @@ class TestModelIterators: ] model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) i = 0 - for state in stormpy.state.State(0, model.transition_matrix): + for state in model.states: for transition in model.transition_matrix.row_iter(state.id, state.id): transition_orig = transitions_orig[i] i += 1 assert state.id == transition_orig[0] assert transition.column == transition_orig[1] assert transition.value() == transition_orig[2] + + def test_parametric_transitions(self): + import pycarl + program = stormpy.parse_prism_program(get_example_path("pmdp", "two_dice.nm")) + model = stormpy.build_parametric_model(program) + assert model.states[1].id == 1 + one = pycarl.FactorizedPolynomial(pycarl.Rational(1)) + i = 0 + for state in model.states: + assert state.id == i + i += 1 + j = 0 + for action in state.actions: + assert j == 0 or j == 1 + j += 1 + for transition in action.transitions: + assert transition.value().denominator == one From 9618b5ca31a7f91c50aaa9a3caebe05f437c27ce Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 16 Mar 2017 14:16:55 +0100 Subject: [PATCH 09/11] Length for states and actions --- src/storage/matrix.cpp | 2 ++ src/storage/state.cpp | 4 ++++ src/storage/state.h | 26 +++++++++++++++++--------- tests/storage/test_state.py | 5 +++++ 4 files changed, 28 insertions(+), 9 deletions(-) diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp index 5073c42..b5a8554 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -107,6 +107,7 @@ void define_sparse_matrix(py::module& m) { .def("__iter__", [](storm::storage::SparseMatrix::rows& rows) { return py::make_iterator(rows.begin(), rows.end()); }, py::keep_alive<0, 1>()) + .def("__len__", &storm::storage::SparseMatrix::rows::getNumberOfEntries) .def("__str__", [](storm::storage::SparseMatrix::const_rows& rows) { std::stringstream stream; for (auto transition : rows) { @@ -120,6 +121,7 @@ void define_sparse_matrix(py::module& m) { .def("__iter__", [](storm::storage::SparseMatrix::rows& rows) { return py::make_iterator(rows.begin(), rows.end()); }, py::keep_alive<0, 1>()) + .def("__len__", &storm::storage::SparseMatrix::rows::getNumberOfEntries) .def("__str__", [](storm::storage::SparseMatrix::const_rows& rows) { std::stringstream stream; for (auto transition : rows) { diff --git a/src/storage/state.cpp b/src/storage/state.cpp index d3724c1..fadd676 100644 --- a/src/storage/state.cpp +++ b/src/storage/state.cpp @@ -5,9 +5,11 @@ void define_state(py::module& m) { // SparseModelStates py::class_>(m, "SparseModelStates", "States in sparse model") .def("__getitem__", &SparseModelStates::getState) + .def("__len__", &SparseModelStates::getSize) ; py::class_>(m, "SparseParametricModelStates", "States in sparse parametric model") .def("__getitem__", &SparseModelStates::getState) + .def("__len__", &SparseModelStates::getSize) ; // SparseModelState py::class_>(m, "SparseModelState", "State in sparse model") @@ -26,9 +28,11 @@ void define_state(py::module& m) { // SparseModelActions py::class_>(m, "SparseModelActions", "Actions for state in sparse model") .def("__getitem__", &SparseModelActions::getAction) + .def("__len__", &SparseModelActions::getSize) ; py::class_>(m, "SparseParametricModelActions", "Actions for state in sparse parametric model") .def("__getitem__", &SparseModelActions::getAction) + .def("__len__", &SparseModelActions::getSize) ; // SparseModelAction py::class_>(m, "SparseModelAction", "Action for state in sparse model") diff --git a/src/storage/state.h b/src/storage/state.h index a2db40e..0e91a11 100644 --- a/src/storage/state.h +++ b/src/storage/state.h @@ -20,20 +20,20 @@ class SparseModelState { } s_index getIndex() const { - return this->stateIndex; + return stateIndex; } - std::set getLabels() { + std::set getLabels() const { return this->model.getStateLabeling().getLabelsOfState(this->stateIndex); } - SparseModelActions getActions() { + SparseModelActions getActions() const { return SparseModelActions(this->model, stateIndex); } - std::string toString() { + std::string toString() const { std::stringstream stream; - stream << this->getIndex(); + stream << stateIndex; return stream.str(); } @@ -51,7 +51,11 @@ class SparseModelStates { length = model.getNumberOfStates(); } - SparseModelState getState(s_index index) { + s_index getSize() const { + return length; + } + + SparseModelState getState(s_index index) const { if (index < length) { return SparseModelState(model, index); } else { @@ -81,9 +85,9 @@ class SparseModelAction { return model.getTransitionMatrix().getRow(stateIndex, actionIndex); } - std::string toString() { + std::string toString() const { std::stringstream stream; - stream << this->getIndex(); + stream << actionIndex; return stream.str(); } @@ -103,7 +107,11 @@ class SparseModelActions { length = model.getTransitionMatrix().getRowGroupSize(stateIndex); } - SparseModelAction getAction(size_t index) { + s_index getSize() const { + return length; + } + + SparseModelAction getAction(size_t index) const { if (index < length) { return SparseModelAction(model, stateIndex, index); } else { diff --git a/tests/storage/test_state.py b/tests/storage/test_state.py index add9dcd..a46c620 100644 --- a/tests/storage/test_state.py +++ b/tests/storage/test_state.py @@ -6,6 +6,7 @@ class TestState: model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) i = 0 states = model.states + assert len(states) == 13 for state in states: assert state.id == i i += 1 @@ -18,6 +19,7 @@ class TestState: def test_states_mdp(self): model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab")) i = 0 + assert len(model.states) == 169 for state in model.states: assert state.id == i i += 1 @@ -41,12 +43,14 @@ class TestState: def test_actions_dtmc(self): model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) for state in model.states: + assert len(state.actions) == 1 for action in state.actions: assert action.id == 0 def test_actions_mdp(self): model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab")) for state in model.states: + assert len(state.actions) == 1 or len(state.actions) == 2 for action in state.actions: assert action.id == 0 or action.id == 1 @@ -61,6 +65,7 @@ class TestState: i = 0 for state in model.states: for action in state.actions: + assert (state.id < 7 and len(action.transitions) == 3) or (state.id >= 7 and len(action.transitions) == 1) for transition in action.transitions: transition_orig = transitions_orig[i] i += 1 From 968901cca5ca87607220923699f601562c5b1e56 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 16 Mar 2017 14:36:06 +0100 Subject: [PATCH 10/11] Change test for merged failed states --- tests/dft/test_build.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/dft/test_build.py b/tests/dft/test_build.py index 059b027..df32062 100644 --- a/tests/dft/test_build.py +++ b/tests/dft/test_build.py @@ -13,7 +13,7 @@ class TestBuild: assert model.nr_transitions == 5 assert len(model.initial_states) == 1 initial_state = model.initial_states[0] - assert initial_state == 0 + assert initial_state == 1 result = stormpy.model_checking(model, formulas[0]) assert math.isclose(result.at(initial_state), 3) From 20b1b01139b177057bbef32d202827df566fdd2c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 28 Mar 2017 14:01:29 +0200 Subject: [PATCH 11/11] Bisimulation takes properties --- lib/stormpy/__init__.py | 7 ++++--- src/core/bisimulation.cpp | 8 ++++---- tests/core/test_bisimulation.py | 17 +++++++++++++++-- 3 files changed, 23 insertions(+), 9 deletions(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 7893c6f..7337b65 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -94,11 +94,12 @@ def build_parametric_model_from_drn(file): else: raise RuntimeError("Not supported parametric model constructed") -def perform_bisimulation(model, property, bisimulation_type): +def perform_bisimulation(model, properties, bisimulation_type): + formulae = [prop.raw_formula for prop in properties] if model.supports_parameters: - return core._perform_parametric_bisimulation(model, property.raw_formula, bisimulation_type) + return core._perform_parametric_bisimulation(model, formulae, bisimulation_type) else: - return core._perform_bisimulation(model, property.raw_formula, bisimulation_type) + return core._perform_bisimulation(model, formulae, bisimulation_type) def model_checking(model, property): if model.supports_parameters: diff --git a/src/core/bisimulation.cpp b/src/core/bisimulation.cpp index 3eafc80..cdd3bf0 100644 --- a/src/core/bisimulation.cpp +++ b/src/core/bisimulation.cpp @@ -2,16 +2,16 @@ // Thin wrapper for bisimulation template -std::shared_ptr> performBisimulation(std::shared_ptr> const& model, std::shared_ptr const& formula, storm::storage::BisimulationType bisimulationType) { - return storm::performBisimulationMinimization>(model, formula, bisimulationType); +std::shared_ptr> performBisimulation(std::shared_ptr> const& model, std::vector> const& formulas, storm::storage::BisimulationType bisimulationType) { + return storm::performBisimulationMinimization>(model, formulas, bisimulationType); } // Define python bindings void define_bisimulation(py::module& m) { // Bisimulation - m.def("_perform_bisimulation", &performBisimulation, "Perform bisimulation", py::arg("model"), py::arg("formula"), py::arg("bisimulation_type")); - m.def("_perform_parametric_bisimulation", &performBisimulation, "Perform bisimulation on parametric model", py::arg("model"), py::arg("formula"), py::arg("bisimulation_type")); + m.def("_perform_bisimulation", &performBisimulation, "Perform bisimulation", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type")); + m.def("_perform_parametric_bisimulation", &performBisimulation, "Perform bisimulation on parametric model", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type")); // BisimulationType py::enum_(m, "BisimulationType", "Types of bisimulation") diff --git a/tests/core/test_bisimulation.py b/tests/core/test_bisimulation.py index ae69462..bb69111 100644 --- a/tests/core/test_bisimulation.py +++ b/tests/core/test_bisimulation.py @@ -2,6 +2,8 @@ import stormpy import stormpy.logic from helpers.helper import get_example_path +import math + class TestBisimulation: def test_bisimulation(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds5_5.pm")) @@ -14,13 +16,21 @@ class TestBisimulation: assert model.nr_transitions == 13041 assert model.model_type == stormpy.ModelType.DTMC assert not model.supports_parameters - model_bisim = stormpy.perform_bisimulation(model, properties[0], stormpy.BisimulationType.STRONG) + initial_state = model.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(model, properties[0]) + model_bisim = stormpy.perform_bisimulation(model, properties, stormpy.BisimulationType.STRONG) assert model_bisim.nr_states == 64 assert model_bisim.nr_transitions == 104 assert model_bisim.model_type == stormpy.ModelType.DTMC assert not model_bisim.supports_parameters + result_bisim = stormpy.model_checking(model_bisim, properties[0]) + initial_state_bisim = model_bisim.initial_states[0] + assert initial_state_bisim == 34 + assert math.isclose(result.at(initial_state), result_bisim.at(initial_state_bisim), rel_tol=1e-4) def test_parametric_bisimulation(self): + import pycarl program = stormpy.parse_prism_program(get_example_path("pdtmc", "crowds3_5.pm")) assert program.nr_modules == 1 assert program.model_type == stormpy.PrismModelType.DTMC @@ -32,8 +42,11 @@ class TestBisimulation: assert model.nr_transitions == 2027 assert model.model_type == stormpy.ModelType.DTMC assert model.has_parameters - model_bisim = stormpy.perform_bisimulation(model, properties[0], stormpy.BisimulationType.STRONG) + result = stormpy.model_checking(model, properties[0]) + model_bisim = stormpy.perform_bisimulation(model, properties, stormpy.BisimulationType.STRONG) assert model_bisim.nr_states == 80 assert model_bisim.nr_transitions == 120 assert model_bisim.model_type == stormpy.ModelType.DTMC assert model_bisim.has_parameters + result_bisim = stormpy.model_checking(model_bisim, properties[0]) + assert result.result_function == result_bisim.result_function