Changed state and action for models

lib/stormpy/storage/__init__.py

@@ -1,6 +1,5 @@
 from . import storage
 from .storage import *
-from . import state,action
 
 class ModelInstantiator:
     def __init__(self, model):

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, matrix):
-        """ Initialize
-        :param row_group_start: Start index of the row group in the matrix
-        :param row_group_end: End index of the row group in the matrix
-        :param row: Index of the corresponding row in the matrix
-        :param matrix: Corresponding matrix
-        """
-        self.row_group_start = row_group_start
-        self.row_group_end = row_group_end
-        self.row = row - 1
-        self.matrix = matrix
-        assert row >= -1 and row + row_group_start <= row_group_end
-
-    def __iter__(self):
-        return self
-
-    def __next__(self):
-        if self.row + self.row_group_start >= self.row_group_end - 1:
-            raise StopIteration
-        else:
-            self.row += 1
-            return self
-
-    def __str__(self):
-        return "{}".format(self.row)
-
-    def transitions(self):
-        """ Get transitions associated with the action
-        :return List of tranistions
-        """
-        row = self.row_group_start + self.row
-        #return self.model.transition_matrix().get_row(self.row_group_start + self.row)
-        return self.matrix.row_iter(row, row)

lib/stormpy/storage/state.py

@@ -1,34 +0,0 @@
-from . import action
-
-class State:
-    """ Represents a state in the matrix """
-
-    def __init__(self, id, matrix):
-        """ Initialize
-        :param id: Id of the state
-        :param matrix: Corresponding matrix
-        """
-        self.id = id - 1
-        self.matrix = matrix
-
-    def __iter__(self):
-        return self
-
-    def __next__(self):
-        if self.id >= self.matrix.nr_row_groups - 1:
-            raise StopIteration
-        else:
-            self.id += 1
-            return self
-
-    def __str__(self):
-        return "{}".format(self.id)
-
-    def actions(self):
-        """ Get actions associated with the state
-        :return List of actions
-        """
-        row_group_indices = self.matrix._row_group_indices
-        start = row_group_indices[self.id]
-        end = row_group_indices[self.id+1]
-        return action.Action(start, end, 0, self.matrix)

src/mod_storage.cpp

@@ -3,6 +3,7 @@
 #include "storage/bitvector.h"
 #include "storage/model.h"
 #include "storage/matrix.h"
+#include "storage/state.h"
 #include "storage/labeling.h"
 
 PYBIND11_PLUGIN(storage) {
@@ -16,6 +17,7 @@ PYBIND11_PLUGIN(storage) {
     define_bitvector(m);
     define_model(m);
     define_sparse_matrix(m);
+    define_state(m);
     define_model_instantiator(m);
     define_labeling(m);
     return m.ptr();

src/storage/matrix.cpp

@@ -15,7 +15,7 @@ void define_sparse_matrix(py::module& m) {
                 stream << entry;
                 return stream.str();
             })
-        //def_property threw "pointer being freed not allocated" after exiting
+        //Note: def_property threw "pointer being freed not allocated" after exiting
         .def("value", &storm::storage::MatrixEntry<entry_index, double>::getValue, "Value")
         .def("set_value", &storm::storage::MatrixEntry<entry_index, double>::setValue, py::arg("value"), "Set value")
         .def_property_readonly("column", &storm::storage::MatrixEntry<entry_index, double>::getColumn, "Column")
@@ -27,7 +27,7 @@ void define_sparse_matrix(py::module& m) {
                 stream << entry;
                 return stream.str();
             })
-        //def_property threw "pointer being freed not allocated" after exiting
+        //Note: def_property threw "pointer being freed not allocated" after exiting
         .def("value", &storm::storage::MatrixEntry<parametric_entry_index, storm::RationalFunction>::getValue, "Value")
         .def("set_value", &storm::storage::MatrixEntry<parametric_entry_index, storm::RationalFunction>::setValue, py::arg("value"), "Set value")
         .def_property_readonly("column", &storm::storage::MatrixEntry<parametric_entry_index, storm::RationalFunction>::getColumn, "Column")
@@ -61,7 +61,7 @@ void define_sparse_matrix(py::module& m) {
                     stream << transition << ", ";
                 }
                 return stream.str();
