some refactoring of QED stuff

5 files changed, 221 insertions, 220 deletions

diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs
index 51f7f328..576d6163 100644
--- a/Source/Concurrency/LinearSets.cs
+++ b/Source/Concurrency/LinearSets.cs
@@ -47,7 +47,7 @@ namespace Microsoft.Boogie
             this.varToDomainName = new Dictionary<Variable, string>();

             this.linearDomains = new Dictionary<string, LinearDomain>();

         }

-        public void Typecheck()

+        public void TypeCheck()

         {

             this.VisitProgram(program);

             foreach (string domainName in domainNameToType.Keys)

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 0a918ad1..53d61ba5 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -7,31 +7,173 @@ using System.Diagnostics;
 

 namespace Microsoft.Boogie

 {

-    /*

-     * Typechecking rules:

-     * At most one atomic specification per procedure

-     * The gate of an atomic specification refers only to global and input variables       

-     */

+    public enum MoverType

+    {

+        Top,

+        Atomic,

+        Right,

+        Left,

+        Both

+    }

+

+    public class ActionInfo

+    {

+        public Procedure proc;

+        public MoverType moverType;

+        public int phaseNum;

+        public List<AssertCmd> thisGate;

+        public CodeExpr thisAction;

+        public List<Variable> thisInParams;

+        public List<Variable> thisOutParams;

+        public List<AssertCmd> thatGate;

+        public CodeExpr thatAction;

+        public List<Variable> thatInParams;

+        public List<Variable> thatOutParams;

+

+        public bool IsRightMover

+        {

+            get { return moverType == MoverType.Right || moverType == MoverType.Both; }

+        }

+

+        public bool IsLeftMover

+        {

+            get { return moverType == MoverType.Left || moverType == MoverType.Both; }

+        }

+

+        public ActionInfo(Procedure proc, CodeExpr codeExpr, MoverType moverType, int phaseNum)

+        {

+            this.proc = proc;

+            this.moverType = moverType;

+            this.phaseNum = phaseNum;

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

+

+            var cmds = thisAction.Blocks[0].Cmds;

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

+            {

+                AssertCmd assertCmd = cmds[i] as AssertCmd;

+                if (assertCmd == null) break;

+                thisGate.Add(assertCmd);

+                cmds[i] = new AssumeCmd(assertCmd.tok, assertCmd.Expr);

+            }

+

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

+                this.thatInParams.Add(y);

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

+            }

+            foreach (Variable x in proc.OutParams)

+            {

+                this.thisOutParams.Add(x);

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

+                this.thatOutParams.Add(y);

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

+            }

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

+            foreach (Variable x in thisAction.LocVars)

+            {

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

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

+                otherLocVars.Add(y);

+            }

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

+            Substitution subst = Substituter.SubstitutionFromHashtable(map);

+            foreach (AssertCmd assertCmd in thisGate)

+            {

+                thatGate.Add((AssertCmd)Substituter.Apply(subst, assertCmd));

+            }

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

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

+            foreach (Block block in thisAction.Blocks)

+            {

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

+                foreach (Cmd cmd in block.Cmds)

+                {

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

+                }

+                Block otherBlock = new Block();

+                otherBlock.Cmds = otherCmds;

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

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

+                otherBlocks.Add(otherBlock);

+                blockMap[block] = otherBlock;

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

+                    }

+                }

+            }

+            foreach (Block block in thisAction.Blocks)

+            {

+                if (block.TransferCmd is ReturnExprCmd)

+                {

+                    blockMap[block].TransferCmd = new ReturnExprCmd(block.TransferCmd.tok, Expr.True);

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

+            }

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

+        }

+    }

+

     public class MoverCheck

     {

+        public static MoverType GetMoverType(Ensures e, out int phaseNum)

+        {

+            phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "atomic", int.MaxValue);

+            if (phaseNum != int.MaxValue)

+                return MoverType.Atomic;

+            phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "right", int.MaxValue);

+            if (phaseNum != int.MaxValue)

