modified desugaring so that in commutatitivity checks copies of original

codeexpr is made.

3 files changed, 1963 insertions, 1919 deletions

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index ed069d5d..7c6d4ac4 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -1,648 +1,673 @@
-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using System.Diagnostics.Contracts;

-using System.Diagnostics;

-

-namespace Microsoft.Boogie

-{

-    public class MoverCheck

-    {

-        LinearTypeChecker linearTypeChecker;

-        MoverTypeChecker moverTypeChecker;

-        List<Declaration> decls;

-        HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> commutativityCheckerCache;

-        HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> gatePreservationCheckerCache;

-        HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> failurePreservationCheckerCache;

-        private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)

-        {

-            this.linearTypeChecker = linearTypeChecker;

-            this.moverTypeChecker = moverTypeChecker;

-            this.decls = decls;

-            this.commutativityCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();

-            this.gatePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();

-            this.failurePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();

-        }

-

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

-        {

-            if (moverTypeChecker.procToActionInfo.Count == 0)

-                return;

-

-            List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern));

-            sortedByCreatedLayerNum.Sort((x, y) => { return (x.createdAtLayerNum == y.createdAtLayerNum) ? 0 : (x.createdAtLayerNum < y.createdAtLayerNum) ? -1 : 1; });

-            List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern));

-            sortedByAvailableUptoLayerNum.Sort((x, y) => { return (x.availableUptoLayerNum == y.availableUptoLayerNum) ? 0 : (x.availableUptoLayerNum < y.availableUptoLayerNum) ? -1 : 1; });

-

-            Dictionary<int, HashSet<AtomicActionInfo>> pools = new Dictionary<int, HashSet<AtomicActionInfo>>();

-            int indexIntoSortedByCreatedLayerNum = 0;

-            int indexIntoSortedByAvailableUptoLayerNum = 0;

-            HashSet<AtomicActionInfo> currPool = new HashSet<AtomicActionInfo>();

-            while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count)

-            {

-                var currLayerNum = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum].createdAtLayerNum;

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

-                while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count)

-                {

-                    var actionInfo = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum] as AtomicActionInfo;

-                    if (actionInfo.createdAtLayerNum > currLayerNum) break;

-                    pools[currLayerNum].Add(actionInfo);

-                    indexIntoSortedByCreatedLayerNum++;

-                }

-                while (indexIntoSortedByAvailableUptoLayerNum < sortedByAvailableUptoLayerNum.Count)

-                {

-                    var actionInfo = sortedByAvailableUptoLayerNum[indexIntoSortedByAvailableUptoLayerNum] as AtomicActionInfo;

-                    if (actionInfo.availableUptoLayerNum > currLayerNum) break;

-                    pools[currLayerNum].Remove(actionInfo);

-                    indexIntoSortedByAvailableUptoLayerNum++;

-                }

-                currPool = pools[currLayerNum];

-            }

-

-            Program program = moverTypeChecker.program;

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

-            foreach (int layerNum in pools.Keys)

-            {

-                foreach (AtomicActionInfo first in pools[layerNum])

-                {

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

-                    if (first.moverType == MoverType.Atomic)

-                        continue;

-                    foreach (AtomicActionInfo second in pools[layerNum])

-                    {

-                        if (first.IsRightMover)

-                        {

-                            moverChecking.CreateCommutativityChecker(program, first, second);

-                            moverChecking.CreateGatePreservationChecker(program, second, first);

-                        }

-                        if (first.IsLeftMover)

-                        {

-                            moverChecking.CreateCommutativityChecker(program, second, first);

-                            moverChecking.CreateGatePreservationChecker(program, first, second);

-                            moverChecking.CreateFailurePreservationChecker(program, second, first);

-                        }

-                    }

-                }

-            }

-            foreach (AtomicActionInfo atomicActionInfo in sortedByCreatedLayerNum)

-            {

-                if (atomicActionInfo.IsLeftMover && atomicActionInfo.hasAssumeCmd)

-                {

-                    moverChecking.CreateNonBlockingChecker(program, atomicActionInfo);

-                }

-            }

-        }

-

-        public sealed class MyDuplicator : Duplicator

-        {

-            public override Expr VisitIdentifierExpr(IdentifierExpr node)

-            {

-                IdentifierExpr ret = (IdentifierExpr) base.VisitIdentifierExpr(node);

-                if (ret.Decl is GlobalVariable)

-                {

-                    return new OldExpr(Token.NoToken, ret);

-                }

-                else

-                {

-                    return ret;

-                }

-            }

-        }

-

-        public class TransitionRelationComputation

-        {

-            private Program program;

-            private AtomicActionInfo first;  // corresponds to that*

-            private AtomicActionInfo second; // corresponds to this*

-            private Stack<Cmd> cmdStack;

-            private List<PathInfo> paths;

-            private HashSet<Variable> frame;

-            private HashSet<Variable> postExistVars;

-

-            public TransitionRelationComputation(Program program, AtomicActionInfo second, HashSet<Variable> frame, HashSet<Variable> postExistVars)

-            {

-                this.postExistVars = postExistVars;

-                this.frame = frame;

-                TransitionRelationComputationHelper(program, null, second);

-            }

-

-            public TransitionRelationComputation(Program program, AtomicActionInfo first, AtomicActionInfo second, HashSet<Variable> frame, HashSet<Variable> postExistVars)

-            {

-                this.postExistVars = postExistVars;

-                this.frame = frame;

-                TransitionRelationComputationHelper(program, first, second);

-            }

-

-            private void TransitionRelationComputationHelper(Program program, AtomicActionInfo first, AtomicActionInfo second)

-            {

-                this.program = program;

-                this.first = first;

-                this.second = second;

-                this.cmdStack = new Stack<Cmd>();

-                this.paths = new List<PathInfo>();

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

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

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

-                if (havocVars.Count > 0)

-                {

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

-                    cmdStack.Push(havocCmd);

-                }

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

-            }

-

-            private void Substitute(Dictionary<Variable, Expr> map, ref List<Expr> pathExprs, ref Dictionary<Variable, Expr> varToExpr)

-            {

-                Substitution subst = Substituter.SubstitutionFromHashtable(map);

-                List<Expr> oldPathExprs = pathExprs;

-                pathExprs = new List<Expr>();

-                foreach (Expr pathExpr in oldPathExprs)

-                {

-                    pathExprs.Add(Substituter.Apply(subst, pathExpr));

-                }

-                Dictionary<Variable, Expr> oldVarToExpr = varToExpr;

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

-                foreach (Variable v in oldVarToExpr.Keys)

-                {

-                    varToExpr[v] = Substituter.Apply(subst, oldVarToExpr[v]);

-                }

-            }

-

-            struct PathInfo

-            {

-                public HashSet<Variable> existsVars;

-                public Dictionary<Variable, Expr> varToExpr;

-                public List<Expr> pathExprs;

-

-                public PathInfo(HashSet<Variable> existsVars, Dictionary<Variable, Expr> varToExpr, List<Expr> pathExprs)

-                {

-                    this.existsVars = existsVars;

-                    this.varToExpr = varToExpr;

-                    this.pathExprs = pathExprs;

-                }

-            }

-            

-            private void FlattenAnd(Expr x, List<Expr> xs)

-            {

-                NAryExpr naryExpr = x as NAryExpr;

-                if (naryExpr != null && naryExpr.Fun.FunctionName == "&&")

-                {

-                    FlattenAnd(naryExpr.Args[0], xs);

-                    FlattenAnd(naryExpr.Args[1], xs);

-                }

-                else

-                {

-                    xs.Add(x);

-                }

-            }

-

-            private void AddPath()

-            {

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

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

-                foreach (Variable v in frame)

-                {

-                    varToExpr[v] = Expr.Ident(v);

-                }

-                if (first != null)

-                {

-                    foreach (Variable v in first.thatOutParams)

-                    {

-                        varToExpr[v] = Expr.Ident(v);

-                    }

-                }

-                foreach (Variable v in second.thisOutParams)

-                {

-                    varToExpr[v] = Expr.Ident(v);

-                }

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

-                int boundVariableCount = 0;

-                foreach (Cmd cmd in cmdStack)

-                {

-                    if (cmd is AssumeCmd)

-                    {

-                        AssumeCmd assumeCmd = cmd as AssumeCmd;

-                        FlattenAnd(assumeCmd.Expr, pathExprs);

-                    }

-                    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];

-                        }

-                        Substitute(map, ref pathExprs, ref varToExpr);

-                    }

-                    else if (cmd is HavocCmd)

-                    {

-                        HavocCmd havocCmd = cmd as HavocCmd;

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

-                        foreach (IdentifierExpr ie in havocCmd.Vars)

-                        {

-                            BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "#tmp_" + boundVariableCount++, ie.Decl.TypedIdent.Type));

-                            map[ie.Decl] = Expr.Ident(bv);

-                            existsVars.Add(bv);

-                        }

-                        Substitute(map, ref pathExprs, ref varToExpr);

-                    }

-                    else

-                    {

-                        Debug.Assert(false);

-                    }

-                }

-                paths.Add(new PathInfo(existsVars, varToExpr, pathExprs));

-            }

-

-            private Expr CalculatePathCondition(PathInfo path)

-            {

-                Expr returnExpr = Expr.True;

-

-                HashSet<Variable> existsVars = path.existsVars;

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

-

-                Dictionary<Variable, Expr> varToExpr = path.varToExpr;

-                foreach (Variable v in varToExpr.Keys)

-                {

-                    if (postExistVars.Contains(v)) continue;

-                    IdentifierExpr ie = varToExpr[v] as IdentifierExpr;

-                    if (ie != null && !existsMap.ContainsKey(ie.Decl) && existsVars.Contains(ie.Decl))

-                    {

-                        existsMap[ie.Decl] = Expr.Ident(v);

-                        existsVars.Remove(ie.Decl);

-                    }

-                    else

-                    {

-                        returnExpr = Expr.And(returnExpr, Expr.Eq(Expr.Ident(v), (new MyDuplicator()).VisitExpr(varToExpr[v])));

-                        returnExpr.Type = Type.Bool;

-                    }

-                }

-

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

-                path.pathExprs.ForEach(x => pathExprs.Add((new MyDuplicator()).VisitExpr(x)));

-                foreach (Expr x in pathExprs)

-                {

-                    Variable boundVar;

-                    Expr boundVarExpr;

-                    if (InferSubstitution(x, out boundVar, out boundVarExpr) && existsVars.Contains(boundVar))

-                    {

-                        existsMap[boundVar] = boundVarExpr;

-                        existsVars.Remove(boundVar);

-                    }

-                    else

-                    {

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

-                        returnExpr.Type = Type.Bool;

-                    }

-                }

-                

-                returnExpr = Substituter.Apply(Substituter.SubstitutionFromHashtable(existsMap), returnExpr);

-                if (existsVars.Count > 0)

-                {

-                    returnExpr = new ExistsExpr(Token.NoToken, new List<Variable>(existsVars), returnExpr);

-                }

-                return returnExpr;

-            }

-

-            bool InferSubstitution(Expr x, out Variable var, out Expr expr)

-            {

-                var = null;

-                expr = null;

-                NAryExpr naryExpr = x as NAryExpr;

-                if (naryExpr == null || naryExpr.Fun.FunctionName != "==")

-                {

-                    return false;

-                }

-                IdentifierExpr arg0 = naryExpr.Args[0] as IdentifierExpr;

-                if (arg0 != null && arg0.Decl is BoundVariable)

-                {

-                    var = arg0.Decl;

-                    expr = naryExpr.Args[1];

-                    return true;

-                }

-                IdentifierExpr arg1 = naryExpr.Args[1] as IdentifierExpr;

-                if (arg1 != null && arg1.Decl is BoundVariable)

-                {

-                    var = arg1.Decl;

-                    expr = naryExpr.Args[0];

-                    return true;

-                }

-                return false;

-            }

-

-            public Expr TransitionRelationCompute()

-            {

-                Expr transitionRelation = Expr.False;

-                foreach (PathInfo path in paths)

-                {

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

-                }

-                ResolutionContext rc = new ResolutionContext(null);

-                rc.StateMode = ResolutionContext.State.Two;

-                transitionRelation.Resolve(rc);

-                transitionRelation.Typecheck(new TypecheckingContext(null));

-                return transitionRelation;

-            }

-

-            private void Search(Block b, bool inFirst)

-            {

-                int pathSizeAtEntry = cmdStack.Count;

-                foreach (Cmd cmd in b.Cmds)

-                {

-                    cmdStack.Push(cmd);

-                }

-                if (b.TransferCmd is ReturnCmd)

-                {

-                    if (first == null || inFirst)

-                    {

-                        AddPath();

-                    }

-                    else

-                    {

-                        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);

-                            cmdStack.Push(havocCmd);

-                        }

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

-                    }

-                }

-                else

-                {

-                    GotoCmd gotoCmd = b.TransferCmd as GotoCmd;

-                    foreach (Block target in gotoCmd.labelTargets)

-                    {

-                        Search(target, inFirst);

-                    }

-                }

-                Debug.Assert(cmdStack.Count >= pathSizeAtEntry);

-                while (cmdStack.Count > pathSizeAtEntry)

-                {

-                    cmdStack.Pop();

-                }

-            }

-        }

-

-        private static List<Block> CloneBlocks(List<Block> blocks)

-        {

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

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

-            foreach (Block block in blocks)

-            {

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

-                foreach (Cmd cmd in block.Cmds)

-                {

-                    otherCmds.Add(cmd);

-                }

-                Block otherBlock = new Block();

-                otherBlock.Cmds = otherCmds;

-                otherBlock.Label = block.Label;

-                otherBlocks.Add(otherBlock);

-                blockMap[block] = otherBlock;

-            }

-            foreach (Block block in blocks)

-            {

-                if (block.TransferCmd is ReturnCmd) continue;

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

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

-                GotoCmd gotoCmd = block.TransferCmd as GotoCmd;

-                foreach (Block target in gotoCmd.labelTargets)

-                {

-                    otherGotoCmdLabelTargets.Add(blockMap[target]);

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

-                }

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

-            }

-            return otherBlocks;

-        }

-

-        private List<Requires> DisjointnessRequires(Program program, AtomicActionInfo first, AtomicActionInfo second, HashSet<Variable> frame)

-        {

-            List<Requires> requires = new List<Requires>();

-            Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();

-            foreach (var domainName in linearTypeChecker.linearDomains.Keys)

-            {

-                domainNameToScope[domainName] = new HashSet<Variable>();

-            }

-            foreach (Variable v in frame)

-            {

-                var domainName = linearTypeChecker.FindDomainName(v);

-                if (domainName == null) continue;

-                if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

-                domainNameToScope[domainName].Add(v);

-            }

-            if (first != null)

-            {

-                foreach (Variable v in first.thatInParams)

-                {

-                    var domainName = linearTypeChecker.FindDomainName(v);

-                    if (domainName == null) continue;

-                    if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

-                    domainNameToScope[domainName].Add(v);

-                }

-            }

-            foreach (Variable v in second.thisInParams)

-            {

-                var domainName = linearTypeChecker.FindDomainName(v);

-                if (domainName == null) continue;

-                if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

-                domainNameToScope[domainName].Add(v);

-            }

-            foreach (string domainName in domainNameToScope.Keys)

-            {

-                requires.Add(new Requires(false, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName])));

-            }

-            return requires;

-        }

-

-        private void CreateCommutativityChecker(Program program, AtomicActionInfo first, AtomicActionInfo second)

-        {

-            if (first == second && first.thatInParams.Count == 0 && first.thatOutParams.Count == 0)

-                return;

-            if (first.CommutesWith(second))

-                return;

-            Tuple<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second);

-            if (commutativityCheckerCache.Contains(actionPair))

-                return;

-            commutativityCheckerCache.Add(actionPair);

-

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

-            inputs.AddRange(first.thatInParams);

-            inputs.AddRange(second.thisInParams);

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

-            outputs.AddRange(first.thatOutParams);

-            outputs.AddRange(second.thisOutParams);

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

-            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)

-                {

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

-                    bs.Add(secondBlocks[0]);

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

-                    ls.Add(secondBlocks[0].Label);

-                    b.TransferCmd = new GotoCmd(Token.NoToken, ls, bs);

-                }

-            }

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

-            blocks.AddRange(firstBlocks);

-            blocks.AddRange(secondBlocks);

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

-            frame.UnionWith(first.gateUsedGlobalVars);

-            frame.UnionWith(first.actionUsedGlobalVars);

-            frame.UnionWith(second.gateUsedGlobalVars);

-            frame.UnionWith(second.actionUsedGlobalVars);

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