-            }, py::arg("row"), "Print row")
+            }, py::arg("row"), "Print rows from start to end")
         // Entry_index lead to problems
         .def("row_iter", [](storm::storage::SparseMatrix<double>& matrix, row_index start, row_index end) {
                 return py::make_iterator(matrix.begin(start), matrix.end(end));

src/storage/model.cpp

@@ -1,4 +1,6 @@
 #include "model.h"
+#include "state.h"
+
 #include "storm/models/ModelBase.h"
 #include "storm/models/sparse/Model.h"
 #include "storm/models/sparse/Dtmc.h"
@@ -78,6 +80,9 @@ void define_model(py::module& m) {
         .def_property_readonly("initial_states", &getInitialStates<double>, "Initial 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_property_readonly("states", [](storm::models::sparse::Model<double>& model) {
+                return SparseModelStates<double>(model);
+            }, "Get states")
     ;
     py::class_<storm::models::sparse::Dtmc<double>, std::shared_ptr<storm::models::sparse::Dtmc<double>>>(m, "SparseDtmc", "DTMC in sparse representation", model)
     ;
@@ -90,12 +95,15 @@ void define_model(py::module& m) {
 
     py::class_<storm::models::sparse::Model<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Model<storm::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("collect_reward_parameters", &rewardVariables, "Collect reward parameters")
         .def_property_readonly("labeling", &getLabeling<storm::RationalFunction>, "Labels")
         .def("labels_state", &storm::models::sparse::Model<storm::RationalFunction>::getLabelsOfState, py::arg("state"), "Get labels of state")
         .def_property_readonly("initial_states", &getInitialStates<storm::RationalFunction>, "Initial states")
         .def_property_readonly("transition_matrix", &getTransitionMatrix<storm::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_property_readonly("states", [](storm::models::sparse::Model<storm::RationalFunction>& model) {
+                return SparseModelStates<storm::RationalFunction>(model);
+            }, "Get states")
     ;
     py::class_<storm::models::sparse::Dtmc<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", modelRatFunc)
     ;

src/storage/state.cpp

@@ -0,0 +1,45 @@
+#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)
+    ;
+    py::class_<SparseModelStates<storm::RationalFunction>>(m, "SparseParametricModelStates", "States in sparse parametric model")
+        .def("__getitem__", &SparseModelStates<storm::RationalFunction>::getState)
+    ;
+    // 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)
+    ;
+    py::class_<SparseModelActions<storm::RationalFunction>>(m, "SparseParametricModelActions", "Actions for state in sparse parametric model")
+        .def("__getitem__", &SparseModelActions<storm::RationalFunction>::getAction)
+    ;
+    // 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,122 @@
+#ifndef PYTHON_STORAGE_STATE_H_
+#define PYTHON_STORAGE_STATE_H_
+
+#include "common.h"
+
+#include "storm/storage/SparseMatrix.h"
+#include "storm/models/sparse/Model.h"
+
+// Forward declaration
+template<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 this->stateIndex;
+        }
+
+        std::set<std::string> getLabels() {
+            return this->model.getStateLabeling().getLabelsOfState(this->stateIndex);
+        }
+
+        SparseModelActions<ValueType> getActions() {
+            return SparseModelActions<ValueType>(this->model, stateIndex);
+        }
+
+        std::string toString() {
+            std::stringstream stream;
+            stream << this->getIndex();
+            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();
+        }
+        
+        SparseModelState<ValueType> getState(s_index index) {
+            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() {
+            std::stringstream stream;
+            stream << this->getIndex();
+            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);
+        }
+        
+        SparseModelAction<ValueType> getAction(size_t index) {
+            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/storage/test_matrix.py

@@ -68,9 +68,9 @@ class TestMatrix:
         assert math.isclose(resValue, 0.06923076923076932)
         
         # Change probabilities again
-        for state in stormpy.state.State(0, model.transition_matrix):
-            for action in state.actions():
-                for transition in action.transitions():
+        for state in model.states:
+            for action in state.actions:
+                for transition in action.transitions:
                     if transition.value() == 0.3:
                         transition.set_value(0.8)
                     elif transition.value() == 0.7:

tests/storage/test_model_iterators.py → tests/storage/test_state.py

@@ -1,38 +1,54 @@
 import stormpy
 from helpers.helper import get_example_path
 
-class TestModelIterators:
+class TestState:
     def test_states_dtmc(self):
         model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
-        s = stormpy.state.State(0, model.transition_matrix)
         i = 0
-        for state in stormpy.state.State(0, model.transition_matrix):
+        states = model.states
+        for state in states:
             assert state.id == i
             i += 1
         assert i == model.nr_states
+        state = model.states[2]
+        assert state.id == 2
+        state = states[5]
+        assert state.id == 5
     
     def test_states_mdp(self):
         model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab"))
-        s = stormpy.state.State(0, model.transition_matrix)
         i = 0
-        for state in stormpy.state.State(0, model.transition_matrix):
+        for state in model.states:
             assert state.id == i
             i += 1
         assert i == model.nr_states
+        states = model.states
+        state = model.states[6]
+        assert state.id == 6
+        state = states[1]
+        assert state.id == 1
+    
+    def test_labels_dtmc(self):
+        model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
+        labelsOrig = [["init"], [], [], [], [], [], [], ["one", "done"], ["two", "done"], ["three", "done"], ["four", "done"], ["five", "done"], ["six", "done"]]
+        i = 0
+        for state in model.states:
+            labels = state.labels
+            for label in labelsOrig[i]:
+                assert label in labels
+            i += 1
     
     def test_actions_dtmc(self):
         model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
-        s = stormpy.state.State(0, model.transition_matrix)
-        for state in stormpy.state.State(0, model.transition_matrix):
-            for action in state.actions():
-                assert action.row == 0
+        for state in model.states:
+            for action in state.actions:
+                assert action.id == 0
     
     def test_actions_mdp(self):
         model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab"))
-        s = stormpy.state.State(0, model.transition_matrix)
-        for state in stormpy.state.State(0, model.transition_matrix):
-            for action in state.actions():
-                assert action.row == 0 or action.row == 1
+        for state in model.states:
+            for action in state.actions:
+                assert action.id == 0 or action.id == 1
     
     def test_transitions_dtmc(self):
         transitions_orig = [(0, 0, 0), (0, 1, 0.5), (0, 2, 0.5), (1, 1, 0), (1, 3, 0.5), (1, 4, 0.5), 
@@ -42,11 +58,10 @@ class TestModelIterators:
                 (9, 9, 1), (10, 10, 1), (11, 11, 1), (12, 12, 1)
             ]
         model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
-        s = stormpy.state.State(0, model.transition_matrix)
         i = 0
-        for state in stormpy.state.State(0, model.transition_matrix):
-            for action in state.actions():
-                for transition in action.transitions():
+        for state in model.states:
+            for action in state.actions:
+                for transition in action.transitions:
                     transition_orig = transitions_orig[i]
                     i += 1
                     assert state.id == transition_orig[0]
@@ -55,12 +70,12 @@ class TestModelIterators:
     
     def test_transitions_mdp(self):
         model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab"))
-        s = stormpy.state.State(0, model.transition_matrix)
-        for state in stormpy.state.State(0, model.transition_matrix):
+        assert model.states[1].id == 1
+        for state in model.states:
             i = 0
-            for action in state.actions():
+            for action in state.actions:
                 i += 1
-                for transition in action.transitions():
+                for transition in action.transitions:
                     assert transition.value() == 0.5 or transition.value() == 1
             assert i == 1 or i == 2
 
@@ -73,10 +88,27 @@ class TestModelIterators:
             ]
         model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
         i = 0
-        for state in stormpy.state.State(0, model.transition_matrix):
+        for state in model.states:
             for transition in model.transition_matrix.row_iter(state.id, state.id):
                 transition_orig = transitions_orig[i]
                 i += 1
                 assert state.id == transition_orig[0]
                 assert transition.column == transition_orig[1]
                 assert transition.value() == transition_orig[2]
+    
+    def test_parametric_transitions(self):
+        import pycarl
+        program = stormpy.parse_prism_program(get_example_path("pmdp", "two_dice.nm"))
+        model = stormpy.build_parametric_model(program)
+        assert model.states[1].id == 1
+        one = pycarl.FactorizedPolynomial(pycarl.Rational(1))
+        i = 0
+        for state in model.states:
+            assert state.id == i
+            i += 1
+            j = 0
+            for action in state.actions:
+                assert j == 0 or j == 1
+                j += 1
+                for transition in action.transitions:
+                    assert transition.value().denominator == one