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 theupdate
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 theupdate
method is returned from the method. The caller,processAutomaton
uses it to determineguardedUpdate
. It is subsequently used to updateautGuardedUpdates
andglobalGuardedUpdatesByEvent
.globalGuardedUpdatesByEvent
is a private field. It can only can be obtained via public methodgetGlobalGuardedUpdatesByEvent
.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