-            foreach (AssertCmd assertCmd in first.thatGate)

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

-            foreach (AssertCmd assertCmd in second.thisGate)

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

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

-            Expr transitionRelation = (new TransitionRelationComputation(program, first, second, frame, new HashSet<Variable>())).TransitionRelationCompute();

-            Ensures ensureCheck = new Ensures(false, transitionRelation);

-            ensureCheck.ErrorData = string.Format("Commutativity check between {0} and {1} failed", first.proc.Name, second.proc.Name);

-            ensures.Add(ensureCheck);

-            string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name);

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

-            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

-            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);

-            Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, blocks);

-            impl.Proc = proc;

-            this.decls.Add(impl);

-            this.decls.Add(proc);

-        }

-

-        private void CreateGatePreservationChecker(Program program, AtomicActionInfo first, AtomicActionInfo second)

-        {

-            if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)

-                return;

-            Tuple<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second);

-            if (gatePreservationCheckerCache.Contains(actionPair))

-                return;

-            gatePreservationCheckerCache.Add(actionPair);

-

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

-            inputs.AddRange(first.thatInParams);

-            inputs.AddRange(second.thisInParams);

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

-            outputs.AddRange(first.thatOutParams);

-            outputs.AddRange(second.thisOutParams);

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

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

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

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

-            frame.UnionWith(first.gateUsedGlobalVars);

-            frame.UnionWith(second.gateUsedGlobalVars);

-            frame.UnionWith(second.actionUsedGlobalVars);

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

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

-            foreach (AssertCmd assertCmd in first.thatGate)

-            {

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

-                Ensures ensureCheck = new Ensures(assertCmd.tok, false, assertCmd.Expr, null);

-                ensureCheck.ErrorData = string.Format("Gate not preserved by {0}", second.proc.Name);

-                ensures.Add(ensureCheck);

-            }

-            foreach (AssertCmd assertCmd in second.thisGate)

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

-            string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);

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

-            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

-            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);

-            Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);

-            impl.Proc = proc;

-            this.decls.Add(impl);

-            this.decls.Add(proc);

-        }

-

-        private void CreateFailurePreservationChecker(Program program, AtomicActionInfo first, AtomicActionInfo second)

-        {

-            if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)

-                return;

-            Tuple<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second);

-            if (failurePreservationCheckerCache.Contains(actionPair))

-                return;

-            failurePreservationCheckerCache.Add(actionPair);

-

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

-            inputs.AddRange(first.thatInParams);

-            inputs.AddRange(second.thisInParams);

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

-            outputs.AddRange(first.thatOutParams);

-            outputs.AddRange(second.thisOutParams);

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

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

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

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

-            frame.UnionWith(first.gateUsedGlobalVars);

-            frame.UnionWith(second.gateUsedGlobalVars);

-            frame.UnionWith(second.actionUsedGlobalVars);

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

-            Expr gateExpr = Expr.True;

-            foreach (AssertCmd assertCmd in first.thatGate)

-            {

-                gateExpr = Expr.And(gateExpr, assertCmd.Expr);

-                gateExpr.Type = Type.Bool;

-            }

-            gateExpr = Expr.Not(gateExpr);

-            gateExpr.Type = Type.Bool;

-            requires.Add(new Requires(false, gateExpr));

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

-            Ensures ensureCheck = new Ensures(false, gateExpr);

-            ensureCheck.ErrorData = string.Format("Gate failure of {0} not preserved by {1}", first.proc.Name, second.proc.Name);

-            ensures.Add(ensureCheck);

-            foreach (AssertCmd assertCmd in second.thisGate)

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

-            string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);

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

-            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

-            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);

-            Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);

-            impl.Proc = proc;

-            this.decls.Add(impl);

-            this.decls.Add(proc);

-        }

-

-        private void CreateNonBlockingChecker(Program program, AtomicActionInfo second)

-        {

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

-            inputs.AddRange(second.thisInParams);

-

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

-            frame.UnionWith(second.gateUsedGlobalVars);

-            frame.UnionWith(second.actionUsedGlobalVars);

-            List<Requires> requires = DisjointnessRequires(program, null, second, frame);

-            foreach (AssertCmd assertCmd in second.thisGate)

-            {

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

-            }

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

-            postExistVars.UnionWith(frame);

-            postExistVars.UnionWith(second.thisOutParams);

-            Expr ensuresExpr = (new TransitionRelationComputation(program, second, frame, postExistVars)).TransitionRelationCompute();

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

-            Ensures ensureCheck = new Ensures(false, ensuresExpr);

-            ensureCheck.ErrorData = string.Format("{0} is blocking", second.proc.Name);

-            ensures.Add(ensureCheck);

-

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

-            blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));

-            string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name);

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

-            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

-            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, globalVars, ensures);

-            Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);

-            impl.Proc = proc;

-            this.decls.Add(impl);

-            this.decls.Add(proc);

-        }

-    }

