When applying controller checks to supervisors, the finite response check don't resolve. I can get it working for smaller models (with 4 states) but for larger models (order of 10^20) it will not resolve: after an hour it is still running.
This is curious since in version 0.6 the finite response check for the same model would be resolved in seconds.
In version 0.7 a confluence check has been added. Perhaps this is the cause of the performance degredation.
Related issues
This issue fixed the regression, but not the performance issues for the confluence check. See also:
Issue #686 (closed) is about adding more debug/progress output, and more termination checks.
Issue #693 (closed) is about making the conversion of updates to MDDs more efficient.
Issue #695 (closed) is about making the check more efficient in general, as well as discussing BDDs, MDDs, and their implementations as it relates to these checks.
This issue can be reproduced using the bridge example in our CIF examples repository. After synthesizing a supervisor using do1_synthesize.tooldef, checking finite response with ESCET v0.6 concludes within a few seconds that there is no finite response. Checking finite response (and disabling confluence checking in the tool options) does not terminate with ESCET v 0.10.
I also notice now that the user-triggert termination is not catched by the tool, so I had to force close ESCET v0.10.
The problem is somewhere in the PrepareChecks class (so it doesn't matter which, if any, controller check is selected). When I run the checks in debug mode, I get eventually stuck at this line.
It seems that tree.conjunct takes more and more time with each cycle of the for loop of the variables.
Looking at the titles of the merge requests that are part of %v0.7, I think we indeed need to look at !351 (merged), where the confluence check was added to the CIF controller property checker tool.
I dug a bit in into !351 (merged). Some observations:
The line that @mgoorden7u4 indicates the algorithm gets stuck, is introduced here.
The class was renamed, and the method changed a bit, here. The changes to the update method don't seem to consequential.
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.
When we introduced the confluence checker, some of the common calculations between the confluence checker and the finite response checker were moved from the finite response checker to a PrepareChecks class. However, computing updates is new for the finite response checker, as it did not yet have that, see here for the PrepareChecks class as introduced then, and here for the parts of the finite response checker that were (re)moved (Gitlab may not scroll to the right place by itself).
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.
So, my preliminary conclusion is that the confluence checker needs expensive computations, and these got added to the PrepareChecks that it shares with the finite response checker. The finite response checker does not need these extra computations, but nonetheless they are executed, leading to a severe performance regression.
@ahofkamp Do you remember why you added the updates to the shared class, while they are not needed for the finite response check? Could we just separate that again?
@koenveldik Thanks for reporting the issue. We solved it. Can you wait for the next Eclipse ESCET release at the end of September, or do you need this more urgently?
Dennis Hendrikschanged title from Performance regression in finite response checker to Performance regression in finite response check after adding confluence check
changed title from Performance regression in finite response checker to Performance regression in finite response check after adding confluence check