cleaned up some names

7 files changed, 112 insertions, 113 deletions

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/CivlRefinement.cs
index d861e2f3..43d0f60c 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/CivlRefinement.cs
@@ -13,7 +13,7 @@ namespace Microsoft.Boogie
 {
     public class MyDuplicator : Duplicator
     {
-        MoverTypeChecker moverTypeChecker;
+        CivlTypeChecker civlTypeChecker;
         public int layerNum;
         Procedure enclosingProc;
         Implementation enclosingImpl;
@@ -23,9 +23,9 @@ namespace Microsoft.Boogie
         public HashSet<Procedure> yieldingProcs;
         public List<Implementation> impls;
 
-        public MyDuplicator(MoverTypeChecker moverTypeChecker, int layerNum)
+        public MyDuplicator(CivlTypeChecker civlTypeChecker, int layerNum)
         {
-            this.moverTypeChecker = moverTypeChecker;
+            this.civlTypeChecker = civlTypeChecker;
             this.layerNum = layerNum;
             this.enclosingProc = null;
             this.enclosingImpl = null;
@@ -38,19 +38,19 @@ namespace Microsoft.Boogie
 
         private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List<Cmd> newCmds)
         {
-            int enclosingProcLayerNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum;
+            int enclosingProcLayerNum = civlTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum;
             Procedure originalProc = originalCallCmd.Proc;
             
-            if (moverTypeChecker.procToAtomicProcedureInfo.ContainsKey(originalProc))
+            if (civlTypeChecker.procToAtomicProcedureInfo.ContainsKey(originalProc))
             {
-                if (moverTypeChecker.CallExists(originalCallCmd, enclosingProcLayerNum, layerNum))
+                if (civlTypeChecker.CallExists(originalCallCmd, enclosingProcLayerNum, layerNum))
                 {
                     newCmds.Add(callCmd);
                 }
             }
-            else if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc))
+            else if (civlTypeChecker.procToActionInfo.ContainsKey(originalProc))
             {
-                AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo;
+                AtomicActionInfo atomicActionInfo = civlTypeChecker.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) })));
@@ -78,7 +78,7 @@ namespace Microsoft.Boogie
             int maxCalleeLayerNum = 0;
             foreach (CallCmd iter in originalParCallCmd.CallCmds)
             {
-                int calleeLayerNum = moverTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum;
+                int calleeLayerNum = civlTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum;
                 if (calleeLayerNum > maxCalleeLayerNum)
                     maxCalleeLayerNum = calleeLayerNum;
             }
@@ -156,7 +156,7 @@ namespace Microsoft.Boogie
 
         public override Procedure VisitProcedure(Procedure node)
         {
-            if (!moverTypeChecker.procToActionInfo.ContainsKey(node))
+            if (!civlTypeChecker.procToActionInfo.ContainsKey(node))
                 return node;
             if (!procMap.ContainsKey(node))
             {
@@ -167,7 +167,7 @@ namespace Microsoft.Boogie
                 proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies);
                 proc.OutParams = this.VisitVariableSeq(node.OutParams);
 
-                ActionInfo actionInfo = moverTypeChecker.procToActionInfo[node];
+                ActionInfo actionInfo = civlTypeChecker.procToActionInfo[node];
                 if (actionInfo.createdAtLayerNum < layerNum)
                 {
                     proc.Requires = new List<Requires>();
@@ -210,7 +210,7 @@ namespace Microsoft.Boogie
                 }
                 procMap[node] = proc;
                 proc.Modifies = new List<IdentifierExpr>();
-                moverTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));
+                civlTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));
             }
             return procMap[node];
         }
@@ -232,7 +232,7 @@ namespace Microsoft.Boogie
             Requires requires = base.VisitRequires(node);
             if (node.Free)
                 return requires;
-            if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum))
+            if (!civlTypeChecker.absyToLayerNums[node].Contains(layerNum))
                 requires.Condition = Expr.True;
             return requires;
         }
@@ -242,12 +242,12 @@ namespace Microsoft.Boogie
             Ensures ensures = base.VisitEnsures(node);
             if (node.Free)
                 return ensures;
