Parametric sparse matrix builder and tests

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()
+

src/storage/matrix.cpp

@@ -63,9 +63,40 @@ void define_sparse_matrix(py::module& m) {
               :param std::vector<double> 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_<SparseMatrixBuilder<RationalFunction>>(m, "ParametricSparseMatrixBuilder", "Builder of parametric sparse matrix")
+            .def(py::init<double , double , double , bool , bool , double>(), "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<RationalFunction>::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_<SparseMatrixBuilder<RationalFunction>>(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<RationalFunction>::newRowGroup, py::arg("starting_row"), "Start a new row group in the matrix")
+            .def("build", &SparseMatrixBuilder<RationalFunction>::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<RationalFunction>::getLastRow, "Get the most recently used row")
+            .def("get_current_row_group_count", &SparseMatrixBuilder<RationalFunction>::getCurrentRowGroupCount, "Get the current row group count")
+            .def("get_last_column", &SparseMatrixBuilder<RationalFunction>::getLastColumn, "the most recently used column")
+            .def("replace_columns", &SparseMatrixBuilder<RationalFunction>::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<double> 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_<SparseMatrix<double>>(m, "SparseMatrix", "Sparse matrix")

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