added nonblocking checker for left movers

1 files changed, 43 insertions, 5 deletions

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index f30213a0..fc300444 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -86,6 +86,7 @@ namespace Microsoft.Boogie
                                     moverChecking.CreateCommutativityChecker(program, second, first);

                                     moverChecking.CreateGatePreservationChecker(program, first, second);

                                     moverChecking.CreateFailurePreservationChecker(program, second, first);

+                                    moverChecking.CreateNonBlockingChecker(program, first);

                                 }

                             }

                         }

@@ -446,12 +447,15 @@ namespace Microsoft.Boogie
                 if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

                 domainNameToScope[domainName].Add(v);

             }

-            foreach (Variable v in first.thatInParams)

+            if (first != null)

             {

-                var domainName = linearTypeChecker.FindDomainName(v);

-                if (domainName == null) continue;

-                if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

-                domainNameToScope[domainName].Add(v);

+                foreach (Variable v in first.thatInParams)

+                {

+                    var domainName = linearTypeChecker.FindDomainName(v);

+                    if (domainName == null) continue;

+                    if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

+                    domainNameToScope[domainName].Add(v);

+                }

             }

             foreach (Variable v in second.thisInParams)

             {

@@ -600,5 +604,39 @@ namespace Microsoft.Boogie
             this.decls.Add(impl);

             this.decls.Add(proc);

         }

+

+        private void CreateNonBlockingChecker(Program program, ActionInfo second)

+        {

+            if (second.isNonBlocking)

+                return;

+

+            List<Variable> inputs = new List<Variable>();

+            inputs.AddRange(second.thisInParams);

+

+            Expr failureExpr = Expr.True;

+            List<Requires> requires = DisjointnessRequires(program, null, second);

+            requires.Add(new Requires(false, failureExpr));

+            foreach (AssertCmd assertCmd in second.thisGate)

+            {

+                requires.Add(new Requires(false, assertCmd.Expr));

+            }

+

+            Expr ensuresExpr = (new TransitionRelationComputation(program, second)).LeftMoverCompute(failureExpr);

+            List<Ensures> ensures = new List<Ensures>();

+            Ensures ensureCheck = new Ensures(false, ensuresExpr);

+            ensureCheck.ErrorData = string.Format("{0} is blocking", second.proc.Name);

+            ensures.Add(ensureCheck);

+

+            List<Block> blocks = new List<Block>();

+            blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));

+            string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name);

+            List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

+            program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(x)));

+            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, globalVars, ensures);

+            Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);

+            impl.Proc = proc;

+            this.decls.Add(impl);

+            this.decls.Add(proc);

+        }

     }

 }
\ No newline at end of file