added the framing for the refinement check

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);

                 }