+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics.Contracts;
+using System.Diagnostics;
+
+namespace Microsoft.Boogie
+{
+    public class MoverCheck
+    {
+        LinearTypeChecker linearTypeChecker;
+        MoverTypeChecker moverTypeChecker;
+        List<Declaration> decls;
+        HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> commutativityCheckerCache;
+        HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> gatePreservationCheckerCache;
+        HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> failurePreservationCheckerCache;
+        private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
+        {
+            this.linearTypeChecker = linearTypeChecker;
+            this.moverTypeChecker = moverTypeChecker;
+            this.decls = decls;
+            this.commutativityCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();
+            this.gatePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();
+            this.failurePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();
+        }
+
+        public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
+        {
+            if (moverTypeChecker.procToActionInfo.Count == 0)
+                return;
+
+            List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern));
+            sortedByCreatedLayerNum.Sort((x, y) => { return (x.createdAtLayerNum == y.createdAtLayerNum) ? 0 : (x.createdAtLayerNum < y.createdAtLayerNum) ? -1 : 1; });
+            List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern));
+            sortedByAvailableUptoLayerNum.Sort((x, y) => { return (x.availableUptoLayerNum == y.availableUptoLayerNum) ? 0 : (x.availableUptoLayerNum < y.availableUptoLayerNum) ? -1 : 1; });
+
+            Dictionary<int, HashSet<AtomicActionInfo>> pools = new Dictionary<int, HashSet<AtomicActionInfo>>();
+            int indexIntoSortedByCreatedLayerNum = 0;
+            int indexIntoSortedByAvailableUptoLayerNum = 0;
+            HashSet<AtomicActionInfo> currPool = new HashSet<AtomicActionInfo>();
+            while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count)
+            {
+                var currLayerNum = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum].createdAtLayerNum;
+                pools[currLayerNum] = new HashSet<AtomicActionInfo>(currPool);
+                while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count)
+                {
+                    var actionInfo = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum] as AtomicActionInfo;
+                    if (actionInfo.createdAtLayerNum > currLayerNum) break;
+                    pools[currLayerNum].Add(actionInfo);
+                    indexIntoSortedByCreatedLayerNum++;
+                }
+                while (indexIntoSortedByAvailableUptoLayerNum < sortedByAvailableUptoLayerNum.Count)
+                {
+                    var actionInfo = sortedByAvailableUptoLayerNum[indexIntoSortedByAvailableUptoLayerNum] as AtomicActionInfo;
+                    if (actionInfo.availableUptoLayerNum > currLayerNum) break;
+                    pools[currLayerNum].Remove(actionInfo);
+                    indexIntoSortedByAvailableUptoLayerNum++;
+                }
+                currPool = pools[currLayerNum];
+            }
+
+            Program program = moverTypeChecker.program;
+            MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls);
+            foreach (int layerNum in pools.Keys)
+            {
+                foreach (AtomicActionInfo first in pools[layerNum])
+                {
+                    Debug.Assert(first.moverType != MoverType.Top);
+                    if (first.moverType == MoverType.Atomic)
+                        continue;
+                    foreach (AtomicActionInfo second in pools[layerNum])
+                    {
+                        if (first.IsRightMover)
+                        {
+                            moverChecking.CreateCommutativityChecker(program, first, second);
+                            moverChecking.CreateGatePreservationChecker(program, second, first);
+                        }
+                        if (first.IsLeftMover)
+                        {
+                            moverChecking.CreateCommutativityChecker(program, second, first);
+                            moverChecking.CreateGatePreservationChecker(program, first, second);
+                            moverChecking.CreateFailurePreservationChecker(program, second, first);
+                        }
+                    }
+                }
+            }
+            foreach (AtomicActionInfo atomicActionInfo in sortedByCreatedLayerNum)
+            {
+                if (atomicActionInfo.IsLeftMover && atomicActionInfo.hasAssumeCmd)
+                {
+                    moverChecking.CreateNonBlockingChecker(program, atomicActionInfo);
+                }
+            }
+        }
+
+        public sealed class MyDuplicator : Duplicator
+        {
+            public override Expr VisitIdentifierExpr(IdentifierExpr node)
+            {
+                IdentifierExpr ret = (IdentifierExpr) base.VisitIdentifierExpr(node);
+                if (ret.Decl is GlobalVariable)
+                {
+                    return new OldExpr(Token.NoToken, ret);
+                }
+                else
+                {
+                    return ret;
+                }
+            }
+        }
+
+        public class TransitionRelationComputation
+        {
+            private Program program;
+            private AtomicActionInfo first;  // corresponds to that*
+            private AtomicActionInfo second; // corresponds to this*
+            private Stack<Cmd> cmdStack;
+            private List<PathInfo> paths;
+            private HashSet<Variable> frame;
+            private HashSet<Variable> postExistVars;
+
+            public TransitionRelationComputation(Program program, AtomicActionInfo second, HashSet<Variable> frame, HashSet<Variable> postExistVars)
+            {
+                this.postExistVars = postExistVars;
+                this.frame = frame;
+                TransitionRelationComputationHelper(program, null, second);
+            }
+
+            public TransitionRelationComputation(Program program, AtomicActionInfo first, AtomicActionInfo second, HashSet<Variable> frame, HashSet<Variable> postExistVars)
+            {
+                this.postExistVars = postExistVars;
+                this.frame = frame;
+                TransitionRelationComputationHelper(program, first, second);
+            }
+
+            private void TransitionRelationComputationHelper(Program program, AtomicActionInfo first, AtomicActionInfo second)
+            {
+                this.program = program;
+                this.first = first;
+                this.second = second;
+                this.cmdStack = new Stack<Cmd>();
+                this.paths = new List<PathInfo>();
+                List<IdentifierExpr> havocVars = new List<IdentifierExpr>();
+                this.second.thisOutParams.ForEach(v => havocVars.Add(Expr.Ident(v)));
+                this.second.thisAction.LocVars.ForEach(v => havocVars.Add(Expr.Ident(v)));
+                if (havocVars.Count > 0)
+                {
+                    HavocCmd havocCmd = new HavocCmd(Token.NoToken, havocVars);
+                    cmdStack.Push(havocCmd);
+                }
+                Search(this.second.thisAction.Blocks[0], false);
+            }
+
+            private void Substitute(Dictionary<Variable, Expr> map, ref List<Expr> pathExprs, ref Dictionary<Variable, Expr> varToExpr)
+            {
+                Substitution subst = Substituter.SubstitutionFromHashtable(map);
+                List<Expr> oldPathExprs = pathExprs;
+                pathExprs = new List<Expr>();
+                foreach (Expr pathExpr in oldPathExprs)
+                {
+                    pathExprs.Add(Substituter.Apply(subst, pathExpr));
+                }
+                Dictionary<Variable, Expr> oldVarToExpr = varToExpr;
+                varToExpr = new Dictionary<Variable, Expr>();
+                foreach (Variable v in oldVarToExpr.Keys)
+                {
+                    varToExpr[v] = Substituter.Apply(subst, oldVarToExpr[v]);
+                }
+            }
+
+            struct PathInfo
+            {
+                public HashSet<Variable> existsVars;
+                public Dictionary<Variable, Expr> varToExpr;
+                public List<Expr> pathExprs;
+
+                public PathInfo(HashSet<Variable> existsVars, Dictionary<Variable, Expr> varToExpr, List<Expr> pathExprs)
+                {
+                    this.existsVars = existsVars;
+                    this.varToExpr = varToExpr;
+                    this.pathExprs = pathExprs;
+                }
+            }
+            
+            private void FlattenAnd(Expr x, List<Expr> xs)
+            {
+                NAryExpr naryExpr = x as NAryExpr;
+                if (naryExpr != null && naryExpr.Fun.FunctionName == "&&")
+                {
+                    FlattenAnd(naryExpr.Args[0], xs);
+                    FlattenAnd(naryExpr.Args[1], xs);
+                }
+                else
+                {
+                    xs.Add(x);
+                }
+            }
+
+            private void AddPath()
+            {
+                HashSet<Variable> existsVars = new HashSet<Variable>();
+                Dictionary<Variable, Expr> varToExpr = new Dictionary<Variable, Expr>();
+                foreach (Variable v in frame)
+                {
+                    varToExpr[v] = Expr.Ident(v);
+                }
+                if (first != null)
+                {
+                    foreach (Variable v in first.thatOutParams)
+                    {
+                        varToExpr[v] = Expr.Ident(v);
+                    }
+                }
+                foreach (Variable v in second.thisOutParams)
+                {
+                    varToExpr[v] = Expr.Ident(v);
+                }
+                List<Expr> pathExprs = new List<Expr>();
+                int boundVariableCount = 0;
+                foreach (Cmd cmd in cmdStack)
+                {
+                    if (cmd is AssumeCmd)
+                    {
+                        AssumeCmd assumeCmd = cmd as AssumeCmd;
+                        FlattenAnd(assumeCmd.Expr, pathExprs);
+                    }
+                    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];
+                        }
+                        Substitute(map, ref pathExprs, ref varToExpr);
+                    }
+                    else if (cmd is HavocCmd)
+                    {
+                        HavocCmd havocCmd = cmd as HavocCmd;
+                        Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+                        foreach (IdentifierExpr ie in havocCmd.Vars)
+                        {
+                            BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "#tmp_" + boundVariableCount++, ie.Decl.TypedIdent.Type));
+                            map[ie.Decl] = Expr.Ident(bv);
+                            existsVars.Add(bv);
+                        }
+                        Substitute(map, ref pathExprs, ref varToExpr);
+                    }
+                    else
+                    {
+                        Debug.Assert(false);
+                    }
+                }
+                paths.Add(new PathInfo(existsVars, varToExpr, pathExprs));
+            }
+
+            private Expr CalculatePathCondition(PathInfo path)
+            {
+                Expr returnExpr = Expr.True;
+
+                HashSet<Variable> existsVars = path.existsVars;
+                Dictionary<Variable, Expr> existsMap = new Dictionary<Variable, Expr>();
+
+                Dictionary<Variable, Expr> varToExpr = path.varToExpr;
+                foreach (Variable v in varToExpr.Keys)
+                {
+                    if (postExistVars.Contains(v)) continue;
+                    IdentifierExpr ie = varToExpr[v] as IdentifierExpr;
+                    if (ie != null && !existsMap.ContainsKey(ie.Decl) && existsVars.Contains(ie.Decl))
+                    {
+                        existsMap[ie.Decl] = Expr.Ident(v);
+                        existsVars.Remove(ie.Decl);
+                    }
+                    else
+                    {
+                        returnExpr = Expr.And(returnExpr, Expr.Eq(Expr.Ident(v), (new MyDuplicator()).VisitExpr(varToExpr[v])));
+                        returnExpr.Type = Type.Bool;
+                    }
+                }
+
+                List<Expr> pathExprs = new List<Expr>();
+                path.pathExprs.ForEach(x => pathExprs.Add((new MyDuplicator()).VisitExpr(x)));
+                foreach (Expr x in pathExprs)
+                {
+                    Variable boundVar;
+                    Expr boundVarExpr;
+                    if (InferSubstitution(x, out boundVar, out boundVarExpr) && existsVars.Contains(boundVar))
+                    {
+                        existsMap[boundVar] = boundVarExpr;
+                        existsVars.Remove(boundVar);
+                    }
+                    else
+                    {
+                        returnExpr = Expr.And(returnExpr, x);
+                        returnExpr.Type = Type.Bool;
+                    }
+                }
+                
+                returnExpr = Substituter.Apply(Substituter.SubstitutionFromHashtable(existsMap), returnExpr);
+                if (existsVars.Count > 0)
+                {
+                    returnExpr = new ExistsExpr(Token.NoToken, new List<Variable>(existsVars), returnExpr);
+                }
+                return returnExpr;
+            }
+
+            bool InferSubstitution(Expr x, out Variable var, out Expr expr)
+            {
+                var = null;
+                expr = null;
+                NAryExpr naryExpr = x as NAryExpr;
+                if (naryExpr == null || naryExpr.Fun.FunctionName != "==")
+                {
+                    return false;
+                }
+                IdentifierExpr arg0 = naryExpr.Args[0] as IdentifierExpr;
+                if (arg0 != null && arg0.Decl is BoundVariable)
+                {
+                    var = arg0.Decl;
+                    expr = naryExpr.Args[1];
+                    return true;
+                }
+                IdentifierExpr arg1 = naryExpr.Args[1] as IdentifierExpr;
+                if (arg1 != null && arg1.Decl is BoundVariable)
+                {
+                    var = arg1.Decl;
+                    expr = naryExpr.Args[0];
+                    return true;
+                }
+                return false;
+            }
+
+            public Expr TransitionRelationCompute(bool withOriginalInOutVariables = false)
+            {
+                Expr transitionRelation = Expr.False;
+                foreach (PathInfo path in paths)
+                {
+                    transitionRelation = Expr.Or(transitionRelation, CalculatePathCondition(path));
+                }
+                ResolutionContext rc = new ResolutionContext(null);
+                rc.StateMode = ResolutionContext.State.Two;
+                transitionRelation.Resolve(rc);
+                transitionRelation.Typecheck(new TypecheckingContext(null));
+
+                if (withOriginalInOutVariables)
+                {
+                    Dictionary<Variable, Expr> invertedMap = new Dictionary<Variable, Expr>();
+                    if (first != null)
+                    {
+                        foreach (var x in first.thatMap)
+                        {
+                            invertedMap[((IdentifierExpr)x.Value).Decl] = Expr.Ident(x.Key);
+                        }
+                    }
+                    if (second != null)
+                    {
+                        foreach (var x in second.thisMap)
+                        {
+                            invertedMap[((IdentifierExpr)x.Value).Decl] = Expr.Ident(x.Key);
+                        }
+                    }
+                    Substitution subst = Substituter.SubstitutionFromHashtable(invertedMap);
+                    return Substituter.Apply(subst, transitionRelation);
+                }
+                else
+                {
+                    return transitionRelation;
+                }
+
+            }
+
+            private void Search(Block b, bool inFirst)
+            {
+                int pathSizeAtEntry = cmdStack.Count;
+                foreach (Cmd cmd in b.Cmds)
+                {
+                    cmdStack.Push(cmd);
+                }
+                if (b.TransferCmd is ReturnCmd)
+                {
+                    if (first == null || inFirst)
+                    {
+                        AddPath();
+                    }
+                    else
+                    {
+                        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);
+                            cmdStack.Push(havocCmd);
+                        }
+                        Search(first.thatAction.Blocks[0], true);
+                    }
+                }
+                else
+                {
+                    GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
+                    foreach (Block target in gotoCmd.labelTargets)
+                    {
+                        Search(target, inFirst);
+                    }
+                }
+                Debug.Assert(cmdStack.Count >= pathSizeAtEntry);
+                while (cmdStack.Count > pathSizeAtEntry)
+                {
+                    cmdStack.Pop();
+                }
+            }
+        }
+
+        private static List<Block> CloneBlocks(List<Block> blocks)
+        {
+            Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
+            List<Block> otherBlocks = new List<Block>();
+            foreach (Block block in blocks)
+            {
+                List<Cmd> otherCmds = new List<Cmd>();
+                foreach (Cmd cmd in block.Cmds)
+                {
+                    otherCmds.Add(cmd);
+                }
+                Block otherBlock = new Block();
+                otherBlock.Cmds = otherCmds;
+                otherBlock.Label = block.Label;
+                otherBlocks.Add(otherBlock);
+                blockMap[block] = otherBlock;
+            }
+            foreach (Block block in blocks)
+            {
+                if (block.TransferCmd is ReturnCmd) continue;
+                List<Block> otherGotoCmdLabelTargets = new List<Block>();
+                List<string> otherGotoCmdLabelNames = new List<string>();
+                GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+                foreach (Block target in gotoCmd.labelTargets)
+                {
+                    otherGotoCmdLabelTargets.Add(blockMap[target]);
+                    otherGotoCmdLabelNames.Add(blockMap[target].Label);
+                }
+                blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets);
+            }
+            return otherBlocks;
+        }
+
+        private List<Requires> DisjointnessRequires(Program program, AtomicActionInfo first, AtomicActionInfo second, HashSet<Variable> frame)
+        {
+            List<Requires> requires = new List<Requires>();
+            Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
+            foreach (var domainName in linearTypeChecker.linearDomains.Keys)
+            {
+                domainNameToScope[domainName] = new HashSet<Variable>();
+            }
+            foreach (Variable v in frame)
+            {
+                var domainName = linearTypeChecker.FindDomainName(v);
+                if (domainName == null) continue;
+                if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
+                domainNameToScope[domainName].Add(v);
+            }
+            if (first != null)
+            {
+                foreach (Variable v in first.thatInParams)
+                {
+                    var domainName = linearTypeChecker.FindDomainName(v);
+                    if (domainName == null) continue;
+                    if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
+                    domainNameToScope[domainName].Add(v);
+                }
+            }
+            foreach (Variable v in second.thisInParams)
+            {
+                var domainName = linearTypeChecker.FindDomainName(v);
+                if (domainName == null) continue;
+                if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
+                domainNameToScope[domainName].Add(v);
+            }
+            foreach (string domainName in domainNameToScope.Keys)
+            {
+                requires.Add(new Requires(false, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName])));
+            }
+            return requires;
+        }
+
+        private void CreateCommutativityChecker(Program program, AtomicActionInfo first, AtomicActionInfo second)
+        {
+            if (first == second && first.thatInParams.Count == 0 && first.thatOutParams.Count == 0)
+                return;
+            if (first.CommutesWith(second))
+                return;
+            Tuple<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second);
+            if (commutativityCheckerCache.Contains(actionPair))
+                return;
+            commutativityCheckerCache.Add(actionPair);
+
+            List<Variable> inputs = new List<Variable>();
+            inputs.AddRange(first.thatInParams);
+            inputs.AddRange(second.thisInParams);
+            List<Variable> outputs = new List<Variable>();
+            outputs.AddRange(first.thatOutParams);
+            outputs.AddRange(second.thisOutParams);
+            List<Variable> locals = new List<Variable>();
+            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)
+                {
+                    List<Block> bs = new List<Block>();
+                    bs.Add(secondBlocks[0]);
+                    List<string> ls = new List<string>();
+                    ls.Add(secondBlocks[0].Label);
+                    b.TransferCmd = new GotoCmd(Token.NoToken, ls, bs);
+                }
+            }
+            List<Block> blocks = new List<Block>();
+            blocks.AddRange(firstBlocks);
+            blocks.AddRange(secondBlocks);
+            HashSet<Variable> frame = new HashSet<Variable>();
+            frame.UnionWith(first.gateUsedGlobalVars);
+            frame.UnionWith(first.actionUsedGlobalVars);
+            frame.UnionWith(second.gateUsedGlobalVars);
+            frame.UnionWith(second.actionUsedGlobalVars);
+            List<Requires> requires = DisjointnessRequires(program, first, second, frame);
+            foreach (AssertCmd assertCmd in first.thatGate)
+                requires.Add(new Requires(false, assertCmd.Expr));
+            foreach (AssertCmd assertCmd in second.thisGate)
+                requires.Add(new Requires(false, assertCmd.Expr));
+            List<Ensures> ensures = new List<Ensures>();
+            Expr transitionRelation = (new TransitionRelationComputation(program, first, second, frame, new HashSet<Variable>())).TransitionRelationCompute();
+            Ensures ensureCheck = new Ensures(false, transitionRelation);
+            ensureCheck.ErrorData = string.Format("Commutativity check between {0} and {1} failed", first.proc.Name, second.proc.Name);
+            ensures.Add(ensureCheck);
+            string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name);
+            List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
+            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
+            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);
+            Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, blocks);
+            impl.Proc = proc;
+            this.decls.Add(impl);
+            this.decls.Add(proc);
+        }
+
+        private void CreateGatePreservationChecker(Program program, AtomicActionInfo first, AtomicActionInfo second)
+        {
+            if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)
+                return;
+            Tuple<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second);
+            if (gatePreservationCheckerCache.Contains(actionPair))
+                return;
+            gatePreservationCheckerCache.Add(actionPair);
+
+            List<Variable> inputs = new List<Variable>();
+            inputs.AddRange(first.thatInParams);
+            inputs.AddRange(second.thisInParams);
+            List<Variable> outputs = new List<Variable>();
+            outputs.AddRange(first.thatOutParams);
+            outputs.AddRange(second.thisOutParams);
+            List<Variable> locals = new List<Variable>();
+            locals.AddRange(second.thisAction.LocVars);
+            List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks);
+            HashSet<Variable> frame = new HashSet<Variable>();
+            frame.UnionWith(first.gateUsedGlobalVars);
+            frame.UnionWith(second.gateUsedGlobalVars);
+            frame.UnionWith(second.actionUsedGlobalVars);
+            List<Requires> requires = DisjointnessRequires(program, first, second, frame);
+            List<Ensures> ensures = new List<Ensures>();
+            foreach (AssertCmd assertCmd in first.thatGate)
+            {
+                requires.Add(new Requires(false, assertCmd.Expr));
+                Ensures ensureCheck = new Ensures(assertCmd.tok, false, assertCmd.Expr, null);
+                ensureCheck.ErrorData = string.Format("Gate not preserved by {0}", second.proc.Name);
+                ensures.Add(ensureCheck);
+            }
+            foreach (AssertCmd assertCmd in second.thisGate)
+                requires.Add(new Requires(false, assertCmd.Expr));
+            string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
+            List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
+            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
+            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);
+            Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);
+            impl.Proc = proc;
+            this.decls.Add(impl);
+            this.decls.Add(proc);
+        }
+
+        private void CreateFailurePreservationChecker(Program program, AtomicActionInfo first, AtomicActionInfo second)
+        {
+            if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)
+                return;
+            Tuple<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second);
+            if (failurePreservationCheckerCache.Contains(actionPair))
+                return;
+            failurePreservationCheckerCache.Add(actionPair);
+
+            List<Variable> inputs = new List<Variable>();
+            inputs.AddRange(first.thatInParams);
+            inputs.AddRange(second.thisInParams);
+            List<Variable> outputs = new List<Variable>();
+            outputs.AddRange(first.thatOutParams);
+            outputs.AddRange(second.thisOutParams);
+            List<Variable> locals = new List<Variable>();
+            locals.AddRange(second.thisAction.LocVars);
+            List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks);
+            HashSet<Variable> frame = new HashSet<Variable>();
+            frame.UnionWith(first.gateUsedGlobalVars);
+            frame.UnionWith(second.gateUsedGlobalVars);
+            frame.UnionWith(second.actionUsedGlobalVars);
+            List<Requires> requires = DisjointnessRequires(program, first, second, frame);
+            Expr gateExpr = Expr.True;
+            foreach (AssertCmd assertCmd in first.thatGate)
+            {
+                gateExpr = Expr.And(gateExpr, assertCmd.Expr);
+                gateExpr.Type = Type.Bool;
+            }
+            gateExpr = Expr.Not(gateExpr);
+            gateExpr.Type = Type.Bool;
+            requires.Add(new Requires(false, gateExpr));
+            List<Ensures> ensures = new List<Ensures>();
+            Ensures ensureCheck = new Ensures(false, gateExpr);
+            ensureCheck.ErrorData = string.Format("Gate failure of {0} not preserved by {1}", first.proc.Name, second.proc.Name);
+            ensures.Add(ensureCheck);
+            foreach (AssertCmd assertCmd in second.thisGate)
+                requires.Add(new Requires(false, assertCmd.Expr));
+            string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
+            List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
+            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
+            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);
+            Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);
+            impl.Proc = proc;
+            this.decls.Add(impl);
+            this.decls.Add(proc);
+        }
+
+        private void CreateNonBlockingChecker(Program program, AtomicActionInfo second)
+        {
+            List<Variable> inputs = new List<Variable>();
+            inputs.AddRange(second.thisInParams);
+
+            HashSet<Variable> frame = new HashSet<Variable>();
+            frame.UnionWith(second.gateUsedGlobalVars);
+            frame.UnionWith(second.actionUsedGlobalVars);
+            List<Requires> requires = DisjointnessRequires(program, null, second, frame);
+            foreach (AssertCmd assertCmd in second.thisGate)
+            {
+                requires.Add(new Requires(false, assertCmd.Expr));
+            }
+            HashSet<Variable> postExistVars = new HashSet<Variable>();
+            postExistVars.UnionWith(frame);
+            postExistVars.UnionWith(second.thisOutParams);
+            Expr ensuresExpr = (new TransitionRelationComputation(program, second, frame, postExistVars)).TransitionRelationCompute();
+            List<Ensures> ensures = new List<Ensures>();
+            Ensures ensureCheck = new Ensures(false, ensuresExpr);
+            ensureCheck.ErrorData = string.Format("{0} is blocking", second.proc.Name);
+            ensures.Add(ensureCheck);
+
+            List<Block> blocks = new List<Block>();
+            blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));
+            string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name);
+            List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
+            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
+            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, globalVars, ensures);
+            Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);
+            impl.Proc = proc;
+            this.decls.Add(impl);
+            this.decls.Add(proc);
+        }
+    }
 }
\ No newline at end of file
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 626f2c4a..2ad08024 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -1,1206 +1,1206 @@
-using System;

-using System.Collections;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using System.Threading.Tasks;

-using Microsoft.Boogie;

-using System.Diagnostics;

-using System.Diagnostics.Contracts;

-using Microsoft.Boogie.GraphUtil;

-

-namespace Microsoft.Boogie

-{

-    public class MyDuplicator : Duplicator

-    {

-        MoverTypeChecker moverTypeChecker;

-        public int layerNum;

-        Procedure enclosingProc;

-        Implementation enclosingImpl;

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

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

-        public Dictionary<Implementation, Implementation> implMap; /* Duplicate -> Original */

-        public HashSet<Procedure> yieldingProcs;

-        public List<Implementation> impls;

-

-        public MyDuplicator(MoverTypeChecker moverTypeChecker, int layerNum)

-        {

-            this.moverTypeChecker = moverTypeChecker;

-            this.layerNum = layerNum;

-            this.enclosingProc = null;

-            this.enclosingImpl = null;

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

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

-            this.implMap = new Dictionary<Implementation, Implementation>();

-            this.yieldingProcs = new HashSet<Procedure>();

-            this.impls = new List<Implementation>();

-        }

-

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

-        {

-            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 && layerNum == enclosingProcLayerNum)

-                {

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

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

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

-                    {

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

-                    }

-                    Substitution subst = Substituter.SubstitutionFromHashtable(map);

-                    foreach (AssertCmd assertCmd in atomicActionInfo.thisGate)

-                    {

-                        newCmds.Add(Substituter.Apply(subst, assertCmd));

-                    }

-                }

-            }

-            newCmds.Add(callCmd);

-        }

-

-        private void ProcessParCallCmd(ParCallCmd originalParCallCmd, ParCallCmd parCallCmd, List<Cmd> newCmds)

-        {

-            int maxCalleeLayerNum = 0;

-            foreach (CallCmd iter in originalParCallCmd.CallCmds)

-            {

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

-                if (calleeLayerNum > maxCalleeLayerNum)

-                    maxCalleeLayerNum = calleeLayerNum;

-            }

-            if (layerNum > maxCalleeLayerNum)

-            {

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

-                {

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

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

-                }

-            }

-            else

-            {

-                newCmds.Add(parCallCmd);

-            }

-        }

-

-        public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq)

-        {

-            List<Cmd> cmds = base.VisitCmdSeq(cmdSeq);

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

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

-            {

-                Cmd originalCmd = cmdSeq[i];

-                Cmd cmd = cmds[i];

-

-                CallCmd originalCallCmd = originalCmd as CallCmd;

-                if (originalCallCmd != null)

-                {

-                    ProcessCallCmd(originalCallCmd, cmd as CallCmd, newCmds);

-                    continue;

-                }

-

-                ParCallCmd originalParCallCmd = originalCmd as ParCallCmd;

-                if (originalParCallCmd != null)

-                {

-                    ProcessParCallCmd(originalParCallCmd, cmd as ParCallCmd, newCmds);

-                    continue;

-                }

-             

-                newCmds.Add(cmd);

-            }

-            return newCmds;

-        }

-

-        public override YieldCmd VisitYieldCmd(YieldCmd node)

-        {

-            YieldCmd yieldCmd = base.VisitYieldCmd(node);

-            absyMap[yieldCmd] = node;

-            return yieldCmd;

-        }

