systematic renaming of phase to layer

4 files changed, 90 insertions, 91 deletions

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 9a2203c3..1dd350de 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -35,34 +35,34 @@ namespace Microsoft.Boogie
             {

                 AtomicActionInfo atomicAction = action as AtomicActionInfo;

                 if (atomicAction == null) continue;

-                foreach (int phaseNum in moverTypeChecker.AllLayerNums)

+                foreach (int layerNum in moverTypeChecker.AllLayerNums)

                 {

-                    if (action.phaseNum < phaseNum && phaseNum <= action.availableUptoLayerNum)

+                    if (action.createdAtLayerNum < layerNum && layerNum <= action.availableUptoLayerNum)

                     {

-                        if (!pools.ContainsKey(phaseNum))

+                        if (!pools.ContainsKey(layerNum))

                         {

-                            pools[phaseNum] = new HashSet<AtomicActionInfo>();

+                            pools[layerNum] = new HashSet<AtomicActionInfo>();

                         }

-                        pools[phaseNum].Add(atomicAction);

+                        pools[layerNum].Add(atomicAction);

                     }

                 }

             }

 

             Program program = moverTypeChecker.program;

             MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls);

-            foreach (int phaseNum1 in pools.Keys)

+            foreach (int layerNum1 in pools.Keys)

             {

-                foreach (AtomicActionInfo first in pools[phaseNum1])

+                foreach (AtomicActionInfo first in pools[layerNum1])

                 {

                     Debug.Assert(first.moverType != MoverType.Top);

                     if (first.moverType == MoverType.Atomic)

                         continue;

-                    foreach (int phaseNum2 in pools.Keys)

+                    foreach (int layerNum2 in pools.Keys)

                     {

-                        if (phaseNum2 < phaseNum1) continue;

-                        foreach (AtomicActionInfo second in pools[phaseNum2])

+                        if (layerNum2 < layerNum1) continue;

+                        foreach (AtomicActionInfo second in pools[layerNum2])

                         {

-                            if (second.phaseNum < phaseNum1)

+                            if (second.createdAtLayerNum < layerNum1)

                             {

                                 if (first.IsRightMover)

                                 {

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index f656da57..e485e1bc 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -14,7 +14,7 @@ namespace Microsoft.Boogie
     public class MyDuplicator : Duplicator

     {

         MoverTypeChecker moverTypeChecker;

-        public int phaseNum;

+        public int layerNum;

         Procedure enclosingProc;

         Implementation enclosingImpl;

         public Dictionary<Procedure, Procedure> procMap; /* Original -> Duplicate */

@@ -23,10 +23,10 @@ namespace Microsoft.Boogie
         public HashSet<Procedure> yieldingProcs;

         public List<Implementation> impls;

 

-        public MyDuplicator(MoverTypeChecker moverTypeChecker, int phaseNum)

+        public MyDuplicator(MoverTypeChecker moverTypeChecker, int layerNum)

         {

             this.moverTypeChecker = moverTypeChecker;

-            this.phaseNum = phaseNum;

+            this.layerNum = layerNum;

             this.enclosingProc = null;

             this.enclosingImpl = null;

             this.procMap = new Dictionary<Procedure, Procedure>();

@@ -38,12 +38,12 @@ namespace Microsoft.Boogie
 

         private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List<Cmd> newCmds)

         {

-            int enclosingProcLayerNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].phaseNum;

+            int enclosingProcLayerNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum;

             Procedure originalProc = originalCallCmd.Proc;

             if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc))

             {

                 AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo;

-                if (atomicActionInfo != null && atomicActionInfo.thisGate.Count > 0 && phaseNum == enclosingProcLayerNum)

+                if (atomicActionInfo != null && atomicActionInfo.thisGate.Count > 0 && layerNum == enclosingProcLayerNum)

                 {

                     newCmds.Add(new HavocCmd(Token.NoToken, new List<IdentifierExpr>(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) })));

                     Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();

@@ -66,11 +66,11 @@ namespace Microsoft.Boogie
             int maxCalleeLayerNum = 0;

             foreach (CallCmd iter in originalParCallCmd.CallCmds)

             {

-                int calleeLayerNum = moverTypeChecker.procToActionInfo[iter.Proc].phaseNum;

+                int calleeLayerNum = moverTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum;

                 if (calleeLayerNum > maxCalleeLayerNum)

                     maxCalleeLayerNum = calleeLayerNum;

             }

-            if (phaseNum > maxCalleeLayerNum)

+            if (layerNum > maxCalleeLayerNum)

             {

                 for (int i = 0; i < parCallCmd.CallCmds.Count; i++) 

                 {

@@ -150,13 +150,13 @@ namespace Microsoft.Boogie
             {

                 enclosingProc = node;

                 Procedure proc = (Procedure)node.Clone();

-                proc.Name = string.Format("{0}_{1}", node.Name, phaseNum);

+                proc.Name = string.Format("{0}_{1}", node.Name, layerNum);

                 proc.InParams = this.VisitVariableSeq(node.InParams);

                 proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies);

                 proc.OutParams = this.VisitVariableSeq(node.OutParams);

 

                 ActionInfo actionInfo = moverTypeChecker.procToActionInfo[node];

-                if (actionInfo.phaseNum < phaseNum)

+                if (actionInfo.createdAtLayerNum < layerNum)

                 {

                     proc.Requires = new List<Requires>();

                     proc.Ensures = new List<Ensures>();

@@ -220,7 +220,7 @@ namespace Microsoft.Boogie
             Requires requires = base.VisitRequires(node);

             if (node.Free)

                 return requires;

-            if (!moverTypeChecker.absyToLayerNums[node].Contains(phaseNum))

+            if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum))

                 requires.Condition = Expr.True;

             return requires;

         }

@@ -232,7 +232,7 @@ namespace Microsoft.Boogie
                 return ensures;

             AtomicActionInfo atomicActionInfo =  moverTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo;

             bool isAtomicSpecification = atomicActionInfo != null && atomicActionInfo.ensures == node;

-            if (isAtomicSpecification || !moverTypeChecker.absyToLayerNums[node].Contains(phaseNum))

+            if (isAtomicSpecification || !moverTypeChecker.absyToLayerNums[node].Contains(layerNum))

             {

                 ensures.Condition = Expr.True;

                 ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes);

@@ -243,7 +243,7 @@ namespace Microsoft.Boogie
         public override Cmd VisitAssertCmd(AssertCmd node)

         {

             AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node);

-            if (!moverTypeChecker.absyToLayerNums[node].Contains(phaseNum))

+            if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum))

                 assertCmd.Expr = Expr.True;

             return assertCmd;

         }

@@ -256,7 +256,7 @@ namespace Microsoft.Boogie
         Dictionary<Absy, Absy> absyMap;

         Dictionary<Implementation, Implementation> implMap;

         HashSet<Procedure> yieldingProcs;

-        int phaseNum;

+        int layerNum;

         List<IdentifierExpr> globalMods;

         Dictionary<string, Procedure> asyncAndParallelCallDesugarings;

         List<Procedure> yieldCheckerProcs;

@@ -274,7 +274,7 @@ namespace Microsoft.Boogie
             this.linearTypeChecker = linearTypeChecker;

             this.moverTypeChecker = moverTypeChecker;

             this.absyMap = duplicator.absyMap;

-            this.phaseNum = duplicator.phaseNum;

+            this.layerNum = duplicator.layerNum;

             this.implMap = duplicator.implMap;

             this.yieldingProcs = duplicator.yieldingProcs;

             Program program = linearTypeChecker.program;

@@ -319,7 +319,7 @@ namespace Microsoft.Boogie
                     Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);

                     inputs.Add(f);

                 }

