first cut of refinement checking

7 files changed, 288 insertions, 718 deletions

diff --git a/Source/Concurrency/Concurrency.csproj b/Source/Concurrency/Concurrency.csproj
index 7d0febf5..8d7e3979 100644
--- a/Source/Concurrency/Concurrency.csproj
+++ b/Source/Concurrency/Concurrency.csproj
@@ -76,7 +76,6 @@
     <Compile Include="OwickiGries.cs" />

     <Compile Include="Program.cs" />

     <Compile Include="Properties\AssemblyInfo.cs" />

-    <Compile Include="RefinementCheck.cs" />

     <Compile Include="TypeCheck.cs" />

     <Compile Include="YieldTypeChecker.cs" />

   </ItemGroup>

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 76a4b098..d1e5929d 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -141,12 +141,12 @@ namespace Microsoft.Boogie
             }

         }

 

-        class TransitionRelationComputation

+        public class TransitionRelationComputation

         {

             private Program program;

-            private ActionInfo first;

-            private ActionInfo second;

-            private Stack<Block> dfsStack;

+            private ActionInfo first;  // corresponds to that*

+            private ActionInfo second; // corresponds to this*

+            private Stack<Cmd> path;

             private Expr transitionRelation;

             private int boundVariableCount;

 

@@ -155,7 +155,7 @@ namespace Microsoft.Boogie
                 this.program = program;

                 this.first = null;

                 this.second = second;

-                this.dfsStack = new Stack<Block>();

+                this.path = new Stack<Cmd>();

                 this.transitionRelation = Expr.False;

                 this.boundVariableCount = 0;

             }

@@ -165,7 +165,7 @@ namespace Microsoft.Boogie
                 this.program = program;

                 this.first = first;

                 this.second = second;

-                this.dfsStack = new Stack<Block>();

+                this.path = new Stack<Cmd>();

                 this.transitionRelation = Expr.False;

                 this.boundVariableCount = 0;

             }

@@ -177,29 +177,16 @@ namespace Microsoft.Boogie
 

             public Expr Compute()

             {

-                Search(second.thatAction.Blocks[0], false);

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

-                List<Variable> boundVars = new List<Variable>();

-                if (first != null)

-                {

-                    foreach (Variable v in first.thisAction.LocVars)

-                    {

-                        BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type));

-                        map[v] = new IdentifierExpr(Token.NoToken, bv);

-                        boundVars.Add(bv);

-                    }

-                }

-                foreach (Variable v in second.thatAction.LocVars)

+                List<IdentifierExpr> havocVars = new List<IdentifierExpr>();

+                second.thisOutParams.ForEach(v => havocVars.Add(Expr.Ident(v)));

+                second.thisAction.LocVars.ForEach(v => havocVars.Add(Expr.Ident(v)));

+                if (havocVars.Count > 0)

                 {

-                    BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type));

-                    map[v] = new IdentifierExpr(Token.NoToken, bv);

-                    boundVars.Add(bv);

+                    HavocCmd havocCmd = new HavocCmd(Token.NoToken, havocVars);

+                    path.Push(havocCmd);

                 }

-                Substitution subst = Substituter.SubstitutionFromHashtable(map);

-                if (boundVars.Count > 0)

-                    return new ExistsExpr(Token.NoToken, boundVars, Substituter.Apply(subst, transitionRelation));

-                else

-                    return transitionRelation;

+                Search(second.thisAction.Blocks[0], false);

+                return transitionRelation;

             }

 

             private Expr CalculatePathCondition()

@@ -212,60 +199,54 @@ namespace Microsoft.Boogie
                 }

                 if (first != null)

                 {

-                    foreach (Variable v in first.thisOutParams)

+                    foreach (Variable v in first.thatOutParams)

                     {

                         var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));

                         returnExpr = Expr.And(eqExpr, returnExpr);

                     }

                 }

-                foreach (Variable v in second.thatOutParams)

+                foreach (Variable v in second.thisOutParams)

                 {

                     var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));

                     returnExpr = Expr.And(eqExpr, returnExpr);

                 }

-                Block[] dfsStackAsArray = dfsStack.Reverse().ToArray();

-                for (int i = dfsStackAsArray.Length - 1; i >= 0; i--)

+                foreach (Cmd cmd in path)

                 {

-                    Block b = dfsStackAsArray[i];

-                    for (int j = b.Cmds.Count - 1; j >= 0; j--)

+                    if (cmd is AssumeCmd)

                     {

-                        Cmd cmd = b.Cmds[j];

-                        if (cmd is AssumeCmd)

-                        {

-                            AssumeCmd assumeCmd = cmd as AssumeCmd;

-                            returnExpr = Expr.And(new OldExpr(Token.NoToken, assumeCmd.Expr), returnExpr);

-                        }

-                        else if (cmd is AssignCmd)

-                        {

-                            AssignCmd assignCmd = (cmd as AssignCmd).AsSimpleAssignCmd;

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

-                            for (int k = 0; k < assignCmd.Lhss.Count; k++)

-                            {

-                                map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k];

-                            }

-                            Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary<Variable, Expr>());

-                            Substitution oldSubst = Substituter.SubstitutionFromHashtable(map);

-                            returnExpr = (Expr) new MySubstituter(subst, oldSubst).Visit(returnExpr);

-                        }

-                        else if (cmd is HavocCmd)

+                        AssumeCmd assumeCmd = cmd as AssumeCmd;

+                        returnExpr = Expr.And(new OldExpr(Token.NoToken, assumeCmd.Expr), returnExpr);

+                    }

+                    else if (cmd is AssignCmd)

+                    {

+                        AssignCmd assignCmd = (cmd as AssignCmd).AsSimpleAssignCmd;

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

+                        for (int k = 0; k < assignCmd.Lhss.Count; k++)

                         {

-                            HavocCmd havocCmd = cmd as HavocCmd;

-                            List<Variable> existVars = new List<Variable>();

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

-                            foreach (IdentifierExpr ie in havocCmd.Vars)

-                            {

-                                BoundVariable bv = GetBoundVariable(ie.Decl.TypedIdent.Type);

-                                map[ie.Decl] = new IdentifierExpr(Token.NoToken, bv);

-                                existVars.Add(bv);

-                            }

-                            Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary<Variable, Expr>());

-                            Substitution oldSubst = Substituter.SubstitutionFromHashtable(map);

-                            returnExpr = new ExistsExpr(Token.NoToken, existVars, (Expr) new MySubstituter(subst, oldSubst).Visit(returnExpr));

+                            map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k];

                         }

-                        else

+                        Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary<Variable, Expr>());

+                        Substitution oldSubst = Substituter.SubstitutionFromHashtable(map);

+                        returnExpr = (Expr)new MySubstituter(subst, oldSubst).Visit(returnExpr);

+                    }

+                    else if (cmd is HavocCmd)

+                    {

+                        HavocCmd havocCmd = cmd as HavocCmd;

+                        List<Variable> existVars = new List<Variable>();

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

+                        foreach (IdentifierExpr ie in havocCmd.Vars)

                         {

-                            Debug.Assert(false);

+                            BoundVariable bv = GetBoundVariable(ie.Decl.TypedIdent.Type);

+                            map[ie.Decl] = new IdentifierExpr(Token.NoToken, bv);

+                            existVars.Add(bv);

                         }

+                        Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary<Variable, Expr>());

+                        Substitution oldSubst = Substituter.SubstitutionFromHashtable(map);

+                        returnExpr = new ExistsExpr(Token.NoToken, existVars, (Expr)new MySubstituter(subst, oldSubst).Visit(returnExpr));

