diff --git a/CMakeLists.txt b/CMakeLists.txt index a1ac635..9cb25c7 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -24,7 +24,7 @@ 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}) - + if(ARGC GREATER 2) # Additional libraries target_include_directories(${NAME} PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${storm_INCLUDE_DIR} ${ARGV3} ${CMAKE_CURRENT_BINARY_DIR}/src/generated) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index b71c36b..c18038a 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -13,10 +13,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] @@ -34,9 +36,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] @@ -51,12 +56,54 @@ 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): +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): 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/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/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/lib/stormpy/storage/__init__.py b/lib/stormpy/storage/__init__.py index 550dbc5..08aeb77 100644 --- a/lib/stormpy/storage/__init__.py +++ b/lib/stormpy/storage/__init__.py @@ -1,7 +1,5 @@ from . import storage from .storage import * -from . import state, action - class ModelInstantiator: def __init__(self, model): @@ -9,8 +7,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/lib/stormpy/storage/action.py b/lib/stormpy/storage/action.py deleted file mode 100644 index 420f5b3..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, model): - """ 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 - """ - self.row_group_start = row_group_start - self.row_group_end = row_group_end - self.row = row - 1 - self.model = model - 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.model.transition_matrix.row_iter(row, row) diff --git a/lib/stormpy/storage/state.py b/lib/stormpy/storage/state.py deleted file mode 100644 index 40b2806..0000000 --- a/lib/stormpy/storage/state.py +++ /dev/null @@ -1,35 +0,0 @@ -from . import action - - -class State: - """ Represents a state in the model """ - - def __init__(self, id, model): - """ Initialize - :param id: Id of the state - :param model: Corresponding model - """ - self.id = id - 1 - self.model = model - - def __iter__(self): - return self - - def __next__(self): - if self.id >= self.model.nr_states - 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.model.transition_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) diff --git a/setup.py b/setup.py index 12694be..a3e2363 100755 --- a/setup.py +++ b/setup.py @@ -106,7 +106,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=''), @@ -114,7 +114,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={'build_ext': CMakeBuild, 'test': PyTest}, zip_safe=False, 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/src/core/core.cpp b/src/core/core.cpp index a191403..0458165 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( @@ -57,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/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..587d8c3 --- /dev/null +++ b/src/dft/dft.cpp @@ -0,0 +1,34 @@ +#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" +#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, 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); + 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"), 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); +} 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/src/mod_storage.cpp b/src/mod_storage.cpp index 003646b..2755911 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -3,6 +3,8 @@ #include "storage/bitvector.h" #include "storage/model.h" #include "storage/matrix.h" +#include "storage/state.h" +#include "storage/labeling.h" PYBIND11_PLUGIN(storage) { py::module m("storage"); @@ -15,6 +17,8 @@ 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/bitvector.cpp b/src/storage/bitvector.cpp index 130b3dc..7c99036 100644 --- a/src/storage/bitvector.cpp +++ b/src/storage/bitvector.cpp @@ -15,7 +15,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("__len__", [](BitVector const& b) { return b.size(); }) .def("__getitem__", [](BitVector const& b, uint_fast64_t i) { 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/matrix.cpp b/src/storage/matrix.cpp index 9152157..9b6e3e0 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -18,7 +18,7 @@ void define_sparse_matrix(py::module& m) { .def("set_value", &MatrixEntry::setValue, py::arg("value"), "Set value") .def_property_readonly("column", &MatrixEntry::getColumn, "Column") ; - + py::class_>(m, "ParametricSparseMatrixEntry", "Entry of parametric sparse matrix") .def("__str__", &streamToString>) //def_property threw "pointer being freed not allocated" after exiting @@ -51,7 +51,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", [](SparseMatrix& matrix, row_index start, row_index end) { return py::make_iterator(matrix.begin(start), matrix.end(end)); @@ -126,6 +126,7 @@ void define_sparse_matrix(py::module& m) { return py::make_iterator(rows.begin(), rows.end()); }, py::keep_alive<0, 1>()) .def("__str__", &containerToString::rows>) + .def("__len__", &storm::storage::SparseMatrix::rows::getNumberOfEntries) ; py::class_::rows>(m, "ParametricSparseMatrixRows", "Set of rows in a parametric sparse matrix") @@ -133,5 +134,6 @@ void define_sparse_matrix(py::module& m) { return py::make_iterator(rows.begin(), rows.end()); }, py::keep_alive<0, 1>()) .def("__str__", &containerToString::rows>) + .def("__len__", &storm::storage::SparseMatrix::rows::getNumberOfEntries) ; } diff --git a/src/storage/model.cpp b/src/storage/model.cpp index eada29d..e37c38e 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" @@ -18,6 +20,8 @@ using RationalFunctionVariable = storm::RationalFunctionVariable; template using Model = storm::models::sparse::Model; template using Dtmc = storm::models::sparse::Dtmc; template using Mdp = storm::models::sparse::Mdp; +template using Ctmc = storm::models::sparse::Ctmc; +template using MarkovAutomaton = storm::models::sparse::MarkovAutomaton; template using SparseMatrix = storm::storage::SparseMatrix; // Thin wrapper for getting initial states @@ -36,6 +40,11 @@ SparseMatrix& getTransitionMatrix(Model& model) { return model.getTransitionMatrix(); } +template +storm::storage::SparseMatrix getBackwardTransitionMatrix(storm::models::sparse::Model& model) { + return model.getBackwardTransitions(); +} + // requires pycarl.Variable std::set probabilityVariables(Model const& model) { return storm::models::sparse::getProbabilityParameters(model); @@ -63,6 +72,11 @@ std::function const&)> getModelInfoPrinter(std::st }; } +template +storm::models::sparse::StateLabeling& getLabeling(storm::models::sparse::Model& model) { + return model.getStateLabeling(); +} + // Define python bindings void define_model(py::module& m) { @@ -86,18 +100,22 @@ void define_model(py::module& m) { .def("_as_pdtmc", &ModelBase::as>, "Get model as pDTMC") .def("_as_mdp", &ModelBase::as>, "Get model as MDP") .def("_as_pmdp", &ModelBase::as>, "Get model as pMDP") + .def("_as_ctmc", &ModelBase::as>, "Get model as CTMC") + .def("_as_pctmc", &ModelBase::as>, "Get model as pCTMC") + .def("_as_ma", &ModelBase::as>, "Get model as MA") + .def("_as_pma", &ModelBase::as>, "Get model as pMA") ; // Models -//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", [](Model& model) { - return model.getStateLabeling().getLabels(); - }, "Labels") + model.def_property_readonly("labeling", &getLabeling, "Labels") .def("labels_state", &Model::getLabelsOfState, py::arg("state"), "Get labels of state") .def_property_readonly("initial_states", &getInitialStates, "Initial states") + .def_property_readonly("states", [](Model& model) { + return SparseModelStates(model); + }, "Get 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("__str__", getModelInfoPrinter()) ; py::class_, std::shared_ptr>>(m, "SparseDtmc", "DTMC in sparse representation", model) @@ -106,25 +124,39 @@ void define_model(py::module& m) { py::class_, std::shared_ptr>>(m, "SparseMdp", "MDP in sparse representation", model) .def("__str__", getModelInfoPrinter("MDP")) ; + 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") .def("collect_reward_parameters", &rewardVariables, "Collect reward parameters") - .def_property_readonly("labels", [](Model& model) { - return model.getStateLabeling().getLabels(); - }, "Labels") + .def_property_readonly("labeling", &getLabeling, "Labels") .def("labels_state", &Model::getLabelsOfState, py::arg("state"), "Get labels of state") .def_property_readonly("initial_states", &getInitialStates, "Initial states") + .def_property_readonly("states", [](Model& model) { + return SparseModelStates(model); + }, "Get 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("__str__", getModelInfoPrinter("ParametricModel")) ; + py::class_, std::shared_ptr>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", modelRatFunc) .def("__str__", getModelInfoPrinter("ParametricDTMC")) ; + py::class_, std::shared_ptr>>(m, "SparseParametricMdp", "pMDP in sparse representation", modelRatFunc) .def("__str__", getModelInfoPrinter("ParametricMDP")) ; + py::class_, std::shared_ptr>>(m, "SparseParametricCtmc", "pCTMC in sparse representation", modelRatFunc) + ; + + py::class_, std::shared_ptr>>(m, "SparseParametricMA", "pMA in sparse representation", modelRatFunc) + ; + } // Model instantiator @@ -138,4 +170,12 @@ void define_model_instantiator(py::module& m) { .def(py::init>(), "parametric model"_a) .def("instantiate", &storm::utility::ModelInstantiator, Mdp>::instantiate, "Instantiate model with given parameter values") ; + + py::class_,Ctmc>>(m, "PctmcInstantiator", "Instantiate PCTMCs to CTMCs") + .def(py::init>(), "parametric model"_a) + .def("instantiate", &storm::utility::ModelInstantiator, Ctmc>::instantiate, "Instantiate model with given parameter values"); + + py::class_,MarkovAutomaton>>(m, "PmaInstantiator", "Instantiate PMAs to MAs") + .def(py::init>(), "parametric model"_a) + .def("instantiate", &storm::utility::ModelInstantiator, MarkovAutomaton>::instantiate, "Instantiate model with given parameter values"); } diff --git a/src/storage/state.cpp b/src/storage/state.cpp new file mode 100644 index 0000000..fadd676 --- /dev/null +++ b/src/storage/state.cpp @@ -0,0 +1,49 @@ +#include "state.h" + +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") + .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) + .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") + .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..0e91a11 --- /dev/null +++ b/src/storage/state.h @@ -0,0 +1,130 @@ +#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 stateIndex; + } + + std::set getLabels() const { + return this->model.getStateLabeling().getLabelsOfState(this->stateIndex); + } + + SparseModelActions getActions() const { + return SparseModelActions(this->model, stateIndex); + } + + std::string toString() const { + std::stringstream stream; + stream << stateIndex; + 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(); + } + + s_index getSize() const { + return length; + } + + SparseModelState getState(s_index index) const { + 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() const { + std::stringstream stream; + stream << actionIndex; + 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); + } + + s_index getSize() const { + return length; + } + + SparseModelAction getAction(size_t index) const { + 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/core/test_bisimulation.py b/tests/core/test_bisimulation.py index 539e87a..49ef8ec 100644 --- a/tests/core/test_bisimulation.py +++ b/tests/core/test_bisimulation.py @@ -3,6 +3,8 @@ import stormpy.logic from helpers.helper import get_example_path import math +import math + class TestBisimulation: def test_bisimulation(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds5_5.pm")) @@ -19,7 +21,7 @@ class TestBisimulation: initial_state = model.initial_states[0] assert initial_state == 0 result = stormpy.model_checking(model, properties[0]) - model_bisim = stormpy.perform_bisimulation(model, properties[0], stormpy.BisimulationType.STRONG) + 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 @@ -28,8 +30,9 @@ class TestBisimulation: 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 @@ -42,9 +45,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 diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 0777e3d..b9f7f28 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -76,3 +76,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 139d145..b0332bf 100644 --- a/tests/core/test_parse.py +++ b/tests/core/test_parse.py @@ -37,3 +37,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 + diff --git a/tests/dft/test_build.py b/tests/dft/test_build.py new file mode 100644 index 0000000..df32062 --- /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 == 1 + result = stormpy.model_checking(model, formulas[0]) + assert math.isclose(result.at(initial_state), 3) + 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_matrix.py b/tests/storage/test_matrix.py index 3b9c610..d29b04b 100644 --- a/tests/storage/test_matrix.py +++ b/tests/storage/test_matrix.py @@ -15,6 +15,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 @@ -59,9 +69,9 @@ class TestMatrix: assert math.isclose(resValue, 0.06923076923076932) # Change probabilities again - for state in stormpy.state.State(0, model): - 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.py b/tests/storage/test_model.py index 21dbb63..3d6b838 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -68,17 +68,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) @@ -86,18 +75,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 diff --git a/tests/storage/test_model_iterators.py b/tests/storage/test_state.py similarity index 56% rename from tests/storage/test_model_iterators.py rename to tests/storage/test_state.py index 2a97d50..55a7ec9 100644 --- a/tests/storage/test_model_iterators.py +++ b/tests/storage/test_state.py @@ -1,40 +1,59 @@ 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) i = 0 - for state in stormpy.state.State(0, model): + states = model.states + assert len(states) == 13 + 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) i = 0 - for state in stormpy.state.State(0, model): + assert len(model.states) == 169 + 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) - for state in stormpy.state.State(0, model): - for action in state.actions(): - assert action.row == 0 - + 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")) - s = stormpy.state.State(0, model) - for state in stormpy.state.State(0, model): - for action in state.actions(): - assert action.row == 0 or action.row == 1 - + 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 + 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), (2, 2, 0), (2, 5, 0.5), (2, 6, 0.5), (3, 1, 0.5), (3, 3, 0), (3, 7, 0.5), @@ -43,25 +62,25 @@ 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) i = 0 - for state in stormpy.state.State(0, model): - for action in state.actions(): - for transition in action.transitions(): + 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 assert state.id == transition_orig[0] assert transition.column == transition_orig[1] assert transition.value() == transition_orig[2] - + 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): + 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 @@ -74,10 +93,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): + 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