renamed :phase to :layer

1 files changed, 12 insertions, 12 deletions

diff --git a/Test/og/Program5.bpl b/Test/og/Program5.bpl
index 51d5fe3c..af87eac5 100644
--- a/Test/og/Program5.bpl
+++ b/Test/og/Program5.bpl
@@ -5,8 +5,8 @@ const unique nil: Tid;
 function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;

 function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;

 

-var {:phase 0,3} Color:int;

-var {:phase 0,3} lock:Tid;

+var {:layer 0,3} Color:int;

+var {:layer 0,3} lock:Tid;

 

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

 {

@@ -26,14 +26,14 @@ function {:inline} White(i:int) returns(bool) { i == 1 }
 function {:inline} Gray(i:int) returns(bool) { i == 2 }

 function {:inline} Black(i:int) returns(bool) { i >= 3 }

 

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

-ensures {:phase 2} Color >= old(Color);

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

+ensures {:layer 2} Color >= old(Color);

 {

   yield;

-  assert {:phase 2} Color >= old(Color);

+  assert {:layer 2} Color >= old(Color);

 }

 

-procedure {:yields} {:phase 2,3} TopWriteBarrier({:linear "tid"} tid:Tid)

+procedure {:yields} {:layer 2,3} TopWriteBarrier({:linear "tid"} tid:Tid)

 ensures {:atomic} |{ A: assert tid != nil; goto B, C; 

                      B: assume White(Color); Color := GRAY(); return true; 

                      C: return true;}|;

@@ -46,7 +46,7 @@ ensures {:atomic} |{ A: assert tid != nil; goto B, C;
   yield;

 }

 

-procedure {:yields} {:phase 1,2} MidWriteBarrier({:linear "tid"} tid:Tid)

+procedure {:yields} {:layer 1,2} MidWriteBarrier({:linear "tid"} tid:Tid)

 ensures {:atomic} |{ A: assert tid != nil; goto B, C; 

                      B: assume White(Color); Color := GRAY(); return true; 

                      C: return true; }|;

@@ -60,18 +60,18 @@ ensures {:atomic} |{ A: assert tid != nil; goto B, C;
        yield;

 }

 

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

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

   ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;

 

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

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

   ensures {:left} |{ A: assert tid != nil; assert lock == tid; lock := nil; return true; }|;

 

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

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

   ensures {:atomic} |{A: assert tid != nil; assert lock == tid; Color := newCol; return true;}|;

 

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

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

   ensures {:both} |{A: assert tid != nil; assert lock == tid; col := Color; return true;}|;

 

-procedure {:yields} {:phase 1,2} GetColorNoLock() returns (col:int);

+procedure {:yields} {:layer 1,2} GetColorNoLock() returns (col:int);

   ensures {:atomic} |{A: col := Color; return true;}|;