From 36e016acf963b7c19d59640b11b4a40f2072943e Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Sat, 3 May 2014 10:06:13 -0700
Subject: checkpoint

---
 Test/og/lock.bpl | 24 +++++++++++++++---------
 1 file changed, 15 insertions(+), 9 deletions(-)

(limited to 'Test/og/lock.bpl')

diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl
index 92b803a4..4a6e002d 100644
--- a/Test/og/lock.bpl
+++ b/Test/og/lock.bpl
@@ -1,14 +1,18 @@
-var {:qed} b: bool;
+var {:phase 2} b: bool;
 
-procedure {:yields} {:entrypoint} main()
+procedure {:yields} {:phase 2} main()
 {
     while (*)
     {
+        yield;
+
         async call Customer();
+
+        yield;
     }
 }
 
-procedure {:yields} {:stable} Customer()
+procedure {:yields} {:phase 2} Customer()
 {
     while (*) 
     {
@@ -19,13 +23,15 @@ procedure {:yields} {:stable} Customer()
     	yield;
 
     	call Leave();
+
+        yield;
     }
 
     yield;
 }
 
-procedure {:yields} Enter() 
-ensures {:atomic 1} |{ A: assume !b; b := true; return true; }|;
+procedure {:yields} {:phase 1,2} Enter() 
+ensures {:atomic} |{ A: assume !b; b := true; return true; }|;
 {
     var status: bool;
     yield;
@@ -44,12 +50,12 @@ ensures {:atomic 1} |{ A: assume !b; b := true; return true; }|;
 	goto L;
 }
 
-procedure {:yields} CAS(prev: bool, next: bool) returns (status: bool);
-ensures {:atomic 0} |{ 
+procedure {:yields} {:phase 0,2} CAS(prev: bool, next: bool) returns (status: bool);
+ensures {:atomic} |{ 
 A: goto B, C; 
 B: assume b == prev; b := next; status := true; return true; 
 C: status := false; return true; 
 }|;
 
-procedure {:yields} Leave();
-ensures {:atomic 0} |{ A: b := false; return true; }|;
+procedure {:yields} {:phase 0,2} Leave();
+ensures {:atomic} |{ A: b := false; return true; }|;
-- 
cgit v1.2.3