-        

-        public override Block VisitBlock(Block node)

-        {

-            Block block = base.VisitBlock(node);

-            absyMap[block] = node;

-            return block;

-        }

-        

-        public override Cmd VisitCallCmd(CallCmd node)

-        {

-            CallCmd callCmd = (CallCmd) base.VisitCallCmd(node);

-            callCmd.Proc = VisitProcedure(callCmd.Proc);

-            callCmd.callee = callCmd.Proc.Name;

-            absyMap[callCmd] = node;

-            return callCmd;

-        }

-

-        public override Cmd VisitParCallCmd(ParCallCmd node)

-        {

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

-            absyMap[parCallCmd] = node;

-            return parCallCmd;

-        }

-

-        public override Procedure VisitProcedure(Procedure node)

-        {

-            if (!moverTypeChecker.procToActionInfo.ContainsKey(node))

-                return node;

-            if (!procMap.ContainsKey(node))

-            {

-                enclosingProc = node;

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

-                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.createdAtLayerNum < layerNum)

-                {

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

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

-                    Implementation impl;

-                    AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;

-                    if (atomicActionInfo != null)

-                    {

-                        CodeExpr action = (CodeExpr)VisitCodeExpr(atomicActionInfo.thisAction);

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

-                        foreach (AssertCmd assertCmd in atomicActionInfo.thisGate)

-                        {

-                            cmds.Add(new AssumeCmd(Token.NoToken, (Expr)Visit(assertCmd.Expr)));

-                        }

-                        Block newInitBlock = new Block(Token.NoToken, "_init", cmds,

-                            new GotoCmd(Token.NoToken, new List<string>(new string[] { action.Blocks[0].Label }),

-                                                       new List<Block>(new Block[] { action.Blocks[0] })));

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

-                        newBlocks.Add(newInitBlock);

-                        newBlocks.AddRange(action.Blocks);

-                        impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, action.LocVars, newBlocks);

-                    }

-                    else

-                    {

-                        Block newInitBlock = new Block(Token.NoToken, "_init", new List<Cmd>(), new ReturnCmd(Token.NoToken));

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

-                        newBlocks.Add(newInitBlock);

-                        impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, new List<Variable>(), newBlocks);

-                    }

-                    impl.Proc = proc;

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

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

-                    impls.Add(impl);

-                }

-                else

-                {

-                    yieldingProcs.Add(proc);

-                    proc.Requires = this.VisitRequiresSeq(node.Requires);

-                    proc.Ensures = this.VisitEnsuresSeq(node.Ensures);

-                }

-                procMap[node] = proc;

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

-                moverTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));

-            }

-            return procMap[node];

-        }

-

-        private Variable dummyLocalVar;

-        public override Implementation VisitImplementation(Implementation node)

-        {

-            enclosingImpl = node;

-            dummyLocalVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_dummy", Type.Bool));

-            Implementation impl = base.VisitImplementation(node);

-            implMap[impl] = node;

-            impl.LocVars.Add(dummyLocalVar);

-            impl.Name = impl.Proc.Name;

-            return impl;

-        }

-

-        public override Requires VisitRequires(Requires node)

-        {

-            Requires requires = base.VisitRequires(node);

-            if (node.Free)

-                return requires;

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

-                requires.Condition = Expr.True;

-            return requires;

-        }

-

-        public override Ensures VisitEnsures(Ensures node)

-        {

-            Ensures ensures = base.VisitEnsures(node);

-            if (node.Free)

-                return ensures;

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

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

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

-            {

-                ensures.Condition = Expr.True;

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

-            }

-            return ensures;

-        }

-

-        public override Cmd VisitAssertCmd(AssertCmd node)

-        {

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

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

-                assertCmd.Expr = Expr.True;

-            return assertCmd;

-        }

-    }

-

-    public class OwickiGries

-    {

-        LinearTypeChecker linearTypeChecker;

-        MoverTypeChecker moverTypeChecker;

-        Dictionary<Absy, Absy> absyMap;

-        Dictionary<Implementation, Implementation> implMap;

-        HashSet<Procedure> yieldingProcs;

-        int layerNum;

-        List<IdentifierExpr> globalMods;

-        Dictionary<string, Procedure> asyncAndParallelCallDesugarings;

-        List<Procedure> yieldCheckerProcs;

-        List<Implementation> yieldCheckerImpls;

-        Procedure yieldProc;

-

-        Variable pc;

-        Variable ok;

-        Expr alpha;

-        Expr beta;

-        HashSet<Variable> frame;

-

-        public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator)

-        {

-            this.linearTypeChecker = linearTypeChecker;

-            this.moverTypeChecker = moverTypeChecker;

-            this.absyMap = duplicator.absyMap;

-            this.layerNum = duplicator.layerNum;

-            this.implMap = duplicator.implMap;

-            this.yieldingProcs = duplicator.yieldingProcs;

-            Program program = linearTypeChecker.program;

-            globalMods = new List<IdentifierExpr>();

-            foreach (Variable g in moverTypeChecker.SharedVariables)

-            {

-                globalMods.Add(Expr.Ident(g));

-            }

-            asyncAndParallelCallDesugarings = new Dictionary<string, Procedure>();

-            yieldCheckerProcs = new List<Procedure>();

-            yieldCheckerImpls = new List<Implementation>();

-            yieldProc = null;

-        }

-

-        private IEnumerable<Variable> AvailableLinearVars(Absy absy)

-        {

-            return linearTypeChecker.AvailableLinearVars(absyMap[absy]);

-        }

-

-        private CallCmd CallToYieldProc(IToken tok, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)

-        {

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

-            foreach (string domainName in linearTypeChecker.linearDomains.Keys)

-            {

-                exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName]));

-            }

-            foreach (IdentifierExpr ie in globalMods)

-            {

-                exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl]));

-            }

-            if (yieldProc == null)

-            {

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

-                foreach (string domainName in linearTypeChecker.linearDomains.Keys)

-                {

-                    var domain = linearTypeChecker.linearDomains[domainName];

-                    Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);

-                    inputs.Add(f);

-                }

-                foreach (IdentifierExpr ie in globalMods)

-                {

-                    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}", 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>());

-            yieldCallCmd.Proc = yieldProc;

-            return yieldCallCmd;

-        }

-

-        private void AddCallToYieldProc(IToken tok, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)

-        {

-            if (!CommandLineOptions.Clo.TrustNonInterference)

-            {

-                CallCmd yieldCallCmd = CallToYieldProc(tok, ogOldGlobalMap, domainNameToLocalVar);

-                newCmds.Add(yieldCallCmd);

-            }

-

-            if (pc != null)

-            {

-                Expr aa = OldEqualityExprForGlobals(ogOldGlobalMap);

-                Expr bb = OldEqualityExpr(ogOldGlobalMap);

-

-                // assert pc || g_old == g || beta(i, g_old, o, g);

-                Expr assertExpr = Expr.Or(Expr.Ident(pc), Expr.Or(aa, beta));

-                assertExpr.Typecheck(new TypecheckingContext(null));

-                AssertCmd skipOrBetaAssertCmd = new AssertCmd(tok, assertExpr);

-                skipOrBetaAssertCmd.ErrorData = "Transition invariant in initial state violated";

-                newCmds.Add(skipOrBetaAssertCmd);

-

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

-                assertExpr = Expr.Imp(Expr.Ident(pc), bb);

-                assertExpr.Typecheck(new TypecheckingContext(null));

-                AssertCmd skipAssertCmd = new AssertCmd(tok, assertExpr);

-                skipAssertCmd.ErrorData = "Transition invariant in final state violated"; ;

-                newCmds.Add(skipAssertCmd);

-

-                // pc, ok := g_old == g ==> pc, ok || beta(i, g_old, o, g);

-                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[] { 

-                        Expr.Imp(aa, Expr.Ident(pc)),

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

-                    });

-                foreach (Expr e in pcUpdateRHS)

-                {

-                    e.Typecheck(new TypecheckingContext(null));

-                }

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

-            }

-        }

-

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

-        {

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

-            foreach (var domainName in linearTypeChecker.linearDomains.Keys)

-            {

-                var expr = Expr.Ident(domainNameToInputVar[domainName]);

-                expr.Resolve(new ResolutionContext(null));

-                expr.Typecheck(new TypecheckingContext(null));

-                domainNameToExpr[domainName] = expr;

-            }

-            foreach (Variable v in availableLinearVars)

-            {

-                var domainName = linearTypeChecker.FindDomainName(v);

-                if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

-                var domain = linearTypeChecker.linearDomains[domainName];

-                if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue;

-                Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List<Expr> { Expr.Ident(v) });

-                var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { ie, domainNameToExpr[domainName] });

-                expr.Resolve(new ResolutionContext(null));

-                expr.Typecheck(new TypecheckingContext(null));

-                domainNameToExpr[domainName] = expr;

-            }

-            return domainNameToExpr;

-        }

-

-        private void AddUpdatesToOldGlobalVars(List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<string, Expr> domainNameToExpr)

-        {

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

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

-            foreach (var domainName in linearTypeChecker.linearDomains.Keys)

-            {

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

-                rhss.Add(domainNameToExpr[domainName]);

-            }

-            foreach (Variable g in ogOldGlobalMap.Keys)

-            {

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

-                rhss.Add(Expr.Ident(g));

-            }

-            if (lhss.Count > 0)

-            {

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

-            }

-        }

-

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

-        {

-            Expr bb = Expr.True;

-            foreach (Variable o in ogOldGlobalMap.Keys)

-            {

-                if (o is GlobalVariable && !frame.Contains(o)) continue;

-                bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o])));

-                bb.Type = Type.Bool;

-            }

-            return bb;

-        }

-

-        private Expr OldEqualityExprForGlobals(Dictionary<Variable, Variable> ogOldGlobalMap)

-        {

-            Expr bb = Expr.True;

-            foreach (Variable o in ogOldGlobalMap.Keys)

-            {

-                if (o is GlobalVariable && frame.Contains(o))

-                {

-                    bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o])));

-                    bb.Type = Type.Bool;

-                }

-            }

-            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(yieldCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);

-

-            if (globalMods.Count > 0)

-            {

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

-                if (pc != null)

-                {

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

-                    Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);

-                    assumeExpr.Type = Type.Bool;

-                    newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));

-                }

-            }

-

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

-            AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);

-

-            for (int j = 0; j < cmds.Count; j++)

-            {

-                PredicateCmd predCmd = (PredicateCmd)cmds[j];

-                newCmds.Add(new AssumeCmd(Token.NoToken, predCmd.Expr));

-            }

-        }

-

-        public void DesugarParallelCallCmd(List<Cmd> newCmds, ParCallCmd parCallCmd)

-        {

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

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

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

-            string procName = "og";

-            foreach (CallCmd callCmd in parCallCmd.CallCmds)

-            {

-                procName = procName + "_" + callCmd.Proc.Name;

-                ins.AddRange(callCmd.Ins);

-                outs.AddRange(callCmd.Outs);

-            }

-            Procedure proc;

-            if (asyncAndParallelCallDesugarings.ContainsKey(procName))

-            {

-                proc = asyncAndParallelCallDesugarings[procName];

-            }

-            else

-            {

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

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

-                List<Requires> requiresSeq = new List<Requires>();

-                List<Ensures> ensuresSeq = new List<Ensures>();

-                int count = 0;

-                foreach (CallCmd callCmd in parCallCmd.CallCmds)

-                {

-                    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, string.Format("og_{0}_{1}", count, x.Name), x.TypedIdent.Type), true);

-                        inParams.Add(y);

-                        map[x] = Expr.Ident(y);

-                    }

-                    foreach (Variable x in callCmd.Proc.OutParams)

-                    {

-                        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] = Expr.Ident(y);

-                    }

-                    Contract.Assume(callCmd.Proc.TypeParameters.Count == 0);

-                    Substitution subst = Substituter.SubstitutionFromHashtable(map);

-                    foreach (Requires req in callCmd.Proc.Requires)

-                    {

-                        requiresSeq.Add(new Requires(req.tok, req.Free, Substituter.Apply(subst, req.Condition), null, req.Attributes));

-                    }

-                    foreach (Ensures ens in callCmd.Proc.Ensures)

-                    {

-                        ensuresSeq.Add(new Ensures(ens.tok, ens.Free, Substituter.Apply(subst, ens.Condition), null, ens.Attributes));

-                    }

-                    count++;

-                }

-                proc = new Procedure(Token.NoToken, procName, new List<TypeVariable>(), inParams, outParams, requiresSeq, globalMods, ensuresSeq);

-                asyncAndParallelCallDesugarings[procName] = proc;

-            }

-            CallCmd dummyCallCmd = new CallCmd(parCallCmd.tok, proc.Name, ins, outs, parCallCmd.Attributes);

-            dummyCallCmd.Proc = proc;

-            newCmds.Add(dummyCallCmd);

-        }

-

-        private void CreateYieldCheckerImpl(Implementation impl, List<List<Cmd>> yields)

-        {

-            if (yields.Count == 0) return;

-

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

-            foreach (Variable local in impl.LocVars)

-            {

-                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type));

-                map[local] = Expr.Ident(copy);

-            }

-

-            Program program = linearTypeChecker.program;

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

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

-            foreach (IdentifierExpr ie in map.Values)

-            {

-                locals.Add(ie.Decl);

-            }

-            for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++)

-            {

-                Variable inParam = impl.InParams[i];

-                Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));

-                locals.Add(copy);

-                map[impl.InParams[i]] = Expr.Ident(copy);

-            }

-            {

-                int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count;

-                foreach (string domainName in linearTypeChecker.linearDomains.Keys)

-                {

-                    Variable inParam = impl.InParams[i];

-                    Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true);

-                    inputs.Add(copy);

-                    map[impl.InParams[i]] = Expr.Ident(copy);

-                    i++;

-                }

-            }

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

-            {

-                Variable outParam = impl.OutParams[i];

-                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type));

-                locals.Add(copy);

-                map[impl.OutParams[i]] = Expr.Ident(copy);

-            }

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

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

-            foreach (IdentifierExpr ie in globalMods)

-            {

-                Variable g = ie.Decl;

-                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_local_old_{0}", g.Name), g.TypedIdent.Type));

-                locals.Add(copy);

-                ogOldLocalMap[g] = Expr.Ident(copy);

-                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type), true);

-                inputs.Add(f);

-                assumeMap[g] = Expr.Ident(f);

-            }

-            

-            Substitution assumeSubst = Substituter.SubstitutionFromHashtable(assumeMap);

-            Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap);

-            Substitution subst = Substituter.SubstitutionFromHashtable(map);

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

-            List<String> labels = new List<String>();

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

-            Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken));

-            labels.Add(yieldCheckerBlock.Label);

-            labelTargets.Add(yieldCheckerBlock);

-            yieldCheckerBlocks.Add(yieldCheckerBlock);

-            int yieldCount = 0;

-            foreach (List<Cmd> cs in yields)

-            {

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

-                foreach (Cmd cmd in cs)

-                {

-                    PredicateCmd predCmd = (PredicateCmd)cmd;

-                    newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr)));

-                }

-                foreach (Cmd cmd in cs)

-                {

-                    PredicateCmd predCmd = (PredicateCmd)cmd;

-                    var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr);

-                    if (predCmd is AssertCmd)

-                    {

-                        AssertCmd assertCmd = new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes);

-                        assertCmd.ErrorData = "Non-interference check failed";

-                        newCmds.Add(assertCmd);

-                    }

-                    else

-                    {

-                        newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));

-                    }

-                }

-                newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False));

-                yieldCheckerBlock = new Block(Token.NoToken, "L" + yieldCount++, newCmds, new ReturnCmd(Token.NoToken));

-                labels.Add(yieldCheckerBlock.Label);

-                labelTargets.Add(yieldCheckerBlock);

-                yieldCheckerBlocks.Add(yieldCheckerBlock);

-            }

-            yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), new GotoCmd(Token.NoToken, labels, labelTargets)));

-

-            // Create the yield checker procedure

-            var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", "Impl", impl.Name);

-            var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, impl.TypeParameters, inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());

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

-            yieldCheckerProcs.Add(yieldCheckerProc);

-

-            // Create the yield checker implementation

-            var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, impl.TypeParameters, inputs, new List<Variable>(), locals, yieldCheckerBlocks);

-            yieldCheckerImpl.Proc = yieldCheckerProc;

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

-            yieldCheckerImpls.Add(yieldCheckerImpl);

-        }

-

-        private bool IsYieldingHeader(Graph<Block> graph, Block header)

