Merge from dft_bindings

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)

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):

lib/stormpy/dft/__init__.py

@@ -0,0 +1,4 @@
+from . import dft
+from .dft import *
+
+dft._set_up()

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

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"
+        }
+    ]
+}

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)
+        return self._instantiator.instantiate(point)

lib/stormpy/storage/action.py

@@ -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)

lib/stormpy/storage/state.py

@@ -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)

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,

src/core/bisimulation.cpp

@@ -2,16 +2,16 @@
 
 // Thin wrapper for bisimulation
 template<typename ValueType>
-std::shared_ptr<storm::models::sparse::Model<ValueType>> performBisimulation(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::shared_ptr<storm::logic::Formula const> const& formula, storm::storage::BisimulationType bisimulationType) {
-    return storm::performBisimulationMinimization<storm::models::sparse::Model<ValueType>>(model, formula, bisimulationType);
+std::shared_ptr<storm::models::sparse::Model<ValueType>> performBisimulation(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType bisimulationType) {
+    return storm::performBisimulationMinimization<storm::models::sparse::Model<ValueType>>(model, formulas, bisimulationType);
 }
 
 // Define python bindings
 void define_bisimulation(py::module& m) {
 
     // Bisimulation
-    m.def("_perform_bisimulation", &performBisimulation<double>, "Perform bisimulation", py::arg("model"), py::arg("formula"), py::arg("bisimulation_type"));
-    m.def("_perform_parametric_bisimulation", &performBisimulation<storm::RationalFunction>, "Perform bisimulation on parametric model", py::arg("model"), py::arg("formula"), py::arg("bisimulation_type"));
+    m.def("_perform_bisimulation", &performBisimulation<double>, "Perform bisimulation", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"));
+    m.def("_perform_parametric_bisimulation", &performBisimulation<storm::RationalFunction>, "Perform bisimulation on parametric model", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"));
 
     // BisimulationType 
     py::enum_<storm::storage::BisimulationType>(m, "BisimulationType", "Types of bisimulation")

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<double>, "Build the model", py::arg("program"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
     m.def("_build_sparse_parametric_model_from_prism_program", &storm::buildSparseModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formulas"));
+    m.def("_build_sparse_model_from_drn", &storm::buildExplicitDRNModel<double>, "Build the model from DRN", py::arg("file"));
+    m.def("_build_sparse_parametric_model_from_drn", &storm::buildExplicitDRNModel<storm::RationalFunction>, "Build the parametric model from DRN", py::arg("file"));
     
 }

src/dft/common.h

@@ -0,0 +1 @@
+#include "src/common.h"

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<typename ValueType>
+std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModelFromJsonDft(std::string const& jsonDft, bool symred) {
+    // Build DFT
+    storm::parser::DFTJsonParser<ValueType> parser;
+    storm::storage::DFT<ValueType> dft = parser.parseJson(jsonDft);
+    // Build model
+    std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
+    storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
+    if (symred) {
+        auto colouring = dft.colourDFT();
+        symmetries = dft.findSymmetries(colouring);
+    }
+    storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, true);
+    typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::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<storm::settings::modules::DFTSettings>();
+        }, "Initialize Storm-dft");
+    // Build model
+    m.def("build_sparse_model_from_json_dft", &buildModelFromJsonDft<double>, "Build the model", py::arg("jsonDft"), py::arg("symred") = false);
+    m.def("build_sparse_parametric_model_from_json_dft", &buildModelFromJsonDft<storm::RationalFunction>, "Build the parametric model", py::arg("jsonDft"), py::arg("symred") = false);
+}

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_ */

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();
+}

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();
 }

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) {

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_<storm::models::sparse::StateLabeling, std::shared_ptr<storm::models::sparse::StateLabeling>>(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();
+            })
+    ;
+
+}

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_ */

src/storage/matrix.cpp

@@ -18,7 +18,7 @@ void define_sparse_matrix(py::module& m) {
         .def("set_value", &MatrixEntry<double>::setValue, py::arg("value"), "Set value")
         .def_property_readonly("column", &MatrixEntry<double>::getColumn, "Column")
     ;
- 
+
     py::class_<MatrixEntry<RationalFunction>>(m, "ParametricSparseMatrixEntry", "Entry of parametric sparse matrix")
         .def("__str__", &streamToString<MatrixEntry<RationalFunction>>)
         //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<double>& 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<SparseMatrix<double>::rows>)
+        .def("__len__", &storm::storage::SparseMatrix<double>::rows::getNumberOfEntries)
     ;
 
     py::class_<SparseMatrix<RationalFunction>::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<SparseMatrix<RationalFunction>::rows>)
