From 80e6c54ccfeac0a2ae07c18f3c8f21970e483185 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Mon, 28 Sep 2015 09:42:55 -0700 Subject: cleaned up some names --- Source/Concurrency/MoverCheck.cs | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'Source/Concurrency/MoverCheck.cs') 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 decls; HashSet> commutativityCheckerCache; HashSet> gatePreservationCheckerCache; HashSet> failurePreservationCheckerCache; - private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List decls) + private MoverCheck(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List decls) { this.linearTypeChecker = linearTypeChecker; - this.moverTypeChecker = moverTypeChecker; + this.civlTypeChecker = civlTypeChecker; this.decls = decls; this.commutativityCheckerCache = new HashSet>(); this.gatePreservationCheckerCache = new HashSet>(); this.failurePreservationCheckerCache = new HashSet>(); } - public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List decls) + public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List decls) { - if (moverTypeChecker.procToActionInfo.Count == 0) + if (civlTypeChecker.procToActionInfo.Count == 0) return; - List sortedByCreatedLayerNum = new List(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); + List sortedByCreatedLayerNum = new List(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 sortedByAvailableUptoLayerNum = new List(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); + List sortedByAvailableUptoLayerNum = new List(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> pools = new Dictionary>(); @@ -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 globalVars = new List(); - 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(), inputs, outputs, requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), 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 globalVars = new List(); - 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(), inputs, outputs, requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), 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 globalVars = new List(); - 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(), inputs, outputs, requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), inputs, outputs, locals, secondBlocks); impl.Proc = proc; @@ -662,7 +662,7 @@ namespace Microsoft.Boogie blocks.Add(new Block(Token.NoToken, "L", new List(), new ReturnCmd(Token.NoToken))); string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name); List globalVars = new List(); - 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(), inputs, new List(), requires, globalVars, ensures); Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), inputs, new List(), new List(), blocks); impl.Proc = proc; -- cgit v1.2.3