diff --git a/stormpy/src/storage/matrix.cpp b/stormpy/src/storage/matrix.cpp index 526801232..4bc0644ee 100644 --- a/stormpy/src/storage/matrix.cpp +++ b/stormpy/src/storage/matrix.cpp @@ -3,6 +3,7 @@ #include "src/storage/SparseMatrix.h" typedef storm::storage::SparseMatrix::index_type entry_index; +typedef storm::storage::SparseMatrix::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::getColumn, "Column") ; + py::class_>(m, "ParametricSparseMatrixEntry", "Entry of parametric sparse matrix") + .def("__str__", [](storm::storage::MatrixEntry 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::getValue, "Value") + .def("set_value", &storm::storage::MatrixEntry::setValue, py::arg("value"), "Set value") + .def("column", &storm::storage::MatrixEntry::getColumn, "Column") + ; + + // SparseMatrix py::class_>(m, "SparseMatrix", "Sparse matrix") .def("__iter__", [](storm::storage::SparseMatrix& 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_>(m, "ParametricSparseMatrix", "Parametric sparse matrix") + .def("__iter__", [](storm::storage::SparseMatrix& 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 const& matrix) { + std::stringstream stream; + stream << matrix; + return stream.str(); }) + .def("nr_rows", &storm::storage::SparseMatrix::getRowCount, "Number of rows") + .def("nr_columns", &storm::storage::SparseMatrix::getColumnCount, "Number of columns") + .def("nr_entries", &storm::storage::SparseMatrix::getEntryCount, "Number of non-zero entries") + .def("_row_group_indices", &storm::storage::SparseMatrix::getRowGroupIndices, "Get starting rows of row groups") + .def("get_row", [](storm::storage::SparseMatrix& 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& 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 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::rows& rows) { return py::make_iterator(rows.begin(), rows.end()); }, py::keep_alive<0, 1>()) - .def("__str__", [](storm::storage::SparseMatrix::rows& rows) { + .def("__str__", [](storm::storage::SparseMatrix::const_rows& rows) { + std::stringstream stream; + for (auto transition : rows) { + stream << transition << ", "; + } + return stream.str(); + }) + ; + + py::class_::rows>(m, "ParametricSparseMatrixRows", "Set of rows in a parametric sparse matrix") + .def("__iter__", [](storm::storage::SparseMatrix::rows& rows) { + return py::make_iterator(rows.begin(), rows.end()); + }, py::keep_alive<0, 1>()) + .def("__str__", [](storm::storage::SparseMatrix::const_rows& rows) { std::stringstream stream; for (auto transition : rows) { stream << transition << ", "; diff --git a/stormpy/src/storage/model.cpp b/stormpy/src/storage/model.cpp index 7932dc2d1..0f29cac93 100644 --- a/stormpy/src/storage/model.cpp +++ b/stormpy/src/storage/model.cpp @@ -68,6 +68,7 @@ void define_model(py::module& m) { }, "Get labels") .def("labels_state", &storm::models::sparse::Model::getLabelsOfState, "Get labels") .def("initial_states", &getInitialStates, "Get initial states") + .def("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Get transition matrix") ; py::class_, std::shared_ptr>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", py::base>()) ; diff --git a/stormpy/tests/storage/test_matrix.py b/stormpy/tests/storage/test_matrix.py index 0f02f3193..3310bb1fe 100644 --- a/stormpy/tests/storage/test_matrix.py +++ b/stormpy/tests/storage/test_matrix.py @@ -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