+        .def("__len__", &storm::storage::SparseMatrix<storm::RationalFunction>::rows::getNumberOfEntries)
     ;
 }

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<typename ValueType> using Model = storm::models::sparse::Model<ValueType>;
 template<typename ValueType> using Dtmc = storm::models::sparse::Dtmc<ValueType>;
 template<typename ValueType> using Mdp = storm::models::sparse::Mdp<ValueType>;
+template<typename ValueType> using Ctmc = storm::models::sparse::Ctmc<ValueType>;
+template<typename ValueType> using MarkovAutomaton = storm::models::sparse::MarkovAutomaton<ValueType>;
 template<typename ValueType> using SparseMatrix = storm::storage::SparseMatrix<ValueType>;
 
 // Thin wrapper for getting initial states
@@ -36,6 +40,11 @@ SparseMatrix<ValueType>& getTransitionMatrix(Model<ValueType>& model) {
     return model.getTransitionMatrix();
 }
 
+template<typename ValueType>
+storm::storage::SparseMatrix<ValueType> getBackwardTransitionMatrix(storm::models::sparse::Model<ValueType>& model) {
+    return model.getBackwardTransitions();
+}
+
 // requires pycarl.Variable
 std::set<RationalFunctionVariable> probabilityVariables(Model<RationalFunction> const& model) {
     return storm::models::sparse::getProbabilityParameters(model);
@@ -63,6 +72,11 @@ std::function<std::string (Model<ValueType> const&)> getModelInfoPrinter(std::st
     };
 }
 
+template<typename ValueType>
+storm::models::sparse::StateLabeling& getLabeling(storm::models::sparse::Model<ValueType>& 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<Dtmc<RationalFunction>>, "Get model as pDTMC")
         .def("_as_mdp", &ModelBase::as<Mdp<double>>, "Get model as MDP")
         .def("_as_pmdp", &ModelBase::as<Mdp<RationalFunction>>, "Get model as pMDP")
+        .def("_as_ctmc", &ModelBase::as<Ctmc<double>>, "Get model as CTMC")
+        .def("_as_pctmc", &ModelBase::as<Ctmc<storm::RationalFunction>>, "Get model as pCTMC")
+        .def("_as_ma", &ModelBase::as<MarkovAutomaton<double>>, "Get model as MA")
+        .def("_as_pma", &ModelBase::as<MarkovAutomaton<storm::RationalFunction>>, "Get model as pMA")
     ;
 
     // Models
-//storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >
-
     py::class_<Model<double>, std::shared_ptr<Model<double>>> 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<double>& model) {
-            return model.getStateLabeling().getLabels();
-        }, "Labels")
+    model.def_property_readonly("labeling", &getLabeling<double>, "Labels")
         .def("labels_state", &Model<double>::getLabelsOfState, py::arg("state"), "Get labels of state")
         .def_property_readonly("initial_states", &getInitialStates<double>, "Initial states")