-                yieldProc = new Procedure(Token.NoToken, string.Format("og_yield_{0}", phaseNum), new List<TypeVariable>(), inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());

+                yieldProc = new Procedure(Token.NoToken, string.Format("og_yield_{0}", layerNum), new List<TypeVariable>(), inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());

                 yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

             }

             CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List<IdentifierExpr>());

@@ -716,7 +716,7 @@ namespace Microsoft.Boogie
 

             Procedure originalProc = implMap[impl].Proc;

             ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc];

-            if (actionInfo.phaseNum == this.phaseNum)

+            if (actionInfo.createdAtLayerNum == this.layerNum)

             {

                 pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool));

                 newLocalVars.Add(pc);

@@ -742,11 +742,11 @@ namespace Microsoft.Boogie
                 HashSet<Variable> introducedVars = new HashSet<Variable>();

                 foreach (Variable v in program.GlobalVariables)

                 {

-                    if (moverTypeChecker.hideLayerNums[v] <= actionInfo.phaseNum || moverTypeChecker.introduceLayerNums[v] > actionInfo.phaseNum)

+                    if (moverTypeChecker.hideLayerNums[v] <= actionInfo.createdAtLayerNum || moverTypeChecker.introduceLayerNums[v] > actionInfo.createdAtLayerNum)

                     {

                         frame.Remove(v);

                     }

-                    if (moverTypeChecker.introduceLayerNums[v] == actionInfo.phaseNum)

+                    if (moverTypeChecker.introduceLayerNums[v] == actionInfo.createdAtLayerNum)

                     {

                         introducedVars.Add(v);

                     }

@@ -1159,11 +1159,11 @@ namespace Microsoft.Boogie
         public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)

         {

             Program program = linearTypeChecker.program;

-            foreach (int phaseNum in moverTypeChecker.AllLayerNums.Except(new int[] { 0 }))

+            foreach (int layerNum in moverTypeChecker.AllLayerNums.Except(new int[] { 0 }))

             {

-                if (CommandLineOptions.Clo.TrustLayersDownto <= phaseNum || phaseNum <= CommandLineOptions.Clo.TrustLayersUpto) continue;

+                if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue;

 

-                MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, phaseNum);

+                MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, layerNum);

                 foreach (var proc in program.Procedures)

                 {

                     if (!moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue;

@@ -1174,7 +1174,7 @@ namespace Microsoft.Boogie
                 OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator);

                 foreach (var impl in program.Implementations)

                 {

-                    if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].phaseNum < phaseNum)