-            AtomicActionInfo atomicActionInfo =  moverTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo;
+            AtomicActionInfo atomicActionInfo =  civlTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo;
             bool isAtomicSpecification = atomicActionInfo != null && atomicActionInfo.ensures == node;
-            if (isAtomicSpecification || !moverTypeChecker.absyToLayerNums[node].Contains(layerNum))
+            if (isAtomicSpecification || !civlTypeChecker.absyToLayerNums[node].Contains(layerNum))
             {
                 ensures.Condition = Expr.True;
-                ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes);
+                ensures.Attributes = CivlRefinement.RemoveMoverAttribute(ensures.Attributes);
             }
             return ensures;
         }
@@ -255,16 +255,16 @@ namespace Microsoft.Boogie
         public override Cmd VisitAssertCmd(AssertCmd node)
         {
             AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node);
-            if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum))
+            if (!civlTypeChecker.absyToLayerNums[node].Contains(layerNum))
                 assertCmd.Expr = Expr.True;
             return assertCmd;
         }
     }
 
-    public class OwickiGries
+    public class CivlRefinement
     {
         LinearTypeChecker linearTypeChecker;
-        MoverTypeChecker moverTypeChecker;
+        CivlTypeChecker civlTypeChecker;
         Dictionary<Absy, Absy> absyMap;
         Dictionary<Implementation, Implementation> implMap;
         HashSet<Procedure> yieldingProcs;
@@ -281,17 +281,17 @@ namespace Microsoft.Boogie
         Expr beta;
         HashSet<Variable> frame;
 
-        public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator)
+        public CivlRefinement(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, MyDuplicator duplicator)
         {
             this.linearTypeChecker = linearTypeChecker;
-            this.moverTypeChecker = moverTypeChecker;
+            this.civlTypeChecker = civlTypeChecker;
             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)
+            foreach (Variable g in civlTypeChecker.SharedVariables)
             {
                 globalMods.Add(Expr.Ident(g));
             }
@@ -304,17 +304,17 @@ namespace Microsoft.Boogie
         private IEnumerable<Variable> AvailableLinearVars(Absy absy)
         {
             HashSet<Variable> availableVars = new HashSet<Variable>(linearTypeChecker.AvailableLinearVars(absyMap[absy]));
-            foreach (var g in moverTypeChecker.globalVarToSharedVarInfo.Keys)
+            foreach (var g in civlTypeChecker.globalVarToSharedVarInfo.Keys)
             {
-                SharedVariableInfo info = moverTypeChecker.globalVarToSharedVarInfo[g];
+                SharedVariableInfo info = civlTypeChecker.globalVarToSharedVarInfo[g];
                 if (!(info.introLayerNum <= layerNum && layerNum <= info.hideLayerNum))
                 {
                     availableVars.Remove(g);
                 }
             }
-            foreach (var v in moverTypeChecker.localVarToLocalVariableInfo.Keys)
+            foreach (var v in civlTypeChecker.localVarToLocalVariableInfo.Keys)
             {
-                LocalVariableInfo info = moverTypeChecker.localVarToLocalVariableInfo[v];
+                LocalVariableInfo info = civlTypeChecker.localVarToLocalVariableInfo[v];
                 if (info.isGhost)
                 {
                     if (info.layer != layerNum)
@@ -754,7 +754,7 @@ namespace Microsoft.Boogie
             }
 
             Procedure originalProc = implMap[impl].Proc;
-            ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc];
+            ActionInfo actionInfo = civlTypeChecker.procToActionInfo[originalProc];
             if (actionInfo.createdAtLayerNum == this.layerNum)
             {
                 pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool));
@@ -777,11 +777,11 @@ namespace Microsoft.Boogie
                     foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);
                 }
                 Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);
