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 | |
| parent | 93613c6cbff215b8e1898ee7d7503c5afa10312e (diff) | |
added the framing for the refinement check
Diffstat (limited to 'Source/Concurrency')
| -rw-r--r-- | Source/Concurrency/MoverCheck.cs | 19 | ||||
| -rw-r--r-- | Source/Concurrency/OwickiGries.cs | 10 | ||||
| -rw-r--r-- | Source/Concurrency/TypeCheck.cs | 2 |
3 files changed, 27 insertions, 4 deletions
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index db2bfb23..4957c829 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -141,13 +141,28 @@ namespace Microsoft.Boogie private ActionInfo second; // corresponds to this*
private Stack<Cmd> cmdStack;
private List<PathInfo> paths;
+ private HashSet<Variable> frame;
- public TransitionRelationComputation(Program program, ActionInfo second) : this(program, null, second)
+ public TransitionRelationComputation(Program program, ActionInfo second, HashSet<Variable> frame)
{
+ this.frame = frame;
+ TransitionRelationComputationHelper(program, null, second);
+ }
+
+ public TransitionRelationComputation(Program program, ActionInfo second)
+ {
+ this.frame = new HashSet<Variable>(program.GlobalVariables());
+ TransitionRelationComputationHelper(program, null, second);
}
public TransitionRelationComputation(Program program, ActionInfo first, ActionInfo second)
{
+ this.frame = new HashSet<Variable>(program.GlobalVariables());
+ TransitionRelationComputationHelper(program, first, second);
+ }
+
+ private void TransitionRelationComputationHelper(Program program, ActionInfo first, ActionInfo second)
+ {
this.program = program;
this.first = first;
this.second = second;
@@ -213,7 +228,7 @@ namespace Microsoft.Boogie {
HashSet<Variable> existsVars = new HashSet<Variable>();
Dictionary<Variable, Expr> varToExpr = new Dictionary<Variable, Expr>();
- foreach (Variable v in program.GlobalVariables())
+ foreach (Variable v in frame)
{
varToExpr[v] = Expr.Ident(v);
}
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)
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index a8266e79..5a15c707 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -192,7 +192,7 @@ namespace Microsoft.Boogie CheckingContext checkingContext;
public int errorCount;
- Dictionary<Variable, int> qedGlobalVariables;
+ public Dictionary<Variable, int> qedGlobalVariables;
Procedure enclosingProc;
public Dictionary<Procedure, ActionInfo> procToActionInfo;
public Program program;
|