checkpoint

1 files changed, 31 insertions, 13 deletions

diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl
index 831d2b97..400f5a4e 100644
--- a/Test/og/foo.bpl
+++ b/Test/og/foo.bpl
@@ -1,37 +1,55 @@
-var g:int;

+var {:phase 1} g:int;

 

-procedure {:yields} {:stable} PB()

-modifies g;

+procedure {:yields} {:phase 1} PB()

 {

-  g := g + 1;

+  yield;

+  call Incr();

+  yield;

 }

 

-procedure {:yields} PC()

-ensures g == 3;

+procedure {:yields} {:phase 0,1} Incr();

+ensures {:atomic}

+|{A:

+  g := g + 1; return true;

+}|;

+

+procedure {:yields} {:phase 0,1} Set(v: int);

+ensures {:atomic}

+|{A:

+  g := v; return true;

+}|;

+

+procedure {:yields} {:phase 1} PC()

+ensures {:phase 1} g == 3;

 {

-  g := 3;

   yield;

-  assert g == 3;

+  call Set(3);

+  yield;

+  assert {:phase 1} g == 3;

 }

 

-procedure {:yields} {:stable} PE()

+procedure {:yields} {:phase 1} PE()

 {

   call PC();

 }

 

-procedure {:yields} {:stable} PD()

+procedure {:yields} {:phase 1} PD()

 {

   call PC();

-  assert g == 3;

-  yield;

+  assert {:phase 1} g == 3;

 }

 

-procedure {:entrypoint} {:yields} Main()

+procedure {:yields} {:phase 1} Main()

 {

+  yield;

   while (*)

   {

+    yield;

     async call PB();

+    yield;

     async call PE();

+    yield;

     async call PD();

+    yield;

   }

 }