+                    }

+                    else

+                    {

+                        Debug.Assert(false);

                     }

                 }

                 return returnExpr;

@@ -273,7 +254,10 @@ namespace Microsoft.Boogie
 

             private void Search(Block b, bool inFirst)

             {

-                dfsStack.Push(b);

+                foreach (Cmd cmd in b.Cmds)

+                {

+                    path.Push(cmd);

+                }

                 if (b.TransferCmd is ReturnCmd)

                 {

                     if (first == null || inFirst)

@@ -282,7 +266,15 @@ namespace Microsoft.Boogie
                     }

                     else

                     {

-                        Search(first.thisAction.Blocks[0], true);

+                        List<IdentifierExpr> havocVars = new List<IdentifierExpr>();

+                        first.thatOutParams.ForEach(v => havocVars.Add(Expr.Ident(v)));

+                        first.thatAction.LocVars.ForEach(v => havocVars.Add(Expr.Ident(v)));

+                        if (havocVars.Count > 0)

+                        {

+                            HavocCmd havocCmd = new HavocCmd(Token.NoToken, havocVars);

+                            path.Push(havocCmd);

+                        }

+                        Search(first.thatAction.Blocks[0], true);

                     }

                 }

                 else

@@ -293,7 +285,10 @@ namespace Microsoft.Boogie
                         Search(target, inFirst);

                     }

                 }

-                dfsStack.Pop();

+                foreach (Cmd cmd in b.Cmds)

+                {

+                    path.Pop();

+                }

             }

         }

 

@@ -344,17 +339,17 @@ namespace Microsoft.Boogie
                 if (domainName == null) continue;

                 domainNameToScope[domainName].Add(v);

             }

-            foreach (Variable v in first.thisInParams)

+            foreach (Variable v in first.thatInParams)

             {

                 var domainName = linearTypeChecker.FindDomainName(v);

                 if (domainName == null) continue;

                 domainNameToScope[domainName].Add(v);

             }

-            for (int i = 0; i < second.thatInParams.Count; i++)

+            foreach (Variable v in second.thisInParams)

             {

-                var domainName = linearTypeChecker.FindDomainName(second.thisInParams[i]);

+                var domainName = linearTypeChecker.FindDomainName(v);

                 if (domainName == null) continue;

-                domainNameToScope[domainName].Add(second.thatInParams[i]);

+                domainNameToScope[domainName].Add(v);

             }

             foreach (string domainName in domainNameToScope.Keys)

             {

@@ -371,16 +366,16 @@ namespace Microsoft.Boogie
             commutativityCheckerCache.Add(actionPair);

 

             List<Variable> inputs = new List<Variable>();

-            inputs.AddRange(first.thisInParams);

-            inputs.AddRange(second.thatInParams);

+            inputs.AddRange(first.thatInParams);

+            inputs.AddRange(second.thisInParams);

             List<Variable> outputs = new List<Variable>();

-            outputs.AddRange(first.thisOutParams);

-            outputs.AddRange(second.thatOutParams);

+            outputs.AddRange(first.thatOutParams);

+            outputs.AddRange(second.thisOutParams);

             List<Variable> locals = new List<Variable>();

-            locals.AddRange(first.thisAction.LocVars);

-            locals.AddRange(second.thatAction.LocVars);

-            List<Block> firstBlocks = CloneBlocks(first.thisAction.Blocks);

-            List<Block> secondBlocks = CloneBlocks(second.thatAction.Blocks);

+            locals.AddRange(first.thatAction.LocVars);

+            locals.AddRange(second.thisAction.LocVars);

+            List<Block> firstBlocks = CloneBlocks(first.thatAction.Blocks);

+            List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks);

             foreach (Block b in firstBlocks)

             {

                 if (b.TransferCmd is ReturnCmd)

@@ -417,17 +412,17 @@ namespace Microsoft.Boogie
             gatePreservationCheckerCache.Add(actionPair);

 

             List<Variable> inputs = new List<Variable>();

-            inputs.AddRange(first.thisInParams);

-            inputs.AddRange(second.thatInParams);

+            inputs.AddRange(first.thatInParams);

+            inputs.AddRange(second.thisInParams);

             List<Variable> outputs = new List<Variable>();

-            outputs.AddRange(first.thisOutParams);

-            outputs.AddRange(second.thatOutParams);

+            outputs.AddRange(first.thatOutParams);

+            outputs.AddRange(second.thisOutParams);

             List<Variable> locals = new List<Variable>();

-            locals.AddRange(second.thatAction.LocVars);

-            List<Block> secondBlocks = CloneBlocks(second.thatAction.Blocks);

+            locals.AddRange(second.thisAction.LocVars);

+            List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks);

             List<Requires> requires = DisjointnessRequires(program, first, second);

             List<Ensures> ensures = new List<Ensures>();

-            foreach (AssertCmd assertCmd in first.thisGate)

+            foreach (AssertCmd assertCmd in first.thatGate)

             {

                 requires.Add(new Requires(false, assertCmd.Expr));

                 ensures.Add(new Ensures(false, assertCmd.Expr));

@@ -450,18 +445,18 @@ namespace Microsoft.Boogie
             failurePreservationCheckerCache.Add(actionPair);

 

             List<Variable> inputs = new List<Variable>();

-            inputs.AddRange(first.thisInParams);

-            inputs.AddRange(second.thatInParams);

+            inputs.AddRange(first.thatInParams);

+            inputs.AddRange(second.thisInParams);

 

             Expr transitionRelation = (new TransitionRelationComputation(program, second)).Compute();

             Expr expr = Expr.True;

-            foreach (AssertCmd assertCmd in first.thisGate)

+            foreach (AssertCmd assertCmd in first.thatGate)

             {

                 expr = Expr.And(assertCmd.Expr, expr);

             }

             List<Requires> requires = DisjointnessRequires(program, first, second);

             requires.Add(new Requires(false, Expr.Not(expr)));

-            foreach (AssertCmd assertCmd in second.thatGate)

+            foreach (AssertCmd assertCmd in second.thisGate)

             {

                 requires.Add(new Requires(false, assertCmd.Expr));

             }

@@ -475,7 +470,7 @@ namespace Microsoft.Boogie
                 boundVars.Add(bv);

                 map[v] = new IdentifierExpr(Token.NoToken, bv);

             }

-            foreach (Variable v in second.thatOutParams)

+            foreach (Variable v in second.thisOutParams)

             {

                 {

                     BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type));

@@ -488,7 +483,7 @@ namespace Microsoft.Boogie
                     oldMap[v] = new IdentifierExpr(Token.NoToken, bv);

                 }

             }

-            foreach (Variable v in second.thatAction.LocVars)

