diff --git a/lib/stormpy/storage/__init__.py b/lib/stormpy/storage/__init__.py index 0d3e560..08aeb77 100644 --- a/lib/stormpy/storage/__init__.py +++ b/lib/stormpy/storage/__init__.py @@ -1,6 +1,5 @@ from . import storage from .storage import * -from . import state,action class ModelInstantiator: def __init__(self, model): diff --git a/lib/stormpy/storage/action.py b/lib/stormpy/storage/action.py deleted file mode 100644 index ad6f68e..0000000 --- a/lib/stormpy/storage/action.py +++ /dev/null @@ -1,36 +0,0 @@ -class Action: - """ Represents an action in the model """ - - def __init__(self, row_group_start, row_group_end, row, matrix): - """ Initialize - :param row_group_start: Start index of the row group in the matrix - :param row_group_end: End index of the row group in the matrix - :param row: Index of the corresponding row in the matrix - :param matrix: Corresponding matrix - """ - self.row_group_start = row_group_start - self.row_group_end = row_group_end - self.row = row - 1 - self.matrix = matrix - assert row >= -1 and row + row_group_start <= row_group_end - - def __iter__(self): - return self - - def __next__(self): - if self.row + self.row_group_start >= self.row_group_end - 1: - raise StopIteration - else: - self.row += 1 - return self - - def __str__(self): - return "{}".format(self.row) - - def transitions(self): - """ Get transitions associated with the action - :return List of tranistions - """ - row = self.row_group_start + self.row - #return self.model.transition_matrix().get_row(self.row_group_start + self.row) - return self.matrix.row_iter(row, row) diff --git a/lib/stormpy/storage/state.py b/lib/stormpy/storage/state.py deleted file mode 100644 index 613316e..0000000 --- a/lib/stormpy/storage/state.py +++ /dev/null @@ -1,34 +0,0 @@ -from . import action - -class State: - """ Represents a state in the matrix """ - - def __init__(self, id, matrix): - """ Initialize - :param id: Id of the state - :param matrix: Corresponding matrix - """ - self.id = id - 1 - self.matrix = matrix - - def __iter__(self): - return self - - def __next__(self): - if self.id >= self.matrix.nr_row_groups - 1: - raise StopIteration - else: - self.id += 1 - return self - - def __str__(self): - return "{}".format(self.id) - - def actions(self): - """ Get actions associated with the state - :return List of actions - """ - row_group_indices = self.matrix._row_group_indices - start = row_group_indices[self.id] - end = row_group_indices[self.id+1] - return action.Action(start, end, 0, self.matrix) diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 658043c..2755911 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -3,6 +3,7 @@ #include "storage/bitvector.h" #include "storage/model.h" #include "storage/matrix.h" +#include "storage/state.h" #include "storage/labeling.h" PYBIND11_PLUGIN(storage) { @@ -16,6 +17,7 @@ PYBIND11_PLUGIN(storage) { define_bitvector(m); define_model(m); define_sparse_matrix(m); + define_state(m); define_model_instantiator(m); define_labeling(m); return m.ptr(); diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp index 567cbdf..5073c42 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -15,7 +15,7 @@ void define_sparse_matrix(py::module& m) { stream << entry; return stream.str(); }) - //def_property threw "pointer being freed not allocated" after exiting + //Note: def_property threw "pointer being freed not allocated" after exiting .def("value", &storm::storage::MatrixEntry::getValue, "Value") .def("set_value", &storm::storage::MatrixEntry::setValue, py::arg("value"), "Set value") .def_property_readonly("column", &storm::storage::MatrixEntry::getColumn, "Column") @@ -27,7 +27,7 @@ void define_sparse_matrix(py::module& m) { stream << entry; return stream.str(); }) - //def_property threw "pointer being freed not allocated" after exiting + //Note: def_property threw "pointer being freed not allocated" after exiting .def("value", &storm::storage::MatrixEntry::getValue, "Value") .def("set_value", &storm::storage::MatrixEntry::setValue, py::arg("value"), "Set value") .def_property_readonly("column", &storm::storage::MatrixEntry::getColumn, "Column") @@ -61,7 +61,7 @@ void define_sparse_matrix(py::module& m) { stream << transition << ", "; } return stream.str(); - }, py::arg("row"), "Print row") + }, py::arg("row"), "Print rows from start to end") // Entry_index lead to problems .def("row_iter", [](storm::storage::SparseMatrix& matrix, row_index start, row_index end) { return py::make_iterator(matrix.begin(start), matrix.end(end)); diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 839ee4e..dc091e1 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -1,4 +1,6 @@ #include "model.h" +#include "state.h" + #include "storm/models/ModelBase.h" #include "storm/models/sparse/Model.h" #include "storm/models/sparse/Dtmc.h" @@ -78,6 +80,9 @@ void define_model(py::module& m) { .def_property_readonly("initial_states", &getInitialStates, "Initial states") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") .def_property_readonly("backward_transition_matrix", &getBackwardTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") + .def_property_readonly("states", [](storm::models::sparse::Model& model) { + return SparseModelStates(model); + }, "Get states") ; py::class_, std::shared_ptr>>(m, "SparseDtmc", "DTMC in sparse representation", model) ; @@ -90,12 +95,15 @@ void define_model(py::module& m) { py::class_, std::shared_ptr>> modelRatFunc(m, "_SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix", modelBase); modelRatFunc.def("collect_probability_parameters", &probabilityVariables, "Collect parameters") - .def("collect_reward_parameters", &rewardVariables, "Collect reward parameters") + .def("collect_reward_parameters", &rewardVariables, "Collect reward parameters") .def_property_readonly("labeling", &getLabeling, "Labels") .def("labels_state", &storm::models::sparse::Model::getLabelsOfState, py::arg("state"), "Get labels of state") .def_property_readonly("initial_states", &getInitialStates, "Initial states") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") .def_property_readonly("backward_transition_matrix", &getBackwardTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") + .def_property_readonly("states", [](storm::models::sparse::Model& model) { + return SparseModelStates(model); + }, "Get states") ; py::class_, std::shared_ptr>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", modelRatFunc) ; diff --git a/src/storage/state.cpp b/src/storage/state.cpp new file mode 100644 index 0000000..d3724c1 --- /dev/null +++ b/src/storage/state.cpp @@ -0,0 +1,45 @@ +#include "state.h" + +void define_state(py::module& m) { + + // SparseModelStates + py::class_>(m, "SparseModelStates", "States in sparse model") + .def("__getitem__", &SparseModelStates::getState) + ; + py::class_>(m, "SparseParametricModelStates", "States in sparse parametric model") + .def("__getitem__", &SparseModelStates::getState) + ; + // SparseModelState + py::class_>(m, "SparseModelState", "State in sparse model") + .def("__str__", &SparseModelState::toString) + .def_property_readonly("id", &SparseModelState::getIndex, "Id") + .def_property_readonly("labels", &SparseModelState::getLabels, "Labels") + .def_property_readonly("actions", &SparseModelState::getActions, "Get actions") + ; + py::class_>(m, "SparseParametricModelState", "State in sparse parametric model") + .def("__str__", &SparseModelState::toString) + .def_property_readonly("id", &SparseModelState::getIndex, "Id") + .def_property_readonly("labels", &SparseModelState::getLabels, "Labels") + .def_property_readonly("actions", &SparseModelState::getActions, "Get actions") + ; + + // SparseModelActions + py::class_>(m, "SparseModelActions", "Actions for state in sparse model") + .def("__getitem__", &SparseModelActions::getAction) + ; + py::class_>(m, "SparseParametricModelActions", "Actions for state in sparse parametric model") + .def("__getitem__", &SparseModelActions::getAction) + ; + // SparseModelAction + py::class_>(m, "SparseModelAction", "Action for state in sparse model") + .def("__str__", &SparseModelAction::toString) + .def_property_readonly("id", &SparseModelAction::getIndex, "Id") + .def_property_readonly("transitions", &SparseModelAction::getTransitions, "Get transitions") + ; + py::class_>(m, "SparseParametricModelAction", "Action for state in sparse parametric model") + .def("__str__", &SparseModelAction::toString) + .def_property_readonly("id", &SparseModelAction::getIndex, "Id") + .def_property_readonly("transitions", &SparseModelAction::getTransitions, "Get transitions") + ; + +} diff --git a/src/storage/state.h b/src/storage/state.h new file mode 100644 index 0000000..a2db40e --- /dev/null +++ b/src/storage/state.h @@ -0,0 +1,122 @@ +#ifndef PYTHON_STORAGE_STATE_H_ +#define PYTHON_STORAGE_STATE_H_ + +#include "common.h" + +#include "storm/storage/SparseMatrix.h" +#include "storm/models/sparse/Model.h" + +// Forward declaration +template +class SparseModelActions; + +// State definition +template +class SparseModelState { + using s_index = typename storm::storage::SparseMatrix::index_type; + + public: + SparseModelState(storm::models::sparse::Model& model, s_index stateIndex) : model(model), stateIndex(stateIndex) { + } + + s_index getIndex() const { + return this->stateIndex; + } + + std::set getLabels() { + return this->model.getStateLabeling().getLabelsOfState(this->stateIndex); + } + + SparseModelActions getActions() { + return SparseModelActions(this->model, stateIndex); + } + + std::string toString() { + std::stringstream stream; + stream << this->getIndex(); + return stream.str(); + } + + private: + s_index stateIndex; + storm::models::sparse::Model& model; +}; + +template +class SparseModelStates { + using s_index = typename storm::storage::SparseMatrix::index_type; + + public: + SparseModelStates(storm::models::sparse::Model& model) : model(model) { + length = model.getNumberOfStates(); + } + + SparseModelState getState(s_index index) { + if (index < length) { + return SparseModelState(model, index); + } else { + throw py::index_error(); + } + } + + private: + s_index length; + storm::models::sparse::Model& model; +}; + +// Action definition +template +class SparseModelAction { + using s_index = typename storm::storage::SparseMatrix::index_type; + + public: + SparseModelAction(storm::models::sparse::Model& model, s_index stateIndex, s_index actionIndex) : model(model), stateIndex(stateIndex), actionIndex(actionIndex) { + } + + s_index getIndex() const { + return this->actionIndex; + } + + typename storm::storage::SparseMatrix::rows getTransitions() { + return model.getTransitionMatrix().getRow(stateIndex, actionIndex); + } + + std::string toString() { + std::stringstream stream; + stream << this->getIndex(); + return stream.str(); + } + + + private: + s_index stateIndex; + s_index actionIndex; + storm::models::sparse::Model& model; +}; + +template +class SparseModelActions { + using s_index = typename storm::storage::SparseMatrix::index_type; + + public: + SparseModelActions(storm::models::sparse::Model& model, s_index stateIndex) : model(model), stateIndex(stateIndex) { + length = model.getTransitionMatrix().getRowGroupSize(stateIndex); + } + + SparseModelAction getAction(size_t index) { + if (index < length) { + return SparseModelAction(model, stateIndex, index); + } else { + throw py::index_error(); + } + } + + private: + s_index stateIndex; + s_index length; + storm::models::sparse::Model& model; +}; + +void define_state(py::module& m); + +#endif /* PYTHON_STORAGE_STATE_H_ */ diff --git a/tests/storage/test_matrix.py b/tests/storage/test_matrix.py index 53fdc91..8d9fb65 100644 --- a/tests/storage/test_matrix.py +++ b/tests/storage/test_matrix.py @@ -68,9 +68,9 @@ class TestMatrix: assert math.isclose(resValue, 0.06923076923076932) # Change probabilities again - for state in stormpy.state.State(0, model.transition_matrix): - for action in state.actions(): - for transition in action.transitions(): + for state in model.states: + for action in state.actions: + for transition in action.transitions: if transition.value() == 0.3: transition.set_value(0.8) elif transition.value() == 0.7: diff --git a/tests/storage/test_model_iterators.py b/tests/storage/test_state.py similarity index 59% rename from tests/storage/test_model_iterators.py rename to tests/storage/test_state.py index 1f80e97..add9dcd 100644 --- a/tests/storage/test_model_iterators.py +++ b/tests/storage/test_state.py @@ -1,38 +1,54 @@ import stormpy from helpers.helper import get_example_path -class TestModelIterators: +class TestState: def test_states_dtmc(self): model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) - s = stormpy.state.State(0, model.transition_matrix) i = 0 - for state in stormpy.state.State(0, model.transition_matrix): + states = model.states + for state in states: assert state.id == i i += 1 assert i == model.nr_states + state = model.states[2] + assert state.id == 2 + state = states[5] + assert state.id == 5 def test_states_mdp(self): model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab")) - s = stormpy.state.State(0, model.transition_matrix) i = 0 - for state in stormpy.state.State(0, model.transition_matrix): + for state in model.states: assert state.id == i i += 1 assert i == model.nr_states + states = model.states + state = model.states[6] + assert state.id == 6 + state = states[1] + assert state.id == 1 + + def test_labels_dtmc(self): + model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) + labelsOrig = [["init"], [], [], [], [], [], [], ["one", "done"], ["two", "done"], ["three", "done"], ["four", "done"], ["five", "done"], ["six", "done"]] + i = 0 + for state in model.states: + labels = state.labels + for label in labelsOrig[i]: + assert label in labels + i += 1 def test_actions_dtmc(self): model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) - s = stormpy.state.State(0, model.transition_matrix) - for state in stormpy.state.State(0, model.transition_matrix): - for action in state.actions(): - assert action.row == 0 + for state in model.states: + for action in state.actions: + assert action.id == 0 def test_actions_mdp(self): model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab")) - s = stormpy.state.State(0, model.transition_matrix) - for state in stormpy.state.State(0, model.transition_matrix): - for action in state.actions(): - assert action.row == 0 or action.row == 1 + for state in model.states: + for action in state.actions: + assert action.id == 0 or action.id == 1 def test_transitions_dtmc(self): transitions_orig = [(0, 0, 0), (0, 1, 0.5), (0, 2, 0.5), (1, 1, 0), (1, 3, 0.5), (1, 4, 0.5), @@ -42,11 +58,10 @@ class TestModelIterators: (9, 9, 1), (10, 10, 1), (11, 11, 1), (12, 12, 1) ] model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) - s = stormpy.state.State(0, model.transition_matrix) i = 0 - for state in stormpy.state.State(0, model.transition_matrix): - for action in state.actions(): - for transition in action.transitions(): + for state in model.states: + for action in state.actions: + for transition in action.transitions: transition_orig = transitions_orig[i] i += 1 assert state.id == transition_orig[0] @@ -55,12 +70,12 @@ class TestModelIterators: def test_transitions_mdp(self): model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab")) - s = stormpy.state.State(0, model.transition_matrix) - for state in stormpy.state.State(0, model.transition_matrix): + assert model.states[1].id == 1 + for state in model.states: i = 0 - for action in state.actions(): + for action in state.actions: i += 1 - for transition in action.transitions(): + for transition in action.transitions: assert transition.value() == 0.5 or transition.value() == 1 assert i == 1 or i == 2 @@ -73,10 +88,27 @@ class TestModelIterators: ] model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) i = 0 - for state in stormpy.state.State(0, model.transition_matrix): + for state in model.states: for transition in model.transition_matrix.row_iter(state.id, state.id): transition_orig = transitions_orig[i] i += 1 assert state.id == transition_orig[0] assert transition.column == transition_orig[1] assert transition.value() == transition_orig[2] + + def test_parametric_transitions(self): + import pycarl + program = stormpy.parse_prism_program(get_example_path("pmdp", "two_dice.nm")) + model = stormpy.build_parametric_model(program) + assert model.states[1].id == 1 + one = pycarl.FactorizedPolynomial(pycarl.Rational(1)) + i = 0 + for state in model.states: + assert state.id == i + i += 1 + j = 0 + for action in state.actions: + assert j == 0 or j == 1 + j += 1 + for transition in action.transitions: + assert transition.value().denominator == one