fixed a problem with the nonblocking check

2 files changed, 11 insertions, 8 deletions

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

                                     moverChecking.CreateGatePreservationChecker(program, first, second);

                                     moverChecking.CreateFailurePreservationChecker(program, second, first);

-                                    moverChecking.CreateNonBlockingChecker(program, first);

                                 }

                             }

                         }

                     }

                 }

             }

+            foreach (ActionInfo action in moverTypeChecker.procToActionInfo.Values)

+            {

+                if (action.IsLeftMover && action.hasAssumeCmd)

+                {

+                    moverChecking.CreateNonBlockingChecker(program, action);

+                }

+            }

         }

 

         public sealed class MyDuplicator : Duplicator

@@ -562,7 +568,7 @@ namespace Microsoft.Boogie
 

         private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)

         {

-            if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0 && second.isNonBlocking)

+            if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)

                 return;

 

             Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second); 

@@ -607,9 +613,6 @@ namespace Microsoft.Boogie
 

         private void CreateNonBlockingChecker(Program program, ActionInfo second)

         {

-            if (second.isNonBlocking)

-                return;

-

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

             inputs.AddRange(second.thisInParams);

 

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index a3e35a70..ce29a700 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -34,7 +34,7 @@ namespace Microsoft.Boogie
         public HashSet<Variable> usedGlobalVars;

         public HashSet<Variable> modifiedGlobalVars;

         public HashSet<Variable> gateUsedGlobalVars;

-        public bool isNonBlocking;

+        public bool hasAssumeCmd;

 

         public bool CommutesWith(ActionInfo actionInfo)

         {

@@ -68,11 +68,11 @@ namespace Microsoft.Boogie
             this.thatGate = new List<AssertCmd>();

             this.thatInParams = new List<Variable>();

             this.thatOutParams = new List<Variable>();

-            this.isNonBlocking = true;

+            this.hasAssumeCmd = false;

             

             foreach (Block block in codeExpr.Blocks)

             {

-                block.Cmds.ForEach(x => this.isNonBlocking = this.isNonBlocking && !(x is AssumeCmd));

+                block.Cmds.ForEach(x => this.hasAssumeCmd = this.hasAssumeCmd || x is AssumeCmd);

             }

 

             var cmds = thisAction.Blocks[0].Cmds;