+            foreach (Variable v in second.thisAction.LocVars)

             {

                 BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "pre_" + v.Name, v.TypedIdent.Type));

                 boundVars.Add(bv);

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 414aac59..598a4510 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -13,10 +13,11 @@ namespace Microsoft.Boogie
     public class MyDuplicator : Duplicator

     {

         MoverTypeChecker moverTypeChecker;

-        int phaseNum;

+        public int phaseNum;

         int enclosingProcPhaseNum;

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

-        public Dictionary<Absy, Absy> absyMap; /* Original -> Duplicate */

+        public Dictionary<Absy, Absy> absyMap; /* Duplicate -> Original */

+        public Dictionary<Block, Block> blockMap; /* Original -> Duplicate */

         public MyDuplicator(MoverTypeChecker moverTypeChecker, int phaseNum)

         {

             this.moverTypeChecker = moverTypeChecker;

@@ -24,6 +25,7 @@ namespace Microsoft.Boogie
             this.enclosingProcPhaseNum = int.MaxValue;

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

             this.absyMap = new Dictionary<Absy, Absy>();

+            this.blockMap = new Dictionary<Block, Block>();

         }

 

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

@@ -37,7 +39,6 @@ namespace Microsoft.Boogie
                 {

                     map[originalProc.InParams[i]] = callCmd.Ins[i];

                 }

-

                 Substitution subst = Substituter.SubstitutionFromHashtable(map);

                 foreach (AssertCmd assertCmd in gate)

                 {

@@ -61,6 +62,7 @@ namespace Microsoft.Boogie
                 for (int i = 0; i < parCallCmd.CallCmds.Count; i++) 

                 {

                     ProcessCallCmd(originalParCallCmd.CallCmds[i], parCallCmd.CallCmds[i], newCmds);

+                    absyMap[parCallCmd.CallCmds[i]] = originalParCallCmd;

                 }

             }

             else

@@ -100,14 +102,15 @@ namespace Microsoft.Boogie
         public override YieldCmd VisitYieldCmd(YieldCmd node)

         {

             YieldCmd yieldCmd = base.VisitYieldCmd(node);

-            absyMap[node] = yieldCmd;

+            absyMap[yieldCmd] = node;

             return yieldCmd;

         }

         

         public override Block VisitBlock(Block node)

         {

             Block block = base.VisitBlock(node);

-            absyMap[node] = block;

+            blockMap[node] = block;

+            absyMap[block] = node;

             return block;

         }

         

@@ -116,14 +119,14 @@ namespace Microsoft.Boogie
             CallCmd callCmd = (CallCmd) base.VisitCallCmd(node);

             callCmd.Proc = VisitProcedure(callCmd.Proc);

             callCmd.callee = callCmd.Proc.Name;

-            absyMap[node] = callCmd;

+            absyMap[callCmd] = node;

             return callCmd;

         }

 

         public override Cmd VisitParCallCmd(ParCallCmd node)

         {

             ParCallCmd parCallCmd = (ParCallCmd) base.VisitParCallCmd(node);

-            absyMap[node] = parCallCmd;

+            absyMap[parCallCmd] = node;

             return parCallCmd;

         }

 

@@ -152,6 +155,7 @@ namespace Microsoft.Boogie
             }

             return procMap[node];

         }

+

         public override Implementation VisitImplementation(Implementation node)

         {

             enclosingProcPhaseNum = moverTypeChecker.FindPhaseNumber(node.Proc);

@@ -165,7 +169,7 @@ namespace Microsoft.Boogie
                 List<string> labelNames = new List<string>();

                 foreach (Block x in gotoCmd.labelTargets)

                 {

-                    Block y = (Block)absyMap[x];

+                    Block y = (Block)blockMap[x];

                     labelTargets.Add(y);

                     labelNames.Add(y.Label);

                 }

@@ -210,7 +214,9 @@ namespace Microsoft.Boogie
     public class OwickiGries

     {

         LinearTypeChecker linearTypeChecker;

+        MoverTypeChecker moverTypeChecker;

         Dictionary<Absy, Absy> absyMap;

+        Dictionary<Procedure, Procedure> reverseProcMap;

         int phaseNum;

         List<Declaration> decls;

         List<IdentifierExpr> globalMods;

@@ -219,11 +225,17 @@ namespace Microsoft.Boogie
         List<Implementation> yieldCheckerImpls;

         Procedure yieldProc;

 

-        public OwickiGries(LinearTypeChecker linearTypeChecker, Dictionary<Absy, Absy> absyMap, int phaseNum, List<Declaration> decls)

+        public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator, List<Declaration> decls)

         {

             this.linearTypeChecker = linearTypeChecker;

-            this.absyMap = absyMap;

-            this.phaseNum = phaseNum;

+            this.moverTypeChecker = moverTypeChecker;

+            this.absyMap = duplicator.absyMap;

+            this.phaseNum = duplicator.phaseNum;

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

+            foreach (Procedure proc in duplicator.procMap.Keys)

+            {

+                this.reverseProcMap[duplicator.procMap[proc]] = proc;

+            }

             this.decls = decls;

             Program program = linearTypeChecker.program;

             globalMods = new List<IdentifierExpr>();

@@ -273,6 +285,32 @@ namespace Microsoft.Boogie
             CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List<IdentifierExpr>());

             yieldCallCmd.Proc = yieldProc;

             newCmds.Add(yieldCallCmd);

+

+            if (pc != null)

+            {

+                Expr bb = OldEqualityExpr(ogOldGlobalMap);

+

+                // assert pc ==> o_old == o && g_old == g;

+                newCmds.Add(new AssertCmd(Token.NoToken, Expr.Imp(Expr.Ident(pc), bb)));

+

+                // assert (o_old == o && g_old == g) || beta(i, g_old, o, g);

+                AssertCmd betaAssertCmd = new AssertCmd(Token.NoToken, Expr.Or(bb, beta));

+                newCmds.Add(betaAssertCmd);

+

+                // pc, ok := ite(o_old == o && g_old == g, pc, true), ok || beta(i, g_old, o, g);

+                List<Expr> iteArgs = new List<Expr>(new Expr[] { bb, Expr.Ident(pc), Expr.True });

+                List<AssignLhs> pcUpdateLHS = new List<AssignLhs>(

+                    new AssignLhs[] { 

+                        new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)), 

+                        new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok))

+                    });

+                List<Expr> pcUpdateRHS = new List<Expr>(

+                    new Expr[] { 

+                        new NAryExpr(Token.NoToken, new IfThenElse(Token.NoToken), iteArgs),

+                        Expr.Or(Expr.Ident(ok), beta)

+                    });

+                newCmds.Add(new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS));

+            }

         }

 

         private Dictionary<string, Expr> ComputeAvailableExprs(HashSet<Variable> availableLinearVars, Dictionary<string, Variable> domainNameToInputVar)

@@ -311,13 +349,28 @@ namespace Microsoft.Boogie
             {

                 lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g])));

                 rhss.Add(new IdentifierExpr(Token.NoToken, g));

-            } 

+            }

             if (lhss.Count > 0)

             {

                 newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));

             }

         }

 

+        Variable pc;

+        Variable ok;

+        Expr alpha;

+        Expr beta;

+

+        private Expr OldEqualityExpr(Dictionary<Variable, Variable> ogOldGlobalMap)

+        {

+            Expr bb = Expr.True;

+            foreach (Variable o in ogOldGlobalMap.Keys)

+            {

+                bb = Expr.Binary(BinaryOperator.Opcode.And, bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o])));

+            }

+            return bb;

+        }

+

         private void DesugarYield(YieldCmd yieldCmd, List<Cmd> cmds, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar)

         {

             AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);

@@ -325,7 +378,13 @@ namespace Microsoft.Boogie
             if (globalMods.Count > 0)

             {

                 newCmds.Add(new HavocCmd(Token.NoToken, globalMods));

+                if (pc != null)

+                {

+                    // assume pc || alpha(i, g);

+                    newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Or(Expr.Ident(pc), alpha)));

+                }

             }

+

             Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(yieldCmd), domainNameToInputVar);

             AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);

 

@@ -370,13 +429,13 @@ namespace Microsoft.Boogie
                     Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();

                     foreach (Variable x in callCmd.Proc.InParams)

                     {

-                        Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), true);

+                        Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_{0}_{1}", count, x.Name), x.TypedIdent.Type), true);

                         inParams.Add(y);

                         map[x] = new IdentifierExpr(Token.NoToken, y);

                     }

                     foreach (Variable x in callCmd.Proc.OutParams)

                     {

-                        Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), false);

