relaxed the check for created and hidden layers for skip actions

1 files changed, 14 insertions, 6 deletions

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 793012e6..542d3515 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -388,11 +388,6 @@ namespace Microsoft.Boogie
                     Error(proc, "Incorrect number of layers");
                     continue;
                 }
-                if (availableUptoLayerNum <= createdAtLayerNum)
-                {
-                    Error(proc, "Creation layer number must be less than the available upto layer number");
-                    continue;
-                }
                 foreach (Ensures e in proc.Ensures)
                 {
                     MoverType moverType = GetMoverType(e);
@@ -408,6 +403,11 @@ namespace Microsoft.Boogie
                         Error(proc, "A procedure can have at most one atomic action");
                         continue;
                     }
+                    if (availableUptoLayerNum <= createdAtLayerNum)
+                    {
+                        Error(proc, "Creation layer number must be less than the available upto layer number");
+                        continue;
+                    }
 
                     minLayerNum = int.MaxValue;
                     maxLayerNum = -1;
@@ -432,7 +432,15 @@ namespace Microsoft.Boogie
                 if (errorCount > 0) continue;
                 if (!procToActionInfo.ContainsKey(proc))
                 {
-                    procToActionInfo[proc] = new ActionInfo(proc, createdAtLayerNum, availableUptoLayerNum);
+                    if (availableUptoLayerNum < createdAtLayerNum)
+                    {
+                        Error(proc, "Creation layer number must be no more than the available upto layer number");
+                        continue;
+                    }
+                    else
+                    {
+                        procToActionInfo[proc] = new ActionInfo(proc, createdAtLayerNum, availableUptoLayerNum);
+                    }
                 }
             }
             if (errorCount > 0) return;