SparseMatrixBuilder¶

class SparseMatrixBuilder[ValueType]( rows: SupportsInt | SupportsIndex = 0, columns: SupportsInt | SupportsIndex = 0, entries: SupportsInt | SupportsIndex = 0, force_dimensions: bool = True, has_custom_row_grouping: bool = False, row_groups: SupportsInt | SupportsIndex = 0, )¶

Builder of sparse matrix

Template arguments:

ValueType (type)

Available specializations:

SparseMatrixBuilder[float]
SparseMatrixBuilder[stormpy.numbers.Rational]
SparseMatrixBuilder[stormpy.numbers.Interval]
SparseMatrixBuilder[stormpy.numbers.RationalInterval]
SparseMatrixBuilder[stormpy.numbers.RationalFunction]

Construction

The default specialization is SparseMatrixBuilder[float].

Members¶

SparseMatrixBuilder.add_next_value()¶

For SparseMatrixBuilder[float]:

add_next_value(self: stormpy.datastructures.SparseMatrixBuilder[ValueType], row: typing.SupportsInt | typing.SupportsIndex, column: typing.SupportsInt | typing.SupportsIndex, value: typing.SupportsFloat | typing.SupportsIndex) -> None

Sets the matrix entry at the given row and column to the given value. After all entries have been added, calling function build() 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.

Parameters:

row (double) – The row in which the matrix entry is to be set
column (double) – The column in which the matrix entry is to be set
value (double) – The value that is to be set at the specified row and column

For SparseMatrixBuilder[stormpy.numbers.Rational], SparseMatrixBuilder[stormpy.numbers.Interval], SparseMatrixBuilder[stormpy.numbers.RationalInterval], SparseMatrixBuilder[stormpy.numbers.RationalFunction]:

add_next_value(self: stormpy.datastructures.SparseMatrixBuilder[ValueType], row: typing.SupportsInt | typing.SupportsIndex, column: typing.SupportsInt | typing.SupportsIndex, value: ValueType) -> None

Sets the matrix entry at the given row and column to the given value. After all entries have been added, calling function build() is mandatory.

Parameters:

row (double) – The row in which the matrix entry is to be set
column (double) – The column in which the matrix entry is to be set
value (double) – The value that is to be set at the specified row and column

SparseMatrixBuilder.add_next_values()¶

For SparseMatrixBuilder[float]:

add_next_values(self: stormpy.datastructures.SparseMatrixBuilder[ValueType], rows: collections.abc.Sequence[typing.SupportsInt | typing.SupportsIndex], cols: collections.abc.Sequence[typing.SupportsInt | typing.SupportsIndex], values: collections.abc.Sequence[typing.SupportsFloat | typing.SupportsIndex], row_group_indices: collections.abc.Sequence[typing.SupportsInt | typing.SupportsIndex] = []) -> None

Calls stormpy.storage.SparseMatrixBuilder.add_next_value() for each (row, col, value) triple. Accepts any sequence of scalars (e.g. plain Python lists).

Parameters:

rows (list[int]) – Row indices.
cols (list[int]) – Column indices.
values (list[float]) – Entry values.
row_group_indices (list[int]) – Starting row of each row group, in ascending order (optional).

add_next_values(self: stormpy.datastructures.SparseMatrixBuilder[ValueType], rows: collections.abc.Sequence[typing.SupportsInt | typing.SupportsIndex], cols: collections.abc.Sequence[typing.SupportsInt | typing.SupportsIndex], values: collections.abc.Sequence[ValueType], row_group_indices: collections.abc.Sequence[typing.SupportsInt | typing.SupportsIndex] = []) -> None

Calls stormpy.storage.SparseMatrixBuilder.add_next_value() for each (row, col, value) triple. Accepts any sequence of scalars (e.g. plain Python lists).

Parameters:

rows (list[int]) – Row indices.
cols (list[int]) – Column indices.
values (list[float]) – Entry values.
row_group_indices (list[int]) – Starting row of each row group, in ascending order (optional).

SparseMatrixBuilder.build( self: stormpy.datastructures.SparseMatrixBuilder[ValueType], overridden_row_count: SupportsInt | SupportsIndex = 0, overridden_column_count: SupportsInt | SupportsIndex = 0, overridden_row_group_count: SupportsInt | SupportsIndex = 0, )¶: Finalize the sparse matrix

SparseMatrixBuilder.get_current_row_group_count( self: stormpy.datastructures.SparseMatrixBuilder[ValueType], ) → int¶: Get the current row group count

SparseMatrixBuilder.get_last_column( self: stormpy.datastructures.SparseMatrixBuilder[ValueType], ) → int¶: the most recently used column

SparseMatrixBuilder.get_last_row(self: stormpy.datastructures.SparseMatrixBuilder[ValueType]) → int¶: Get the most recently used row

SparseMatrixBuilder.new_row_group( self: stormpy.datastructures.SparseMatrixBuilder[ValueType], starting_row: SupportsInt | SupportsIndex, ) → None¶: Start a new row group in the matrix

SparseMatrixBuilder.replace_columns( self: stormpy.datastructures.SparseMatrixBuilder[ValueType], replacements: collections.abc.Sequence[SupportsInt | SupportsIndex], offset: SupportsInt | SupportsIndex, ) → None¶

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.

Parameters:

replacements (std::vector<double> const&) – replacements Mapping indicating the replacements from offset+i -> value of i
offset (int) – Offset to add to each id in vector index.