+                        Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_{0}_{1}", count, x.Name), x.TypedIdent.Type), false);

                         outParams.Add(y);

                         map[x] = new IdentifierExpr(Token.NoToken, y);

                     }

@@ -663,6 +722,50 @@ namespace Microsoft.Boogie
                 ogOldGlobalMap[g] = l;

                 impl.LocVars.Add(l);

             }

+

+            Procedure originalProc = reverseProcMap[impl.Proc];

+            if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc))

+            {

+                ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc];

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

+                {

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

+                    impl.LocVars.Add(pc);

+                    ok = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_ok", Type.Bool));

+                    impl.LocVars.Add(ok);

+                    Dictionary<Variable, Expr> alwaysMap = new Dictionary<Variable, Expr>();

+                    for (int i = 0; i < originalProc.InParams.Count; i++)

+                    {

+                        alwaysMap[originalProc.InParams[i]] = Expr.Ident(impl.InParams[i]);

+                    }

+                    for (int i = 0; i < originalProc.OutParams.Count; i++)

+                    {

+                        alwaysMap[originalProc.OutParams[i]] = Expr.Ident(impl.OutParams[i]);

+                    }

+                    Substitution always = Substituter.SubstitutionFromHashtable(alwaysMap);

+                    Dictionary<Variable, Expr> foroldMap = new Dictionary<Variable, Expr>();

+                    foreach (IdentifierExpr ie in globalMods)

+                    {

+                        foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);

+                    }

+                    Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);

+                    Expr betaExpr = new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, actionInfo).Compute();

+                    beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr);

+                    Expr alphaExpr = Expr.True;

+                    foreach (AssertCmd assertCmd in actionInfo.thisGate)

+                    {

+                        alphaExpr = Expr.And(alphaExpr, assertCmd.Expr);

+                    }

+                    alpha = Substituter.Apply(always, alphaExpr);

+                    foreach (Variable f in impl.OutParams)

+                    {

+                        LocalVariable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_old_{0}", f.Name), f.TypedIdent.Type));

+                        impl.LocVars.Add(copy);

+                        ogOldGlobalMap[f] = copy;

+                    }

+                }

+            }

+

             Dictionary<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();

             Dictionary<string, Variable> domainNameToLocalVar = new Dictionary<string, Variable>();

             {

@@ -780,19 +883,43 @@ namespace Microsoft.Boogie
                 if (b.TransferCmd is ReturnCmd && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields"))

                 {

                     AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);

+                    if (pc != null)

+                    {

+                        newCmds.Add(new AssertCmd(Token.NoToken, Expr.Ident(ok)));

+                    }

                 }

                 b.Cmds = newCmds;

             }

 

             foreach (Block header in yieldingHeaders)

             {

+                LocalVariable oldPc = null;

+                LocalVariable oldOk = null;

+                if (pc != null)

+                {

+                    oldPc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}", pc.Name, header.Label), Type.Bool));

+                    impl.LocVars.Add(oldPc);

+                    oldOk = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}", ok.Name, header.Label), Type.Bool));

+                    impl.LocVars.Add(oldOk);

+                }

                 Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(header), domainNameToInputVar);

                 foreach (Block pred in header.Predecessors)

                 {

                     AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);

+                    if (pc != null && !graph.BackEdgeNodes(header).Contains(pred))

+                    {

+                        pred.Cmds.Add(new AssignCmd(Token.NoToken, new List<AssignLhs>(

+                            new AssignLhs[] { new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)), new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)) }), 

+                            new List<Expr>(new Expr[] { Expr.Ident(pc), Expr.Ident(ok) })));

+                    }

                     AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);

                 }

                 List<Cmd> newCmds = new List<Cmd>();

+                if (pc != null)

+                {

+                    newCmds.Add(new AssertCmd(Token.NoToken, Expr.Eq(Expr.Ident(pc), Expr.Ident(oldPc))));

+                    newCmds.Add(new AssertCmd(Token.NoToken, Expr.Eq(Expr.Ident(ok), Expr.Ident(oldOk))));

+                } 

                 foreach (string domainName in linearTypeChecker.linearDomains.Keys)

                 {

                     newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName])));

@@ -809,6 +936,13 @@ namespace Microsoft.Boogie
                 // Add initial block

                 List<AssignLhs> lhss = new List<AssignLhs>();

                 List<Expr> rhss = new List<Expr>();

+                if (pc != null)

+                {

+                    lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)));

+                    rhss.Add(Expr.False);

+                    lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok)));

+                    rhss.Add(Expr.False);

+                }

                 Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();

                 foreach (var domainName in linearTypeChecker.linearDomains.Keys)

                 {

@@ -1018,13 +1152,6 @@ namespace Microsoft.Boogie
             return (QKeyValue.FindBoolAttribute(iter, "stable")) ? iter.Next : iter;

         }

 

-        public static QKeyValue RemovePhaseAttribute(QKeyValue iter)

-        {

-            if (iter == null) return null;

-            iter.Next = RemovePhaseAttribute(iter.Next);

-            return (QKeyValue.FindIntAttribute(iter, "phase", int.MaxValue) != int.MaxValue) ? iter.Next : iter;

-        }

-

         public static QKeyValue RemoveQedAttribute(QKeyValue iter)

         {

             if (iter == null) return null;

@@ -1045,10 +1172,13 @@ namespace Microsoft.Boogie
                 return iter;

         }

 

-        public void Transform(List<Implementation> impls, List<Procedure> procs)

+        private void Transform(List<Implementation> impls, List<Procedure> procs)

         {

             foreach (var impl in impls)

             {

+                pc = null;

+                alpha = null;

+                beta = null;

                 TransformImpl(impl);

             }

             foreach (var proc in procs)

@@ -1068,28 +1198,6 @@ namespace Microsoft.Boogie
                 decls.Add(proc);

             }

             AddYieldProcAndImpl();

-            foreach (var proc in procs)

-            {

-                if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))

-                {

-                    HashSet<Variable> modifiedVars = new HashSet<Variable>();

-                    proc.Modifies.Iter(x => modifiedVars.Add(x.Decl));

-                    foreach (GlobalVariable g in linearTypeChecker.program.GlobalVariables())

-                    {

-                        if (modifiedVars.Contains(g)) continue;

-                        proc.Modifies.Add(new IdentifierExpr(Token.NoToken, g));

-                    }

-                    proc.Attributes = RemoveYieldsAttribute(proc.Attributes);

-                    proc.Attributes = RemoveStableAttribute(proc.Attributes);

-                }

-                decls.Add(proc);

-            }

-            foreach (var impl in impls)

-            {

-                impl.Attributes = RemoveYieldsAttribute(impl.Attributes);

-                impl.Attributes = RemoveStableAttribute(impl.Attributes);

-                decls.Add(impl);

-            }

         }

 

         public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)

@@ -1108,8 +1216,9 @@ namespace Microsoft.Boogie
                     procs.Add(duplicateProc);

                     if (moverTypeChecker.procToActionInfo.ContainsKey(proc) && moverTypeChecker.procToActionInfo[proc].phaseNum < phaseNum)

                     {

-                        duplicateProc.Attributes = OwickiGries.RemoveYieldsAttribute(duplicateProc.Attributes);

-                        program.GlobalVariables().Iter(x => duplicateProc.Modifies.Add(new IdentifierExpr(Token.NoToken, x)));

+                        duplicateProc.Attributes = null;

+                        duplicateProc.Modifies = new List<IdentifierExpr>();

+                        program.GlobalVariables().Iter(x => duplicateProc.Modifies.Add(Expr.Ident(x)));

                         CodeExpr action = (CodeExpr)duplicator.VisitCodeExpr(moverTypeChecker.procToActionInfo[proc].thisAction);

                         Implementation impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, new List<Variable>(), action.Blocks);

                         impl.Proc = duplicateProc;