-                frame = new HashSet<Variable>(moverTypeChecker.SharedVariables);
-                foreach (Variable v in moverTypeChecker.SharedVariables)
+                frame = new HashSet<Variable>(civlTypeChecker.SharedVariables);
+                foreach (Variable v in civlTypeChecker.SharedVariables)
                 {
-                    if (moverTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || 
-                        moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum)
+                    if (civlTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || 
+                        civlTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum)
                     {
                         frame.Remove(v);
                     }
@@ -798,7 +798,7 @@ namespace Microsoft.Boogie
                 }
                 else
                 {
-                    Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, atomicActionInfo, frame, new HashSet<Variable>())).TransitionRelationCompute(true);
+                    Expr betaExpr = (new MoverCheck.TransitionRelationComputation(civlTypeChecker.program, atomicActionInfo, frame, new HashSet<Variable>())).TransitionRelationCompute(true);
                     beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr);
                     Expr alphaExpr = Expr.True;
                     foreach (AssertCmd assertCmd in atomicActionInfo.gate)
@@ -1209,31 +1209,31 @@ namespace Microsoft.Boogie
             return decls;
         }
 
-        public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
+        public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls)
         {
             Program program = linearTypeChecker.program;
-            foreach (int layerNum in moverTypeChecker.AllImplementedLayerNums)
+            foreach (int layerNum in civlTypeChecker.AllImplementedLayerNums)
             {
                 if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue;
 
-                MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, layerNum);
+                MyDuplicator duplicator = new MyDuplicator(civlTypeChecker, layerNum);
                 foreach (var proc in program.Procedures)
                 {
-                    if (!moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue;
+                    if (!civlTypeChecker.procToActionInfo.ContainsKey(proc)) continue;
                     Procedure duplicateProc = duplicator.VisitProcedure(proc);
                     decls.Add(duplicateProc);
                 }
                 decls.AddRange(duplicator.impls);
-                OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator);
+                CivlRefinement civlTransform = new CivlRefinement(linearTypeChecker, civlTypeChecker, duplicator);
                 foreach (var impl in program.Implementations)
                 {
-                    if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum)
+                    if (!civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum)
                         continue;
                     Implementation duplicateImpl = duplicator.VisitImplementation(impl);
-                    ogTransform.TransformImpl(duplicateImpl);
+                    civlTransform.TransformImpl(duplicateImpl);
                     decls.Add(duplicateImpl);
                 }
-                decls.AddRange(ogTransform.Collect());
+                decls.AddRange(civlTransform.Collect());
             }
         }
     }
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/CivlTypeChecker.cs
index 0e257f30..dba7ab4b 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/CivlTypeChecker.cs
@@ -357,7 +357,7 @@ namespace Microsoft.Boogie
         }
     }
 