+                    if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum)

                         continue;

                     Implementation duplicateImpl = duplicator.VisitImplementation(impl);

                     ogTransform.TransformImpl(duplicateImpl);

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index be40bbf0..39d75119 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -20,13 +20,13 @@ namespace Microsoft.Boogie
     public class ActionInfo

     {

         public Procedure proc;

-        public int phaseNum;

+        public int createdAtLayerNum;

         public int availableUptoLayerNum;

 

-        public ActionInfo(Procedure proc, int phaseNum, int availableUptoLayerNum)

+        public ActionInfo(Procedure proc, int createdAtLayerNum, int availableUptoLayerNum)

         {

             this.proc = proc;

-            this.phaseNum = phaseNum;

+            this.createdAtLayerNum = createdAtLayerNum;

             this.availableUptoLayerNum = availableUptoLayerNum;

         }

 

@@ -77,8 +77,8 @@ namespace Microsoft.Boogie
             get { return moverType == MoverType.Left || moverType == MoverType.Both; }

         }

 

-        public AtomicActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int phaseNum, int availableUptoLayerNum)

-            : base(proc, phaseNum, availableUptoLayerNum)

+        public AtomicActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int layerNum, int availableUptoLayerNum)

+            : base(proc, layerNum, availableUptoLayerNum)

         {

             CodeExpr codeExpr = ensures.Condition as CodeExpr;

             this.ensures = ensures;

@@ -216,13 +216,12 @@ namespace Microsoft.Boogie
         public Dictionary<Absy, HashSet<int>> absyToLayerNums;

         HashSet<Variable> auxVars;

 

-        private static List<int> FindIntAttributes(QKeyValue kv, string name)

+        private static List<int> FindLayers(QKeyValue kv)

         {

-            Contract.Requires(name != null);

             HashSet<int> attrs = new HashSet<int>();

             for (; kv != null; kv = kv.Next)

             {

-                if (kv.Key != name) continue;

+                if (kv.Key != "layer") continue;

                 foreach (var o in kv.Params)

                 {

                     Expr e = o as Expr;

@@ -232,9 +231,9 @@ namespace Microsoft.Boogie
                         attrs.Add(l.asBigNum.ToIntSafe);

                 }

             }

-            List<int> phases = attrs.ToList();

-            phases.Sort();

-            return phases;

+            List<int> layers = attrs.ToList();

+            layers.Sort();

+            return layers;

         }

 

         private static MoverType GetMoverType(Ensures e)

@@ -260,7 +259,7 @@ namespace Microsoft.Boogie
                     allLayerNums = new HashSet<int>();

                     foreach (ActionInfo actionInfo in procToActionInfo.Values)

                     {

-                        allLayerNums.Add(actionInfo.phaseNum);

+                        allLayerNums.Add(actionInfo.createdAtLayerNum);

                     }

                 }

                 return allLayerNums;