@@ -1128,13 +1237,16 @@ namespace Microsoft.Boogie
                     Implementation duplicateImpl = duplicator.VisitImplementation(impl);

                     impls.Add(duplicateImpl);

                 }

-                Dictionary<Absy, Absy> reverseAbsyMap = new Dictionary<Absy, Absy>();

-                foreach (Absy key in duplicator.absyMap.Keys)

+                OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator, decls);

+                ogTransform.Transform(impls, procs);

+                foreach (var proc in procs)

                 {

-                    reverseAbsyMap[duplicator.absyMap[key]] = key;

+                    decls.Add(proc);

+                }

+                foreach (var impl in impls)

+                {

+                    decls.Add(impl);

                 }

-                OwickiGries ogTransform = new OwickiGries(linearTypeChecker, reverseAbsyMap, phaseNum, decls);

-                ogTransform.Transform(impls, procs);

             }

         }

     }

diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs
index 7c2c0c74..45d538df 100644
--- a/Source/Concurrency/Program.cs
+++ b/Source/Concurrency/Program.cs
@@ -33,8 +33,21 @@ namespace Microsoft.Boogie
             List<Declaration> decls = new List<Declaration>();

             OwickiGries.AddCheckers(linearTypeChecker, moverTypeChecker, decls);

             MoverCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls);

-            //RefinementCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls);

 

+            foreach (Declaration decl in decls)

+            {

+                Procedure proc = decl as Procedure;

+                if (proc != null && QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))

+                {

+                    proc.Modifies = new List<IdentifierExpr>();

+                    linearTypeChecker.program.GlobalVariables().Iter(x => proc.Modifies.Add(Expr.Ident(x)));

+                }

+            }

+            foreach (Declaration decl in decls)

+            {

+                decl.Attributes = OwickiGries.RemoveYieldsAttribute(decl.Attributes);

+                decl.Attributes = OwickiGries.RemoveStableAttribute(decl.Attributes);

+            }

             program.TopLevelDeclarations.RemoveAll(x => originalDecls.Contains(x));

             program.TopLevelDeclarations.AddRange(decls);

         }

diff --git a/Source/Concurrency/RefinementCheck.cs b/Source/Concurrency/RefinementCheck.cs
deleted file mode 100644
index bba7bd35..00000000
--- a/Source/Concurrency/RefinementCheck.cs
+++ /dev/null
@@ -1,552 +0,0 @@
-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using Microsoft.Boogie;

-using Microsoft.Boogie.AbstractInterpretation;

-using Microsoft.Boogie.GraphUtil;

-using System.Diagnostics;

-using System.Diagnostics.Contracts;

-

-

-namespace Microsoft.Boogie

-{

-    using Bpl = Microsoft.Boogie;

-    class RefinementCheck

-    {

-        Program refinementCheckerProgram;

-        LinearTypeChecker linearTypeChecker;

-        MoverTypeChecker moverTypeChecker;

-

-        public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)

-        {

-            RefinementCheck refinementChecking = new RefinementCheck(linearTypeChecker, moverTypeChecker);

-            foreach (Declaration decl in linearTypeChecker.program.TopLevelDeclarations)

-            {

-                if (decl is Implementation)

-                {

-                    Implementation impl = decl as Implementation;

-                    refinementChecking.createRefinementChecker(impl);

-                }

-            }

-        }

-

-        private RefinementCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)

-        {

-            this.linearTypeChecker = linearTypeChecker;

-            this.moverTypeChecker = moverTypeChecker;

-            this.refinementCheckerProgram = new Program();

-            foreach (Declaration decl in linearTypeChecker.program.TopLevelDeclarations)

-            {

-                if (decl is TypeCtorDecl || decl is TypeSynonymDecl || decl is Constant || decl is Function || decl is Axiom)

-                    this.refinementCheckerProgram.TopLevelDeclarations.Add(decl);

-            }

-            foreach (Variable v in linearTypeChecker.program.GlobalVariables())

-            {

-                this.refinementCheckerProgram.TopLevelDeclarations.Add(v);

-            }

-        }

-

-        private void createRefinementChecker(Implementation impl)

-        {

-            addRefinementCheckingAnnotations(impl);

-            refinementCheckerProgram.TopLevelDeclarations.Add(impl);

-            refinementCheckerProgram.TopLevelDeclarations.Add(impl.Proc);

-        }

-

-        private Expr createNewAlpha(Implementation impl)

-        {

-            Expr result;

-            result = Expr.True;

-            foreach (AssertCmd aC in moverTypeChecker.procToActionInfo[impl.Proc].thisGate)

-            {

-                Expr aCExprClone = (Expr)aC.OrigExpr.Clone();

-                result = Expr.Binary(BinaryOperator.Opcode.And, result, aCExprClone);

-            }

-            return result;

-        }

-

-        private Expr createNewAlphaOfGOld(Implementation impl, List<Variable> originalGVars,

-            Dictionary<Variable, Variable> regularToOldGVar)

-        {

-            Expr result;

-            result = Expr.True;

-            foreach (AssertCmd aC in moverTypeChecker.procToActionInfo[impl.Proc].thisGate)

-            {

-                Expr aCExprClone = (Expr)aC.OrigExpr.Clone();

-                result = Expr.Binary(BinaryOperator.Opcode.And, result, aCExprClone);

-            }

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

-            foreach (Variable v in originalGVars)

-            {

-                map[v] = Expr.Ident(regularToOldGVar[v]);

-            }

-            Substitution subst = Substituter.SubstitutionFromHashtable(map);

-            MySubstituter mySubst = new MySubstituter(subst, subst);// ST: Check with Shaz

-            result = (Expr)mySubst.Visit(result);

-            return result;

-        }

-

-

-        private HavocCmd createNewHavocGCmd()

-        {

-            List<IdentifierExpr> gList = new List<IdentifierExpr>();

-            foreach (GlobalVariable g in refinementCheckerProgram.GlobalVariables())

-                gList.Add(new IdentifierExpr(Token.NoToken, g));

-            HavocCmd havocG = new HavocCmd(Token.NoToken, gList);

-            return havocG;

-        }

-

-        private AssignCmd createNewAssignGOldGetsG(List<Variable> originalGVars, Dictionary<Variable, Variable> regularToOldGVar)

-        {

-            List<AssignLhs> lhss_g = new List<AssignLhs>();

-            List<Expr> rhss_g = new List<Expr>();

-            foreach (Variable g in originalGVars)

-            {

-                rhss_g.Add(new IdentifierExpr(Token.NoToken, g));

-                lhss_g.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(regularToOldGVar[g])));

-            }

-

-            AssignCmd gOldGetsG = new AssignCmd(Token.NoToken, lhss_g, rhss_g);

-            return gOldGetsG;

-        }

-

-        private AssignCmd createNewAssignOOldGetsO(Implementation impl, Dictionary<Variable, Variable> regularToOldOVar)

-        {

-            List<AssignLhs> lhss = new List<AssignLhs>();

-            List<Expr> rhss = new List<Expr>();

-            foreach (Variable o in impl.OutParams)

-            {

-                rhss.Add(new IdentifierExpr(Token.NoToken, o));

-                lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(regularToOldOVar[o])));