+                return MoverType.Right;

+            phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "left", int.MaxValue);

+            if (phaseNum != int.MaxValue)

+                return MoverType.Left;

+            phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "both", int.MaxValue);

+            if (phaseNum != int.MaxValue)

+                return MoverType.Both;

+            return MoverType.Top;

+        }

+

         HashSet<Tuple<ActionInfo, ActionInfo>> commutativityCheckerCache;

         HashSet<Tuple<ActionInfo, ActionInfo>> gatePreservationCheckerCache;

         HashSet<Tuple<ActionInfo, ActionInfo>> failurePreservationCheckerCache;

         LinearTypeChecker linearTypeChecker;

+        MoverTypeChecker moverTypeChecker;

         Program moverCheckerProgram;

-        private MoverCheck(LinearTypeChecker linearTypeChecker)

+        private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)

         {

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

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

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

             this.linearTypeChecker = linearTypeChecker;

+            this.moverTypeChecker = moverTypeChecker;

             this.moverCheckerProgram = new Program();

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

+            foreach (Declaration decl in moverTypeChecker.program.TopLevelDeclarations)

             {

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

                     this.moverCheckerProgram.TopLevelDeclarations.Add(decl);

             }

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

+            foreach (Variable v in moverTypeChecker.program.GlobalVariables())

             {

                 this.moverCheckerProgram.TopLevelDeclarations.Add(v);

             }

@@ -84,163 +226,18 @@ namespace Microsoft.Boogie
             }

         }

 

-        enum MoverType

-        {

-            Top,

-            Atomic,

-            Right,

-            Left,

-            Both

-        }

-

-        class ActionInfo

-        {

-            public Procedure proc;

-            public MoverType moverType;

-            public List<AssertCmd> thisGate;

-            public CodeExpr thisAction;

-            public List<Variable> thisInParams;

-            public List<Variable> thisOutParams;

-            public List<AssertCmd> thatGate;

-            public CodeExpr thatAction;

-            public List<Variable> thatInParams;

-            public List<Variable> thatOutParams;

-

-            public bool IsRightMover

-            {

-                get { return moverType == MoverType.Right || moverType == MoverType.Both; }

-            }

-            

-            public bool IsLeftMover

-            {

-                get { return moverType == MoverType.Left || moverType == MoverType.Both; }

-            }

-

-            public ActionInfo(Procedure proc, CodeExpr codeExpr, MoverType moverType)

-            {

-                this.proc = proc;

-                this.moverType = moverType;

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

-

-                var cmds = thisAction.Blocks[0].Cmds;

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

-                {

-                    AssertCmd assertCmd = cmds[i] as AssertCmd;

-                    if (assertCmd == null) break;

-                    thisGate.Add(assertCmd);

-                    cmds[i] = new AssumeCmd(assertCmd.tok, assertCmd.Expr);

-                }

-

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

-                    this.thatInParams.Add(y);

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

-                }

-                foreach (Variable x in proc.OutParams)

-                {

-                    this.thisOutParams.Add(x);

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

-                    this.thatOutParams.Add(y);

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

-                }

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

-                foreach (Variable x in thisAction.LocVars)

-                {

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

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

-                    otherLocVars.Add(y);

-                }

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

-                Substitution subst = Substituter.SubstitutionFromHashtable(map);

-                foreach (AssertCmd assertCmd in thisGate)

-                {

-                    thatGate.Add((AssertCmd)Substituter.Apply(subst, assertCmd));

-                }

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

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

-                foreach (Block block in thisAction.Blocks)

-                {

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

-                    foreach (Cmd cmd in block.Cmds)

-                    {

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

-                    }

-                    Block otherBlock = new Block();

-                    otherBlock.Cmds = otherCmds;

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

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

-                    otherBlocks.Add(otherBlock);

-                    blockMap[block] = otherBlock;

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

-                        }

-                    }

-                }

-                foreach (Block block in thisAction.Blocks)