-        {

-            foreach (Block backEdgeNode in graph.BackEdgeNodes(header))

-            {

-                foreach (Block x in graph.NaturalLoops(header, backEdgeNode))

-                {

-                    foreach (Cmd cmd in x.Cmds)

-                    {

-                        if (cmd is YieldCmd)

-                            return true;

-                        if (cmd is ParCallCmd)

-                            return true;

-                        CallCmd callCmd = cmd as CallCmd;

-                        if (callCmd == null) continue;

-                        if (yieldingProcs.Contains(callCmd.Proc))

-                            return true;

-                    }

-                }

-            }

-            return false;

-        }

-

-        private Graph<Block> ComputeYieldingLoopHeaders(Implementation impl, out HashSet<Block> yieldingHeaders)

-        {

-            Graph<Block> graph; 

-            impl.PruneUnreachableBlocks();

-            impl.ComputePredecessorsForBlocks();

-            graph = Program.GraphFromImpl(impl);

-            graph.ComputeLoops();

-            if (!graph.Reducible)

-            {

-                throw new Exception("Irreducible flow graphs are unsupported.");

-            }

-            yieldingHeaders = new HashSet<Block>();

-            IEnumerable<Block> sortedHeaders = graph.SortHeadersByDominance();

-            foreach (Block header in sortedHeaders)

-            {

-                if (yieldingHeaders.Any(x => graph.DominatorMap.DominatedBy(x, header)))

-                {

-                    yieldingHeaders.Add(header);

-                }

-                else if (IsYieldingHeader(graph, header))

-                {

-                    yieldingHeaders.Add(header);

-                }

-                else

-                {

-                    continue;

-                }

-            }

-            return graph;

-        }

-

-        private void SetupRefinementCheck(Implementation impl, 

-            out List<Variable> newLocalVars,

-            out Dictionary<string, Variable> domainNameToInputVar, out Dictionary<string, Variable> domainNameToLocalVar, out Dictionary<Variable, Variable> ogOldGlobalMap)

-        {

-            pc = null;

-            ok = null;

-            alpha = null;

-            beta = null;

-            frame = null;

-            

-            newLocalVars = new List<Variable>();

-            Program program = linearTypeChecker.program;

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

-            foreach (IdentifierExpr ie in globalMods)

-            {

-                Variable g = ie.Decl;

-                LocalVariable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type));

-                ogOldGlobalMap[g] = l;

-                newLocalVars.Add(l);

-            }

-

-            Procedure originalProc = implMap[impl].Proc;

-            ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc];

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

-            {

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

-                newLocalVars.Add(pc);

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

-                newLocalVars.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);

-                frame = new HashSet<Variable>(moverTypeChecker.SharedVariables);

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

-                foreach (Variable v in moverTypeChecker.SharedVariables)

-                {

-                    if (moverTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || 

-                        moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum)

-                    {

-                        frame.Remove(v);

-                    }

-                    if (moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum == actionInfo.createdAtLayerNum)

-                    {

-                        introducedVars.Add(v);

-                    }

-                }

-                AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;

-                if (atomicActionInfo == null)

-                {

-                    beta = Expr.True;

-                    foreach (var v in frame)

-                    {

-                        beta = Expr.And(beta, Expr.Eq(Expr.Ident(v), foroldMap[v]));

-                    }

-                    alpha = Expr.True;

-                }

-                else

-                {

-                    Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, atomicActionInfo, frame, introducedVars)).TransitionRelationCompute();

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

-                    Expr alphaExpr = Expr.True;

-                    foreach (AssertCmd assertCmd in atomicActionInfo.thisGate)

-                    {

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

-                        alphaExpr.Type = Type.Bool;

-                    }

-                    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));

-                    newLocalVars.Add(copy);

-                    ogOldGlobalMap[f] = copy;

-                }

-            }

-

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

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

-            {

-                int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count;

-                foreach (string domainName in linearTypeChecker.linearDomains.Keys)

-                {

-                    Variable inParam = impl.InParams[i];

-                    domainNameToInputVar[domainName] = inParam;

-                    Variable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name + "_local", inParam.TypedIdent.Type));

-                    domainNameToLocalVar[domainName] = l;

-                    newLocalVars.Add(l);

-                    i++;

-                }

-            }

-        }

-

-        private void TransformImpl(Implementation impl)

-        {

-            HashSet<Block> yieldingHeaders;

-            Graph<Block> graph = ComputeYieldingLoopHeaders(impl, out yieldingHeaders);

-

-            List<Variable> newLocalVars;

-            Dictionary<string, Variable> domainNameToInputVar, domainNameToLocalVar;

-            Dictionary<Variable, Variable> ogOldGlobalMap;

-            SetupRefinementCheck(impl, out newLocalVars, out domainNameToInputVar, out domainNameToLocalVar, out ogOldGlobalMap);

-

-            List<List<Cmd>> yields = CollectAndDesugarYields(impl, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap);

-

-            List<Variable> oldPcs, oldOks;

-            ProcessLoopHeaders(impl, graph, yieldingHeaders, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap, out oldPcs, out oldOks);

-

-            AddInitialBlock(impl, oldPcs, oldOks, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap);

-

-            CreateYieldCheckerImpl(impl, yields);

-            

-            impl.LocVars.AddRange(newLocalVars);

-            impl.LocVars.AddRange(oldPcs);

-            impl.LocVars.AddRange(oldOks);

-

-            UnifyCallsToYieldProc(impl, ogOldGlobalMap, domainNameToLocalVar);

-        }

-

-        private void UnifyCallsToYieldProc(Implementation impl, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)

-        {

-            CallCmd yieldCallCmd = CallToYieldProc(Token.NoToken, ogOldGlobalMap, domainNameToLocalVar);

-            Block yieldCheckBlock = new Block(Token.NoToken, "CallToYieldProc", new List<Cmd>(new Cmd[] { yieldCallCmd, new AssumeCmd(Token.NoToken, Expr.False) }), new ReturnCmd(Token.NoToken));

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

-            foreach (Block b in impl.Blocks)

-            {

-                TransferCmd transferCmd = b.TransferCmd;

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

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

-                {

-                    CallCmd callCmd = b.Cmds[i] as CallCmd;

-                    if (callCmd == null || callCmd.Proc != yieldProc)

-                    {

-                        newCmds.Insert(0, b.Cmds[i]);

-                    }

-                    else

-                    {

-                        Block newBlock = new Block(Token.NoToken, b.Label + i, newCmds, transferCmd);

-                        newCmds = new List<Cmd>();

-                        transferCmd = new GotoCmd(Token.NoToken, new List<string>(new string[] { newBlock.Label, yieldCheckBlock.Label }), 

-                                                                 new List<Block>(new Block[] { newBlock, yieldCheckBlock }));

-                        newBlocks.Add(newBlock);

-                    }

-                }

-                b.Cmds = newCmds;

-                b.TransferCmd = transferCmd;

-            }

-            impl.Blocks.AddRange(newBlocks);

-            impl.Blocks.Add(yieldCheckBlock);

-        }

-

-        private List<List<Cmd>> CollectAndDesugarYields(Implementation impl,

-            Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap)

-        {

-            // Collect the yield predicates and desugar yields

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

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

-            foreach (Block b in impl.Blocks)

-            {

-                YieldCmd yieldCmd = null;

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

-                for (int i = 0; i < b.Cmds.Count; i++)

-                {

-                    Cmd cmd = b.Cmds[i];

-                    if (cmd is YieldCmd)

-                    {

-                        yieldCmd = (YieldCmd)cmd;

-                        continue;

-                    }

-                    if (yieldCmd != null)

-                    {

-                        PredicateCmd pcmd = cmd as PredicateCmd;

-                        if (pcmd == null)

-                        {

-                            DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar);

-                            if (cmds.Count > 0)

-                            {

-                                yields.Add(cmds);

-                                cmds = new List<Cmd>();

-                            }

-                            yieldCmd = null;

-                        }

-                        else

-                        {

-                            cmds.Add(pcmd);

-                        }

-                    }

-

-                    if (cmd is CallCmd)

-                    {

-                        CallCmd callCmd = cmd as CallCmd;

-                        if (yieldingProcs.Contains(callCmd.Proc))

-                        {

-                            AddCallToYieldProc(callCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);

-                        }

-                        if (callCmd.IsAsync)

-                        {

-                            if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name))

-                            {

-                                asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List<IdentifierExpr>(), new List<Ensures>());

-                            }

-                            var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name];

-                            CallCmd dummyCallCmd = new CallCmd(callCmd.tok, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs, callCmd.Attributes);

-                            dummyCallCmd.Proc = dummyAsyncTargetProc;

-                            newCmds.Add(dummyCallCmd);

-                        }

-                        else

-                        {

-                            newCmds.Add(callCmd);

-                        }

-                        if (yieldingProcs.Contains(callCmd.Proc))

-                        {

-                            HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(callCmd));

-                            linearTypeChecker.AddAvailableVars(callCmd, availableLinearVars);

-

-                            if (!callCmd.IsAsync && globalMods.Count > 0 && pc != null)

-                            {

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

-                                Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);

-                                assumeExpr.Type = Type.Bool;

-                                newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));

-                            }

-

-                            Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);

-                            AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);

-                        }

-                    }

-                    else if (cmd is ParCallCmd)

-                    {

-                        ParCallCmd parCallCmd = cmd as ParCallCmd;

-                        AddCallToYieldProc(parCallCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);

-                        DesugarParallelCallCmd(newCmds, parCallCmd);

-                        HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(parCallCmd));

-                        linearTypeChecker.AddAvailableVars(parCallCmd, availableLinearVars);

-

-                        if (globalMods.Count > 0 && pc != null)

-                        {

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

-                            Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);

-                            assumeExpr.Type = Type.Bool;

-                            newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));

-                        }

-

-                        Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);

-                        AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);

-                    }

-                    else

-                    {

-                        newCmds.Add(cmd);

-                    }

-                }

-                if (yieldCmd != null)

-                {

-                    DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar);

-                    if (cmds.Count > 0)

-                    {

-                        yields.Add(cmds);

-                        cmds = new List<Cmd>();

-                    }

-                }

-                if (b.TransferCmd is ReturnCmd)

-                {

-                    AddCallToYieldProc(b.TransferCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);

-                    if (pc != null)

-                    {

-                        AssertCmd assertCmd = new AssertCmd(b.TransferCmd.tok, Expr.Ident(ok));

-                        assertCmd.ErrorData = "Failed to execute atomic action before procedure return";

-                        newCmds.Add(assertCmd);

-                    }

-                }

-                b.Cmds = newCmds;

-            }

-            return yields;

-        }

-

-        private void ProcessLoopHeaders(Implementation impl, Graph<Block> graph, HashSet<Block> yieldingHeaders, 

-            Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap,

-            out List<Variable> oldPcs, out List<Variable> oldOks)

-        {

-            oldPcs = new List<Variable>();

-            oldOks = new List<Variable>();

-            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));

-                    oldPcs.Add(oldPc);

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

-                    oldOks.Add(oldOk);

-                }

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

-                foreach (Block pred in header.Predecessors)

-                {

-                    AddCallToYieldProc(header.tok, 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)

-                {

-                    AssertCmd assertCmd;

-                    assertCmd = new AssertCmd(header.tok, Expr.Eq(Expr.Ident(oldPc), Expr.Ident(pc)));

-                    assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers";

-                    newCmds.Add(assertCmd);

-                    assertCmd = new AssertCmd(header.tok, Expr.Imp(Expr.Ident(oldOk), Expr.Ident(ok)));

-                    assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers";

-                    newCmds.Add(assertCmd);

-                }

-                foreach (string domainName in linearTypeChecker.linearDomains.Keys)

-                {

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

-                }

-                foreach (Variable v in ogOldGlobalMap.Keys)

-                {

-                    newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(v), Expr.Ident(ogOldGlobalMap[v]))));

-                }

-                newCmds.AddRange(header.Cmds);

-                header.Cmds = newCmds;

-            }

-        }

-

-        private void AddInitialBlock(Implementation impl, List<Variable> oldPcs, List<Variable> oldOks,

-            Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap)

-        {

-            // 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);

-                foreach (Variable oldPc in oldPcs)

-                {

-                    lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)));

-                    rhss.Add(Expr.False);

-                }

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

-                rhss.Add(Expr.False);

-                foreach (Variable oldOk in oldOks)

-                {

-                    lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)));

-                    rhss.Add(Expr.False);

-                }

-            }

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

-            foreach (var domainName in linearTypeChecker.linearDomains.Keys)

-            {

-                domainNameToExpr[domainName] = Expr.Ident(domainNameToInputVar[domainName]);

-            }

-            for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++)

-            {

-                Variable v = impl.InParams[i];

-                var domainName = linearTypeChecker.FindDomainName(v);

-                if (domainName == null) continue;

-                if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

-                var domain = linearTypeChecker.linearDomains[domainName];

-                if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue;

-                Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List<Expr> { Expr.Ident(v) });

-                domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { ie, domainNameToExpr[domainName] });

-            }

-            foreach (string domainName in linearTypeChecker.linearDomains.Keys)

-            {

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

-                rhss.Add(domainNameToExpr[domainName]);

-            }

-            foreach (Variable g in ogOldGlobalMap.Keys)

-            {

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

-                rhss.Add(Expr.Ident(g));

-            }

-            if (lhss.Count > 0)

-            {

-                Block initBlock = new Block(Token.NoToken, "og_init", new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] }));

-                impl.Blocks.Insert(0, initBlock);

-            }

-        }

-

-        private void AddYieldProcAndImpl(List<Declaration> decls) 

-        {

-            if (yieldProc == null) return;

-

-            Program program = linearTypeChecker.program;

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

-            foreach (string domainName in linearTypeChecker.linearDomains.Keys)

-            {

-                var domain = linearTypeChecker.linearDomains[domainName];

-                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);

-                inputs.Add(f);

-            }

-            foreach (IdentifierExpr ie in globalMods)

-            {

-                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);

-            } 

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

-            TransferCmd transferCmd = new ReturnCmd(Token.NoToken);

-            if (yieldCheckerProcs.Count > 0)

-            {

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

-                List<String> labelTargets = new List<String>();

-                int labelCount = 0;

-                foreach (Procedure proc in yieldCheckerProcs)

-                {

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

-                    foreach (Variable v in inputs)

-                    {

-                        exprSeq.Add(Expr.Ident(v));

-                    }

-                    CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List<IdentifierExpr>());

-                    callCmd.Proc = proc;

-                    string label = string.Format("L_{0}", labelCount++);

-                    Block block = new Block(Token.NoToken, label, new List<Cmd> { callCmd }, new ReturnCmd(Token.NoToken));

-                    labelTargets.Add(label);

-                    blockTargets.Add(block);

-                    blocks.Add(block);

-                }

-                transferCmd = new GotoCmd(Token.NoToken, labelTargets, blockTargets);

-            }

-            blocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), transferCmd));

-            

-            var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);

-            yieldImpl.Proc = yieldProc;

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

-            decls.Add(yieldProc);

-            decls.Add(yieldImpl);

-        }

-

-        public static QKeyValue RemoveYieldsAttribute(QKeyValue iter)

-        {

-            if (iter == null) return null;

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

-            return (iter.Key == "yields") ? iter.Next : iter;

-        }

-

-        public static QKeyValue RemoveMoverAttribute(QKeyValue iter)

-        {

-            if (iter == null) return null;

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

-            if (iter.Key == "atomic" || iter.Key == "right" || iter.Key == "left" || iter.Key == "both") 

-                return iter.Next;

-            else 

-                return iter;

-        }

-

-        private List<Declaration> Collect()

-        {

-            List<Declaration> decls = new List<Declaration>();

-            foreach (Procedure proc in yieldCheckerProcs)

-            {

-                decls.Add(proc);

-            }

-            foreach (Implementation impl in yieldCheckerImpls)

-            {

-                decls.Add(impl);

-            }

-            foreach (Procedure proc in asyncAndParallelCallDesugarings.Values)

-            {

-                decls.Add(proc);

-            }

-            AddYieldProcAndImpl(decls);

-            return decls;

-        }

-

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

-        {

-            Program program = linearTypeChecker.program;

-            foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum }))

-            {

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

-

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

-                foreach (var proc in program.Procedures)

-                {

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

-                    Procedure duplicateProc = duplicator.VisitProcedure(proc);

-                    decls.Add(duplicateProc);

-                }

-                decls.AddRange(duplicator.impls);

-                OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator);

-                foreach (var impl in program.Implementations)

-                {

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

-                        continue;

-                    Implementation duplicateImpl = duplicator.VisitImplementation(impl);

-                    ogTransform.TransformImpl(duplicateImpl);

-                    decls.Add(duplicateImpl);

-                }

