moves-rwth / storm

A Modern Probabilistic Model Checker
https://www.stormchecker.org
GNU General Public License v3.0
135 stars 74 forks source link

Fix assertion in SparseMatrix #571

Closed volkm closed 3 months ago

volkm commented 3 months ago

Assertion was violated for empty matrix.

sjunges commented 3 months ago

Is it on purpose that I can now iterate over row 20 if there are no rows, but i cannot iterate over row 20 if there are 5 rows?

volkm commented 3 months ago

Good point. I revised the assertion.

sjunges commented 3 months ago

Thanks, but what is the use case to be able to iterate over a non-existing row?

volkm commented 3 months ago

In my view, it should be possible to create an empty matrix. But then the new test in this PR fails, because in the constructor we call updateNonzeroEntryCount which tries to iterate over all entries. My goal is to support the iterators for empty matrices as well, such that for example begin() != end() always works.

sjunges commented 3 months ago

I agree that begin() should work, but I dont know whether begin(0) needs to work?

volkm commented 3 months ago

I think we need to support 0 because it is the default argument for begin().

sjunges commented 3 months ago

I see. Then I am ok with this solution, but would personally have considered seperating the implementation of the functions without argument.

The comment about the "end" code still stands? As in, shouldnt one be able to also call end(0) now?

tquatmann commented 3 months ago

I also think that begin() and begin(index_type row) should be two different overloads. Then, begin(i) is only valid iff row i exists and its the same for end.

volkm commented 3 months ago

Thanks for your comments. I decoupled begin() and begin(row). This is also now consistent with end which already had both these functions.

sjunges commented 3 months ago

LGTM