EventBag, EventChannel, EventQueue added more test cases + minor fixes

p-org · Jan 20, 2025 · 08003e3 · 08003e3
1 parent 632ba13
commit 08003e3
Show file tree

Hide file tree

Showing 12 changed files with 249 additions and 90 deletions.
diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventBag.cs
@@ -194,9 +194,7 @@ public EnqueueStatus Enqueue(Event e, EventInfo info)
                 Bag.Remove(availableEvent);
                 deferredEvents.Add(availableEvent);
                 availableEvent = default;
-
             }
-
         }
 
         Bag.AddRange(deferredEvents);

diff --git a/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs b/Src/PChecker/CheckerCore/Runtime/StateMachines/EventQueues/EventChannel.cs
@@ -183,6 +183,10 @@ public EnqueueStatus Enqueue(Event e, EventInfo info)
                 if (Map.TryGetValue(stateMachine, out var eventList) && eventList.Count > 0)
                 {
                     nextAvailableEvent = TryDequeueEvent(stateMachine, checkOnly);
+                }
+
+                if (nextAvailableEvent != default)
+                {
                     SenderMachineNames.AddRange(temp);
                     break;
                 }

diff --git a/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerNameManager.cs b/Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerNameManager.cs
@@ -17,7 +17,8 @@ internal class PCheckerNameManager : NameManagerBase
             "case", "default", "lock", "try", "throw", "catch", "finally", "goto", "break", "continue", "return", "public", "private", "internal",
             "protected", "static", "readonly", "sealed", "const", "fixed", "stackalloc", "volatile", "new", "override", "abstract", "virtual",
             "event", "extern", "ref", "out", "in", "is", "as", "params", "__arglist", "__makeref", "__reftype", "__refvalue", "this", "base",
-            "namespace", "using", "class", "struct", "interface", "enum", "delegate", "checked", "unchecked", "unsafe", "operator", "implicit", "explicit"
+            "namespace", "using", "class", "struct", "interface", "enum", "delegate", "checked", "unchecked", "unsafe", "operator", "implicit", "explicit",
+            "eventbag", "eventqueue", "eventchannel"
         };
 
         public PCheckerNameManager(string namePrefix) : base(namePrefix)

diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventChannel/EventChannel.p b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventChannel/EventChannel.p
@@ -12,14 +12,9 @@ eventchannel machine Main {
 		entry {
 			count1 = 0;
 			count2 = 10;
-			m1 = new M1((sender= this, num= count1));
-			m2 = new M2((sender= this, num= count2));
+			m1 = new M1(this);
+			m2 = new M2(this);
 			i = 0;
-			while (i < 10)
-			{
-				print format("Waiting {0}", i);
-				i = i + 1;
-			}
 		}
 		on e do (p: int) {
 			assert p == count1;
@@ -36,13 +31,11 @@ machine M1 {
 	var i: int;
 	var j: int;
 	start state Init {
-		entry (payload: (sender: Main, num: int)) {
-			print format("sender: {0}", payload.sender);
-			i = payload.num;
-			j = i + 10;
-			while (i < j)
+		entry (payload: Main) {
+			i = 0;
+			while (i < 10)
 			{
-				send payload.sender, e, i;
+				send payload, e, i;
 				i = i + 1;
 			}
 		}
@@ -53,13 +46,11 @@ machine M2 {
 	var i: int;
 	var j: int;
 	start state Init {
-		entry (payload: (sender: Main, num: int)) {
-			print format("sender: {0}", payload.sender);
-			i = payload.num;
-			j = i + 10;
-			while (i < j)
+		entry (payload: Main) {
+			i = 10;
+			while (i < 20)
 			{
-				send payload.sender, e2, i;
+				send payload, e2, i;
 				i = i + 1;
 			}
 		}

diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventQueue/EventQueue.p b/Tst/RegressionTests/Feature1SMLevelDecls/Correct/EventQueue/EventQueue.p
@@ -0,0 +1,50 @@
+event A: int;
+event B: M1;
+event C: int;
+event unblock;
+
+machine Main {
+	var m1: M1;
+	var m2: M2;
+	start state Init {
+		entry {
+      m1 = new M1();
+      m2 = new M2();
+			send m1, A, 1;
+      send m2, B, m1;
+		}
+	}
+}
+
+eventqueue machine M1 {
+	start state Init {
+    on unblock do {
+      goto dequeueEvents;
+    }
+    defer A;
+    defer C;
+  }
+  state dequeueEvents {
+    on A do {
+			goto receivedA;
+    }
+    on C do {
+      assert false, "Event C was received before A";
+    }
+	}
+  state receivedA {
+    on C do {
+      assert true;
+    }
+  }
+}
+
+machine M2 {
+	start state Init {
+		on B do (payload: M1) {
+      send payload, C, 1;
+      send payload, unblock;
+    }
+	}
+}
+
diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EvengBag/EventBag.p b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EvengBag/EventBag.p
@@ -7,14 +7,9 @@ eventbag machine Main {
 	start state Init {
 
 		entry {
-			m1 = new M1((sender= this, num= 0));
+			m1 = new M1(this);
 			i = 0;
 			prev = 0;
-			while (i < 100)
-			{
-				print format("Waiting for events to pile up {0}", i);
-				i = i + 1;
-			}
 		}
 		on e do (p: int) {
 			assert p >= prev;
@@ -27,13 +22,11 @@ machine M1 {
 	var i: int;
 	var j: int;
 	start state Init {
-		entry (payload: (sender: Main, num: int)) {
-			print format("sender: {0}", payload.sender);
-			i = payload.num;
-			j = i + 10;
-			while (i < j)
+		entry (payload: Main) {
+			i = 0;
+			while (i < 10)
 			{
-				send payload.sender, e, i;
+				send payload, e, i;
 				i = i + 1;
 			}
 		}

diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventBag2/EventBag2.p b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventBag2/EventBag2.p
@@ -0,0 +1,60 @@
+event A: Main;
+event B: M1;
+event C: int;
+event unblock;
+event iter;
+
+machine Main {
+	var m1: M1;
+	var m2: M2;
+  var i: int;
+	start state Init {
+		entry {
+      m1 = new M1();
+      m2 = new M2();
+			send m1, A, this;
+      send m2, B, m1;
+      i = 0;
+		}
+    // Repeat until M1 receives event C before A
+    on iter do {
+      send m1, A, this;
+      send m2, B, m1;
+    }
+	}
+}
+
+eventbag machine M1 {
+  var m: Main;
+	start state Init {
+    on unblock do {
+      goto dequeueEvents;
+    }
+    defer A;
+    defer C;
+  }
+  state dequeueEvents {
+    on A do (payload: Main){
+      m = payload;
+			goto receivedA;
+    }
+    on C do {
+      assert false, "Event C was received before A";
+    }
+	}
+  state receivedA {
+    on C do {
+      send m, iter;
+      goto Init;
+    }
+  }
+}
+
+machine M2 {
+	start state Init {
+		on B do (payload: M1) {
+      send payload, C, 1;
+      send payload, unblock;
+    }
+	}
+}
diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventChannel/EventChannel.p b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventChannel/EventChannel.p
@@ -4,22 +4,15 @@ event e2: int;
 eventchannel machine Main {
 	var m1: M1;
 	var m2: M2;
-	var i: int;
 	var count1: int;
 	var count2: int;
 	start state Init {
 
 		entry {
 			count1 = 0;
 			count2 = 10;
-			m1 = new M1((sender= this, num= count1));
-			m2 = new M2((sender= this, num= count2));
-			i = 0;
-			while (i < 10)
-			{
-				print format("Waiting {0}", i);
-				i = i + 1;
-			}
+			m1 = new M1(this);
+			m2 = new M2(this);
 		}
 		on e do (p: int) {
 			assert p != count1;
@@ -36,13 +29,11 @@ machine M1 {
 	var i: int;
 	var j: int;
 	start state Init {
-		entry (payload: (sender: Main, num: int)) {
-			print format("sender: {0}", payload.sender);
-			i = payload.num;
-			j = i + 10;
-			while (i < j)
+		entry (payload: Main) {
+			i = 0;
+			while (i < 10)
 			{
-				send payload.sender, e, i;
+				send payload, e, i;
 				i = i + 1;
 			}
 		}
@@ -53,13 +44,11 @@ machine M2 {
 	var i: int;
 	var j: int;
 	start state Init {
-		entry (payload: (sender: Main, num: int)) {
-			print format("sender: {0}", payload.sender);
-			i = payload.num;
-			j = i + 10;
-			while (i < j)
+		entry (payload: Main) {
+			i = 10;
+			while (i < 20)
 			{
-				send payload.sender, e2, i;
+				send payload, e2, i;
 				i = i + 1;
 			}
 		}

diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventChannel2/EventChannel2.p b/Tst/RegressionTests/Feature1SMLevelDecls/DynamicError/EventChannel2/EventChannel2.p
@@ -0,0 +1,60 @@
+event A: Main;
+event B: M1;
+event C: int;
+event unblock;
+event iter;
+
+machine Main {
+	var m1: M1;
+	var m2: M2;
+  var i: int;
+	start state Init {
+		entry {
+      m1 = new M1();
+      m2 = new M2();
+			send m1, A, this;
+      send m2, B, m1;
+      i = 0;
+		}
+    // Repeat until M1 receives event C before A
+    on iter do {
+      send m1, A, this;
+      send m2, B, m1;
+    }
+	}
+}
+
+eventchannel machine M1 {
+  var m: Main;
+	start state Init {
+    on unblock do {
+      goto dequeueEvents;
+    }
+    defer A;
+    defer C;
+  }
+  state dequeueEvents {
+    on A do (payload: Main){
+      m = payload;
+			goto receivedA;
+    }
+    on C do {
+      assert false, "Event C was received before A";
+    }
+	}
+  state receivedA {
+    on C do {
+      send m, iter;
+      goto Init;
+    }
+  }
+}
+
+machine M2 {
+	start state Init {
+		on B do (payload: M1) {
+      send payload, C, 1;
+      send payload, unblock;
+    }
+	}
+}
diff --git a/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EvengBag/EventBag.p b/Tst/RegressionTests/Feature1SMLevelDecls/StaticError/EvengBag/EventBag.p
@@ -7,14 +7,9 @@ eventBag machine Main {
 	start state Init {
 
 		entry {
-			m1 = new M1((sender= this, num= 0));
+			m1 = new M1(this);
 			i = 0;
 			prev = 0;
-			while (i < 100)
-			{
-				print format("Waiting for events to pile up {0}", i);
-				i = i + 1;
-			}
 		}
 		on e do (p: int) {
 			assert p >= prev;
@@ -27,13 +22,11 @@ machine M1 {
 	var i: int;
 	var j: int;
 	start state Init {
-		entry (payload: (sender: Main, num: int)) {
-			print format("sender: {0}", payload.sender);
-			i = payload.num;
-			j = i + 10;
-			while (i < j)
+		entry (payload: Main) {
+			i = 0;
+			while (i < 10)
 			{
-				send payload.sender, e, i;
+				send payload, e, i;
 				i = i + 1;
 			}
 		}