-            }

-

-            // Implement command list that does o_old := o;

-            AssignCmd oOldGetsO = new AssignCmd(Token.NoToken, lhss, rhss);

-            return oOldGetsO;

-        }

-

-        private AssertCmd createNewAssertGOldEqualsG(List<Variable> originalGVars, Dictionary<Variable, Variable> regularToOldGVar)

-        {

-            Expr gOldEqualsG = Expr.True;

-            foreach (Variable g in originalGVars)

-            {

-                Expr thisVarEqualsOldVar = Expr.Binary(BinaryOperator.Opcode.Eq,

-                                                       new IdentifierExpr(Token.NoToken, g),

-                                                       new IdentifierExpr(Token.NoToken, regularToOldGVar[g]));

-                gOldEqualsG = Expr.Binary(BinaryOperator.Opcode.And, gOldEqualsG, thisVarEqualsOldVar);

-            }

-

-            AssertCmd AssertGOldEqualsGCmd = new AssertCmd(Token.NoToken, gOldEqualsG);

-            return AssertGOldEqualsGCmd;

-        }

-

-        private Expr createNewGOldEqualsG(List<Variable> originalGVars, Dictionary<Variable, Variable> regularToOldGVar)

-        {

-            Expr gOldEqualsG = Expr.True;

-            foreach (Variable g in originalGVars)

-            {

-                Expr thisVarEqualsOldVar = Expr.Binary(BinaryOperator.Opcode.Eq,

-                                                       new IdentifierExpr(Token.NoToken, g),

-                                                       new IdentifierExpr(Token.NoToken, regularToOldGVar[g]));

-                gOldEqualsG = Expr.Binary(BinaryOperator.Opcode.And, gOldEqualsG, thisVarEqualsOldVar);

-            }

-

-            return gOldEqualsG;

-        }

-

-        private AssertCmd createNewAssertOOldEqualsO(Implementation impl, Dictionary<Variable, Variable> regularToOldOVar)

-        {

-            Expr oOldEqualsO = Expr.True;

-            foreach (Variable o in impl.OutParams)

-            {

-                Expr thisOVarEqualsOldOVar = Expr.Binary(BinaryOperator.Opcode.Eq,

-                                                       new IdentifierExpr(Token.NoToken, o),

-                                                       new IdentifierExpr(Token.NoToken, regularToOldOVar[o]));

-                oOldEqualsO = Expr.Binary(BinaryOperator.Opcode.And, oOldEqualsO, thisOVarEqualsOldOVar);

-            }

-

-            AssertCmd AssertOOldEqualsOCmd = new AssertCmd(Token.NoToken, oOldEqualsO);

-            return AssertOOldEqualsOCmd;

-        }

-

-        private Expr createNewOOldEqualsO(Implementation impl, Dictionary<Variable, Variable> regularToOldOVar)

-        {

-            Expr oOldEqualsO = Expr.True;

-            foreach (Variable o in impl.OutParams)

-            {

-                Expr thisOVarEqualsOldOVar = Expr.Binary(BinaryOperator.Opcode.Eq,

-                                                       new IdentifierExpr(Token.NoToken, o),

-                                                       new IdentifierExpr(Token.NoToken, regularToOldOVar[o]));

-                oOldEqualsO = Expr.Binary(BinaryOperator.Opcode.And, oOldEqualsO, thisOVarEqualsOldOVar);

-            }

-

-            return oOldEqualsO;

-        }

-

-

-        private Expr createNewBetaOfOldOOldGoNg(Implementation impl, List<Variable> originalGVars,

-            Dictionary<Variable, Variable> regularToOldGVar,

-            Dictionary<Variable, Variable> regularToOldOVar)

-        {

-            Expr betaOfOOldOGOldG = new TransitionRelationComputation(moverTypeChecker.program,

-                                                          moverTypeChecker.procToActionInfo[impl.Proc],

-                                                          regularToOldGVar,

-                                                          regularToOldOVar).Compute();

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

-            foreach (Variable v in originalGVars)

-            {

-                map[v] = Expr.Ident(regularToOldGVar[v]);

-            }

-            foreach (Variable o in impl.OutParams)

-            {

-                map[o] = Expr.Ident(regularToOldOVar[o]);

-            }

-

-            Substitution always = Substituter.SubstitutionFromHashtable(new Dictionary<Variable, Expr>());

-            Substitution forold = Substituter.SubstitutionFromHashtable(map);

-            betaOfOOldOGOldG = Substituter.ApplyReplacingOldExprs(always, forold, betaOfOOldOGOldG);

-            return betaOfOOldOGOldG;

-        }

-

-        private HavocCmd createNewHavocGnO(Implementation impl, List<Variable> originalGVars)

-        {

-            HavocCmd resultCmd;

-            List<IdentifierExpr> varsList = new List<IdentifierExpr>();

-            foreach (Variable gv in originalGVars)

-            {

-                varsList.Add(new IdentifierExpr(Token.NoToken, gv));

-            }

-            foreach (Variable v in impl.OutParams)

-            {

-                varsList.Add(new IdentifierExpr(Token.NoToken, v));

-            }

-            resultCmd = new HavocCmd(Token.NoToken, varsList);

-            return resultCmd;

-        }

-

-        private void addRefinementCheckingAnnotations(Implementation impl)

-        {

-            // Create variables for pc, ok

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

-            impl.LocVars.Add(pc);

-            LocalVariable pc_old = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "pc_old", Bpl.Type.Bool));

-            impl.LocVars.Add(pc_old);

-            LocalVariable ok = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "ok", Bpl.Type.Bool));

-            impl.LocVars.Add(ok);

-

-

-            // Create variables for g_old, o_old

-            Dictionary<Variable, Variable> regularToOldGVar = new Dictionary<Variable, Variable>();

-            Dictionary<Variable, Variable> regularToOldOVar = new Dictionary<Variable, Variable>();

-            ActionInfo actionInfoForThisProc = moverTypeChecker.procToActionInfo[impl.Proc];

-

-            List<Variable> originalGVars = new List<Variable>();

-            List<Variable> _old_OriginalGVars = new List<Variable>();

-

-

-            foreach (GlobalVariable gv in refinementCheckerProgram.GlobalVariables())

-                originalGVars.Add(gv);

-

-            foreach (Variable v in refinementCheckerProgram.GlobalVariables()) //ST: Check that this is the right set of global vars

-            {

-                GlobalVariable gv = v as GlobalVariable;

-                LocalVariable v_old = new LocalVariable(Token.NoToken,

-                    new TypedIdent(Token.NoToken, gv.TypedIdent.Name + "_old", gv.TypedIdent.Type)); //gv.TypedIdent

-                impl.LocVars.Add(v_old); //ST: Ask Shaz whether to add v_old to proc, probably not.

-                _old_OriginalGVars.Add(v_old);

-                regularToOldGVar.Add(gv, v_old);

-            }

-

-            // List<Variable> originalOVars = new List<Variable>();

-            List<Variable> _old_OriginalOVars = new List<Variable>();

-

-

-            //foreach (Variable v in impl.OutParams)

-            //    originalOVars.Add(v);

-

-            foreach (Variable o in impl.OutParams) //ST: Check that this is the right set of global vars

-            {

-                Variable o_old = new LocalVariable(Token.NoToken,

-                    new TypedIdent(Token.NoToken, o.TypedIdent.Name + "_old", o.TypedIdent.Type));

-

-                _old_OriginalOVars.Add(o_old);

-                regularToOldOVar.Add(o, o_old);

-            }

-

-

