Browse Source

Small refactoring

Former-commit-id: d56214abaf
tempestpy_adaptions
Mavo 9 years ago
committed by Matthias Volk
parent
commit
6835ce853a
  1. 2
      stormpy/lib/stormpy/storage/state.py
  2. 12
      stormpy/src/storage/matrix.cpp
  3. 10
      stormpy/src/storage/model.cpp
  4. 26
      stormpy/tests/storage/test_matrix.py
  5. 4
      stormpy/tests/storage/test_model_iterators.py

2
stormpy/lib/stormpy/storage/state.py

@ -28,7 +28,7 @@ class State:
""" Get actions associated with the state """ Get actions associated with the state
:return List of actions :return List of actions
""" """
row_group_indices = self.model.transition_matrix().row_group_indices()
row_group_indices = self.model.transition_matrix()._row_group_indices()
start = row_group_indices[self.id] start = row_group_indices[self.id]
end = row_group_indices[self.id+1] end = row_group_indices[self.id+1]
return stormpy.action.Action(start, end, 0, self.model) return stormpy.action.Action(start, end, 0, self.model)

12
stormpy/src/storage/matrix.cpp

@ -6,6 +6,7 @@ typedef storm::storage::SparseMatrix<double>::index_type entry_index;
void define_sparse_matrix(py::module& m) { void define_sparse_matrix(py::module& m) {
// MatrixEntry
py::class_<storm::storage::MatrixEntry<entry_index, double>>(m, "SparseMatrixEntry", "Entry of sparse matrix") py::class_<storm::storage::MatrixEntry<entry_index, double>>(m, "SparseMatrixEntry", "Entry of sparse matrix")
.def("__str__", [](storm::storage::MatrixEntry<entry_index, double> const& entry) { .def("__str__", [](storm::storage::MatrixEntry<entry_index, double> const& entry) {
std::stringstream stream; std::stringstream stream;
@ -13,8 +14,8 @@ void define_sparse_matrix(py::module& m) {
return stream.str(); return stream.str();
}) })
//def_property threw "pointer being freed not allocated" after exiting //def_property threw "pointer being freed not allocated" after exiting
.def("val", &storm::storage::MatrixEntry<entry_index, double>::getValue, "Value")
.def("set_val", &storm::storage::MatrixEntry<entry_index, double>::setValue, "Set value")
.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("column", &storm::storage::MatrixEntry<entry_index, double>::getColumn, "Column") .def("column", &storm::storage::MatrixEntry<entry_index, double>::getColumn, "Column")
; ;
@ -30,13 +31,13 @@ void define_sparse_matrix(py::module& m) {
.def("nr_rows", &storm::storage::SparseMatrix<double>::getRowCount, "Number of rows") .def("nr_rows", &storm::storage::SparseMatrix<double>::getRowCount, "Number of rows")
.def("nr_columns", &storm::storage::SparseMatrix<double>::getColumnCount, "Number of columns") .def("nr_columns", &storm::storage::SparseMatrix<double>::getColumnCount, "Number of columns")
.def("nr_entries", &storm::storage::SparseMatrix<double>::getEntryCount, "Number of non-zero entries") .def("nr_entries", &storm::storage::SparseMatrix<double>::getEntryCount, "Number of non-zero entries")
.def("row_group_indices", &storm::storage::SparseMatrix<double>::getRowGroupIndices, "Number of non-zero entries")
.def("_row_group_indices", &storm::storage::SparseMatrix<double>::getRowGroupIndices, "Get starting rows of row groups")
.def("get_row", [](storm::storage::SparseMatrix<double>& matrix, entry_index row) { .def("get_row", [](storm::storage::SparseMatrix<double>& matrix, entry_index row) {
return matrix.getRows(row, row+1); return matrix.getRows(row, row+1);
}, py::keep_alive<0, 1>() /* keep_alive seems to avoid problem with wrong values */, "Get rows from start to end")
}, py::return_value_policy::reference, py::keep_alive<1, 0>(), py::arg("row"), "Get row")
.def("get_rows", [](storm::storage::SparseMatrix<double>& matrix, entry_index start, entry_index end) { .def("get_rows", [](storm::storage::SparseMatrix<double>& matrix, entry_index start, entry_index end) {
return matrix.getRows(start, end); return matrix.getRows(start, end);
}, "Get rows from start to end")
}, py::return_value_policy::reference, py::keep_alive<1, 0>(), py::arg("row_start"), py::arg("row_end"), "Get rows from start to end")
.def("print_row", [](storm::storage::SparseMatrix<double> const& matrix, entry_index row) { .def("print_row", [](storm::storage::SparseMatrix<double> const& matrix, entry_index row) {
std::stringstream stream; std::stringstream stream;
auto rows = matrix.getRows(row, row+1); auto rows = matrix.getRows(row, row+1);
@ -47,6 +48,7 @@ void define_sparse_matrix(py::module& m) {
}) })
; ;
// Rows
py::class_<storm::storage::SparseMatrix<double>::rows>(m, "SparseMatrixRows", "Set of rows in a sparse matrix") py::class_<storm::storage::SparseMatrix<double>::rows>(m, "SparseMatrixRows", "Set of rows in a sparse matrix")
.def("__iter__", [](storm::storage::SparseMatrix<double>::rows& rows) { .def("__iter__", [](storm::storage::SparseMatrix<double>::rows& rows) {
return py::make_iterator(rows.begin(), rows.end()); return py::make_iterator(rows.begin(), rows.end());

10
stormpy/src/storage/model.cpp

@ -17,7 +17,8 @@ std::vector<storm::storage::sparse::state_type> getInitialStates(storm::models::
} }
// Thin wrapper for getting transition matrix // Thin wrapper for getting transition matrix
storm::storage::SparseMatrix<double>& getTransitionMatrix(storm::models::sparse::Model<double>& model) {
template<typename ValueType>
storm::storage::SparseMatrix<ValueType>& getTransitionMatrix(storm::models::sparse::Model<ValueType>& model) {
return model.getTransitionMatrix(); return model.getTransitionMatrix();
} }
@ -48,20 +49,21 @@ void define_model(py::module& m) {
// Models // Models
py::class_<storm::models::sparse::Model<double>, std::shared_ptr<storm::models::sparse::Model<double>>>(m, "SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix", py::base<storm::models::ModelBase>()) py::class_<storm::models::sparse::Model<double>, std::shared_ptr<storm::models::sparse::Model<double>>>(m, "SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix", py::base<storm::models::ModelBase>())
.def("labels", [](storm::models::sparse::Model<double> const& model) {
.def("labels", [](storm::models::sparse::Model<double>& model) {
return model.getStateLabeling().getLabels(); return model.getStateLabeling().getLabels();
}, "Get labels") }, "Get labels")
.def("labels_state", &storm::models::sparse::Model<double>::getLabelsOfState, "Get labels") .def("labels_state", &storm::models::sparse::Model<double>::getLabelsOfState, "Get labels")
.def("initial_states", &getInitialStates<double>, "Get initial states") .def("initial_states", &getInitialStates<double>, "Get initial states")
.def("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Get transition matrix")
.def("transition_matrix", &getTransitionMatrix<double>, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Get transition matrix")
; ;
py::class_<storm::models::sparse::Dtmc<double>, std::shared_ptr<storm::models::sparse::Dtmc<double>>>(m, "SparseDtmc", "DTMC in sparse representation", py::base<storm::models::sparse::Model<double>>()) py::class_<storm::models::sparse::Dtmc<double>, std::shared_ptr<storm::models::sparse::Dtmc<double>>>(m, "SparseDtmc", "DTMC in sparse representation", py::base<storm::models::sparse::Model<double>>())
; ;
py::class_<storm::models::sparse::Mdp<double>, std::shared_ptr<storm::models::sparse::Mdp<double>>>(m, "SparseMdp", "MDP in sparse representation", py::base<storm::models::sparse::Model<double>>()) py::class_<storm::models::sparse::Mdp<double>, std::shared_ptr<storm::models::sparse::Mdp<double>>>(m, "SparseMdp", "MDP in sparse representation", py::base<storm::models::sparse::Model<double>>())
; ;
py::class_<storm::models::sparse::Model<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>>>(m, "SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix", py::base<storm::models::ModelBase>()) py::class_<storm::models::sparse::Model<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>>>(m, "SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix", py::base<storm::models::ModelBase>())
.def("collect_probability_parameters", &storm::models::sparse::getProbabilityParameters, "Collect parameters") .def("collect_probability_parameters", &storm::models::sparse::getProbabilityParameters, "Collect parameters")
.def("labels", [](storm::models::sparse::Model<storm::RationalFunction> const& model) {
.def("labels", [](storm::models::sparse::Model<storm::RationalFunction>& model) {
return model.getStateLabeling().getLabels(); return model.getStateLabeling().getLabels();
}, "Get labels") }, "Get labels")
.def("labels_state", &storm::models::sparse::Model<storm::RationalFunction>::getLabelsOfState, "Get labels") .def("labels_state", &storm::models::sparse::Model<storm::RationalFunction>::getLabelsOfState, "Get labels")

26
stormpy/tests/storage/test_matrix.py

@ -9,20 +9,20 @@ class TestMatrix:
assert matrix.nr_columns() == model.nr_states() assert matrix.nr_columns() == model.nr_states()
assert matrix.nr_entries() == 27 #model.nr_transitions() assert matrix.nr_entries() == 27 #model.nr_transitions()
for e in matrix: for e in matrix:
assert e.val() == 0.5 or e.val() == 0 or (e.val() == 1 and e.column() > 6)
assert e.value() == 0.5 or e.value() == 0 or (e.value() == 1 and e.column() > 6)
def test_change_sparse_matrix(self): def test_change_sparse_matrix(self):
model = stormpy.parse_explicit_model("../examples/dtmc/die/die.tra", "../examples/dtmc/die/die.lab") model = stormpy.parse_explicit_model("../examples/dtmc/die/die.tra", "../examples/dtmc/die/die.lab")
matrix = model.transition_matrix() matrix = model.transition_matrix()
for e in matrix: for e in matrix:
assert e.val() == 0.5 or e.val() == 0 or e.val() == 1
assert e.value() == 0.5 or e.value() == 0 or e.value() == 1
i = 0 i = 0
for e in matrix: for e in matrix:
e.set_val(i)
e.set_value(i)
i += 0.1 i += 0.1
i = 0 i = 0
for e in matrix: for e in matrix:
assert e.val() == i
assert e.value() == i
i += 0.1 i += 0.1
def test_change_sparse_matrix_modelchecking(self): def test_change_sparse_matrix_modelchecking(self):
@ -31,7 +31,7 @@ class TestMatrix:
matrix = model.transition_matrix() matrix = model.transition_matrix()
# Check matrix # Check matrix
for e in matrix: for e in matrix:
assert e.val() == 0.5 or e.val() == 0 or e.val() == 1
assert e.value() == 0.5 or e.value() == 0 or e.value() == 1
# First model checking # First model checking
formulas = stormpy.parse_formulas("P=? [ F \"one\" ]") formulas = stormpy.parse_formulas("P=? [ F \"one\" ]")
result = stormpy.model_checking(model, formulas[0]) result = stormpy.model_checking(model, formulas[0])
@ -40,14 +40,14 @@ class TestMatrix:
# Change probabilities # Change probabilities
i = 0 i = 0
for e in matrix: for e in matrix:
if e.val() == 0.5:
if e.value() == 0.5:
if i % 2 == 0: if i % 2 == 0:
e.set_val(0.3)
e.set_value(0.3)
else: else:
e.set_val(0.7)
e.set_value(0.7)
i += 1 i += 1
for e in matrix: for e in matrix:
assert e.val() == 0.3 or e.val() == 0.7 or e.val() == 1 or e.val() == 0
assert e.value() == 0.3 or e.value() == 0.7 or e.value() == 1 or e.value() == 0
# Second model checking # Second model checking
result = stormpy.model_checking(model, formulas[0]) result = stormpy.model_checking(model, formulas[0])
assert result == 0.06923076923076932 assert result == 0.06923076923076932
@ -56,10 +56,10 @@ class TestMatrix:
for state in stormpy.state.State(0, model): for state in stormpy.state.State(0, model):
for action in state.actions(): for action in state.actions():
for transition in action.transitions(): for transition in action.transitions():
if transition.val() == 0.3:
transition.set_val(0.8)
elif transition.val() == 0.7:
transition.set_val(0.2)
if transition.value() == 0.3:
transition.set_value(0.8)
elif transition.value() == 0.7:
transition.set_value(0.2)
# Third model checking # Third model checking
result = stormpy.model_checking(model, formulas[0]) result = stormpy.model_checking(model, formulas[0])
assert result == 0.3555555555555556 or result == 0.3555555555555557 assert result == 0.3555555555555556 or result == 0.3555555555555557

4
stormpy/tests/storage/test_model_iterators.py

@ -50,7 +50,7 @@ class TestModelIterators:
i += 1 i += 1
assert state.id == transition_orig[0] assert state.id == transition_orig[0]
assert transition.column() == transition_orig[1] assert transition.column() == transition_orig[1]
assert transition.val() == transition_orig[2]
assert transition.value() == transition_orig[2]
def test_transitions_mdp(self): def test_transitions_mdp(self):
model = stormpy.parse_explicit_model("../examples/mdp/two_dice/two_dice.tra", "../examples/mdp/two_dice/two_dice.lab") model = stormpy.parse_explicit_model("../examples/mdp/two_dice/two_dice.tra", "../examples/mdp/two_dice/two_dice.lab")
@ -60,5 +60,5 @@ class TestModelIterators:
for action in state.actions(): for action in state.actions():
i += 1 i += 1
for transition in action.transitions(): for transition in action.transitions():
assert transition.val() == 0.5 or transition.val() == 1
assert transition.value() == 0.5 or transition.value() == 1
assert i == 1 or i == 2 assert i == 1 or i == 2
Loading…
Cancel
Save