-    public class MoverTypeChecker : ReadOnlyVisitor
+    public class CivlTypeChecker : ReadOnlyVisitor
     {
         CheckingContext checkingContext;
         Procedure enclosingProc;
@@ -376,8 +376,7 @@ namespace Microsoft.Boogie
 
         public bool CallExists(CallCmd callCmd, int enclosingProcLayerNum, int layerNum)
         {
-            if (!procToAtomicProcedureInfo.ContainsKey(callCmd.Proc))
-                return true;
+            Debug.Assert(procToAtomicProcedureInfo.ContainsKey(callCmd.Proc));
             var atomicProcedureInfo = procToAtomicProcedureInfo[callCmd.Proc];
             if (callCmd.Proc.Modifies.Count > 0)
             {
@@ -448,7 +447,7 @@ namespace Microsoft.Boogie
             return MoverType.Top;
         }
 
-        public MoverTypeChecker(Program program)
+        public CivlTypeChecker(Program program)
         {
             this.errorCount = 0;
             this.checkingContext = new CheckingContext(null);
@@ -1105,60 +1104,60 @@ namespace Microsoft.Boogie
 
         private class PurityChecker : StandardVisitor
         {
-            private MoverTypeChecker moverTypeChecker;
+            private CivlTypeChecker civlTypeChecker;
 
-            public PurityChecker(MoverTypeChecker moverTypeChecker)
+            public PurityChecker(CivlTypeChecker civlTypeChecker)
             {
-                this.moverTypeChecker = moverTypeChecker;
+                this.civlTypeChecker = civlTypeChecker;
             }
             
             public override Cmd VisitCallCmd(CallCmd node)
             {
-                Procedure enclosingProc = moverTypeChecker.enclosingImpl.Proc;
-                if (!moverTypeChecker.procToAtomicProcedureInfo.ContainsKey(node.Proc))
+                Procedure enclosingProc = civlTypeChecker.enclosingImpl.Proc;
+                if (!civlTypeChecker.procToAtomicProcedureInfo.ContainsKey(node.Proc))
                 {
-                    moverTypeChecker.Error(node, "Atomic procedure can only call an atomic procedure");
+                    civlTypeChecker.Error(node, "Atomic procedure can only call an atomic procedure");
                     return base.VisitCallCmd(node);
                 }
-                var callerInfo = moverTypeChecker.procToAtomicProcedureInfo[enclosingProc];
-                var calleeInfo = moverTypeChecker.procToAtomicProcedureInfo[node.Proc];
+                var callerInfo = civlTypeChecker.procToAtomicProcedureInfo[enclosingProc];
+                var calleeInfo = civlTypeChecker.procToAtomicProcedureInfo[node.Proc];
                 if (calleeInfo.isPure)
                 {
                     // do nothing
                 }
                 else if (callerInfo.isPure)
                 {
-                    moverTypeChecker.Error(node, "Pure procedure can only call pure procedures");
+                    civlTypeChecker.Error(node, "Pure procedure can only call pure procedures");
                 }
                 else if (!callerInfo.layers.IsSubsetOf(calleeInfo.layers))
                 {
-                    moverTypeChecker.Error(node, "Caller layers must be subset of callee layers");
+                    civlTypeChecker.Error(node, "Caller layers must be subset of callee layers");
                 }
                 return base.VisitCallCmd(node);
             }
 
             public override Cmd VisitParCallCmd(ParCallCmd node)
             {
-                moverTypeChecker.Error(node, "Atomic procedures cannot make parallel calls");
+                civlTypeChecker.Error(node, "Atomic procedures cannot make parallel calls");
                 return node;
             }
 
             public override Expr VisitIdentifierExpr(IdentifierExpr node)
             {
-                Procedure enclosingProc = moverTypeChecker.enclosingImpl.Proc;
+                Procedure enclosingProc = civlTypeChecker.enclosingImpl.Proc;
                 if (node.Decl is GlobalVariable)
                 {
-                    if (moverTypeChecker.procToAtomicProcedureInfo[enclosingProc].isPure)
+                    if (civlTypeChecker.procToAtomicProcedureInfo[enclosingProc].isPure)
                     {
-                        moverTypeChecker.Error(node, "Pure procedure cannot access global variables");
+                        civlTypeChecker.Error(node, "Pure procedure cannot access global variables");
                     } 
-                    else if (!moverTypeChecker.globalVarToSharedVarInfo.ContainsKey(node.Decl))
+                    else if (!civlTypeChecker.globalVarToSharedVarInfo.ContainsKey(node.Decl))
                     {
-                        moverTypeChecker.Error(node, "Atomic procedure cannot access a global variable without layer numbers");
+                        civlTypeChecker.Error(node, "Atomic procedure cannot access a global variable without layer numbers");
                     } 
                     else 
                     {
-                        moverTypeChecker.sharedVarsAccessed.Add(node.Decl);
+                        civlTypeChecker.sharedVarsAccessed.Add(node.Decl);
                     }
                 }
                 return node;
diff --git a/Source/Concurrency/Concurrency.csproj b/Source/Concurrency/Concurrency.csproj
index f15ebca3..113019fd 100644
--- a/Source/Concurrency/Concurrency.csproj
+++ b/Source/Concurrency/Concurrency.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
   <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
   <PropertyGroup>
@@ -73,11 +73,11 @@
   <ItemGroup>
     <Compile Include="LinearSets.cs" />
     <Compile Include="MoverCheck.cs" />
-    <Compile Include="OwickiGries.cs" />
+    <Compile Include="CivlRefinement.cs" />
     <Compile Include="Program.cs" />
     <Compile Include="Properties\AssemblyInfo.cs" />
     <Compile Include="SimulationRelation.cs" />
-    <Compile Include="TypeCheck.cs" />
+    <Compile Include="CivlTypeChecker.cs" />
     <Compile Include="YieldTypeChecker.cs" />
   </ItemGroup>
   <ItemGroup>
@@ -112,4 +112,4 @@
   <Target Name="AfterBuild">
   </Target>
   -->
-</Project>
\ No newline at end of file
+</Project>
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 7c6d4ac4..732bcaa4 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -10,29 +10,29 @@ namespace Microsoft.Boogie
     public class MoverCheck
     {
         LinearTypeChecker linearTypeChecker;
-        MoverTypeChecker moverTypeChecker;
+        CivlTypeChecker civlTypeChecker;
         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)
+        private MoverCheck(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls)
         {
             this.linearTypeChecker = linearTypeChecker;
-            this.moverTypeChecker = moverTypeChecker;
+            this.civlTypeChecker = civlTypeChecker;
             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)
+        public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List<Declaration> decls)
         {
-            if (moverTypeChecker.procToActionInfo.Count == 0)
+            if (civlTypeChecker.procToActionInfo.Count == 0)
                 return;
 
-            List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern));
+            List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(civlTypeChecker.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));
+            List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(civlTypeChecker.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>>();
@@ -60,8 +60,8 @@ namespace Microsoft.Boogie
                 currPool = pools[currLayerNum];
             }
 
-            Program program = moverTypeChecker.program;
-            MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls);
+            Program program = civlTypeChecker.program;
+            MoverCheck moverChecking = new MoverCheck(linearTypeChecker, civlTypeChecker, decls);
             foreach (int layerNum in pools.Keys)
             {
                 foreach (AtomicActionInfo first in pools[layerNum])
@@ -537,7 +537,7 @@ namespace Microsoft.Boogie
             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)));
