renamed :phase to :layer

1 files changed, 23 insertions, 23 deletions

diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl
index 72dc4181..47dcc515 100644
--- a/Test/og/treiber-stack.bpl
+++ b/Test/og/treiber-stack.bpl
@@ -16,24 +16,24 @@ axiom (forall x: lmap, i: Node, v: Node :: dom(Add(x, i, v)) == dom(x)[i:=true]
 function Remove(x: lmap, i: Node): (lmap);

 axiom (forall x: lmap, i: Node :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));

 

-procedure {:yields} {:phase 0} ReadTopOfStack() returns (v:Node);

+procedure {:yields} {:layer 0} ReadTopOfStack() returns (v:Node);

 ensures {:right} |{ A: assume dom(Stack)[v] || dom(Used)[v]; return true; }|;

 

-procedure {:yields} {:phase 0} Load(i:Node) returns (v:Node);

+procedure {:yields} {:layer 0} Load(i:Node) returns (v:Node);

 ensures {:right} |{ A: assert dom(Stack)[i] || dom(Used)[i]; goto B,C;

 	            B: assume dom(Stack)[i]; v := map(Stack)[i]; return true; 

 		    C: assume !dom(Stack)[i]; return true; }|;

 

-procedure {:yields} {:phase 0} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap);

+procedure {:yields} {:layer 0} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap);

 ensures {:both} |{ A: assert dom(l_in)[i]; l_out := Add(l_in, i, v); return true; }|;

 

-procedure {:yields} {:phase 0} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);

+procedure {:yields} {:layer 0} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);

 ensures {:atomic} |{ A: assert dom(l_in)[newVal];

 		        goto B,C;

                         B: assume oldVal == TopOfStack; TopOfStack := newVal; l_out := EmptyLmap(); Stack := Add(Stack, newVal, map(l_in)[newVal]); r := true; return true;

 			C: assume oldVal != TopOfStack; l_out := l_in; r := false; return true; }|;

 

-procedure {:yields} {:phase 0} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool);

+procedure {:yields} {:layer 0} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool);

 ensures {:atomic} |{ A: goto B,C;

                         B: assume oldVal == TopOfStack; TopOfStack := newVal; Used := Add(Used, oldVal, map(Stack)[oldVal]); Stack := Remove(Stack, oldVal); r := true; return true;

 		        C: assume oldVal != TopOfStack; r := false; return true; }|;

@@ -50,10 +50,10 @@ function {:inline} Inv(TopOfStack: Node, Stack: lmap) : (bool)
 

 var {:linear "Node"} Used: lmap;

 

-procedure {:yields} {:phase 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap)

-requires {:phase 1} dom(x_lmap)[x];

-requires {:phase 1} Inv(TopOfStack, Stack);

-ensures {:phase 1} Inv(TopOfStack, Stack);

+procedure {:yields} {:layer 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap)

+requires {:layer 1} dom(x_lmap)[x];

+requires {:layer 1} Inv(TopOfStack, Stack);

+ensures {:layer 1} Inv(TopOfStack, Stack);

 ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; return true; }|;

 {

   var t: Node;

@@ -61,30 +61,30 @@ ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; ret
   var {:linear "Node"} t_lmap: lmap;

 

   yield;

-  assert {:phase 1} Inv(TopOfStack, Stack);

+  assert {:layer 1} Inv(TopOfStack, Stack);

   t_lmap := x_lmap;

   while (true)

-  invariant {:phase 1} dom(t_lmap) == dom(x_lmap);

-  invariant {:phase 1} Inv(TopOfStack, Stack);

+  invariant {:layer 1} dom(t_lmap) == dom(x_lmap);

+  invariant {:layer 1} Inv(TopOfStack, Stack);

   {

     call t := ReadTopOfStack();

     call t_lmap := Store(t_lmap, x, t);

     call g, t_lmap := TransferToStack(t, x, t_lmap); 

     if (g) {

-      assert {:phase 1} map(Stack)[x] == t;

+      assert {:layer 1} map(Stack)[x] == t;

       break;

     }

     yield; 

-    assert {:phase 1} dom(t_lmap) == dom(x_lmap);

-    assert {:phase 1} Inv(TopOfStack, Stack);

+    assert {:layer 1} dom(t_lmap) == dom(x_lmap);

+    assert {:layer 1} Inv(TopOfStack, Stack);

   }

   yield; 

-  assert {:expand} {:phase 1} Inv(TopOfStack, Stack);

+  assert {:expand} {:layer 1} Inv(TopOfStack, Stack);

 }

 

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

-requires {:phase 1} Inv(TopOfStack, Stack);

-ensures {:phase 1} Inv(TopOfStack, Stack);

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

+requires {:layer 1} Inv(TopOfStack, Stack);

+ensures {:layer 1} Inv(TopOfStack, Stack);

 ensures {:atomic} |{ var t: Node; 

                      A: assume TopOfStack != null; t := TopOfStack; Used := Add(Used, t, map(Stack)[t]); TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|;

 {

@@ -93,9 +93,9 @@ ensures {:atomic} |{ var t: Node;
   var t: Node;

 

   yield;

-  assert {:phase 1} Inv(TopOfStack, Stack);

+  assert {:layer 1} Inv(TopOfStack, Stack);

   while (true)

-  invariant {:phase 1} Inv(TopOfStack, Stack);

+  invariant {:layer 1} Inv(TopOfStack, Stack);

   {

     call t := ReadTopOfStack();

     if (t != null) {

@@ -106,10 +106,10 @@ ensures {:atomic} |{ var t: Node;
       }

     }

     yield;

-    assert {:phase 1} Inv(TopOfStack, Stack);

+    assert {:layer 1} Inv(TopOfStack, Stack);

   }

   yield;

-  assert {:phase 1} Inv(TopOfStack, Stack);

+  assert {:layer 1} Inv(TopOfStack, Stack);

 }

 

 function Equal([int]bool, [int]bool) returns (bool);