summaryrefslogtreecommitdiff
path: root/Source/Concurrency/OwickiGries.cs
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-12-17 10:26:33 -0800
committerGravatar qadeer <unknown>2014-12-17 10:26:33 -0800
commit75b7f29830013051c14990d515d4948cdf917148 (patch)
treecfccc73d683c6fbab2a2a1433be7c79c8d13b1e7 /Source/Concurrency/OwickiGries.cs
parent609d414cf5e707673bf7e6fd8ed4aee9be70cdff (diff)
some refactoring to separate the concept of shared variables under refinement checking with all global variables
Diffstat (limited to 'Source/Concurrency/OwickiGries.cs')
-rw-r--r--Source/Concurrency/OwickiGries.cs13
1 files changed, 7 insertions, 6 deletions
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index e485e1bc..8865b69e 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -198,7 +198,7 @@ namespace Microsoft.Boogie
}
procMap[node] = proc;
proc.Modifies = new List<IdentifierExpr>();
- moverTypeChecker.program.GlobalVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));
+ moverTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));
}
return procMap[node];
}
@@ -279,7 +279,7 @@ namespace Microsoft.Boogie
this.yieldingProcs = duplicator.yieldingProcs;
Program program = linearTypeChecker.program;
globalMods = new List<IdentifierExpr>();
- foreach (Variable g in program.GlobalVariables)
+ foreach (Variable g in moverTypeChecker.SharedVariables)
{
globalMods.Add(Expr.Ident(g));
}
@@ -738,15 +738,16 @@ namespace Microsoft.Boogie
foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);
}
Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);
- frame = new HashSet<Variable>(program.GlobalVariables);
+ frame = new HashSet<Variable>(moverTypeChecker.SharedVariables);
HashSet<Variable> introducedVars = new HashSet<Variable>();
- foreach (Variable v in program.GlobalVariables)
+ foreach (Variable v in moverTypeChecker.SharedVariables)
{
- if (moverTypeChecker.hideLayerNums[v] <= actionInfo.createdAtLayerNum || moverTypeChecker.introduceLayerNums[v] > actionInfo.createdAtLayerNum)
+ if (moverTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum ||
+ moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum)
{
frame.Remove(v);
}
- if (moverTypeChecker.introduceLayerNums[v] == actionInfo.createdAtLayerNum)
+ if (moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum == actionInfo.createdAtLayerNum)
{
introducedVars.Add(v);
}