-                {

-                    if (block.TransferCmd is ReturnExprCmd)

-                    {

-                        blockMap[block].TransferCmd = new ReturnExprCmd(block.TransferCmd.tok, Expr.True);

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

-                }

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

-            }

-        }

-

-        public static void AddCheckers(LinearTypeChecker linearTypeChecker)

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

         {

-            Program program = linearTypeChecker.program;

-            List<ActionInfo> gatedActions = new List<ActionInfo>();

-            foreach (Declaration decl in program.TopLevelDeclarations)

-            {

-                Procedure proc = decl as Procedure;

-                if (proc == null) continue;

-                foreach (Ensures e in proc.Ensures)

-                {

-                    MoverType moverType = GetMoverType(e);

-                    if (moverType == MoverType.Top) continue;

-                    CodeExpr codeExpr = e.Condition as CodeExpr;

-                    if (codeExpr == null)

-                    {

-                        Console.WriteLine("Warning: an atomic action must be a CodeExpr");

-                        continue;

-                    }

-                    ActionInfo info = new ActionInfo(proc, codeExpr, moverType);

-                    gatedActions.Add(info);

-                }

-            }

-            if (gatedActions.Count == 0)

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

                 return;

-            MoverCheck moverChecking = new MoverCheck(linearTypeChecker);

-            foreach (ActionInfo first in gatedActions)

+            Program program = moverTypeChecker.program;

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

+            foreach (ActionInfo first in moverTypeChecker.procToActionInfo.Values)

             {

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

                 if (first.moverType == MoverType.Atomic)

                     continue;

-                foreach (ActionInfo second in gatedActions)

+                foreach (ActionInfo second in moverTypeChecker.procToActionInfo.Values)

                 {

                     if (first.IsRightMover)

                     {

@@ -274,20 +271,6 @@ namespace Microsoft.Boogie
             }

         }

 

-        private static MoverType GetMoverType(Ensures e)

-        {

-            if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))

-                return MoverType.Atomic;

-            else if (QKeyValue.FindBoolAttribute(e.Attributes, "right"))

-                return MoverType.Right;

-            else if (QKeyValue.FindBoolAttribute(e.Attributes, "left"))

-                return MoverType.Left;

-            else if (QKeyValue.FindBoolAttribute(e.Attributes, "both"))

-                return MoverType.Both;

-            else

-                return MoverType.Top;

-        }

-

         class TransitionRelationComputation

         {

             private Program program;

@@ -638,4 +621,4 @@ namespace Microsoft.Boogie
             this.moverCheckerProgram.TopLevelDeclarations.Add(proc);

         }

     }

-}