+            civlTypeChecker.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;
@@ -580,7 +580,7 @@ namespace Microsoft.Boogie
                 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)));
+            civlTypeChecker.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;
@@ -628,7 +628,7 @@ namespace Microsoft.Boogie
                 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)));
+            civlTypeChecker.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;
@@ -662,7 +662,7 @@ namespace Microsoft.Boogie
             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)));
+            civlTypeChecker.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;
diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs
index b56e1cf3..1be7cc07 100644
--- a/Source/Concurrency/Program.cs
+++ b/Source/Concurrency/Program.cs
@@ -7,20 +7,20 @@ namespace Microsoft.Boogie
 {
     public class Concurrency
     {
-        public static void Transform(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)
+        public static void Transform(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker)
         {
             List<Declaration> originalDecls = new List<Declaration>();
             Program program = linearTypeChecker.program;
             foreach (var decl in program.TopLevelDeclarations)
             {
                 Procedure proc = decl as Procedure;
-                if (proc != null && moverTypeChecker.procToActionInfo.ContainsKey(proc))
+                if (proc != null && civlTypeChecker.procToActionInfo.ContainsKey(proc))
                 {
                     originalDecls.Add(proc);
                     continue;
                 }
                 Implementation impl = decl as Implementation;
-                if (impl != null && moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc))
+                if (impl != null && civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc))
                 {
                     originalDecls.Add(impl);
                 }
@@ -29,12 +29,12 @@ namespace Microsoft.Boogie
             List<Declaration> decls = new List<Declaration>();
             if (!CommandLineOptions.Clo.TrustAtomicityTypes)
             {
-                MoverCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls);
+                MoverCheck.AddCheckers(linearTypeChecker, civlTypeChecker, decls);
             } 
-            OwickiGries.AddCheckers(linearTypeChecker, moverTypeChecker, decls);
+            CivlRefinement.AddCheckers(linearTypeChecker, civlTypeChecker, decls);
             foreach (Declaration decl in decls)
             {
-                decl.Attributes = OwickiGries.RemoveYieldsAttribute(decl.Attributes);
+                decl.Attributes = CivlRefinement.RemoveYieldsAttribute(decl.Attributes);
             }
             program.RemoveTopLevelDeclarations(x => originalDecls.Contains(x));
             program.AddTopLevelDeclarations(decls);
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index 5b479ed5..a69f066d 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -81,7 +81,7 @@ namespace Microsoft.Boogie
             Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();
             if (simulationRelation[initialState].Count == 0)
             {
-                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at layer {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum));
+                civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at layer {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum));
             }
         }
 
