sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

ParametricSparseMatrix 

Former-commit-id: 2d201a6d58
tempestpy_adaptions
Mavo 9 years ago
committed by Matthias Volk
parent
6835ce853a
commit
0fdfdeb5d6
3 changed files with 88 additions and 1 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 58
      stormpy/src/storage/matrix.cpp
  2. 1
      stormpy/src/storage/model.cpp
  3. 30
      stormpy/tests/storage/test_matrix.py

58
stormpy/src/storage/matrix.cpp
View File

@ -3,6 +3,7 @@
#include "src/storage/SparseMatrix.h"
typedef storm::storage::SparseMatrix<double>::index_type entry_index;
typedef storm::storage::SparseMatrix<storm::RationalFunction>::index_type parametric_entry_index;
void define_sparse_matrix(py::module& m) {
@ -19,6 +20,19 @@ void define_sparse_matrix(py::module& m) {
.def("column", &storm::storage::MatrixEntry<entry_index, double>::getColumn, "Column")
;
py::class_<storm::storage::MatrixEntry<entry_index, storm::RationalFunction>>(m, "ParametricSparseMatrixEntry", "Entry of parametric sparse matrix")
.def("__str__", [](storm::storage::MatrixEntry<entry_index, storm::RationalFunction> const& entry) {
std::stringstream stream;
stream << entry;
return stream.str();
})
//def_property threw "pointer being freed not allocated" after exiting
.def("value", &storm::storage::MatrixEntry<entry_index, storm::RationalFunction>::getValue, "Value")
.def("set_value", &storm::storage::MatrixEntry<entry_index, storm::RationalFunction>::setValue, py::arg("value"), "Set value")
.def("column", &storm::storage::MatrixEntry<entry_index, storm::RationalFunction>::getColumn, "Column")
;
// SparseMatrix
py::class_<storm::storage::SparseMatrix<double>>(m, "SparseMatrix", "Sparse matrix")
.def("__iter__", [](storm::storage::SparseMatrix<double>& matrix) {
return py::make_iterator(matrix.begin(), matrix.end());
@ -45,7 +59,36 @@ void define_sparse_matrix(py::module& m) {
stream << transition << ", ";
}
return stream.str();
}, py::arg("row"), "Print row")
;
py::class_<storm::storage::SparseMatrix<storm::RationalFunction>>(m, "ParametricSparseMatrix", "Parametric sparse matrix")
.def("__iter__", [](storm::storage::SparseMatrix<storm::RationalFunction>& matrix) {
return py::make_iterator(matrix.begin(), matrix.end());
}, py::keep_alive<0, 1>() /* Essential: keep object alive while iterator exists */)
.def("__str__", [](storm::storage::SparseMatrix<storm::RationalFunction> const& matrix) {
std::stringstream stream;
stream << matrix;
return stream.str();
})
.def("nr_rows", &storm::storage::SparseMatrix<storm::RationalFunction>::getRowCount, "Number of rows")
.def("nr_columns", &storm::storage::SparseMatrix<storm::RationalFunction>::getColumnCount, "Number of columns")
.def("nr_entries", &storm::storage::SparseMatrix<storm::RationalFunction>::getEntryCount, "Number of non-zero entries")
.def("_row_group_indices", &storm::storage::SparseMatrix<storm::RationalFunction>::getRowGroupIndices, "Get starting rows of row groups")
.def("get_row", [](storm::storage::SparseMatrix<storm::RationalFunction>& matrix, entry_index row) {
return matrix.getRows(row, row+1);
}, py::return_value_policy::reference, py::keep_alive<1, 0>(), py::arg("row"), "Get row")
.def("get_rows", [](storm::storage::SparseMatrix<storm::RationalFunction>& matrix, entry_index start, entry_index end) {
return matrix.getRows(start, 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<storm::RationalFunction> const& matrix, entry_index row) {
std::stringstream stream;
auto rows = matrix.getRows(row, row+1);
for (auto transition : rows) {
stream << transition << ", ";
}
return stream.str();
}, py::arg("row"), "Print row")
;
// Rows
@ -53,7 +96,20 @@ void define_sparse_matrix(py::module& m) {
.def("__iter__", [](storm::storage::SparseMatrix<double>::rows& rows) {
return py::make_iterator(rows.begin(), rows.end());
}, py::keep_alive<0, 1>())
.def("__str__", [](storm::storage::SparseMatrix<double>::rows& rows) {
.def("__str__", [](storm::storage::SparseMatrix<double>::const_rows& rows) {
std::stringstream stream;
for (auto transition : rows) {
stream << transition << ", ";
}
return stream.str();
})
;
py::class_<storm::storage::SparseMatrix<storm::RationalFunction>::rows>(m, "ParametricSparseMatrixRows", "Set of rows in a parametric sparse matrix")
.def("__iter__", [](storm::storage::SparseMatrix<storm::RationalFunction>::rows& rows) {
return py::make_iterator(rows.begin(), rows.end());
}, py::keep_alive<0, 1>())
.def("__str__", [](storm::storage::SparseMatrix<storm::RationalFunction>::const_rows& rows) {
std::stringstream stream;
for (auto transition : rows) {
stream << transition << ", ";

1
stormpy/src/storage/model.cpp
View File

@ -68,6 +68,7 @@ void define_model(py::module& m) {
}, "Get labels")
.def("labels_state", &storm::models::sparse::Model<storm::RationalFunction>::getLabelsOfState, "Get labels")
.def("initial_states", &getInitialStates<storm::RationalFunction>, "Get initial states")
.def("transition_matrix", &getTransitionMatrix<storm::RationalFunction>, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Get transition matrix")
;
py::class_<storm::models::sparse::Dtmc<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", py::base<storm::models::sparse::Model<storm::RationalFunction>>())
;

30
stormpy/tests/storage/test_matrix.py
View File

@ -63,3 +63,33 @@ class TestMatrix:
# Third model checking
result = stormpy.model_checking(model, formulas[0])
assert result == 0.3555555555555556 or result == 0.3555555555555557
def test_change_parametric_sparse_matrix_modelchecking(self):
import stormpy.logic
import pycarl
program = stormpy.parse_prism_program("../examples/pdtmc/brp/brp_16_2.pm")
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"target\" ]", program)
model = stormpy.build_parametric_model(program, formulas[0])
matrix = model.transition_matrix()
# Check matrix
one_pol = pycarl.Rational(1)
one_pol = pycarl.FactorizedPolynomial(one_pol)
one = pycarl.FactorizedRationalFunction(one_pol, one_pol)
for e in matrix:
assert e.value() == one or len(e.value().gather_variables()) > 0
# First model checking
result = stormpy.model_checking(model, formulas[0])
assert len(result.result_function().gather_variables()) > 0
# Change probabilities
two_pol = pycarl.Rational(2)
two_pol = pycarl.FactorizedPolynomial(two_pol)
new_val = pycarl.FactorizedRationalFunction(one_pol, two_pol)
for e in matrix:
if len(e.value().gather_variables()) > 0:
e.set_value(new_val)
for e in matrix:
assert e.value() == new_val or e.value() == one
# Second model checking
result = stormpy.model_checking(model, formulas[0])
assert len(result.result_function().gather_variables()) == 0
Write Preview
Loading…
Cancel
Save