Confluence check: add more debug output and termination checks
This issue
In #639 (comment 1200624), it was noted that 'PrepareChecks' might take a lot of computational resources for the confluence checker (which were not needed for the finite response check).
For the finite response check, the problem was solved by disabling certain checks that are not necessary. But if one runs the confluence check on the bridge model in the CIF examples, it still takes a lot of computation time to perform the confluence check (so much time that I didn't had the patience to wait to let it finish; @koenveldik reported to me in private communication that he is waiting over 2 days for the confluence check to finish on a bridge model (not the CIF example)). Whether or not a faster algorithm or implementation exists for the prepare checks, there are two main end-user experience issues:
- In
debug
mode, nothing is printed to the console during thePrepareChecks
phase. Hence, the user has no idea whether the tool is doing something. Once the code would reach the actual confluence check, debug messages are coded to be printed. - Checking for requested termination is not performed once
PrepareChecks
reaches the problematiccomputeUpdate
part. Thus, a user has to close the ESCET application to terminate the tool.
Related issues
- Issue #693 (closed) is about improving the performance related to the conversion of updates to MDDs.
- Issue #695 (closed) is about improving the performance in general, and also discusses BDDs, MDDs, and their implementations.