+}
\ No newline at end of file
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 27528826..7125bfcd 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -14,14 +14,16 @@ namespace Microsoft.Boogie
     {

         List<IdentifierExpr> globalMods;

         LinearTypeChecker linearTypeChecker;

+        MoverTypeChecker moverTypeChecker;

         Dictionary<string, Procedure> asyncAndParallelCallDesugarings;

         List<Procedure> yieldCheckerProcs;

         List<Implementation> yieldCheckerImpls;

         Procedure yieldProc;

 

-        public OwickiGriesTransform(LinearTypeChecker linearTypeChecker)

+        public OwickiGriesTransform(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)

         {

             this.linearTypeChecker = linearTypeChecker;

+            this.moverTypeChecker = moverTypeChecker;

             Program program = linearTypeChecker.program;

             globalMods = new List<IdentifierExpr>();

             foreach (Variable g in program.GlobalVariables())

@@ -689,11 +691,6 @@ namespace Microsoft.Boogie
 

         public void Transform()

         {

-            MoverCheck.AddCheckers(linearTypeChecker);

-#if QED

-            YieldTypeChecker.PerformYieldTypeChecking(linearTypeChecker);

-            RefinementCheck.AddCheckers(linearTypeChecker);

-#endif

             Program program = linearTypeChecker.program;

             foreach (var decl in program.TopLevelDeclarations)

             {

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index b463bcfd..8f8638d6 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -6,28 +6,62 @@ using Microsoft.Boogie;
 

 namespace Microsoft.Boogie

 {

-    class TypeCheck : StandardVisitor

+    public class MoverTypeChecker : StandardVisitor

     {

-        public static int FindPhaseNumber(Procedure proc)

+        public int FindPhaseNumber(Procedure proc)

         {

-            foreach (Ensures ensures in proc.Ensures)

-            {

-

-            }

-            return int.MaxValue;

+            if (procToActionInfo.ContainsKey(proc))

+                return procToActionInfo[proc].phaseNum;

+            else

+                return int.MaxValue;

         }

 

         CheckingContext checkingContext;

-        int errorCount;

+        public int errorCount;

         HashSet<Variable> globalVariables;

         bool insideYield;

         int phaseNumEnclosingProc;

-                

-        public TypeCheck(Program program)

+        public Dictionary<Procedure, ActionInfo> procToActionInfo;

+        public Program program;

+

+        public void TypeCheck()

+        {

+            foreach (Declaration decl in program.TopLevelDeclarations)

+            {

+                Procedure proc = decl as Procedure;

+                if (proc == null) continue;

+                foreach (Ensures e in proc.Ensures)

+                {

+                    int phaseNum;

+                    MoverType moverType = MoverCheck.GetMoverType(e, out phaseNum);

+                    if (moverType == MoverType.Top) continue;

+                    CodeExpr codeExpr = e.Condition as CodeExpr;

+                    if (codeExpr == null)

+                    {

+                        Error(e, "An atomic action must be a CodeExpr");

+                        continue;

+                    }

+                    if (procToActionInfo.ContainsKey(proc))

+                    {

+                        Error(proc, "A procedure can have at most one atomic action");

+                        continue;

+                    }

+                    procToActionInfo[proc] = new ActionInfo(proc, codeExpr, moverType, phaseNum);

+                }

+            }

+            this.VisitProgram(program);

+#if QED

+            YieldTypeChecker.PerformYieldTypeChecking(this);

+#endif

+        }

+

+        public MoverTypeChecker(Program program)

         {

             globalVariables = new HashSet<Variable>(program.GlobalVariables());

+            procToActionInfo = new Dictionary<Procedure, ActionInfo>();

             this.errorCount = 0;

             this.checkingContext = new CheckingContext(null);

+            this.program = program;

         }

         public override Block VisitBlock(Block node)

         {

@@ -118,14 +152,10 @@ namespace Microsoft.Boogie
             return base.VisitAssumeCmd(node);

         }

 

-        //

-

-        private void Error(Absy node, string message)

+        public void Error(Absy node, string message)

         {

             checkingContext.Error(node, message);

             errorCount++;

         }

-

-       

     }

-}

+}
\ No newline at end of file
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index 2be2ef55..0a3ebfb0 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -26,26 +26,15 @@ namespace Microsoft.Boogie
         static CharSetSolver yieldTypeCheckerAutomatonSolver;

         static string yieldTypeCheckerRegex = @"^((1|2)+(3|4))*((D)+(((5|6))+((7|8))+((1|2))+((3|4)))*[A]((9)+(7)+(3))*)*$";// regex of property to build automaton of YTS language

         static Automaton<BvSet> yieldTypeCheckerAutomaton;

-        static int errorCount;

-        static CheckingContext checkingContext;

-        static Automaton<BvSet> foo;

         static YieldTypeChecker()

         {

             yieldTypeCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7);

-            foo = yieldTypeCheckerAutomatonSolver.Convert(@"^[1-9A-D]*$");

-            yieldTypeCheckerAutomaton = yieldTypeCheckerAutomatonSolver.Convert(yieldTypeCheckerRegex); // YTS property , L(YTSP)

-            yieldTypeCheckerAutomaton = Automaton<BvSet>.MkProduct(yieldTypeCheckerAutomaton, foo, yieldTypeCheckerAutomatonSolver);

-

-            errorCount = 0;

-            checkingContext = new CheckingContext(null);

-        }

-

-        private static void Error(Absy node, string message)

-        {

-            checkingContext.Error(node, message);

-            errorCount++;

+            yieldTypeCheckerAutomaton = 

+                Automaton<BvSet>.MkProduct(yieldTypeCheckerAutomatonSolver.Convert(yieldTypeCheckerRegex), 

+                                           yieldTypeCheckerAutomatonSolver.Convert(@"^[1-9A-D]*$"), 

+                                           yieldTypeCheckerAutomatonSolver);

         }

-

+        

         /*

          Parameter: Automaton<BvSet> implTypeCheckAutomaton :  Automaton of implementation body build with respect to YTSI.

          Return : if L(YTSI) is subset of L(YTSP) {TRUE} else {FALSE}  

@@ -73,20 +62,20 @@ namespace Microsoft.Boogie
         /*

          Parameter : LinearTypeChecker linearTypeChecker : YTS Checker is a component of linearTypeChecker.Adds instance of YTS checker into linearType checker

          */

-        public static void PerformYieldTypeChecking(LinearTypeChecker linearTypeChecker)

+        public static void PerformYieldTypeChecking(MoverTypeChecker moverTypeChecker)

         {

-            Program yieldTypeCheckedProgram = linearTypeChecker.program;

+            Program yieldTypeCheckedProgram = moverTypeChecker.program;

             YieldTypeChecker regExprToAuto = new YieldTypeChecker();

             foreach (var decl in yieldTypeCheckedProgram.TopLevelDeclarations)

             {

                 Implementation impl = decl as Implementation;

                 if (impl == null) continue;

-                int phaseNumSpecImpl = TypeCheck.FindPhaseNumber(impl.Proc);

-                YieldTypeCheckerCore yieldTypeCheckerPerImpl = new YieldTypeCheckerCore(impl, phaseNumSpecImpl);

+                int phaseNumSpecImpl = moverTypeChecker.FindPhaseNumber(impl.Proc);

+                YieldTypeCheckerCore yieldTypeCheckerPerImpl = new YieldTypeCheckerCore(moverTypeChecker, impl, phaseNumSpecImpl);

                 Automaton<BvSet> yieldTypeCheckImpl = yieldTypeCheckerPerImpl.YieldTypeCheckAutomata();

                 if (!IsYieldTypeSafe(yieldTypeCheckImpl))

                 {

-                    Error(impl, "\n Body of " + impl.Proc.Name + " is not yield type safe " + "\n");

+                    moverTypeChecker.Error(impl, "\n Body of " + impl.Proc.Name + " is not yield type safe " + "\n");

                 }

             }

         }

@@ -108,9 +97,11 @@ namespace Microsoft.Boogie
         List<Tuple<int, int>> phaseIntervals; // [MinValue ph0 ] [ph0 ph1] [ph1 ph2] ..... [phk phk+1] intervals

         List<int> finalStates; //final

         List<int> initialStates; // initial states collection. There are epsilon transitions (ASCII 'E') from concreteInitial state to these initial states

+        MoverTypeChecker moverTypeChecker;

 

-        public YieldTypeCheckerCore(Implementation toTypeCheck, int specPhaseNum)

+        public YieldTypeCheckerCore(MoverTypeChecker moverTypeChecker, Implementation toTypeCheck, int specPhaseNum)

         {

+            this.moverTypeChecker = moverTypeChecker;

             ytypeChecked = toTypeCheck;

             

             specPhaseNumImpl = specPhaseNum;

@@ -150,7 +141,7 @@ namespace Microsoft.Boogie
             HashSet<int> callCmdPhaseNumSet = new HashSet<int>();

             foreach (CallCmd callCmd in callCmdsInImpl)

             {

-                int tmpPhaseNum = TypeCheck.FindPhaseNumber(callCmd.Proc);

+                int tmpPhaseNum = moverTypeChecker.FindPhaseNumber(callCmd.Proc);

                 callCmdPhaseNumSet.Add(tmpPhaseNum);       

             }

             callCmdPhaseNumSet.Add(specPhaseNumImpl);