@@ -97,7 +97,7 @@ namespace Microsoft.Boogie
             Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();
             if (simulationRelation[initialState].Count == 0)
             {
-                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at layer {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum));
+                civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at layer {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum));
             }
         }
 
@@ -115,7 +115,7 @@ namespace Microsoft.Boogie
             Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();
             if (simulationRelation[initialState].Count == 0)
             {
-                moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at layer {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum));
+                civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at layer {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum));
             }
         }
 
@@ -124,7 +124,7 @@ namespace Microsoft.Boogie
             foreach (Cmd cmd in block.Cmds)
             {
                 AssertCmd assertCmd = cmd as AssertCmd;
-                if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && moverTypeChecker.absyToLayerNums[assertCmd].Contains(currLayerNum))
+                if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && civlTypeChecker.absyToLayerNums[assertCmd].Contains(currLayerNum))
                 {
                     return true;
                 }
@@ -132,25 +132,25 @@ namespace Microsoft.Boogie
             return false;
         }
         
-        public static void PerformYieldSafeCheck(MoverTypeChecker moverTypeChecker)
+        public static void PerformYieldSafeCheck(CivlTypeChecker civlTypeChecker)
         {
-            foreach (var impl in moverTypeChecker.program.Implementations)
+            foreach (var impl in civlTypeChecker.program.Implementations)
             {
-                if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue;
+                if (!civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue;
                 impl.PruneUnreachableBlocks();
                 Graph<Block> implGraph = Program.GraphFromImpl(impl);
                 implGraph.ComputeLoops();
-                int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum;
-                foreach (int layerNum in moverTypeChecker.AllImplementedLayerNums)
+                int specLayerNum = civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum;
+                foreach (int layerNum in civlTypeChecker.AllImplementedLayerNums)
                 {
                     if (layerNum > specLayerNum) continue;
-                    YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, layerNum, implGraph.Headers);
+                    YieldTypeChecker executor = new YieldTypeChecker(civlTypeChecker, impl, layerNum, implGraph.Headers);
                 }
             }
         }
 
         int stateCounter;
-        MoverTypeChecker moverTypeChecker;
+        CivlTypeChecker civlTypeChecker;
         Implementation impl;
         int currLayerNum;
         Dictionary<Absy, int> absyToNode;
@@ -160,9 +160,9 @@ namespace Microsoft.Boogie
         Dictionary<Tuple<int, int>, int> edgeLabels;
         IEnumerable<Block> loopHeaders;
 
-        private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currLayerNum, IEnumerable<Block> loopHeaders)
+        private YieldTypeChecker(CivlTypeChecker civlTypeChecker, Implementation impl, int currLayerNum, IEnumerable<Block> loopHeaders)
         {
-            this.moverTypeChecker = moverTypeChecker;
+            this.civlTypeChecker = civlTypeChecker;
             this.impl = impl;
             this.currLayerNum = currLayerNum;
             this.loopHeaders = loopHeaders;
@@ -226,20 +226,20 @@ namespace Microsoft.Boogie
                         CallCmd callCmd = cmd as CallCmd;
                         if (callCmd.IsAsync)
                         {
-                            ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
+                            ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc];
                             if (currLayerNum <= actionInfo.createdAtLayerNum)
                                 edgeLabels[edge] = 'L';
                             else
                                 edgeLabels[edge] = 'B';
                         }
