Controller checker: performance issue in converting updates of an edge to an MDD relation

Update conversion

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).

In particular related to the performance degredation of the 'PrepareChecks':

• The for loop in the update method where it gets stuck, is where identity updates are added for all variables that are not assigned on the edge. This prevents them from arbitrarily changing value. We do this in data-based synthesis as well.
• We noted that for BDDs in the data-based synthesis tool, the order in which we add the identity updates can matter a lot, performance-wise. Also, if you have a lot of variables, this can become large. The controller checker uses MDDs, not BDDs. I assume through that these performance characteristics likely hold for MDDs as well. Also note that our implementation of MDDs is nowhere near as optimized as the BDDs library that we use. So, we may be able to speed this up. However, none of this matters, as we'll see below.
• PrepareChecks has the 'problematic' update method where execution seems to stall. The computation within the update method is returned from the method. The caller, processAutomaton uses it to determine guardedUpdate. It is subsequently used to update autGuardedUpdates and globalGuardedUpdatesByEvent. globalGuardedUpdatesByEvent is a private field. It can only can be obtained via public method getGlobalGuardedUpdatesByEvent. ConfluenceChecker invokes that method, FiniteResponseChecker does not.

The particular issue described in #639 (closed) could be solved by avoiding this problematic update of the PrepareChecks when only FiniteResponseChecker is selected as check. Unfortunately, the performance issue is still there if one wants to check ConfluenceChecker. For example, the bridge example supplied with ESCET suffers from this issue. I haven't been able to perform the confluence check for this synthesized supervisor without getting impatient with the tool.

Related issues

• Issue #686 (closed) is about more progress/debug information and more termination checks.
• Issue #695 (closed) is about performance of the check in general, BDDs, MDDs, their implementations, etc. It was split of from this issue.

Addresses #892