diff options
| author |  qadeer <unknown> | 2014-04-16 17:55:55 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2014-04-16 17:55:55 -0700 |
| commit | 934a8491d4526cebfc30d8527cf49f3dc8b5e908 (patch) | |
| tree | 06faacb616ed2f1b5b77eb070ffd6b1acdbc4624 /Source/Concurrency/OwickiGries.cs | |
| parent | 93613c6cbff215b8e1898ee7d7503c5afa10312e (diff) | |
added the framing for the refinement check
Diffstat (limited to 'Source/Concurrency/OwickiGries.cs')
| -rw-r--r-- | Source/Concurrency/OwickiGries.cs | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index 9de83635..3c5c53c8 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -781,7 +781,15 @@ namespace Microsoft.Boogie foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);
}
Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);
- Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, actionInfo)).TransitionRelationCompute();
+ HashSet<Variable> frame = new HashSet<Variable>(program.GlobalVariables());
+ foreach (Variable v in moverTypeChecker.qedGlobalVariables.Keys)
+ {
+ if (moverTypeChecker.qedGlobalVariables[v] <= actionInfo.phaseNum)
+ {
+ frame.Remove(v);
+ }
+ }
+ Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, actionInfo, frame)).TransitionRelationCompute();
beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr);
Expr alphaExpr = Expr.True;
foreach (AssertCmd assertCmd in actionInfo.thisGate)
|