Currently saturation prints no debug information. So when some reachability computation takes a long time, it's now difficult to see why it's taking long or on what part it hangs. Note that there is a corresponding JavaBDD issue (https://github.com/com-github-javabdd/com.github.javabdd/issues/66) to adapt saturation on the side of JavaBDD. Once completed, CifBddReachability must be updated to make use of the added debug functionality, which will (probably) be a callback mechanism.
This was previously discussed at #911 (comment 2684234). I think we should print as debug output:
Whenever the reachable states change due to applying an edge with relnext/relprev, as we do in the other reachability computations.
Some kind of progress notion. Fixed order prints rounds, but for saturation we can do better. Since it saturations for a certain level, it can finish a level before moving to a next one. That gives concrete progress (level x/y). It is not linear progress as different levels may take different amounts of time, but still.
I think we should print the matrix with transition relations and what variables they use, which could give some sense of what to expect in terms of effort to be spent. Like a DSM, having relations only near the diagonal is ideal. This could be printed similarly to how we print a matrix for the workset dependency sets.
Dennis Hendrikschanged title from The saturation exploration strategy should provide debug information to CIF/BDD: The saturation exploration strategy should provide debug information
changed title from The saturation exploration strategy should provide debug information to CIF/BDD: The saturation exploration strategy should provide debug information
I took the partial work of @wytseoortwijn and turned it something more complete. I used it to create the matrices of #911 (comment 2841572). It provided to be quite useful to be able to print this.