+        .def_property_readonly("states", [](Model<double>& model) {
+                return SparseModelStates<double>(model);
+            }, "Get states")
         .def_property_readonly("transition_matrix", &getTransitionMatrix<double>, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix")
+        .def_property_readonly("backward_transition_matrix", &getBackwardTransitionMatrix<double>, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix")
         .def("__str__", getModelInfoPrinter<double>())
     ;
     py::class_<Dtmc<double>, std::shared_ptr<Dtmc<double>>>(m, "SparseDtmc", "DTMC in sparse representation", model)
@@ -106,25 +124,39 @@ void define_model(py::module& m) {
     py::class_<Mdp<double>, std::shared_ptr<Mdp<double>>>(m, "SparseMdp", "MDP in sparse representation", model)
         .def("__str__", getModelInfoPrinter<double>("MDP"))
     ;
+    py::class_<storm::models::sparse::Ctmc<double>, std::shared_ptr<storm::models::sparse::Ctmc<double>>>(m, "SparseCtmc", "CTMC in sparse representation", model)
+    ;
+    py::class_<storm::models::sparse::MarkovAutomaton<double>, std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>>>(m, "SparseMA", "MA in sparse representation", model)
+    ;
 
     py::class_<Model<RationalFunction>, std::shared_ptr<Model<RationalFunction>>> 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<RationalFunction>& model) {
-                return model.getStateLabeling().getLabels();
-            }, "Labels")
+        .def_property_readonly("labeling", &getLabeling<storm::RationalFunction>, "Labels")
         .def("labels_state", &Model<RationalFunction>::getLabelsOfState, py::arg("state"), "Get labels of state")
         .def_property_readonly("initial_states", &getInitialStates<RationalFunction>, "Initial states")
+        .def_property_readonly("states", [](Model<storm::RationalFunction>& model) {
+                return SparseModelStates<storm::RationalFunction>(model);
+            }, "Get states")
         .def_property_readonly("transition_matrix", &getTransitionMatrix<RationalFunction>, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix")
+        .def_property_readonly("backward_transition_matrix", &getBackwardTransitionMatrix<storm::RationalFunction>, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix")
         .def("__str__", getModelInfoPrinter<RationalFunction>("ParametricModel"))
     ;
+
     py::class_<Dtmc<RationalFunction>, std::shared_ptr<Dtmc<RationalFunction>>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", modelRatFunc)
         .def("__str__", getModelInfoPrinter<RationalFunction>("ParametricDTMC"))
     ;
+
     py::class_<Mdp<RationalFunction>, std::shared_ptr<Mdp<RationalFunction>>>(m, "SparseParametricMdp", "pMDP in sparse representation", modelRatFunc)
         .def("__str__", getModelInfoPrinter<RationalFunction>("ParametricMDP"))
     ;
 
+    py::class_<storm::models::sparse::Ctmc<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Ctmc<storm::RationalFunction>>>(m, "SparseParametricCtmc", "pCTMC in sparse representation", modelRatFunc)
+    ;
+
+    py::class_<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>>>(m, "SparseParametricMA", "pMA in sparse representation", modelRatFunc)
+    ;
+
 }
 
 // Model instantiator
@@ -138,4 +170,12 @@ void define_model_instantiator(py::module& m) {
         .def(py::init<Mdp<RationalFunction>>(), "parametric model"_a)
         .def("instantiate", &storm::utility::ModelInstantiator<Mdp<RationalFunction>, Mdp<double>>::instantiate, "Instantiate model with given parameter values")
     ;
+
+    py::class_<storm::utility::ModelInstantiator<Ctmc<storm::RationalFunction>,Ctmc<double>>>(m, "PctmcInstantiator", "Instantiate PCTMCs to CTMCs")
+        .def(py::init<Ctmc<storm::RationalFunction>>(), "parametric model"_a)
+        .def("instantiate", &storm::utility::ModelInstantiator<Ctmc<storm::RationalFunction>, Ctmc<double>>::instantiate, "Instantiate model with given parameter values");
+
+    py::class_<storm::utility::ModelInstantiator<MarkovAutomaton<storm::RationalFunction>,MarkovAutomaton<double>>>(m, "PmaInstantiator", "Instantiate PMAs to MAs")
+        .def(py::init<MarkovAutomaton<storm::RationalFunction>>(), "parametric model"_a)
+        .def("instantiate", &storm::utility::ModelInstantiator<MarkovAutomaton<storm::RationalFunction>, MarkovAutomaton<double>>::instantiate, "Instantiate model with given parameter values");
 }

src/storage/state.cpp

@@ -0,0 +1,49 @@
+#include "state.h"
+
+void define_state(py::module& m) {
+    
+    // SparseModelStates
+    py::class_<SparseModelStates<double>>(m, "SparseModelStates", "States in sparse model")
+        .def("__getitem__", &SparseModelStates<double>::getState)
+        .def("__len__", &SparseModelStates<double>::getSize)
+    ;
+    py::class_<SparseModelStates<storm::RationalFunction>>(m, "SparseParametricModelStates", "States in sparse parametric model")
+        .def("__getitem__", &SparseModelStates<storm::RationalFunction>::getState)
+        .def("__len__", &SparseModelStates<storm::RationalFunction>::getSize)
+    ;
+    // SparseModelState
+    py::class_<SparseModelState<double>>(m, "SparseModelState", "State in sparse model")
+        .def("__str__", &SparseModelState<double>::toString)
+        .def_property_readonly("id", &SparseModelState<double>::getIndex, "Id")
+        .def_property_readonly("labels", &SparseModelState<double>::getLabels, "Labels")
+        .def_property_readonly("actions", &SparseModelState<double>::getActions, "Get actions")
+    ;
+    py::class_<SparseModelState<storm::RationalFunction>>(m, "SparseParametricModelState", "State in sparse parametric model")
+        .def("__str__", &SparseModelState<storm::RationalFunction>::toString)
+        .def_property_readonly("id", &SparseModelState<storm::RationalFunction>::getIndex, "Id")
+        .def_property_readonly("labels", &SparseModelState<storm::RationalFunction>::getLabels, "Labels")
+        .def_property_readonly("actions", &SparseModelState<storm::RationalFunction>::getActions, "Get actions")
+    ;
+    
+    // SparseModelActions
+    py::class_<SparseModelActions<double>>(m, "SparseModelActions", "Actions for state in sparse model")
+        .def("__getitem__", &SparseModelActions<double>::getAction)
+        .def("__len__", &SparseModelActions<double>::getSize)
+    ;
+    py::class_<SparseModelActions<storm::RationalFunction>>(m, "SparseParametricModelActions", "Actions for state in sparse parametric model")
+        .def("__getitem__", &SparseModelActions<storm::RationalFunction>::getAction)
+        .def("__len__", &SparseModelActions<storm::RationalFunction>::getSize)
+    ;
+    // SparseModelAction
+    py::class_<SparseModelAction<double>>(m, "SparseModelAction", "Action for state in sparse model")
+        .def("__str__", &SparseModelAction<double>::toString)
+        .def_property_readonly("id", &SparseModelAction<double>::getIndex, "Id")
+        .def_property_readonly("transitions", &SparseModelAction<double>::getTransitions, "Get transitions")
+    ;
+    py::class_<SparseModelAction<storm::RationalFunction>>(m, "SparseParametricModelAction", "Action for state in sparse parametric model")
+        .def("__str__", &SparseModelAction<storm::RationalFunction>::toString)
+        .def_property_readonly("id", &SparseModelAction<storm::RationalFunction>::getIndex, "Id")
+        .def_property_readonly("transitions", &SparseModelAction<storm::RationalFunction>::getTransitions, "Get transitions")
+    ;
+
+}

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<typename ValueType>
+class SparseModelActions;
+
+// State definition
+template<typename ValueType>
+class SparseModelState {
+        using s_index = typename storm::storage::SparseMatrix<ValueType>::index_type;
+   
+    public:
+        SparseModelState(storm::models::sparse::Model<ValueType>& model, s_index stateIndex) : model(model), stateIndex(stateIndex) {
+        }
+
+        s_index getIndex() const {
+            return stateIndex;
+        }
+
+        std::set<std::string> getLabels() const {
+            return this->model.getStateLabeling().getLabelsOfState(this->stateIndex);
+        }
+
+        SparseModelActions<ValueType> getActions() const {
+            return SparseModelActions<ValueType>(this->model, stateIndex);
+        }
+
+        std::string toString() const {
+            std::stringstream stream;
+            stream << stateIndex;
+            return stream.str();
+        }
+
+    private:
+        s_index stateIndex;
+        storm::models::sparse::Model<ValueType>& model;
+};
+
+template<typename ValueType>
+class SparseModelStates {
+        using s_index = typename storm::storage::SparseMatrix<ValueType>::index_type;
+   
+    public:
+        SparseModelStates(storm::models::sparse::Model<ValueType>& model) : model(model) {
+            length = model.getNumberOfStates();
+        }
+        
+        s_index getSize() const {
+            return length;
+        }
+        
+        SparseModelState<ValueType> getState(s_index index) const {
+            if (index < length) {
+                return SparseModelState<ValueType>(model, index);
+            } else {
+                throw py::index_error();
+            }
+        }
+    
+    private:
+        s_index length;
+        storm::models::sparse::Model<ValueType>& model;
+};
+
+// Action definition
+template<typename ValueType>
+class SparseModelAction {
+        using s_index = typename storm::storage::SparseMatrix<ValueType>::index_type;
+   
+    public:
+        SparseModelAction(storm::models::sparse::Model<ValueType>& model, s_index stateIndex, s_index actionIndex) : model(model), stateIndex(stateIndex), actionIndex(actionIndex) {
+        }
+
+        s_index getIndex() const {
+            return this->actionIndex;
+        }
+
+        typename storm::storage::SparseMatrix<ValueType>::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<ValueType>& model;
+};
+
+template<typename ValueType>
+class SparseModelActions {
+        using s_index = typename storm::storage::SparseMatrix<ValueType>::index_type;
+   
+    public:
+        SparseModelActions(storm::models::sparse::Model<ValueType>& model, s_index stateIndex) : model(model), stateIndex(stateIndex) {
+            length = model.getTransitionMatrix().getRowGroupSize(stateIndex);
+        }
+        
+        s_index getSize() const {
+            return length;
+        }
+        
+        SparseModelAction<ValueType> getAction(size_t index) const {
+            if (index < length) {
+                return SparseModelAction<ValueType>(model, stateIndex, index);
+            } else {
+                throw py::index_error();
+            }
+        }
+    
+    private:
+        s_index stateIndex;
+        s_index length;
+        storm::models::sparse::Model<ValueType>& model;
+};
+
+void define_state(py::module& m);
+
+#endif /* PYTHON_STORAGE_STATE_H_ */

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

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)

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
+    

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)
+    

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

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:

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

tests/storage/test_model_iterators.py → 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