diff --git a/grasshopper/CLHlock-module.spl b/grasshopper/CLHlock-module.spl index 455609b..9668aca 100644 --- 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, a : Node, head : Node)