-            // AssertCmd AssertONGEqualOldONG = new AssertCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.And, oOldEqualsO, gOldEqualsG));

-

-            // Traverse CFG of impl, replace yield's in place.

-            foreach (Block b in impl.Blocks)

-            {

-                List<Cmd> newCmdList = new List<Cmd>();

-                foreach (Cmd c in b.Cmds)

-                {

-                    if (c is YieldCmd)

-                    {

-                        // Code to be inserted instead of yield

-                        // 

-                        // assert !pc ==> \alpha(g_old);

-                        // assert ok;

-                        // if (o_old == o && g_old == g) { // IfCmd

-                        //    // Do nothing

-                        // } else {

-                        //    assert !pc;

-                        //    pc := true;

-                        //    assert \beta(o_old, g_old, o, g);

-                        // }

-                        // havoc o, g;

-                        // o_old := o;

-                        // g_old := g;

-

-                        // Implementing the following instead:

-

-                        // assert !pc ==> \alpha(g_old);

-                        // assert ok;

-                        // bb := (o_old == o && g_old == g) 

-                        // assert !bb ==> !pc;

-                        // pc := ite(!bb,true,pc);

-                        // assert !bb ==> \beta(o_old, g_old, o, g);

-                        // }

-                        // havoc o, g;

-                        // o_old := o;

-                        // g_old := g;

-

-                        Expr notPcImpliesAlphaOfGoldExpr = Expr.Binary(BinaryOperator.Opcode.Imp,

-                                                                       Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not,

-                                                                                    Expr.Ident(pc)),

-                                                                       createNewAlphaOfGOld(impl, originalGVars, regularToOldGVar)

-                                                                       );

-                        AssertCmd notPcImpliesAlphaOfGOldCmd = new AssertCmd(Token.NoToken, notPcImpliesAlphaOfGoldExpr);

-                        newCmdList.Add(notPcImpliesAlphaOfGOldCmd);

-                        AssertCmd assertOkCmd = new AssertCmd(Token.NoToken, new IdentifierExpr(Token.NoToken, ok));

-                        newCmdList.Add(assertOkCmd);

-

-                        Expr bb = Expr.Binary(BinaryOperator.Opcode.And,

-                                    createNewOOldEqualsO(impl, regularToOldOVar),

-                                    createNewGOldEqualsG(originalGVars, regularToOldGVar));

-                        Expr notBB = Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, bb);

-                        Expr notPC = Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, Expr.Ident(pc));

-                        AssertCmd assertNotBBImpliesNotPCCmd = new AssertCmd(Token.NoToken, Expr.Imp(notBB, notPC));

-                        newCmdList.Add(assertNotBBImpliesNotPCCmd);

-

-                        // pc := ite(!bb,true,pc);

-                        List<Expr> iteArgs = new List<Expr>();

-                        iteArgs.Add(Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, bb));

-                        iteArgs.Add(Expr.True);

-                        iteArgs.Add(Expr.Ident(pc));

-                        Expr pcNew = new NAryExpr(Token.NoToken, new IfThenElse(Token.NoToken), iteArgs);

-                        List<AssignLhs> pcUpdateLHS = new List<AssignLhs>();

-                        pcUpdateLHS.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, pc)));

-                        List<Expr> pcUpdateRHS = new List<Expr>();

-                        pcUpdateRHS.Add(pcNew);

-                        AssignCmd pcGetsUpdated = new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS);

-

-                        // assert !bb ==> \beta(o_old, g_old, o, g);

-                        Expr betaExpr = createNewBetaOfOldOOldGoNg(impl, originalGVars, regularToOldGVar, regularToOldOVar);

-                        AssertCmd betaAssertCmd = new AssertCmd(Token.NoToken, Expr.Imp(Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, bb),

-                                                                                        betaExpr));

-                        newCmdList.Add(betaAssertCmd);

-

-                        HavocCmd havocOnG = createNewHavocGnO(impl, originalGVars);

-                        newCmdList.Add(havocOnG);

-

-                        if (originalGVars.Count > 0)

-                        {

-                            AssignCmd gOldGetsG = createNewAssignGOldGetsG(originalGVars, regularToOldGVar);

-                            newCmdList.Add(gOldGetsG);

-                        }

-

-                        if (impl.OutParams.Count > 0)

-                        {

-                            AssignCmd oOldGetsO = createNewAssignOOldGetsO(impl, regularToOldOVar);

-                            newCmdList.Add(oOldGetsO);

-                        }

-                    }

-                    else

-                    {

-                        newCmdList.Add((Cmd)c.Clone());

-                    }

-                }

-                b.Cmds = newCmdList;

-            }

-        }

-

-        private sealed class MySubstituter : Duplicator

-        {

-            private readonly Substitution outsideOld;

-            private readonly Substitution insideOld;

-            [ContractInvariantMethod]

-            void ObjectInvariant()

-            {

-                Contract.Invariant(insideOld != null);

-            }

-

-            public MySubstituter(Substitution outsideOld, Substitution insideOld)

-                : base()

-            {

-                Contract.Requires(outsideOld != null && insideOld != null);

-                this.outsideOld = outsideOld;

-                this.insideOld = insideOld;

-            }

-

-            private bool insideOldExpr = false;

-

-            public override Expr VisitIdentifierExpr(IdentifierExpr node)

-            {

-                Contract.Ensures(Contract.Result<Expr>() != null);

-                Expr e = null;

-

-                if (insideOldExpr)

-                {

-                    e = insideOld(node.Decl);

-                }

-                else

-                {

-                    e = outsideOld(node.Decl);

-                }

-                return e == null ? base.VisitIdentifierExpr(node) : e;

-            }

-

-            public override Expr VisitOldExpr(OldExpr node)

-            {

-                Contract.Ensures(Contract.Result<Expr>() != null);

-                bool previouslyInOld = insideOldExpr;

-                insideOldExpr = true;

-                Expr tmp = (Expr)this.Visit(node.Expr);

-                OldExpr e = new OldExpr(node.tok, tmp);

-                insideOldExpr = previouslyInOld;

-                return e;

-            }

-        }

-

-        class TransitionRelationComputation

-        {

-            private Program program;

-            private ActionInfo first;

-            private ActionInfo second;

-            private Stack<Block> dfsStack;

-            private Expr transitionRelation;

-            private Dictionary<Variable, Variable> regularToOldGVar;

-            private Dictionary<Variable, Variable> regularToOldOVar;

-

-            public TransitionRelationComputation(Program program, ActionInfo second, Dictionary<Variable, Variable> regularToOldGVar, Dictionary<Variable, Variable> regularToOldOVar)

-            {

-                this.program = program;

-                this.first = null;

-                this.second = second;

-                this.regularToOldGVar = regularToOldGVar;

-                this.regularToOldOVar = regularToOldOVar;

-                this.dfsStack = new Stack<Block>();

-                this.transitionRelation = Expr.False;

-            }

-

-            public Expr Compute()

-            {

-                Search(second.thatAction.Blocks[0], false);

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

-                List<Variable> boundVars = new List<Variable>();

-                if (first != null)

-                {

-                    foreach (Variable v in first.thisAction.LocVars)

-                    {

-                        BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type));

-                        map[v] = new IdentifierExpr(Token.NoToken, bv);

-                        boundVars.Add(bv);

-                    }

-                }

-                foreach (Variable v in second.thatAction.LocVars)

-                {

-                    BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type));

-                    map[v] = new IdentifierExpr(Token.NoToken, bv);

-                    boundVars.Add(bv);

-                }

-                Substitution subst = Substituter.SubstitutionFromHashtable(map);

-                if (boundVars.Count > 0)

