Balance term structure for parallel composition operator. #1792
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Before applying alphabet reductions, in this commit we balance the term structure for parallel composition. When having p1 || ... || pn, this results in a term structure of depth log_2(n), instead of n. I have observed 10% speed increases in mcrl22lps on some examples due to this change.
Alphabet reductions performed repeated linear searches in the vector of equations to find a process identifier. In the worst case, every left-hand-side of an equation was searched for at least once. We now, instead, precompute a map of process identifier to equations, so the cost of lookup becomes O(log(n)) instead of O(n) where n is the number of equations. In my example with 413 equation, this leads to a 15% performance improvement.
We probably do not want to enable this by default, as it can change the order in which processes are combined. Inconvenient combinations of processes may lead to poor performance, especially when alphabet reductions are not enabled.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Before applying alphabet reductions, in this commit we balance the term structure for parallel composition. When having p1 || ... || pn, this results in a term structure of depth log_2(n), instead of n.
I have observed 10% speed increases in mcrl22lps on some examples due to this change.
If desired, we could make this an option of mcrl22lps, similar to --balance-summands.