fixed a problem with the nonblocking check

1 files changed, 8 insertions, 5 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);