cosmetics

nyu-acsys · Nov 3, 2024 · 10c098b · 10c098b
1 parent f0f8876
commit 10c098b
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/test/concurrent/lock/ticket-lock.rav b/test/concurrent/lock/ticket-lock.rav
@@ -26,8 +26,7 @@ module TicketLock[R: LockResource]
         own(l, next, n, 1.0)
         && own(l, curr, c, 1.0)
         && n >= 0
-        && (b ==> own(l, tickets, ADS.frag(IntSet.set({|c|}))))
-        && (!b ==> resource(r))
+        && (b ? own(l, tickets, ADS.frag(IntSet.set({|c|}))) : resource(r))
         && own(l, tickets,
           ADS.auth_frag(
             IntSet.set({| i: Int :: 0 <= i && i < n |}),
@@ -135,8 +134,7 @@ module TicketLock[R: LockResource]
 
     val c1: Int := c+1;
     unfold lock_inv(l, r){ b :| b};
-    assert b;
-
+
     l.curr := c1;
 
     fold lock_inv(l, r)[b := false];