-                decls.AddRange(ogTransform.Collect());

-            }

-        }

-    }

-}

+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Threading.Tasks;
+using Microsoft.Boogie;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie.GraphUtil;
+
+namespace Microsoft.Boogie
+{
+    public class MyDuplicator : Duplicator
+    {
+        MoverTypeChecker moverTypeChecker;
+        public int layerNum;
+        Procedure enclosingProc;
+        Implementation enclosingImpl;
+        public Dictionary<Procedure, Procedure> procMap; /* Original -> Duplicate */
+        public Dictionary<Absy, Absy> absyMap; /* Duplicate -> Original */
+        public Dictionary<Implementation, Implementation> implMap; /* Duplicate -> Original */
+        public HashSet<Procedure> yieldingProcs;
+        public List<Implementation> impls;
+
+        public MyDuplicator(MoverTypeChecker moverTypeChecker, int layerNum)
+        {
+            this.moverTypeChecker = moverTypeChecker;
+            this.layerNum = layerNum;
+            this.enclosingProc = null;
+            this.enclosingImpl = null;
+            this.procMap = new Dictionary<Procedure, Procedure>();
+            this.absyMap = new Dictionary<Absy, Absy>();
+            this.implMap = new Dictionary<Implementation, Implementation>();
+            this.yieldingProcs = new HashSet<Procedure>();
+            this.impls = new List<Implementation>();
+        }
+
+        private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List<Cmd> newCmds)
+        {
+            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.gate.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>();
+                    for (int i = 0; i < originalProc.InParams.Count; i++)
+                    {
+                        map[originalProc.InParams[i]] = callCmd.Ins[i];
+                    }
+                    Substitution subst = Substituter.SubstitutionFromHashtable(map);
+                    foreach (AssertCmd assertCmd in atomicActionInfo.gate)
+                    {
+                        newCmds.Add(Substituter.Apply(subst, assertCmd));
+                    }
+                }
+            }
+            newCmds.Add(callCmd);
+        }
+
+        private void ProcessParCallCmd(ParCallCmd originalParCallCmd, ParCallCmd parCallCmd, List<Cmd> newCmds)
+        {
+            int maxCalleeLayerNum = 0;
+            foreach (CallCmd iter in originalParCallCmd.CallCmds)
+            {
+                int calleeLayerNum = moverTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum;
+                if (calleeLayerNum > maxCalleeLayerNum)
+                    maxCalleeLayerNum = calleeLayerNum;
+            }
+            if (layerNum > maxCalleeLayerNum)
+            {
+                for (int i = 0; i < parCallCmd.CallCmds.Count; i++) 
+                {
+                    ProcessCallCmd(originalParCallCmd.CallCmds[i], parCallCmd.CallCmds[i], newCmds);
+                    absyMap[parCallCmd.CallCmds[i]] = originalParCallCmd;
+                }
+            }
+            else
+            {
+                newCmds.Add(parCallCmd);
+            }
+        }
+
+        public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq)
+        {
+            List<Cmd> cmds = base.VisitCmdSeq(cmdSeq);
+            List<Cmd> newCmds = new List<Cmd>();
+            for (int i = 0; i < cmds.Count; i++)
+            {
+                Cmd originalCmd = cmdSeq[i];
+                Cmd cmd = cmds[i];
+
+                CallCmd originalCallCmd = originalCmd as CallCmd;
+                if (originalCallCmd != null)
+                {
+                    ProcessCallCmd(originalCallCmd, cmd as CallCmd, newCmds);
+                    continue;
+                }
+
+                ParCallCmd originalParCallCmd = originalCmd as ParCallCmd;
+                if (originalParCallCmd != null)
+                {
+                    ProcessParCallCmd(originalParCallCmd, cmd as ParCallCmd, newCmds);
+                    continue;
+                }
+             
+                newCmds.Add(cmd);
+            }
+            return newCmds;
+        }
+
+        public override YieldCmd VisitYieldCmd(YieldCmd node)
+        {
+            YieldCmd yieldCmd = base.VisitYieldCmd(node);
+            absyMap[yieldCmd] = node;
+            return yieldCmd;
+        }
+        
+        public override Block VisitBlock(Block node)
+        {
+            Block block = base.VisitBlock(node);
+            absyMap[block] = node;
+            return block;
+        }
+        
+        public override Cmd VisitCallCmd(CallCmd node)
+        {
+            CallCmd callCmd = (CallCmd) base.VisitCallCmd(node);
+            callCmd.Proc = VisitProcedure(callCmd.Proc);
+            callCmd.callee = callCmd.Proc.Name;
+            absyMap[callCmd] = node;
+            return callCmd;
+        }
+
+        public override Cmd VisitParCallCmd(ParCallCmd node)
+        {
+            ParCallCmd parCallCmd = (ParCallCmd) base.VisitParCallCmd(node);
+            absyMap[parCallCmd] = node;
+            return parCallCmd;
+        }
+
+        public override Procedure VisitProcedure(Procedure node)
+        {
+            if (!moverTypeChecker.procToActionInfo.ContainsKey(node))
+                return node;
+            if (!procMap.ContainsKey(node))
+            {
+                enclosingProc = node;
+                Procedure proc = (Procedure)node.Clone();
+                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.createdAtLayerNum < layerNum)
+                {
+                    proc.Requires = new List<Requires>();
+                    proc.Ensures = new List<Ensures>();
+                    Implementation impl;
+                    AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
+                    if (atomicActionInfo != null)
+                    {
+                        CodeExpr action = (CodeExpr)VisitCodeExpr(atomicActionInfo.action);
+                        List<Cmd> cmds = new List<Cmd>();
+                        foreach (AssertCmd assertCmd in atomicActionInfo.gate)
+                        {
+                            cmds.Add(new AssumeCmd(Token.NoToken, (Expr)Visit(assertCmd.Expr)));
+                        }
+                        Block newInitBlock = new Block(Token.NoToken, "_init", cmds,
+                            new GotoCmd(Token.NoToken, new List<string>(new string[] { action.Blocks[0].Label }),
+                                                       new List<Block>(new Block[] { action.Blocks[0] })));
+                        List<Block> newBlocks = new List<Block>();
+                        newBlocks.Add(newInitBlock);
+                        newBlocks.AddRange(action.Blocks);
+                        impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, action.LocVars, newBlocks);
+                    }
+                    else
+                    {
+                        Block newInitBlock = new Block(Token.NoToken, "_init", new List<Cmd>(), new ReturnCmd(Token.NoToken));
+                        List<Block> newBlocks = new List<Block>();
+                        newBlocks.Add(newInitBlock);
+                        impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, new List<Variable>(), newBlocks);
+                    }
+                    impl.Proc = proc;
+                    impl.Proc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
+                    impl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
+                    impls.Add(impl);
+                }
+                else
+                {
+                    yieldingProcs.Add(proc);
+                    proc.Requires = this.VisitRequiresSeq(node.Requires);
+                    proc.Ensures = this.VisitEnsuresSeq(node.Ensures);
+                }
+                procMap[node] = proc;
+                proc.Modifies = new List<IdentifierExpr>();
+                moverTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));
+            }
+            return procMap[node];
+        }
+
+        private Variable dummyLocalVar;
+        public override Implementation VisitImplementation(Implementation node)
+        {
+            enclosingImpl = node;
+            dummyLocalVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_dummy", Type.Bool));
+            Implementation impl = base.VisitImplementation(node);
+            implMap[impl] = node;
+            impl.LocVars.Add(dummyLocalVar);
+            impl.Name = impl.Proc.Name;
+            return impl;
+        }
+
+        public override Requires VisitRequires(Requires node)
+        {
+            Requires requires = base.VisitRequires(node);
+            if (node.Free)
+                return requires;
+            if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum))
+                requires.Condition = Expr.True;
+            return requires;
+        }
+
+        public override Ensures VisitEnsures(Ensures node)
+        {
+            Ensures ensures = base.VisitEnsures(node);
+            if (node.Free)
+                return ensures;
+            AtomicActionInfo atomicActionInfo =  moverTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo;
+            bool isAtomicSpecification = atomicActionInfo != null && atomicActionInfo.ensures == node;
+            if (isAtomicSpecification || !moverTypeChecker.absyToLayerNums[node].Contains(layerNum))
+            {
+                ensures.Condition = Expr.True;
+                ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes);
+            }
+            return ensures;
+        }
+
+        public override Cmd VisitAssertCmd(AssertCmd node)
+        {
+            AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node);
+            if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum))
+                assertCmd.Expr = Expr.True;
+            return assertCmd;
+        }
+    }
+
+    public class OwickiGries
+    {
+        LinearTypeChecker linearTypeChecker;
+        MoverTypeChecker moverTypeChecker;
+        Dictionary<Absy, Absy> absyMap;
+        Dictionary<Implementation, Implementation> implMap;
+        HashSet<Procedure> yieldingProcs;
+        int layerNum;
+        List<IdentifierExpr> globalMods;
+        Dictionary<string, Procedure> asyncAndParallelCallDesugarings;
+        List<Procedure> yieldCheckerProcs;
+        List<Implementation> yieldCheckerImpls;
+        Procedure yieldProc;
+
+        Variable pc;
+        Variable ok;
+        Expr alpha;
+        Expr beta;
+        HashSet<Variable> frame;
+
+        public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator)
+        {
+            this.linearTypeChecker = linearTypeChecker;
+            this.moverTypeChecker = moverTypeChecker;
+            this.absyMap = duplicator.absyMap;
+            this.layerNum = duplicator.layerNum;
+            this.implMap = duplicator.implMap;
+            this.yieldingProcs = duplicator.yieldingProcs;
+            Program program = linearTypeChecker.program;
+            globalMods = new List<IdentifierExpr>();
+            foreach (Variable g in moverTypeChecker.SharedVariables)
+            {
+                globalMods.Add(Expr.Ident(g));
+            }
+            asyncAndParallelCallDesugarings = new Dictionary<string, Procedure>();
+            yieldCheckerProcs = new List<Procedure>();
+            yieldCheckerImpls = new List<Implementation>();
+            yieldProc = null;
+        }
+
+        private IEnumerable<Variable> AvailableLinearVars(Absy absy)
+        {
+            return linearTypeChecker.AvailableLinearVars(absyMap[absy]);
+        }
+
+        private CallCmd CallToYieldProc(IToken tok, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
+        {
+            List<Expr> exprSeq = new List<Expr>();
+            foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+            {
+                exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName]));
+            }
+            foreach (IdentifierExpr ie in globalMods)
+            {
+                exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl]));
+            }
+            if (yieldProc == null)
+            {
+                List<Variable> inputs = new List<Variable>();
+                foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+                {
+                    var domain = linearTypeChecker.linearDomains[domainName];
+                    Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);
+                    inputs.Add(f);
+                }
+                foreach (IdentifierExpr ie in globalMods)
+                {
+                    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}", 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>());
+            yieldCallCmd.Proc = yieldProc;
+            return yieldCallCmd;
+        }
+
+        private void AddCallToYieldProc(IToken tok, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
+        {
+            if (!CommandLineOptions.Clo.TrustNonInterference)
+            {
+                CallCmd yieldCallCmd = CallToYieldProc(tok, ogOldGlobalMap, domainNameToLocalVar);
+                newCmds.Add(yieldCallCmd);
+            }
+
+            if (pc != null)
+            {
+                Expr aa = OldEqualityExprForGlobals(ogOldGlobalMap);
+                Expr bb = OldEqualityExpr(ogOldGlobalMap);
+
+                // assert pc || g_old == g || beta(i, g_old, o, g);
+                Expr assertExpr = Expr.Or(Expr.Ident(pc), Expr.Or(aa, beta));
+                assertExpr.Typecheck(new TypecheckingContext(null));
+                AssertCmd skipOrBetaAssertCmd = new AssertCmd(tok, assertExpr);
+                skipOrBetaAssertCmd.ErrorData = "Transition invariant in initial state violated";
+                newCmds.Add(skipOrBetaAssertCmd);
+
+                // assert pc ==> o_old == o && g_old == g;
+                assertExpr = Expr.Imp(Expr.Ident(pc), bb);
+                assertExpr.Typecheck(new TypecheckingContext(null));
+                AssertCmd skipAssertCmd = new AssertCmd(tok, assertExpr);
+                skipAssertCmd.ErrorData = "Transition invariant in final state violated"; ;
+                newCmds.Add(skipAssertCmd);
+
+                // pc, ok := g_old == g ==> pc, ok || beta(i, g_old, o, g);
+                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[] { 
+                        Expr.Imp(aa, Expr.Ident(pc)),
+                        Expr.Or(Expr.Ident(ok), beta)
+                    });
+                foreach (Expr e in pcUpdateRHS)
+                {
+                    e.Typecheck(new TypecheckingContext(null));
+                }
+                newCmds.Add(new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS));
+            }
+        }
+
+        private Dictionary<string, Expr> ComputeAvailableExprs(IEnumerable<Variable> availableLinearVars, Dictionary<string, Variable> domainNameToInputVar)
+        {
+            Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
+            foreach (var domainName in linearTypeChecker.linearDomains.Keys)
+            {
+                var expr = Expr.Ident(domainNameToInputVar[domainName]);
+                expr.Resolve(new ResolutionContext(null));
+                expr.Typecheck(new TypecheckingContext(null));
+                domainNameToExpr[domainName] = expr;
+            }
+            foreach (Variable v in availableLinearVars)
+            {
+                var domainName = linearTypeChecker.FindDomainName(v);
+                if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
+                var domain = linearTypeChecker.linearDomains[domainName];
+                if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue;
+                Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List<Expr> { Expr.Ident(v) });
+                var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { ie, domainNameToExpr[domainName] });
+                expr.Resolve(new ResolutionContext(null));
+                expr.Typecheck(new TypecheckingContext(null));
+                domainNameToExpr[domainName] = expr;
+            }
+            return domainNameToExpr;
+        }
+
+        private void AddUpdatesToOldGlobalVars(List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<string, Expr> domainNameToExpr)
+        {
+            List<AssignLhs> lhss = new List<AssignLhs>();
+            List<Expr> rhss = new List<Expr>();
+            foreach (var domainName in linearTypeChecker.linearDomains.Keys)
+            {
+                lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName])));
+                rhss.Add(domainNameToExpr[domainName]);
+            }
+            foreach (Variable g in ogOldGlobalMap.Keys)
+            {
+                lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g])));
+                rhss.Add(Expr.Ident(g));
+            }
+            if (lhss.Count > 0)
+            {
+                newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
+            }
+        }
+
+        private Expr OldEqualityExpr(Dictionary<Variable, Variable> ogOldGlobalMap)
+        {
+            Expr bb = Expr.True;
+            foreach (Variable o in ogOldGlobalMap.Keys)
+            {
+                if (o is GlobalVariable && !frame.Contains(o)) continue;
+                bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o])));
+                bb.Type = Type.Bool;
+            }
+            return bb;
+        }
+
+        private Expr OldEqualityExprForGlobals(Dictionary<Variable, Variable> ogOldGlobalMap)
+        {
+            Expr bb = Expr.True;
+            foreach (Variable o in ogOldGlobalMap.Keys)
+            {
+                if (o is GlobalVariable && frame.Contains(o))
+                {
+                    bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o])));
+                    bb.Type = Type.Bool;
+                }
+            }
+            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(yieldCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
+
+            if (globalMods.Count > 0)
+            {
+                newCmds.Add(new HavocCmd(Token.NoToken, globalMods));
+                if (pc != null)
+                {
+                    // assume pc || alpha(i, g);
+                    Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
+                    assumeExpr.Type = Type.Bool;
+                    newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
+                }
+            }
+
+            Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(yieldCmd), domainNameToInputVar);
+            AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
+
+            for (int j = 0; j < cmds.Count; j++)
+            {
+                PredicateCmd predCmd = (PredicateCmd)cmds[j];
+                newCmds.Add(new AssumeCmd(Token.NoToken, predCmd.Expr));
+            }
+        }
+
+        public void DesugarParallelCallCmd(List<Cmd> newCmds, ParCallCmd parCallCmd)
+        {
+            List<string> parallelCalleeNames = new List<string>();
+            List<Expr> ins = new List<Expr>();
+            List<IdentifierExpr> outs = new List<IdentifierExpr>();
+            string procName = "og";
+            foreach (CallCmd callCmd in parCallCmd.CallCmds)
+            {
+                procName = procName + "_" + callCmd.Proc.Name;
+                ins.AddRange(callCmd.Ins);
+                outs.AddRange(callCmd.Outs);
+            }
+            Procedure proc;
+            if (asyncAndParallelCallDesugarings.ContainsKey(procName))
+            {
+                proc = asyncAndParallelCallDesugarings[procName];
+            }
+            else
+            {
+                List<Variable> inParams = new List<Variable>();
+                List<Variable> outParams = new List<Variable>();
+                List<Requires> requiresSeq = new List<Requires>();
+                List<Ensures> ensuresSeq = new List<Ensures>();
+                int count = 0;
+                foreach (CallCmd callCmd in parCallCmd.CallCmds)
+                {
+                    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, string.Format("og_{0}_{1}", count, x.Name), x.TypedIdent.Type), true);
+                        inParams.Add(y);
+                        map[x] = Expr.Ident(y);
+                    }
+                    foreach (Variable x in callCmd.Proc.OutParams)
+                    {
+                        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] = Expr.Ident(y);
+                    }
+                    Contract.Assume(callCmd.Proc.TypeParameters.Count == 0);
+                    Substitution subst = Substituter.SubstitutionFromHashtable(map);
+                    foreach (Requires req in callCmd.Proc.Requires)
+                    {
+                        requiresSeq.Add(new Requires(req.tok, req.Free, Substituter.Apply(subst, req.Condition), null, req.Attributes));
+                    }
+                    foreach (Ensures ens in callCmd.Proc.Ensures)
+                    {
+                        ensuresSeq.Add(new Ensures(ens.tok, ens.Free, Substituter.Apply(subst, ens.Condition), null, ens.Attributes));
+                    }
+                    count++;
+                }
+                proc = new Procedure(Token.NoToken, procName, new List<TypeVariable>(), inParams, outParams, requiresSeq, globalMods, ensuresSeq);
+                asyncAndParallelCallDesugarings[procName] = proc;
+            }
+            CallCmd dummyCallCmd = new CallCmd(parCallCmd.tok, proc.Name, ins, outs, parCallCmd.Attributes);
+            dummyCallCmd.Proc = proc;
+            newCmds.Add(dummyCallCmd);
+        }
+
+        private void CreateYieldCheckerImpl(Implementation impl, List<List<Cmd>> yields)
+        {
+            if (yields.Count == 0) return;
+
+            Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+            foreach (Variable local in impl.LocVars)
+            {
+                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type));
+                map[local] = Expr.Ident(copy);
+            }
+
+            Program program = linearTypeChecker.program;
+            List<Variable> locals = new List<Variable>();
+            List<Variable> inputs = new List<Variable>();
+            foreach (IdentifierExpr ie in map.Values)
+            {
+                locals.Add(ie.Decl);
+            }
+            for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++)
+            {
+                Variable inParam = impl.InParams[i];
+                Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
+                locals.Add(copy);
+                map[impl.InParams[i]] = Expr.Ident(copy);
+            }
+            {
+                int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count;
+                foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+                {
+                    Variable inParam = impl.InParams[i];
+                    Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true);
+                    inputs.Add(copy);
+                    map[impl.InParams[i]] = Expr.Ident(copy);
+                    i++;
+                }
+            }
+            for (int i = 0; i < impl.OutParams.Count; i++)
+            {
+                Variable outParam = impl.OutParams[i];
+                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type));
+                locals.Add(copy);
+                map[impl.OutParams[i]] = Expr.Ident(copy);
+            }
+            Dictionary<Variable, Expr> ogOldLocalMap = new Dictionary<Variable, Expr>();
+            Dictionary<Variable, Expr> assumeMap = new Dictionary<Variable, Expr>(map);
+            foreach (IdentifierExpr ie in globalMods)
+            {
+                Variable g = ie.Decl;
+                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_local_old_{0}", g.Name), g.TypedIdent.Type));
+                locals.Add(copy);
+                ogOldLocalMap[g] = Expr.Ident(copy);
+                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type), true);
+                inputs.Add(f);
+                assumeMap[g] = Expr.Ident(f);
+            }
+            
+            Substitution assumeSubst = Substituter.SubstitutionFromHashtable(assumeMap);
+            Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap);
+            Substitution subst = Substituter.SubstitutionFromHashtable(map);
+            List<Block> yieldCheckerBlocks = new List<Block>();
+            List<String> labels = new List<String>();
+            List<Block> labelTargets = new List<Block>();
+            Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken));
+            labels.Add(yieldCheckerBlock.Label);
+            labelTargets.Add(yieldCheckerBlock);
+            yieldCheckerBlocks.Add(yieldCheckerBlock);
+            int yieldCount = 0;
+            foreach (List<Cmd> cs in yields)
+            {
+                List<Cmd> newCmds = new List<Cmd>();
+                foreach (Cmd cmd in cs)
+                {
+                    PredicateCmd predCmd = (PredicateCmd)cmd;
+                    newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr)));
+                }
+                foreach (Cmd cmd in cs)
+                {
+                    PredicateCmd predCmd = (PredicateCmd)cmd;
+                    var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr);
+                    if (predCmd is AssertCmd)
+                    {
+                        AssertCmd assertCmd = new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes);
+                        assertCmd.ErrorData = "Non-interference check failed";
+                        newCmds.Add(assertCmd);
+                    }
+                    else
+                    {
+                        newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));
+                    }
+                }
+                newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False));
+                yieldCheckerBlock = new Block(Token.NoToken, "L" + yieldCount++, newCmds, new ReturnCmd(Token.NoToken));
+                labels.Add(yieldCheckerBlock.Label);
+                labelTargets.Add(yieldCheckerBlock);
+                yieldCheckerBlocks.Add(yieldCheckerBlock);
+            }
+            yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), new GotoCmd(Token.NoToken, labels, labelTargets)));
+
+            // Create the yield checker procedure
+            var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", "Impl", impl.Name);
+            var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, impl.TypeParameters, inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());
+            yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
+            yieldCheckerProcs.Add(yieldCheckerProc);
+
+            // Create the yield checker implementation
+            var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, impl.TypeParameters, inputs, new List<Variable>(), locals, yieldCheckerBlocks);
+            yieldCheckerImpl.Proc = yieldCheckerProc;
+            yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
+            yieldCheckerImpls.Add(yieldCheckerImpl);
+        }
+
+        private bool IsYieldingHeader(Graph<Block> graph, Block header)
+        {
+            foreach (Block backEdgeNode in graph.BackEdgeNodes(header))
+            {
+                foreach (Block x in graph.NaturalLoops(header, backEdgeNode))
+                {
+                    foreach (Cmd cmd in x.Cmds)
+                    {
+                        if (cmd is YieldCmd)
+                            return true;
+                        if (cmd is ParCallCmd)
+                            return true;
+                        CallCmd callCmd = cmd as CallCmd;
+                        if (callCmd == null) continue;
+                        if (yieldingProcs.Contains(callCmd.Proc))
+                            return true;
+                    }
+                }
+            }
+            return false;
+        }
+
+        private Graph<Block> ComputeYieldingLoopHeaders(Implementation impl, out HashSet<Block> yieldingHeaders)
+        {
+            Graph<Block> graph; 
+            impl.PruneUnreachableBlocks();
+            impl.ComputePredecessorsForBlocks();
+            graph = Program.GraphFromImpl(impl);
+            graph.ComputeLoops();
+            if (!graph.Reducible)
+            {
+                throw new Exception("Irreducible flow graphs are unsupported.");
+            }
+            yieldingHeaders = new HashSet<Block>();
+            IEnumerable<Block> sortedHeaders = graph.SortHeadersByDominance();
+            foreach (Block header in sortedHeaders)
+            {
+                if (yieldingHeaders.Any(x => graph.DominatorMap.DominatedBy(x, header)))
+                {
+                    yieldingHeaders.Add(header);
+                }
+                else if (IsYieldingHeader(graph, header))
+                {
+                    yieldingHeaders.Add(header);
+                }
+                else
+                {
+                    continue;
+                }
+            }
+            return graph;
+        }
+
+        private void SetupRefinementCheck(Implementation impl, 
+            out List<Variable> newLocalVars,
+            out Dictionary<string, Variable> domainNameToInputVar, out Dictionary<string, Variable> domainNameToLocalVar, out Dictionary<Variable, Variable> ogOldGlobalMap)
+        {
+            pc = null;
+            ok = null;
+            alpha = null;
+            beta = null;
+            frame = null;
+            
+            newLocalVars = new List<Variable>();
+            Program program = linearTypeChecker.program;
+            ogOldGlobalMap = new Dictionary<Variable, Variable>();
+            foreach (IdentifierExpr ie in globalMods)
+            {
+                Variable g = ie.Decl;
+                LocalVariable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type));
+                ogOldGlobalMap[g] = l;
+                newLocalVars.Add(l);
+            }
+
+            Procedure originalProc = implMap[impl].Proc;
+            ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc];
+            if (actionInfo.createdAtLayerNum == this.layerNum)
+            {
+                pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool));
+                newLocalVars.Add(pc);
+                ok = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_ok", Type.Bool));
+                newLocalVars.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);
+                frame = new HashSet<Variable>(moverTypeChecker.SharedVariables);
+                HashSet<Variable> introducedVars = new HashSet<Variable>();
+                foreach (Variable v in moverTypeChecker.SharedVariables)
+                {
+                    if (moverTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || 
+                        moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum)
+                    {
+                        frame.Remove(v);
+                    }
+                    if (moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum == actionInfo.createdAtLayerNum)
+                    {
+                        introducedVars.Add(v);
+                    }
+                }
+                AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
+                if (atomicActionInfo == null)
+                {
+                    beta = Expr.True;
+                    foreach (var v in frame)
+                    {
+                        beta = Expr.And(beta, Expr.Eq(Expr.Ident(v), foroldMap[v]));
+                    }
+                    alpha = Expr.True;
+                }
+                else
+                {
+                    Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, atomicActionInfo, frame, introducedVars)).TransitionRelationCompute(true);
+                    beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr);
+                    Expr alphaExpr = Expr.True;
+                    foreach (AssertCmd assertCmd in atomicActionInfo.gate)
+                    {
+                        alphaExpr = Expr.And(alphaExpr, assertCmd.Expr);
+                        alphaExpr.Type = Type.Bool;
+                    }
+                    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));
+                    newLocalVars.Add(copy);
+                    ogOldGlobalMap[f] = copy;
+                }
+            }
+
+            domainNameToInputVar = new Dictionary<string, Variable>();
+            domainNameToLocalVar = new Dictionary<string, Variable>();
+            {
+                int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count;
+                foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+                {
+                    Variable inParam = impl.InParams[i];
+                    domainNameToInputVar[domainName] = inParam;
+                    Variable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name + "_local", inParam.TypedIdent.Type));
+                    domainNameToLocalVar[domainName] = l;
+                    newLocalVars.Add(l);
+                    i++;
+                }
+            }
+        }
+
+        private void TransformImpl(Implementation impl)
+        {
+            HashSet<Block> yieldingHeaders;
+            Graph<Block> graph = ComputeYieldingLoopHeaders(impl, out yieldingHeaders);
+
+            List<Variable> newLocalVars;
+            Dictionary<string, Variable> domainNameToInputVar, domainNameToLocalVar;
+            Dictionary<Variable, Variable> ogOldGlobalMap;
+            SetupRefinementCheck(impl, out newLocalVars, out domainNameToInputVar, out domainNameToLocalVar, out ogOldGlobalMap);
+
+            List<List<Cmd>> yields = CollectAndDesugarYields(impl, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap);
+
+            List<Variable> oldPcs, oldOks;
+            ProcessLoopHeaders(impl, graph, yieldingHeaders, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap, out oldPcs, out oldOks);
+
+            AddInitialBlock(impl, oldPcs, oldOks, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap);
+
+            CreateYieldCheckerImpl(impl, yields);
+            
+            impl.LocVars.AddRange(newLocalVars);
+            impl.LocVars.AddRange(oldPcs);
+            impl.LocVars.AddRange(oldOks);
+
+            UnifyCallsToYieldProc(impl, ogOldGlobalMap, domainNameToLocalVar);
+        }
+
+        private void UnifyCallsToYieldProc(Implementation impl, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
+        {
+            CallCmd yieldCallCmd = CallToYieldProc(Token.NoToken, ogOldGlobalMap, domainNameToLocalVar);
+            Block yieldCheckBlock = new Block(Token.NoToken, "CallToYieldProc", new List<Cmd>(new Cmd[] { yieldCallCmd, new AssumeCmd(Token.NoToken, Expr.False) }), new ReturnCmd(Token.NoToken));
+            List<Block> newBlocks = new List<Block>();
+            foreach (Block b in impl.Blocks)
+            {
+                TransferCmd transferCmd = b.TransferCmd;
+                List<Cmd> newCmds = new List<Cmd>();
+                for (int i = b.Cmds.Count-1; i >= 0; i--)
+                {
+                    CallCmd callCmd = b.Cmds[i] as CallCmd;
+                    if (callCmd == null || callCmd.Proc != yieldProc)
+                    {
+                        newCmds.Insert(0, b.Cmds[i]);
+                    }
+                    else
+                    {
+                        Block newBlock = new Block(Token.NoToken, b.Label + i, newCmds, transferCmd);
+                        newCmds = new List<Cmd>();
+                        transferCmd = new GotoCmd(Token.NoToken, new List<string>(new string[] { newBlock.Label, yieldCheckBlock.Label }), 
+                                                                 new List<Block>(new Block[] { newBlock, yieldCheckBlock }));
+                        newBlocks.Add(newBlock);
+                    }
+                }
+                b.Cmds = newCmds;
+                b.TransferCmd = transferCmd;
+            }
+            impl.Blocks.AddRange(newBlocks);
+            impl.Blocks.Add(yieldCheckBlock);
+        }
+
+        private List<List<Cmd>> CollectAndDesugarYields(Implementation impl,
+            Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap)
+        {
+            // Collect the yield predicates and desugar yields
+            List<List<Cmd>> yields = new List<List<Cmd>>();
+            List<Cmd> cmds = new List<Cmd>();
+            foreach (Block b in impl.Blocks)
+            {
+                YieldCmd yieldCmd = null;
+                List<Cmd> newCmds = new List<Cmd>();
+                for (int i = 0; i < b.Cmds.Count; i++)
+                {
+                    Cmd cmd = b.Cmds[i];
+                    if (cmd is YieldCmd)
+                    {
+                        yieldCmd = (YieldCmd)cmd;
+                        continue;
+                    }
+                    if (yieldCmd != null)
+                    {
+                        PredicateCmd pcmd = cmd as PredicateCmd;
+                        if (pcmd == null)
+                        {
+                            DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar);
+                            if (cmds.Count > 0)
+                            {
+                                yields.Add(cmds);
+                                cmds = new List<Cmd>();
+                            }
+                            yieldCmd = null;
+                        }
+                        else
+                        {
+                            cmds.Add(pcmd);
+                        }
+                    }
+
+                    if (cmd is CallCmd)
+                    {
+                        CallCmd callCmd = cmd as CallCmd;
+                        if (yieldingProcs.Contains(callCmd.Proc))
+                        {
+                            AddCallToYieldProc(callCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
+                        }
+                        if (callCmd.IsAsync)
+                        {
+                            if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name))
+                            {
+                                asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List<IdentifierExpr>(), new List<Ensures>());
+                            }
+                            var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name];
+                            CallCmd dummyCallCmd = new CallCmd(callCmd.tok, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs, callCmd.Attributes);
+                            dummyCallCmd.Proc = dummyAsyncTargetProc;
+                            newCmds.Add(dummyCallCmd);
+                        }
+                        else
+                        {
+                            newCmds.Add(callCmd);
+                        }
+                        if (yieldingProcs.Contains(callCmd.Proc))
+                        {
+                            HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(callCmd));
+                            linearTypeChecker.AddAvailableVars(callCmd, availableLinearVars);
+
+                            if (!callCmd.IsAsync && globalMods.Count > 0 && pc != null)
+                            {
+                                // assume pc || alpha(i, g);
+                                Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
+                                assumeExpr.Type = Type.Bool;
+                                newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
+                            }
+
+                            Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
+                            AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
+                        }
+                    }
+                    else if (cmd is ParCallCmd)
+                    {
+                        ParCallCmd parCallCmd = cmd as ParCallCmd;
+                        AddCallToYieldProc(parCallCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
+                        DesugarParallelCallCmd(newCmds, parCallCmd);
+                        HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(parCallCmd));
+                        linearTypeChecker.AddAvailableVars(parCallCmd, availableLinearVars);
+
+                        if (globalMods.Count > 0 && pc != null)
+                        {
+                            // assume pc || alpha(i, g);
+                            Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
+                            assumeExpr.Type = Type.Bool;
+                            newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
+                        }
+
+                        Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
+                        AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
+                    }
+                    else
+                    {
+                        newCmds.Add(cmd);
+                    }
+                }
+                if (yieldCmd != null)
+                {
+                    DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar);
+                    if (cmds.Count > 0)
+                    {
+                        yields.Add(cmds);
+                        cmds = new List<Cmd>();
+                    }
+                }
+                if (b.TransferCmd is ReturnCmd)
+                {
+                    AddCallToYieldProc(b.TransferCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
+                    if (pc != null)
+                    {
+                        AssertCmd assertCmd = new AssertCmd(b.TransferCmd.tok, Expr.Ident(ok));
+                        assertCmd.ErrorData = "Failed to execute atomic action before procedure return";
+                        newCmds.Add(assertCmd);
+                    }
+                }
+                b.Cmds = newCmds;
+            }
+            return yields;
+        }
+
+        private void ProcessLoopHeaders(Implementation impl, Graph<Block> graph, HashSet<Block> yieldingHeaders, 
+            Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap,
+            out List<Variable> oldPcs, out List<Variable> oldOks)
+        {
+            oldPcs = new List<Variable>();
+            oldOks = new List<Variable>();
+            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));
+                    oldPcs.Add(oldPc);
+                    oldOk = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}", ok.Name, header.Label), Type.Bool));
+                    oldOks.Add(oldOk);
+                }
+                Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(header), domainNameToInputVar);
+                foreach (Block pred in header.Predecessors)
+                {
+                    AddCallToYieldProc(header.tok, 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)
+                {
+                    AssertCmd assertCmd;
+                    assertCmd = new AssertCmd(header.tok, Expr.Eq(Expr.Ident(oldPc), Expr.Ident(pc)));
+                    assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers";
+                    newCmds.Add(assertCmd);
+                    assertCmd = new AssertCmd(header.tok, Expr.Imp(Expr.Ident(oldOk), Expr.Ident(ok)));
+                    assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers";
+                    newCmds.Add(assertCmd);
+                }
+                foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+                {
+                    newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName])));
+                }
+                foreach (Variable v in ogOldGlobalMap.Keys)
+                {
+                    newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(v), Expr.Ident(ogOldGlobalMap[v]))));
+                }
+                newCmds.AddRange(header.Cmds);
+                header.Cmds = newCmds;
+            }
+        }
+
+        private void AddInitialBlock(Implementation impl, List<Variable> oldPcs, List<Variable> oldOks,
+            Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap)
+        {
+            // 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);
+                foreach (Variable oldPc in oldPcs)
+                {
+                    lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)));
+                    rhss.Add(Expr.False);
+                }
+                lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok)));
+                rhss.Add(Expr.False);
+                foreach (Variable oldOk in oldOks)
+                {
+                    lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)));
+                    rhss.Add(Expr.False);
+                }
+            }
+            Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
+            foreach (var domainName in linearTypeChecker.linearDomains.Keys)
+            {
+                domainNameToExpr[domainName] = Expr.Ident(domainNameToInputVar[domainName]);
+            }
+            for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++)
+            {
+                Variable v = impl.InParams[i];
+                var domainName = linearTypeChecker.FindDomainName(v);
+                if (domainName == null) continue;
+                if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
+                var domain = linearTypeChecker.linearDomains[domainName];
+                if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue;
+                Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List<Expr> { Expr.Ident(v) });
+                domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { ie, domainNameToExpr[domainName] });
+            }
+            foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+            {
+                lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName])));
+                rhss.Add(domainNameToExpr[domainName]);
+            }
+            foreach (Variable g in ogOldGlobalMap.Keys)
+            {
+                lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g])));
+                rhss.Add(Expr.Ident(g));
+            }
+            if (lhss.Count > 0)
+            {
+                Block initBlock = new Block(Token.NoToken, "og_init", new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] }));
+                impl.Blocks.Insert(0, initBlock);
+            }
+        }
+
+        private void AddYieldProcAndImpl(List<Declaration> decls) 
+        {
+            if (yieldProc == null) return;
+
+            Program program = linearTypeChecker.program;
+            List<Variable> inputs = new List<Variable>();
+            foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+            {
+                var domain = linearTypeChecker.linearDomains[domainName];
+                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);
+                inputs.Add(f);
+            }
+            foreach (IdentifierExpr ie in globalMods)
+            {
+                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);
+            } 
+            List<Block> blocks = new List<Block>();
+            TransferCmd transferCmd = new ReturnCmd(Token.NoToken);
+            if (yieldCheckerProcs.Count > 0)
+            {
+                List<Block> blockTargets = new List<Block>();
+                List<String> labelTargets = new List<String>();
+                int labelCount = 0;
+                foreach (Procedure proc in yieldCheckerProcs)
+                {
+                    List<Expr> exprSeq = new List<Expr>();
+                    foreach (Variable v in inputs)
+                    {
+                        exprSeq.Add(Expr.Ident(v));
+                    }
+                    CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List<IdentifierExpr>());
+                    callCmd.Proc = proc;
+                    string label = string.Format("L_{0}", labelCount++);
+                    Block block = new Block(Token.NoToken, label, new List<Cmd> { callCmd }, new ReturnCmd(Token.NoToken));
+                    labelTargets.Add(label);
+                    blockTargets.Add(block);
+                    blocks.Add(block);
+                }
+                transferCmd = new GotoCmd(Token.NoToken, labelTargets, blockTargets);
+            }
+            blocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), transferCmd));
+            
+            var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);
+            yieldImpl.Proc = yieldProc;
+            yieldImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
+            decls.Add(yieldProc);
+            decls.Add(yieldImpl);
+        }
+
+        public static QKeyValue RemoveYieldsAttribute(QKeyValue iter)
+        {
+            if (iter == null) return null;
+            iter.Next = RemoveYieldsAttribute(iter.Next);
+            return (iter.Key == "yields") ? iter.Next : iter;
+        }
+
+        public static QKeyValue RemoveMoverAttribute(QKeyValue iter)
+        {
+            if (iter == null) return null;
+            iter.Next = RemoveMoverAttribute(iter.Next);
+            if (iter.Key == "atomic" || iter.Key == "right" || iter.Key == "left" || iter.Key == "both") 
+                return iter.Next;
+            else 
+                return iter;
+        }
+
+        private List<Declaration> Collect()
+        {
+            List<Declaration> decls = new List<Declaration>();
+            foreach (Procedure proc in yieldCheckerProcs)
+            {
+                decls.Add(proc);
+            }
+            foreach (Implementation impl in yieldCheckerImpls)
+            {
+                decls.Add(impl);
+            }
+            foreach (Procedure proc in asyncAndParallelCallDesugarings.Values)
+            {
+                decls.Add(proc);
+            }
+            AddYieldProcAndImpl(decls);
+            return decls;
+        }
+
+        public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
+        {
+            Program program = linearTypeChecker.program;
+            foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum }))
+            {
+                if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue;
+
+                MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, layerNum);
+                foreach (var proc in program.Procedures)
+                {
+                    if (!moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue;
+                    Procedure duplicateProc = duplicator.VisitProcedure(proc);
+                    decls.Add(duplicateProc);
+                }
+                decls.AddRange(duplicator.impls);
+                OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator);
+                foreach (var impl in program.Implementations)
+                {
+                    if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum)
+                        continue;
+                    Implementation duplicateImpl = duplicator.VisitImplementation(impl);
+                    ogTransform.TransformImpl(duplicateImpl);
+                    decls.Add(duplicateImpl);
+                }
+                decls.AddRange(ogTransform.Collect());
+            }
+        }
+    }
+}
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 542d3515..c821117a 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -49,6 +49,8 @@ namespace Microsoft.Boogie
     {
         public Ensures ensures;
         public MoverType moverType;
+        public List<AssertCmd> gate;
+        public CodeExpr action;
         public List<AssertCmd> thisGate;
         public CodeExpr thisAction;
         public List<Variable> thisInParams;
@@ -61,6 +63,8 @@ namespace Microsoft.Boogie
         public HashSet<Variable> modifiedGlobalVars;
         public HashSet<Variable> gateUsedGlobalVars;
         public bool hasAssumeCmd;
+        public Dictionary<Variable, Expr> thisMap;
+        public Dictionary<Variable, Expr> thatMap;
 
         public bool CommutesWith(AtomicActionInfo actionInfo)
         {
@@ -84,122 +88,137 @@ namespace Microsoft.Boogie
         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;
             this.moverType = moverType;
+            this.gate = new List<AssertCmd>();
+            this.action = ensures.Condition as CodeExpr;
             this.thisGate = new List<AssertCmd>();
-            this.thisAction = codeExpr;
             this.thisInParams = new List<Variable>();
             this.thisOutParams = new List<Variable>();
             this.thatGate = new List<AssertCmd>();
             this.thatInParams = new List<Variable>();
             this.thatOutParams = new List<Variable>();
             this.hasAssumeCmd = false;
-            
-            foreach (Block block in codeExpr.Blocks)
+            this.thisMap = new Dictionary<Variable, Expr>();
+            this.thatMap = new Dictionary<Variable, Expr>();
+
+            foreach (Block block in this.action.Blocks)
             {
                 block.Cmds.ForEach(x => this.hasAssumeCmd = this.hasAssumeCmd || x is AssumeCmd);
             }
 
-            var cmds = thisAction.Blocks[0].Cmds;
+            foreach (Block block in this.action.Blocks)
+            {
+                if (block.TransferCmd is ReturnExprCmd)
+                {
+                    block.TransferCmd = new ReturnCmd(block.TransferCmd.tok);
+                }
+            }
+
+            var cmds = this.action.Blocks[0].Cmds;
             for (int i = 0; i < cmds.Count; i++)
             {
                 AssertCmd assertCmd = cmds[i] as AssertCmd;
                 if (assertCmd == null) break;
-                thisGate.Add(assertCmd);
+                this.gate.Add(assertCmd);
                 cmds[i] = new AssumeCmd(assertCmd.tok, Expr.True);
             }
 
-            Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
             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, x.Attributes);
-                this.thatInParams.Add(y);
-                map[x] = Expr.Ident(y);
+                Variable thisx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "this_" + x.Name, x.TypedIdent.Type), true, x.Attributes);
+                this.thisInParams.Add(thisx);
+                this.thisMap[x] = Expr.Ident(thisx);
+                Variable thatx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true, x.Attributes);
+                this.thatInParams.Add(thatx);
+                this.thatMap[x] = Expr.Ident(thatx);
             }
             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, x.Attributes);
