Skip to content

Commit

Permalink
BUGFIX : Fixes #5 issue
Browse files Browse the repository at this point in the history
Thanks to @francomazzanti for an easily reproducible bug report
  • Loading branch information
yanntm committed Jun 6, 2018
1 parent 9608b28 commit a1bee40
Showing 1 changed file with 5 additions and 2 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -283,7 +283,7 @@ public static void computeTransitionSupport(Transition t, Support tread, Support
* s1 :a = x;
* s2 :b = x;
* and have s1 <> s2 (commutative). The trick is that between s1 and s2, no variable read in x can written to.
* x is an arbitrary expression.
* x is an arbitrary expression that is independent of both a and b.
* This function works pretty well on some very specific patterns, but is a bit weak overall.
* TODO : Not sure it handles "if" statements gracefully.
* @param spec the spec whose action we are going to "improve" in place
Expand Down Expand Up @@ -337,7 +337,10 @@ public static void improveCommutativity(Specification spec) {
computeSupport(vref, vsupp);
Support rsupp = new Support();
computeSupport(ass.getRight(), rsupp);

if (rsupp.intersects(vsupp)) {
// e.g. a = a + 1 ; cannot do our trick
continue;
}
for (int j = i+1; j < t.getActions().size() ; j++) {
Statement a2 = t.getActions().get(j);

Expand Down

0 comments on commit a1bee40

Please sign in to comment.