Code cleanup and performance improvements for communication, allow/block and rename #1800
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
This seems a remnant of ancient history, when rest was stored as a pointer. To eliminate, we use the invariant rest[i].empty() == rest_is_null[i].
while (a != b = c) { S } is rather ugly and hard to understand. Replace this with the equivalent:
b = c;
while (a != b) { S ; b = c }
The previous refactoring showed that the body of the loop was executed at most once, and can be replaced by a simple if-then-else
if match_failed[i] == true, tmp[i] is never read anymore.
After refactoring, this code can be shared between can_communicate and might_communicate.
Due to the use of temporary date, can_communicate and might_communicate are tightly couple to comm_entry. This changeset makes this explicit, by pushing the functions into the comm_entry class as methods. This also nicely encapsulates the date contained in comm_entry.
rest[i].empty() iff rest_is_null[i] is not an invariant (we only know rest_is_null[i] implies rest[i].empty())
- Make lhs, rhs in comm_entry constant; this was already the case, but the intent is now also clear in the code. - Use references instead of copies in some places where appropriate.
r_is_null is true iff r.empty()
First step in refactoring this code. Using iterators should avoid a lot of copying and (re)allocation.
Ignore IDE files for Jetbrains
This now allows removing occursinterm in favour of search_free_variable.
Preparation for using std::multiset.
- One vector was copied in combining tuple lists. By using move semantics, we avoid creation and destruction of aterms - Multisets so far do not seem to prove an advantage, so we avoid their use.
Also fix bug that was caught by this test.
In case there were many matches of communication expressions in a single summand, first all possible combinations of matches were explored, and the corresponding condition and summand generated. So, for a single summand that matches n communication expressions, 2^n possible multiactions are generated. In practice, however, many of these multiactions contain actions that are either blocked, or that are not part of any multiaction in an allow set. I added two test cases that were very slow without this change, but that take hardly any time now. These cases are adapted from the mCRL2 translation of a Cordis model, for which without the modification mcrl22lps --no-alph takes 1550s, and with the modification it terminates in 11s.
This significantly cleans up the parameter lists of the methods used.
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.
This pull request has the following main changes:
Major performance improvement
When calculating the communication operator over a complex multiaction, for every combination of matching communication expressions, a new summand is generated. The reason for this are the open terms that can appear as parameters to the multiactions: the decision whether a communication actually succeeds depends on the valuation of the variables. Therefore, when calculating the operators, we do not yet know which of the communications will end up being successful, and we take this into account. If n communication expressions match, this gives rise to 2^n multiactions.
In practice, however, many of the multiactions that are generated will later be filtered out because they are not allowed, or they contain an action that is blocked. The optimization that is implemented is as follows:
Calculate the set of actions that appears in a multiaction in the allow set, and only add multiactions to the result in which all actions appear in this set of actions. This may still generate multiactions that are later removed by the allow, but it already avoids a significant amount of work.
For concrete examples of mCRL2 models generated from Cordis models, this reduces the time for mcrl22lps --no-alpha from 1550s to 11s; for some summands, the number of multiactions generated is reduced from 10^6 to just 1.
TODO