Performance regression in finite response check after adding confluence check
This issue
When applying controller checks to supervisors, the finite response check don't resolve. I can get it working for smaller models (with 4 states) but for larger models (order of 10^20) it will not resolve: after an hour it is still running. This is curious since in version 0.6 the finite response check for the same model would be resolved in seconds.
In version 0.7 a confluence check has been added. Perhaps this is the cause of the performance degredation.
Related issues
This issue fixed the regression, but not the performance issues for the confluence check. See also:
- Issue #686 (closed) is about adding more debug/progress output, and more termination checks.
- Issue #693 (closed) is about making the conversion of updates to MDDs more efficient.
- Issue #695 is about making the check more efficient in general, as well as discussing BDDs, MDDs, and their implementations as it relates to these checks.
Edited by Dennis Hendriks