renamed :phase to :layer

1 files changed, 38 insertions, 38 deletions

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index 9c1b7c9a..70fe1d4c 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -8,10 +8,10 @@ axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
 type X;

 function {:builtin "MapConst"} mapconstbool(bool): [X]bool;

 const nil: X;

-var {:phase 2} t: int;

-var {:phase 2} s: int;

-var {:phase 2} cs: X;

-var {:phase 2} T: [int]bool;

+var {:layer 2} t: int;

+var {:layer 2} s: int;

+var {:layer 2} cs: X;

+var {:layer 2} T: [int]bool;

 

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

 function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

@@ -34,10 +34,10 @@ function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool)
 }

 

 procedure Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

-ensures {:phase 1} {:phase 2} xl != nil;

+ensures {:layer 1} {:layer 2} xl != nil;

 

-procedure {:yields} {:phase 2} main({:linear_in "tid"} xls':[X]bool)

-requires {:phase 2} xls' == mapconstbool(true);

+procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool)

+requires {:layer 2} xls' == mapconstbool(true);

 {

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

     var {:linear "tid"} xls: [X]bool;

@@ -50,8 +50,8 @@ requires {:phase 2} xls' == mapconstbool(true);
     par Yield1() | Yield2();

 

     while (*)

-    invariant {:phase 1} Inv1(T, t);

-    invariant {:phase 2} Inv2(T, s, cs);

+    invariant {:layer 1} Inv1(T, t);

+    invariant {:layer 2} Inv2(T, s, cs);

     {

         call xls, tid := Allocate(xls);

         async call Customer(tid);

@@ -60,14 +60,14 @@ requires {:phase 2} xls' == mapconstbool(true);
     par Yield1() | Yield2();

 }

 

-procedure {:yields} {:phase 2} Customer({:linear_in "tid"} tid: X)

-requires {:phase 1} Inv1(T, t);

-requires {:phase 2} tid != nil && Inv2(T, s, cs);

+procedure {:yields} {:layer 2} Customer({:linear_in "tid"} tid: X)

+requires {:layer 1} Inv1(T, t);

+requires {:layer 2} tid != nil && Inv2(T, s, cs);

 {

     par Yield1() | Yield2();    

     while (*) 

-    invariant {:phase 1} Inv1(T, t);

-    invariant {:phase 2} Inv2(T, s, cs);

+    invariant {:layer 1} Inv1(T, t);

+    invariant {:layer 2} Inv2(T, s, cs);

     {

         call Enter(tid);

         par Yield1() | Yield2() | YieldSpec(tid);

@@ -77,11 +77,11 @@ requires {:phase 2} tid != nil && Inv2(T, s, cs);
     par Yield1() | Yield2();

 }

 

-procedure {:yields} {:phase 2} Enter({:linear "tid"} tid: X)

-requires {:phase 1} Inv1(T, t);

-ensures {:phase 1} Inv1(T,t);

-requires {:phase 2} tid != nil && Inv2(T, s, cs);

-ensures {:phase 2} Inv2(T, s, cs) && cs == tid;

+procedure {:yields} {:layer 2} Enter({:linear "tid"} tid: X)

+requires {:layer 1} Inv1(T, t);

+ensures {:layer 1} Inv1(T,t);

+requires {:layer 2} tid != nil && Inv2(T, s, cs);

+ensures {:layer 2} Inv2(T, s, cs) && cs == tid;

 {

     var m: int;

 

@@ -92,9 +92,9 @@ ensures {:phase 2} Inv2(T, s, cs) && cs == tid;
     par Yield1() | Yield2() | YieldSpec(tid);

 }

 

-procedure {:yields} {:phase 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int)

-requires {:phase 1} Inv1(T, t);

-ensures {:phase 1} Inv1(T, t);

+procedure {:yields} {:layer 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int)

+requires {:layer 1} Inv1(T, t);

+ensures {:layer 1} Inv1(T, t);

 ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|;

 {

     par Yield1();

@@ -102,39 +102,39 @@ ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|;
     par Yield1();

 }

 

-procedure {:yields} {:phase 2} YieldSpec({:linear "tid"} tid: X)

-requires {:phase 2} tid != nil && cs == tid;

-ensures {:phase 2} cs == tid;

+procedure {:yields} {:layer 2} YieldSpec({:linear "tid"} tid: X)

+requires {:layer 2} tid != nil && cs == tid;

+ensures {:layer 2} cs == tid;

 {

     yield;

-    assert {:phase 2} tid != nil && cs == tid;

+    assert {:layer 2} tid != nil && cs == tid;

 }

 

-procedure {:yields} {:phase 2} Yield2()

-requires {:phase 2} Inv2(T, s, cs);

-ensures {:phase 2} Inv2(T, s, cs);

+procedure {:yields} {:layer 2} Yield2()

+requires {:layer 2} Inv2(T, s, cs);

+ensures {:layer 2} Inv2(T, s, cs);

 {

     yield;

-    assert {:phase 2} Inv2(T, s, cs);

+    assert {:layer 2} Inv2(T, s, cs);

 }

 

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

-requires {:phase 1} Inv1(T, t);

-ensures {:phase 1} Inv1(T,t);

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

+requires {:layer 1} Inv1(T, t);

+ensures {:layer 1} Inv1(T,t);

 {

     yield;

-    assert {:phase 1} Inv1(T,t);

+    assert {:layer 1} Inv1(T,t);

 }

 

-procedure {:yields} {:phase 0,2} Init({:linear "tid"} xls:[X]bool);

+procedure {:yields} {:layer 0,2} Init({:linear "tid"} xls:[X]bool);

 ensures {:atomic} |{ A: assert xls == mapconstbool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;

 

-procedure {:yields} {:phase 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int);

+procedure {:yields} {:layer 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int);

 ensures {:atomic} |{ A: m := t; t := t + 1; T[m] := true; return true; }|;

 

-procedure {:yields} {:phase 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int);

+procedure {:yields} {:layer 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int);

 ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|;

 

-procedure {:yields} {:phase 0,2} Leave({:linear "tid"} tid: X);

+procedure {:yields} {:layer 0,2} Leave({:linear "tid"} tid: X);

 ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|;