-                this.thatOutParams.Add(y);
-                map[x] = Expr.Ident(y);
+                Variable thisx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "this_" + x.Name, x.TypedIdent.Type), false, x.Attributes);
+                this.thisOutParams.Add(thisx);
+                this.thisMap[x] = Expr.Ident(thisx);
+                Variable thatx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false, x.Attributes);
+                this.thatOutParams.Add(thatx);
+                this.thatMap[x] = Expr.Ident(thatx);
             }
+            List<Variable> thisLocVars = new List<Variable>();
             List<Variable> thatLocVars = new List<Variable>();
-            foreach (Variable x in thisAction.LocVars)
+            foreach (Variable x in this.action.LocVars)
             {
-                Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
-                map[x] = Expr.Ident(y);
-                thatLocVars.Add(y);
+                Variable thisx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "this_" + x.Name, x.TypedIdent.Type), false);
+                thisMap[x] = Expr.Ident(thisx);
+                thisLocVars.Add(thisx);
+                Variable thatx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
+                thatMap[x] = Expr.Ident(thatx);
+                thatLocVars.Add(thatx);
             }
             Contract.Assume(proc.TypeParameters.Count == 0);
-            Substitution subst = Substituter.SubstitutionFromHashtable(map);
-            foreach (AssertCmd assertCmd in thisGate)
+            Substitution thisSubst = Substituter.SubstitutionFromHashtable(this.thisMap);
+            Substitution thatSubst = Substituter.SubstitutionFromHashtable(this.thatMap);
+            foreach (AssertCmd assertCmd in this.gate)
+            {
+                this.thisGate.Add((AssertCmd)Substituter.Apply(thisSubst, assertCmd));
+                this.thatGate.Add((AssertCmd)Substituter.Apply(thatSubst, assertCmd));
+            }
+            this.thisAction = new CodeExpr(thisLocVars, SubstituteBlocks(this.action.Blocks, thisSubst, "this_"));
+            this.thatAction = new CodeExpr(thatLocVars, SubstituteBlocks(this.action.Blocks, thatSubst, "that_"));
+
             {
-                thatGate.Add((AssertCmd)Substituter.Apply(subst, assertCmd));
+                VariableCollector collector = new VariableCollector();
+                collector.Visit(this.action);
+                this.actionUsedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable));
             }
