Lumping fails with the new sparse matrix implementatation
|Reported by:||ivan.zapreev||Owned by:||ivan.zapreev|
With the DTMC lumping the wscl performance test was crushing.
Here is the reply by David N. Jansen and a fix
I think the problem is really a bug in bscc.c. visit_non_rec() sometimes adds states to a BSCC twice. That doesn't give large problems, only the size of a BSCC is then registered too large. I added a patch that includes a bugfix and an additional internal test as regression test. I took the .tra file from the CTMC lumping test because that file exposed the bug first, and I also found a very small .tra file that still shows the bug. Basically, visit_non_rec() proceeds as follows:
- Process state 0:
1.1. Push all successors of 0 onto dfs_stack, i.e. states 1 and 2
- Process state 2:
2.1. Push all successors of 2 onto dfs_stack, i.e. state 1
-- At this moment, state 1 is on the dfs_stack twice. It may be that the second time, it is no longer necessary to handle it. I found a small bugfix, but perhaps you can find a better one that doesn't handle state 1 twice in this situation.
I tried a few functional tests and the wscl performance test, which now works out fine (wscl03 fails, but that is due to the fact that MRMC now correctly sees that the Markov chain is ergodic).