-                    return new ExistsExpr(Token.NoToken, boundVars, Substituter.Apply(subst, transitionRelation));

-                else

-                    return transitionRelation;

-            }

-

-            private Expr CalculatePathCondition()

-            {

-                Expr returnExpr = Expr.True;

-                foreach (Variable v in program.GlobalVariables())

-                {

-                    var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));

-                    returnExpr = Expr.And(eqExpr, returnExpr);

-                }

-                if (first != null)

-                {

-                    foreach (Variable v in first.thisOutParams)

-                    {

-                        var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));

-                        returnExpr = Expr.And(eqExpr, returnExpr);

-                    }

-                }

-                foreach (Variable v in second.thatOutParams)

-                {

-                    var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));

-                    returnExpr = Expr.And(eqExpr, returnExpr);

-                }

-                Block[] dfsStackAsArray = dfsStack.Reverse().ToArray();

-                for (int i = dfsStackAsArray.Length - 1; i >= 0; i--)

-                {

-                    Block b = dfsStackAsArray[i];

-                    for (int j = b.Cmds.Count - 1; j >= 0; j--)

-                    {

-                        Cmd cmd = b.Cmds[j];

-                        if (cmd is AssumeCmd)

-                        {

-                            AssumeCmd assumeCmd = cmd as AssumeCmd;

-                            returnExpr = Expr.And(new OldExpr(Token.NoToken, assumeCmd.Expr), returnExpr);

-                        }

-                        else if (cmd is AssignCmd)

-                        {

-                            AssignCmd assignCmd = (cmd as AssignCmd).AsSimpleAssignCmd;

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

-                            for (int k = 0; k < assignCmd.Lhss.Count; k++)

-                            {

-                                map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k];

-                            }

-                            Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary<Variable, Expr>());

-                            Substitution oldSubst = Substituter.SubstitutionFromHashtable(map);

-                            returnExpr = (Expr)new MySubstituter(subst, oldSubst).Visit(returnExpr);

-                        }

-                        else

-                        {

-                            Debug.Assert(false);

-                        }

-                    }

-                }

-                return returnExpr;

-            }

-

-            private void Search(Block b, bool inFirst)

-            {

-                dfsStack.Push(b);

-                if (b.TransferCmd is ReturnExprCmd)

-                {

-                    if (first == null || inFirst)

-                    {

-                        transitionRelation = Expr.Or(transitionRelation, CalculatePathCondition());

-                    }

-                    else

-                    {

-                        Search(first.thisAction.Blocks[0], true);

-                    }

-                }

-                else

-                {

-                    GotoCmd gotoCmd = b.TransferCmd as GotoCmd;

-                    foreach (Block target in gotoCmd.labelTargets)

-                    {

-                        Search(target, inFirst);

-                    }

-                }

-                dfsStack.Pop();

-            }

-        }

-    }

-}

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 5affd182..f6d673ab 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -69,23 +69,23 @@ namespace Microsoft.Boogie
             foreach (Variable x in proc.InParams)

             {

                 this.thisInParams.Add(x);

-                Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true);

+                Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true, x.Attributes);

                 this.thatInParams.Add(y);

                 map[x] = new IdentifierExpr(Token.NoToken, y);

             }

             foreach (Variable x in proc.OutParams)

             {

                 this.thisOutParams.Add(x);

-                Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);

+                Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false, x.Attributes);

                 this.thatOutParams.Add(y);

                 map[x] = new IdentifierExpr(Token.NoToken, y);

             }

-            List<Variable> otherLocVars = new List<Variable>();

+            List<Variable> thatLocVars = new List<Variable>();

             foreach (Variable x in thisAction.LocVars)

             {

                 Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);

                 map[x] = new IdentifierExpr(Token.NoToken, y);

-                otherLocVars.Add(y);

+                thatLocVars.Add(y);

             }

             Contract.Assume(proc.TypeParameters.Count == 0);

             Substitution subst = Substituter.SubstitutionFromHashtable(map);

@@ -94,7 +94,7 @@ namespace Microsoft.Boogie
                 thatGate.Add((AssertCmd)Substituter.Apply(subst, assertCmd));

             }

             Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();

-            List<Block> otherBlocks = new List<Block>();

+            List<Block> thatBlocks = new List<Block>();

             foreach (Block block in thisAction.Blocks)

             {

                 List<Cmd> otherCmds = new List<Cmd>();

@@ -102,12 +102,12 @@ namespace Microsoft.Boogie
                 {

                     otherCmds.Add(Substituter.Apply(subst, cmd));

                 }

-                Block otherBlock = new Block();

-                otherBlock.Cmds = otherCmds;

-                otherBlock.Label = "that_" + block.Label;

+                Block thatBlock = new Block();

+                thatBlock.Cmds = otherCmds;

+                thatBlock.Label = "that_" + block.Label;

                 block.Label = "this_" + block.Label;

-                otherBlocks.Add(otherBlock);

-                blockMap[block] = otherBlock;

+                thatBlocks.Add(thatBlock);

+                blockMap[block] = thatBlock;

                 if (block.TransferCmd is GotoCmd)

                 {

                     GotoCmd gotoCmd = block.TransferCmd as GotoCmd;

@@ -125,17 +125,17 @@ namespace Microsoft.Boogie
                     blockMap[block].TransferCmd = new ReturnCmd(block.TransferCmd.tok);

                     continue;

                 }

-                List<Block> otherGotoCmdLabelTargets = new List<Block>();

-                List<string> otherGotoCmdLabelNames = new List<string>();

+                List<Block> thatGotoCmdLabelTargets = new List<Block>();

+                List<string> thatGotoCmdLabelNames = new List<string>();

                 GotoCmd gotoCmd = block.TransferCmd as GotoCmd;

                 foreach (Block target in gotoCmd.labelTargets)

                 {

-                    otherGotoCmdLabelTargets.Add(blockMap[target]);

-                    otherGotoCmdLabelNames.Add(blockMap[target].Label);

+                    thatGotoCmdLabelTargets.Add(blockMap[target]);

+                    thatGotoCmdLabelNames.Add(blockMap[target].Label);

                 }

-                blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets);

+                blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, thatGotoCmdLabelNames, thatGotoCmdLabelTargets);

             }

-            this.thatAction = new CodeExpr(otherLocVars, otherBlocks);

+            this.thatAction = new CodeExpr(thatLocVars, thatBlocks);

         }

     }

 

@@ -220,6 +220,10 @@ namespace Microsoft.Boogie
         public override Procedure VisitProcedure(Procedure node)

         {

             enclosingProcPhaseNum = FindPhaseNumber(node);

+            if (enclosingProcPhaseNum != int.MaxValue)

+            {

+                assertionPhaseNums.Add(enclosingProcPhaseNum);

+            }

             return base.VisitProcedure(node);

         }

         public override Cmd VisitCallCmd(CallCmd node)

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index a734c15e..0e64f6b2 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -72,9 +72,9 @@ ensures {:phase 2} tid != nil && Inv2(T, s, cs);
 ensures {:right 2} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil; cs := tid; return true; }|;

 {

     var m: int;

-    tid := tid';

 

     par Yield1() | Yield2();

+    tid := tid';

     call tid, m := GetTicketAbstract(tid);

     par Yield1();

     call tid := WaitAndEnter(tid, m);

@@ -86,9 +86,8 @@ requires {:phase 1} Inv1(T, t);
 ensures {:phase 1} Inv1(T, t);

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

 {

-    tid := tid';

-

     par Yield1();

+    tid := tid';

     call tid, m := GetTicket(tid);

     par Yield1();

 }