+
+            List<Variable> modifiedVars = new List<Variable>();
+            foreach (Block block in this.action.Blocks)
+            {
+                block.Cmds.ForEach(cmd => cmd.AddAssignedVariables(modifiedVars));
+            }
+            this.modifiedGlobalVars = new HashSet<Variable>(modifiedVars.Where(x => x is GlobalVariable));
+
+            {
+                VariableCollector collector = new VariableCollector();
+                this.gate.ForEach(assertCmd => collector.Visit(assertCmd));
+                this.gateUsedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable));
+            }
+        }
+
+        private List<Block> SubstituteBlocks(List<Block> blocks, Substitution subst, string blockLabelPrefix)
+        {
             Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
-            List<Block> thatBlocks = new List<Block>();
-            foreach (Block block in thisAction.Blocks)
+            List<Block> otherBlocks = new List<Block>();
+            foreach (Block block in blocks)
             {
                 List<Cmd> otherCmds = new List<Cmd>();
                 foreach (Cmd cmd in block.Cmds)
                 {
                     otherCmds.Add(Substituter.Apply(subst, cmd));
                 }
-                Block thatBlock = new Block();
-                thatBlock.Cmds = otherCmds;
-                thatBlock.Label = "that_" + block.Label;
-                block.Label = "this_" + block.Label;
-                thatBlocks.Add(thatBlock);
-                blockMap[block] = thatBlock;
-                if (block.TransferCmd is GotoCmd)
-                {
-                    GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
-                    for (int i = 0; i < gotoCmd.labelNames.Count; i++)
-                    {
-                        gotoCmd.labelNames[i] = "this_" + gotoCmd.labelNames[i];
-                    }
-                }
+                Block otherBlock = new Block();
+                otherBlock.Cmds = otherCmds;
+                otherBlock.Label = blockLabelPrefix + block.Label;
+                otherBlocks.Add(otherBlock);
+                blockMap[block] = otherBlock;
             }
-            foreach (Block block in thisAction.Blocks)
+            foreach (Block block in blocks)
             {
-                if (block.TransferCmd is ReturnExprCmd)
+                if (block.TransferCmd is ReturnCmd)
                 {
-                    block.TransferCmd = new ReturnCmd(block.TransferCmd.tok);
                     blockMap[block].TransferCmd = new ReturnCmd(block.TransferCmd.tok);
                     continue;
                 }
-                List<Block> thatGotoCmdLabelTargets = new List<Block>();
-                List<string> thatGotoCmdLabelNames = new List<string>();
+                List<Block> otherGotoCmdLabelTargets = new List<Block>();
+                List<string> otherGotoCmdLabelNames = new List<string>();
                 GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
                 foreach (Block target in gotoCmd.labelTargets)
                 {
-                    thatGotoCmdLabelTargets.Add(blockMap[target]);
-                    thatGotoCmdLabelNames.Add(blockMap[target].Label);
+                    otherGotoCmdLabelTargets.Add(blockMap[target]);
+                    otherGotoCmdLabelNames.Add(blockMap[target].Label);
                 }
-                blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, thatGotoCmdLabelNames, thatGotoCmdLabelTargets);
-            }
-            this.thatAction = new CodeExpr(thatLocVars, thatBlocks);
-
-            {
-                VariableCollector collector = new VariableCollector();
-                collector.Visit(codeExpr);
-                this.actionUsedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable));
-            }
-
-            List<Variable> modifiedVars = new List<Variable>();
-            foreach (Block block in codeExpr.Blocks)
-            {
-                block.Cmds.ForEach(cmd => cmd.AddAssignedVariables(modifiedVars));
-            }
-            this.modifiedGlobalVars = new HashSet<Variable>(modifiedVars.Where(x => x is GlobalVariable));
-
-            {
-                VariableCollector collector = new VariableCollector();
-                this.thisGate.ForEach(assertCmd => collector.Visit(assertCmd));
-                this.gateUsedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable));
+                blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets);
             }
+            return otherBlocks;
         }
     }