-                        else if (!moverTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc))
+                        else if (!civlTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc))
                         {
                             edgeLabels[edge] = 'P';
                         }
                         else
                         {
                             MoverType moverType;
-                            ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
+                            ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc];
                             if (actionInfo.createdAtLayerNum >= currLayerNum)
                             {
                                 moverType = MoverType.Top;
@@ -280,7 +280,7 @@ namespace Microsoft.Boogie
                         bool isLeftMover = true;
                         foreach (CallCmd callCmd in parCallCmd.CallCmds)
                         {
-                            if (moverTypeChecker.procToActionInfo[callCmd.Proc].createdAtLayerNum >= currLayerNum)
+                            if (civlTypeChecker.procToActionInfo[callCmd.Proc].createdAtLayerNum >= currLayerNum)
                             {
                                 isYield = true;
                             }
@@ -294,7 +294,7 @@ namespace Microsoft.Boogie
                             int numAtomicActions = 0;
                             foreach (CallCmd callCmd in parCallCmd.CallCmds)
                             {
-                                ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
+                                ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc];
                                 isRightMover = isRightMover && actionInfo.IsRightMover;
                                 isLeftMover = isLeftMover && actionInfo.IsLeftMover;
                                 if (actionInfo is AtomicActionInfo)
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 353ac94f..cf44a77f 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -482,8 +482,8 @@ namespace Microsoft.Boogie
         }
 
         LinearTypeChecker linearTypeChecker;
-        MoverTypeChecker moverTypeChecker;
-        PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypeChecker, out moverTypeChecker);
+        CivlTypeChecker civlTypeChecker;
+        PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypeChecker, out civlTypeChecker);
         if (oc != PipelineOutcome.ResolvedAndTypeChecked)
           return;
 
@@ -500,7 +500,7 @@ namespace Microsoft.Boogie
 
         if (CommandLineOptions.Clo.StratifiedInlining == 0)
         {
-          Concurrency.Transform(linearTypeChecker, moverTypeChecker);
+          Concurrency.Transform(linearTypeChecker, civlTypeChecker);
           (new LinearEraser()).VisitProgram(program);
           if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null)
           {
@@ -692,13 +692,13 @@ namespace Microsoft.Boogie
     ///  - TypeCheckingError if a type checking error occurred
     ///  - ResolvedAndTypeChecked if both resolution and type checking succeeded
     /// </summary>
-    public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypeChecker linearTypeChecker, out MoverTypeChecker moverTypeChecker)
+    public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypeChecker linearTypeChecker, out CivlTypeChecker civlTypeChecker)
     {
       Contract.Requires(program != null);
       Contract.Requires(bplFileName != null);
 
       linearTypeChecker = null;
-      moverTypeChecker = null;
+      civlTypeChecker = null;
 
       // ---------- Resolve ------------------------------------------------------------
 
@@ -735,11 +735,11 @@ namespace Microsoft.Boogie
 
       CollectModSets(program);
 
-      moverTypeChecker = new MoverTypeChecker(program);
-      moverTypeChecker.TypeCheck();
-      if (moverTypeChecker.errorCount != 0)
+      civlTypeChecker = new CivlTypeChecker(program);
+      civlTypeChecker.TypeCheck();
+      if (civlTypeChecker.errorCount != 0)
       {
-          Console.WriteLine("{0} type checking errors detected in {1}", moverTypeChecker.errorCount, GetFileNameForConsole(bplFileName));
+          Console.WriteLine("{0} type checking errors detected in {1}", civlTypeChecker.errorCount, GetFileNameForConsole(bplFileName));
           return PipelineOutcome.TypeCheckingError;
       }
 
@@ -1358,8 +1358,8 @@ namespace Microsoft.Boogie
       Program p = ParseBoogieProgram(new List<string> { filename }, false);
       System.Diagnostics.Debug.Assert(p != null);
       LinearTypeChecker linearTypeChecker;
-      MoverTypeChecker moverTypeChecker;
-      PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypeChecker, out moverTypeChecker);
+      CivlTypeChecker civlTypeChecker;
+      PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypeChecker, out civlTypeChecker);
       System.Diagnostics.Debug.Assert(oc == PipelineOutcome.ResolvedAndTypeChecked);
       return p;
     }