renamed :phase to :layer

1 files changed, 9 insertions, 9 deletions

diff --git a/Test/og/Program4.bpl b/Test/og/Program4.bpl
index 5005f77c..61d4fcdc 100644
--- a/Test/og/Program4.bpl
+++ b/Test/og/Program4.bpl
@@ -13,11 +13,11 @@ function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
   x

 }

 

-var {:phase 1} a:[Tid]int;

+var {:layer 1} a:[Tid]int;

 

 procedure Allocate() returns ({:linear "tid"} tid:Tid); 

 

-procedure {:yields} {:phase 1} main() { 

+procedure {:yields} {:layer 1} main() { 

     var {:linear "tid"} tid:Tid;

 

     yield;

@@ -29,28 +29,28 @@ procedure {:yields} {:phase 1} main() {
     yield;

 }

 

-procedure {:yields} {:phase 1} P({:linear "tid"} tid: Tid) 

-ensures {:phase 1} a[tid] == old(a)[tid] + 1; 

+procedure {:yields} {:layer 1} P({:linear "tid"} tid: Tid) 

+ensures {:layer 1} a[tid] == old(a)[tid] + 1; 

 { 

     var t:int;

 

     yield;

-    assert {:phase 1} a[tid] == old(a)[tid];

+    assert {:layer 1} a[tid] == old(a)[tid];

     call t := Read(tid); 

     yield;

-    assert {:phase 1} a[tid] == t; 

+    assert {:layer 1} a[tid] == t; 

     call Write(tid, t + 1); 

     yield;

-    assert {:phase 1} a[tid] == t + 1; 

+    assert {:layer 1} a[tid] == t + 1; 

 }

 

-procedure {:yields} {:phase 0,1} Read({:linear "tid"} tid: Tid) returns (val: int);

+procedure {:yields} {:layer 0,1} Read({:linear "tid"} tid: Tid) returns (val: int);

 ensures {:atomic}

 |{A:

   val := a[tid]; return true;

 }|;

 

-procedure {:yields} {:phase 0,1} Write({:linear "tid"} tid: Tid, val: int);

+procedure {:yields} {:layer 0,1} Write({:linear "tid"} tid: Tid, val: int);

 ensures {:atomic}

 |{A:

   a[tid] := val; return true;