Skip to content

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 the PrepareChecks 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 problematic computeUpdate 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.
Edited by Dennis Hendriks