Rearrange CLHlock predicate for legibility.

septract · Feb 13, 2017 · cc137e1 · cc137e1
1 parent f05640e
commit cc137e1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/grasshopper/CLHlock-module.spl b/grasshopper/CLHlock-module.spl
@@ -11,7 +11,7 @@ requires acc(Foot) {
     && tail in Foot
     && Reach(pred, tail, head)
     && !head.lock
-    && (forall x : Node :: (x in Foot && !x.lock) ==> x.pred == null)
+    && (forall x : Node :: (x in Foot && x.pred != null) ==> x.lock)
 }
 
 predicate looseG(Foot : Set<Node>, a : Node, head : Node)