diff --git a/lib/stormpy/storage/__init__.py b/lib/stormpy/storage/__init__.py index 93188a0..768dadc 100644 --- a/lib/stormpy/storage/__init__.py +++ b/lib/stormpy/storage/__init__.py @@ -8,22 +8,60 @@ def build_sparse_matrix(array, row_group_indices=[]): Build a sparse matrix from numpy array. :param numpy array: The array. - :param List[double] row_group_indices: List containing the starting row of each row group. + :param List[double] row_group_indices: List containing the starting row of each row group in ascending order. :return: Sparse matrix. """ + num_row = array.shape[0] num_col = array.shape[1] - if 0 < len(row_group_indices): + len_group_indices = len(row_group_indices) + if len_group_indices > 0: builder = storage.SparseMatrixBuilder(rows=num_row, columns=num_col, has_custom_row_grouping=True, row_groups=len(row_group_indices)) else: builder = storage.SparseMatrixBuilder(rows=num_row, columns=num_col) + row_group_index = 0 for r in range(num_row): - if r in row_group_indices: + # check whether to start a custom row group + if row_group_index < len_group_indices and r == row_group_indices[row_group_index]: builder.new_row_group(r) + row_group_index += 1 + # insert values of the current row for c in range(num_col): builder.add_next_value(r, c, array[r, c]) return builder.build() + +def build_parametric_sparse_matrix(array, row_group_indices=[]): + """ + Build a sparse matrix from numpy array. + + :param numpy array: The array. + :param List[double] row_group_indices: List containing the starting row of each row group in ascending order. + :return: Parametric sparse matrix. + """ + + num_row = array.shape[0] + num_col = array.shape[1] + + len_group_indices = len(row_group_indices) + if len_group_indices > 0: + builder = storage.ParametricSparseMatrixBuilder(rows=num_row, columns=num_col, has_custom_row_grouping=True, + row_groups=len(row_group_indices)) + else: + builder = storage.ParametricSparseMatrixBuilder(rows=num_row, columns=num_col) + + row_group_index = 0 + for r in range(num_row): + # check whether to start a custom row group + if row_group_index < len_group_indices and r == row_group_indices[row_group_index]: + builder.new_row_group(r) + row_group_index += 1 + # insert values of the current row + for c in range(num_col): + builder.add_next_value(r, c, array[r, c]) + + return builder.build() + diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp index 6149e37..d39224b 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -63,9 +63,40 @@ void define_sparse_matrix(py::module& m) { :param std::vector const& replacements: replacements Mapping indicating the replacements from offset+i -> value of i :param double offset: Offset to add to each id in vector index. )dox", py::arg("replacements"), py::arg("offset")) - ; + ; + + py::class_>(m, "ParametricSparseMatrixBuilder", "Builder of parametric sparse matrix") + .def(py::init(), "rows"_a = 0, "columns"_a = 0, "entries"_a = 0, "force_dimensions"_a = true, "has_custom_row_grouping"_a = false, "row_groups"_a = 0) + + .def("add_next_value", &SparseMatrixBuilder::addNextValue, R"dox( + + Sets the matrix entry at the given row and column to the given value. After all entries have been added, + a call to finalize(false) is mandatory. + + Note: this is a linear setter. That is, it must be called consecutively for each entry, row by row and + column by column. As multiple entries per column are admitted, consecutive calls to this method are + admitted to mention the same row-column-pair. If rows are skipped entirely, the corresponding rows are + treated as empty. If these constraints are not met, an exception is thrown. - // todo py::class_>(m, "SparseMatrixBuilder", "Builder of parametric sparse matrix") + :param double row: The row in which the matrix entry is to be set + :param double column: The column in which the matrix entry is to be set + :param RationalFunction const& value: The value that is to be set at the specified row and column + )dox", py::arg("row"), py::arg("column"), py::arg("value")) + + .def("new_row_group", &SparseMatrixBuilder::newRowGroup, py::arg("starting_row"), "Start a new row group in the matrix") + .def("build", &SparseMatrixBuilder::build, py::arg("overridden_row_count") = 0, py::arg("overridden_column_count") = 0, py::arg("overridden-row_group_count") = 0, "Finalize the sparse matrix") + .def("get_last_row", &SparseMatrixBuilder::getLastRow, "Get the most recently used row") + .def("get_current_row_group_count", &SparseMatrixBuilder::getCurrentRowGroupCount, "Get the current row group count") + .def("get_last_column", &SparseMatrixBuilder::getLastColumn, "the most recently used column") + .def("replace_columns", &SparseMatrixBuilder::replaceColumns, R"dox( + + Replaces all columns with id >= offset according to replacements. + Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted. + + :param std::vector const& replacements: replacements Mapping indicating the replacements from offset+i -> value of i + :param double offset: Offset to add to each id in vector index. + )dox", py::arg("replacements"), py::arg("offset")) + ; // SparseMatrix py::class_>(m, "SparseMatrix", "Sparse matrix") diff --git a/tests/storage/test_matrix_builder.py b/tests/storage/test_matrix_builder.py index ca0eaec..62e1d8e 100644 --- a/tests/storage/test_matrix_builder.py +++ b/tests/storage/test_matrix_builder.py @@ -33,6 +33,44 @@ class TestMatrixBuilder: for e in matrix_5x5: assert (e.value() == 0.1 and e.column == 1) or e.value() == 0 or (e.value() > 20 and e.column > 1) + def test_parametric_matrix_builder(self): + builder = stormpy.ParametricSparseMatrixBuilder(force_dimensions=True) + matrix = builder.build() + assert matrix.nr_columns == 0 + assert matrix.nr_rows == 0 + assert matrix.nr_entries == 0 + + builder_5x5 = stormpy.ParametricSparseMatrixBuilder(5, 5, force_dimensions=False) + + one_pol = stormpy.RationalRF(1) + one_pol = stormpy.FactorizedPolynomial(one_pol) + first_val = stormpy.FactorizedRationalFunction(one_pol) + + two_pol = stormpy.RationalRF(2) + two_pol = stormpy.FactorizedPolynomial(two_pol) + sec_val = stormpy.FactorizedRationalFunction(two_pol) + + builder_5x5.add_next_value(0, 0, first_val) + builder_5x5.add_next_value(0, 1, first_val) + builder_5x5.add_next_value(2, 2, sec_val) + builder_5x5.add_next_value(2, 3, sec_val) + + assert builder_5x5.get_last_column() == 3 + assert builder_5x5.get_last_row() == 2 + + builder_5x5.add_next_value(3, 2, sec_val) + builder_5x5.add_next_value(3, 4, sec_val) + builder_5x5.add_next_value(4, 3, sec_val) + + matrix_5x5 = builder_5x5.build() + + assert matrix_5x5.nr_columns == 5 + assert matrix_5x5.nr_rows == 5 + assert matrix_5x5.nr_entries == 7 + + for e in matrix_5x5: + assert (e.value() == first_val and e.column < 2) or (e.value() == sec_val and e.column > 1) + def test_matrix_replace_columns(self): builder = stormpy.SparseMatrixBuilder(3, 4, force_dimensions=False) @@ -58,10 +96,43 @@ class TestMatrixBuilder: # Check if columns where replaced for e in matrix: assert (e.value() == 0 and e.column == 0) or (e.value() == 3 and e.column == 1) or ( - e.value() == 2 and e.column == 2) or (e.value() == 1 and e.column == 3) + e.value() == 2 and e.column == 2) or (e.value() == 1 and e.column == 3) - def test_matrix_builder_row_grouping(self): + def test_parametric_matrix_replace_columns(self): + builder = stormpy.ParametricSparseMatrixBuilder(3, 4, force_dimensions=False) + + one_pol = stormpy.RationalRF(1) + one_pol = stormpy.FactorizedPolynomial(one_pol) + first_val = stormpy.FactorizedRationalFunction(one_pol, one_pol) + two_pol = stormpy.RationalRF(2) + two_pol = stormpy.FactorizedPolynomial(two_pol) + sec_val = stormpy.FactorizedRationalFunction(two_pol, two_pol) + third_val = stormpy.FactorizedRationalFunction(one_pol, two_pol) + + builder.add_next_value(0, 1, first_val) + builder.add_next_value(0, 2, sec_val) + builder.add_next_value(0, 3, third_val) + + builder.add_next_value(1, 1, first_val) + builder.add_next_value(1, 2, sec_val) + builder.add_next_value(1, 3, third_val) + + builder.add_next_value(2, 1, first_val) + builder.add_next_value(2, 2, sec_val) + builder.add_next_value(2, 3, third_val) + + # replace rows + builder.replace_columns([3, 2], 2) + matrix = builder.build() + + assert matrix.nr_entries == 9 + + # Check if columns where replaced + for e in matrix: + assert (e.value() == first_val and e.column == 1) or (e.value() == third_val and e.column == 2) or ( + e.value() == sec_val and e.column == 3) + def test_matrix_builder_row_grouping(self): num_rows = 5 builder = stormpy.SparseMatrixBuilder(num_rows, 6, has_custom_row_grouping=True, row_groups=2) @@ -78,6 +149,23 @@ class TestMatrixBuilder: assert matrix.get_row_group_start(1) == 4 assert matrix.get_row_group_end(1) == 5 + def test_parametric_matrix_builder_row_grouping(self): + num_rows = 5 + builder = stormpy.ParametricSparseMatrixBuilder(num_rows, 6, has_custom_row_grouping=True, row_groups=2) + + builder.new_row_group(1) + assert builder.get_current_row_group_count() == 1 + + builder.new_row_group(4) + assert builder.get_current_row_group_count() == 2 + matrix = builder.build() + + assert matrix.get_row_group_start(0) == 1 + assert matrix.get_row_group_end(0) == 4 + + assert matrix.get_row_group_start(1) == 4 + assert matrix.get_row_group_end(1) == 5 + def test_matrix_from_numpy(self): array = np.array([[0, 2], [3, 4], @@ -97,6 +185,33 @@ class TestMatrixBuilder: for e in row: assert (e.value() == array[r, e.column]) + def test_parametric_matrix_from_numpy(self): + one_pol = stormpy.RationalRF(1) + one_pol = stormpy.FactorizedPolynomial(one_pol) + first_val = stormpy.FactorizedRationalFunction(one_pol, one_pol) + two_pol = stormpy.RationalRF(2) + two_pol = stormpy.FactorizedPolynomial(two_pol) + sec_val = stormpy.FactorizedRationalFunction(two_pol, two_pol) + third_val = stormpy.FactorizedRationalFunction(one_pol, two_pol) + + array = np.array([[sec_val, first_val], + [first_val, sec_val], + [sec_val, sec_val], + [third_val, third_val]]) + + matrix = stormpy.build_parametric_sparse_matrix(array) + + # Check matrix dimension + assert matrix.nr_rows == array.shape[0] + assert matrix.nr_columns == array.shape[1] + assert matrix.nr_entries == 8 + + # Check matrix values + for r in range(array.shape[1]): + row = matrix.get_row(r) + for e in row: + assert (e.value() == array[r, e.column]) + def test_matrix_from_numpy_row_grouping(self): array = np.array([[0, 2], [3, 4], @@ -122,3 +237,37 @@ class TestMatrixBuilder: assert matrix.get_row_group_start(1) == 3 assert matrix.get_row_group_end(1) == 4 + + def test_parametric_matrix_from_numpy_row_grouping(self): + one_pol = stormpy.RationalRF(1) + one_pol = stormpy.FactorizedPolynomial(one_pol) + first_val = stormpy.FactorizedRationalFunction(one_pol, one_pol) + two_pol = stormpy.RationalRF(2) + two_pol = stormpy.FactorizedPolynomial(two_pol) + sec_val = stormpy.FactorizedRationalFunction(two_pol, two_pol) + third_val = stormpy.FactorizedRationalFunction(one_pol, two_pol) + + array = np.array([[sec_val, first_val], + [first_val, sec_val], + [sec_val, sec_val], + [third_val, third_val]]) + + matrix = stormpy.build_parametric_sparse_matrix(array, row_group_indices=[1, 3]) + + # Check matrix dimension + assert matrix.nr_rows == array.shape[0] + assert matrix.nr_columns == array.shape[1] + assert matrix.nr_entries == 8 + + # Check matrix values + for r in range(array.shape[1]): + row = matrix.get_row(r) + for e in row: + assert (e.value() == array[r, e.column]) + + # Check row groups + assert matrix.get_row_group_start(0) == 1 + assert matrix.get_row_group_end(0) == 3 + + assert matrix.get_row_group_start(1) == 3 + assert matrix.get_row_group_end(1) == 4