@@ -273,21 +272,21 @@ namespace Microsoft.Boogie
             {

                 if (!QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;

 

-                int phaseNum = int.MaxValue;

+                int layerNum = int.MaxValue;

                 int availableUptoLayerNum = int.MaxValue;

-                List<int> attrs = FindIntAttributes(proc.Attributes, "layer");

+                List<int> attrs = FindLayers(proc.Attributes);

                 if (attrs.Count == 1)

                 {

-                    phaseNum = attrs[0];

+                    layerNum = attrs[0];

                 }

                 else if (attrs.Count == 2)

                 {

-                    phaseNum = attrs[0];

+                    layerNum = attrs[0];

                     availableUptoLayerNum = attrs[1];

                 }

                 else

                 {

-                    Error(proc, "Incorrect number of phases");

+                    Error(proc, "Incorrect number of layers");

                     continue;

                 }

                 foreach (Ensures e in proc.Ensures)

@@ -313,7 +312,7 @@ namespace Microsoft.Boogie
                     enclosingImpl = null;

                     base.VisitEnsures(e);

                     canAccessSharedVars = false;

-                    if (maxLayerNum <= phaseNum && availableUptoLayerNum <= minLayerNum)

+                    if (maxLayerNum <= layerNum && availableUptoLayerNum <= minLayerNum)

                     {

                         // ok

                     }

@@ -322,11 +321,11 @@ namespace Microsoft.Boogie
                         Error(e, "A variable being accessed is hidden before this action becomes unavailable");

                     }

 

-                    procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, phaseNum, availableUptoLayerNum);

+                    procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, layerNum, availableUptoLayerNum);

                 }

                 if (!procToActionInfo.ContainsKey(proc))

                 {

-                    procToActionInfo[proc] = new ActionInfo(proc, phaseNum, availableUptoLayerNum);

+                    procToActionInfo[proc] = new ActionInfo(proc, layerNum, availableUptoLayerNum);

                 }

             }

             if (errorCount > 0) return;

@@ -353,25 +352,25 @@ namespace Microsoft.Boogie
             this.maxLayerNum = -1;

             foreach (var g in program.GlobalVariables)

             {

-                List<int> phaseNums = FindIntAttributes(g.Attributes, "layer");

+                List<int> layerNums = FindLayers(g.Attributes);

                 this.introduceLayerNums[g] = 0;

                 this.hideLayerNums[g] = int.MaxValue;

-                if (phaseNums.Count == 0)

+                if (layerNums.Count == 0)

                 {

                     // ok

                 }

-                else if (phaseNums.Count == 1)

+                else if (layerNums.Count == 1)

                 {

-                    this.hideLayerNums[g] = phaseNums[0];

+                    this.hideLayerNums[g] = layerNums[0];

                 }

-                else if (phaseNums.Count == 2)

+                else if (layerNums.Count == 2)

                 {

-                    this.introduceLayerNums[g] = phaseNums[0];

-                    this.hideLayerNums[g] = phaseNums[1];

+                    this.introduceLayerNums[g] = layerNums[0];

+                    this.hideLayerNums[g] = layerNums[1];

                 }

                 else

                 {

-                    Error(g, "Too many phase numbers");

+                    Error(g, "Too many layer numbers");

                 }

             }

         }

