For some very large models, the creation of each update function BDD can take a long time. For example, take the model considered here. Technically, the functions "only" take several hundred thousand nodes at most. But it takes a very long time to evaluate them, and it also could be memory consuming.
One possible solution is given in faster-fnupdate-eval branch, where a smarter, greedy evaluation algorithm is proposed. Instead of following the AST of the formula exactly, it first evaluates smaller chunks of the tree (in terms of symbolic size). Also, it applies distributive laws during evaluation to simplify the formula once it is partially evaluated (if we were to apply them from the start, the formula would explode).
Another possible solution would be to consider more advanced variable ordering techniques, since there doesn't seem to be anything fundamentally problematic about these particular functions.
Finally, it may be possible to "explode" the model using two approaches:
Assuming multiple "transition relations" per variable can be added (this is one of the goals for future design), we could stop evaluating the problematic FnUpdate and separate it into multiple transition relations instead.
A new "mediator" variable could be introduced to subdivide the function between multiple variables. The resulting system is obviously not equivalent, but due to the nature of the mediator variable should still result in equivalent attractors and other behavioral features.
For some very large models, the creation of each update function BDD can take a long time. For example, take the model considered here. Technically, the functions "only" take several hundred thousand nodes at most. But it takes a very long time to evaluate them, and it also could be memory consuming.
One possible solution is given in
faster-fnupdate-evalbranch, where a smarter, greedy evaluation algorithm is proposed. Instead of following the AST of the formula exactly, it first evaluates smaller chunks of the tree (in terms of symbolic size). Also, it applies distributive laws during evaluation to simplify the formula once it is partially evaluated (if we were to apply them from the start, the formula would explode).Another possible solution would be to consider more advanced variable ordering techniques, since there doesn't seem to be anything fundamentally problematic about these particular functions.
Finally, it may be possible to "explode" the model using two approaches:
FnUpdateand separate it into multiple transition relations instead.