diff options
Diffstat (limited to 'Source/Concurrency/MoverCheck.cs')
| -rw-r--r-- | Source/Concurrency/MoverCheck.cs | 19 |
1 files changed, 17 insertions, 2 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);
}
|