@@ -408,7 +407,7 @@ namespace Microsoft.Boogie
 

         public override Cmd VisitCallCmd(CallCmd node)

         {

-            int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].phaseNum;

+            int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].createdAtLayerNum;

             if (procToActionInfo.ContainsKey(node.Proc))

             {

                 ActionInfo actionInfo = procToActionInfo[node.Proc];

@@ -416,11 +415,11 @@ namespace Microsoft.Boogie
                 {

                     Error(node, "Target of async call cannot be an atomic action");

                 }

-                int calleeLayerNum = procToActionInfo[node.Proc].phaseNum;

+                int calleeLayerNum = procToActionInfo[node.Proc].createdAtLayerNum;

                 if (enclosingProcLayerNum < calleeLayerNum ||

                     (enclosingProcLayerNum == calleeLayerNum && actionInfo is AtomicActionInfo))

                 {

-                    Error(node, "The phase of the caller procedure must be greater than the phase of the callee");

+                    Error(node, "The layer of the caller must be greater than the layer of the callee");

                 }

                 else if (enclosingProcLayerNum == calleeLayerNum && enclosingImpl.OutParams.Count > 0)

                 {

@@ -439,7 +438,7 @@ namespace Microsoft.Boogie
                 }

                 if (actionInfo.availableUptoLayerNum < enclosingProcLayerNum)

                 {

-                    Error(node, "The callee is not available in the phase of the caller procedure");

+                    Error(node, "The callee is not available in the caller procedure");

                 }

             }

             return base.VisitCallCmd(node);

@@ -447,7 +446,7 @@ namespace Microsoft.Boogie
 

         public override Cmd VisitParCallCmd(ParCallCmd node)

         {

-            int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].phaseNum;

+            int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].createdAtLayerNum;

             bool isLeftMover = true;

             bool isRightMover = true;

             int maxCalleeLayerNum = 0;

@@ -457,9 +456,9 @@ namespace Microsoft.Boogie
                 ActionInfo actionInfo = procToActionInfo[iter.Proc];

                 isLeftMover = isLeftMover && actionInfo.IsLeftMover;

                 isRightMover = isRightMover && actionInfo.IsRightMover;

-                if (actionInfo.phaseNum > maxCalleeLayerNum)

+                if (actionInfo.createdAtLayerNum > maxCalleeLayerNum)

                 { 

-                    maxCalleeLayerNum = actionInfo.phaseNum; 

+                    maxCalleeLayerNum = actionInfo.createdAtLayerNum; 

                 }

                 if (actionInfo is AtomicActionInfo)

                 {

@@ -472,7 +471,7 @@ namespace Microsoft.Boogie
             }

             if (maxCalleeLayerNum == enclosingProcLayerNum && numAtomicActions > 0)

             {

-                Error(node, "If some callee in the parallel call has the same phase as the enclosing procedure, then no callee can be an atomic action");

+                Error(node, "If some callee in the parallel call has the same layer as the enclosing procedure, then no callee can be an atomic action");

             }

             return base.VisitParCallCmd(node);

         }

@@ -541,7 +540,7 @@ namespace Microsoft.Boogie
             }

             else

             {

-                CheckAndAddLayers(ensures, ensures.Attributes, actionInfo.phaseNum);

+                CheckAndAddLayers(ensures, ensures.Attributes, actionInfo.createdAtLayerNum);

             }

             return ret;

         }

@@ -553,7 +552,7 @@ namespace Microsoft.Boogie
             canAccessSharedVars = true;

             Requires ret = base.VisitRequires(requires);

             canAccessSharedVars = false;

-            CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].phaseNum);

+            CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].createdAtLayerNum);

             return ret;

         }

 

@@ -568,32 +567,32 @@ namespace Microsoft.Boogie
             Cmd ret = base.VisitAssertCmd(node);

             canAccessAuxVars = false;

             canAccessSharedVars = false;

-            CheckAndAddLayers(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].phaseNum);

