fix: peterson create spec

nyu-acsys · Nov 12, 2024 · f367cff · f367cff
1 parent a4c75ff
commit f367cff
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/test/comparison/peterson.rav b/test/comparison/peterson.rav
@@ -44,7 +44,9 @@ module Peterson[R: LockResource]
         returns (l: Ref)
         requires resource(r)
         ensures peterson_inv(l, r)
+        ensures own(l.wait_left, false, 0.5)
         ensures own(l.active_left, false, 0.5)
+        ensures own(l.wait_right, false, 0.5)
         ensures own(l.active_right, false, 0.5)
     {
         l := new(