+            CheckAndAddLayers(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].createdAtLayerNum);

             return ret;

         }

 

         private void CheckAndAddLayers(Absy node, QKeyValue attributes, int enclosingProcLayerNum)

         {

-            List<int> attrs = FindIntAttributes(attributes, "layer");

+            List<int> attrs = FindLayers(attributes);

             if (attrs.Count == 0)

             {

-                Error(node, "phase not present");

+                Error(node, "layer not present");

                 return;

             }

             absyToLayerNums[node] = new HashSet<int>();

-            foreach (int phaseNum in attrs)

+            foreach (int layerNum in attrs)

             {

-                if (phaseNum > enclosingProcLayerNum)

+                if (layerNum > enclosingProcLayerNum)

                 {

-                    Error(node, "The phase cannot be greater than the phase of enclosing procedure");

+                    Error(node, "The layer cannot be greater than the layer of enclosing procedure");

                 }

-                else if (maxLayerNum < phaseNum && phaseNum <= minLayerNum)

+                else if (maxLayerNum < layerNum && layerNum <= minLayerNum)

                 {

-                    absyToLayerNums[node].Add(phaseNum);

+                    absyToLayerNums[node].Add(layerNum);

                 }

                 else

                 {

-                    Error(node, string.Format("A variable being accessed in this specification is unavailable at phase {0}", phaseNum));

+                    Error(node, string.Format("A variable being accessed in this specification is unavailable at layer {0}", layerNum));

                 }

             }

         }

diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index 345841aa..8e844ede 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -81,7 +81,7 @@ namespace Microsoft.Boogie
             Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();

             if (simulationRelation[initialState].Count == 0)

             {

-                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at phase {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum));

+                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at layer {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum));

             }

         }

 

@@ -97,7 +97,7 @@ namespace Microsoft.Boogie
             Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();

             if (simulationRelation[initialState].Count == 0)

             {

-                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at phase {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum));

+                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at layer {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum));

             }

         }

 

@@ -115,7 +115,7 @@ namespace Microsoft.Boogie
             Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();

             if (simulationRelation[initialState].Count == 0)

             {

-                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at phase {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum));

+                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at layer {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum));

             }

         }

 

@@ -136,15 +136,15 @@ namespace Microsoft.Boogie
         {

             foreach (var impl in moverTypeChecker.program.Implementations)

             {

-                if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].phaseNum == 0) continue;

+                if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum == 0) continue;

                 impl.PruneUnreachableBlocks();

                 Graph<Block> implGraph = Program.GraphFromImpl(impl);

                 implGraph.ComputeLoops();

-                int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].phaseNum;

-                foreach (int phaseNum in moverTypeChecker.AllLayerNums)

+                int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum;

+                foreach (int layerNum in moverTypeChecker.AllLayerNums)

                 {

-                    if (phaseNum > specLayerNum) continue;

-                    YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, phaseNum, implGraph.Headers);

+                    if (layerNum > specLayerNum) continue;

+                    YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, layerNum, implGraph.Headers);

                 }

             }

         }

@@ -227,7 +227,7 @@ namespace Microsoft.Boogie
                         if (callCmd.IsAsync)

                         {

                             ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];

-                            if (currLayerNum <= actionInfo.phaseNum)

+                            if (currLayerNum <= actionInfo.createdAtLayerNum)

                                 edgeLabels[edge] = 'L';

                             else

                                 edgeLabels[edge] = 'B';

@@ -240,7 +240,7 @@ namespace Microsoft.Boogie
                         {

                             MoverType moverType;

                             ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];

-                            if (actionInfo.phaseNum >= currLayerNum)

+                            if (actionInfo.createdAtLayerNum >= currLayerNum)

                             {

                                 moverType = MoverType.Top;

                             }

@@ -280,7 +280,7 @@ namespace Microsoft.Boogie
                         bool isLeftMover = true;

                         foreach (CallCmd callCmd in parCallCmd.CallCmds)

                         {

-                            if (moverTypeChecker.procToActionInfo[callCmd.Proc].phaseNum >= currLayerNum)

+                            if (moverTypeChecker.procToActionInfo[callCmd.Proc].createdAtLayerNum >= currLayerNum)

                             {

                                 isYield = true;

                             }