Adding test cases for 'raise' and 'goto' with payload (#767)

Co-authored-by: Christine Zhou <[email protected]>

Src/PChecker/CheckerCore/PRuntime/PMachine.cs

@@ -14,7 +14,6 @@ namespace PChecker.PRuntime
     public class PMachine : StateMachine
     {
         public List<string> creates = new List<string>();
-        protected IPrtValue gotoPayload;
         private string interfaceName;
         public List<string> receives = new List<string>();
         public PMachineValue self;
@@ -104,13 +103,6 @@ public Task<Event> TryReceiveEvent(params Type[] events)
             return ReceiveEventAsync(events);
         }
 
-        public void TryGotoState<T>(IPrtValue payload = null) where T : State
-        {
-            gotoPayload = payload;
-            RaiseGotoStateEvent<T>();
-            throw new PNonStandardReturnException { ReturnKind = NonStandardReturn.Goto };
-        }
-
         public int TryRandomInt(int maxValue)
         {
             return RandomInteger(maxValue);

Src/PChecker/CheckerCore/StateMachines/StateMachine.cs

@@ -20,6 +20,8 @@
 using PChecker.StateMachines.StateTransitions;
 using PChecker.Exceptions;
 using PChecker.IO.Debugging;
+using PChecker.PRuntime.Exceptions;
+using PChecker.PRuntime.Values;
 using PChecker.SystematicTesting;
 using EventInfo = PChecker.StateMachines.Events.EventInfo;
 
@@ -139,6 +141,9 @@ public abstract class StateMachine
         /// The installed runtime json logger.
         /// </summary>
         protected JsonWriter JsonLogger => Runtime.JsonLogger;
+
+        protected IPrtValue gotoPayload;
+
 
         /// <summary>
         /// Initializes a new instance of the <see cref="StateMachine"/> class.
@@ -841,9 +846,12 @@ public void RaiseEvent(Event e)
         /// An Assert is raised if you accidentally try and do two of these operations in a single action.
         /// </remarks>
         /// <typeparam name="S">Type of the state.</typeparam>
-        protected void RaiseGotoStateEvent<S>()
-            where S : State =>
+        public void RaiseGotoStateEvent<S>(IPrtValue payload = null) where S : State
+        {
+            gotoPayload = payload;
             RaiseGotoStateEvent(typeof(S));
+            throw new PNonStandardReturnException { ReturnKind = NonStandardReturn.Goto };
+        }
 
         /// <summary>
         /// Raise a special event that performs a goto state operation at the end of the current action.

Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs

@@ -911,7 +911,7 @@ private void WriteStmt(CompilationContext context, StringWriter output, Function
 
                 case GotoStmt gotoStmt:
                     //last statement
-                    context.Write(output, $"currentMachine.TryGotoState<{context.Names.GetNameForDecl(gotoStmt.State)}>(");
+                    context.Write(output, $"currentMachine.RaiseGotoStateEvent<{context.Names.GetNameForDecl(gotoStmt.State)}>(");
                     if (gotoStmt.Payload != null)
                     {
                         WriteExpr(context, output, gotoStmt.Payload);
@@ -994,11 +994,11 @@ private void WriteStmt(CompilationContext context, StringWriter output, Function
                         WriteExpr(context, output, raiseStmt.Event);
                         context.Write(output, $".Payload = ");
                         WriteExpr(context, output, raiseStmt.Payload.First());
-                        context.Write(output, ";");
+                        context.WriteLine(output, ";");
                     }
                     context.Write(output, "currentMachine.RaiseEvent(");
                     WriteExpr(context, output, raiseStmt.Event);
-                    context.Write(output, ");");
+                    context.WriteLine(output, ");");
                     context.WriteLine(output, "return;");
                     break;
 

Tst/RegressionTests/Feature2Stmts/Correct/goto2/goto2.p

@@ -0,0 +1,16 @@
+/********************
+ * This example tests goto with payload on state machine
+ * ******************/
+
+ machine Main {
+  start state Init {
+    entry {
+      goto S, 1000;
+    }
+  }
+  state S {
+    entry (payload: int) { 
+      assert (payload == 1000), format ("Expected payload to be 1000, actual payload is {0}", payload);
+    }
+  }
+}

Tst/RegressionTests/Feature2Stmts/Correct/goto3/goto3.p

@@ -0,0 +1,29 @@
+/********************
+ * This example tests goto with payload on monitor
+ * ******************/
+
+ event E1;
+
+ machine Main {
+  start state Init {
+    entry {
+      send this, E1;
+    }
+    on E1 do {
+    }
+  }
+}
+ spec M observes E1 {
+  start state Init {
+    on E1 do {
+      goto S, 1000;
+    }
+  }
+  state S {
+    entry (payload: int) { 
+      assert (payload == 1000), format ("Expected payload to be 1000, actual payload is {0}", payload);
+    }
+  }
+}
+
+test DefaultImpl [main=Main]: assert M in { Main };

Tst/RegressionTests/Feature2Stmts/Correct/raise1/raise1.p

@@ -0,0 +1,16 @@
+/********************
+ * This example tests raise with payload on state machine
+ * ******************/
+
+ event E1: int;
+
+ machine Main {
+  start state Init {
+    entry {
+      raise E1, 1000;
+    }
+    on E1 do (payload: int) { 
+      assert (payload == 1000), format ("Expected payload to be 1000, actual payload is {0}", payload);
+    }
+  }
+}

Tst/RegressionTests/Feature2Stmts/Correct/raise2/raise2.p

@@ -0,0 +1,28 @@
+/********************
+ * This example tests raise with payload on monitor
+ * ******************/
+
+ event E1;
+ event E2: int;
+
+ machine Main {
+  start state Init {
+    entry {
+      send this, E1;
+    }
+    on E1 do {
+    }
+  }
+}
+ spec M observes E1, E2 {
+  start state Init {
+    on E1 do {
+      raise E2, 1000;
+    }
+    on E2 do (payload: int) { 
+      assert (payload == 1000), format ("Expected payload to be 1000, actual payload is {0}", payload);
+    }
+  }
+}
+
+test DefaultImpl [main=Main]: assert M in { Main };

Tst/RegressionTests/Feature2Stmts/DynamicError/goto2/goto2.p

@@ -0,0 +1,16 @@
+/********************
+ * This example tests goto with payload on state machine
+ * ******************/
+
+ machine Main {
+  start state Init {
+    entry {
+      goto S, 1000;
+    }
+  }
+  state S {
+    entry (payload: int) { 
+      assert (payload != 1000), format ("Expected payload to be 1000, actual payload is {0}", payload);
+    }
+  }
+}

Tst/RegressionTests/Feature2Stmts/DynamicError/goto3/goto3.p

@@ -0,0 +1,29 @@
+/********************
+ * This example tests goto with payload on monitor
+ * ******************/
+
+ event E1;
+
+ machine Main {
+  start state Init {
+    entry {
+      send this, E1;
+    }
+    on E1 do {
+    }
+  }
+}
+ spec M observes E1 {
+  start state Init {
+    on E1 do {
+      goto S, 1000;
+    }
+  }
+  state S {
+    entry (payload: int) { 
+      assert (payload != 1000), format ("Expected payload to be 1000, actual payload is {0}", payload);
+    }
+  }
+}
+
+test DefaultImpl [main=Main]: assert M in { Main };

Tst/RegressionTests/Feature2Stmts/DynamicError/raise1/raise1.p

@@ -0,0 +1,16 @@
+/********************
+ * This example tests raise with payload on state machine
+ * ******************/
+
+ event E1: int;
+
+ machine Main {
+  start state Init {
+    entry {
+      raise E1, 1000;
+    }
+    on E1 do (payload: int) { 
+      assert (payload != 1000), format ("Expected payload to be 1000, actual payload is {0}", payload);
+    }
+  }
+}

Tst/RegressionTests/Feature2Stmts/DynamicError/raise2/raise2.p

@@ -0,0 +1,28 @@
+/********************
+ * This example tests raise with payload on monitor
+ * ******************/
+
+ event E1;
+ event E2: int;
+
+ machine Main {
+  start state Init {
+    entry {
+      send this, E1;
+    }
+    on E1 do {
+    }
+  }
+}
+ spec M observes E1, E2 {
+  start state Init {
+    on E1 do {
+      raise E2, 1000;
+    }
+    on E2 do (payload: int) { 
+      assert (payload != 1000), format ("Expected payload to be 1000, actual payload is {0}", payload);
+    }
+  }
+}
+
+test DefaultImpl [main=Main]: assert M in { Main };

Tst/RegressionTests/Feature2Stmts/StaticError/goto2/goto2.p

@@ -0,0 +1,16 @@
+/********************
+ * This example tests goto with payload on state machine
+ * ******************/
+
+ machine Main {
+  start state Init {
+    entry {
+      goto S;
+    }
+  }
+  state S {
+    entry (payload: int) { 
+      assert (payload == 1000), format ("Expected payload to be 1000, actual payload is {0}", payload);
+    }
+  }
+}

Tst/RegressionTests/Feature2Stmts/StaticError/goto3/goto3.p

@@ -0,0 +1,29 @@
+/********************
+ * This example tests goto with payload on monitor
+ * ******************/
+
+ event E1;
+
+ machine Main {
+  start state Init {
+    entry {
+      send this, E1;
+    }
+    on E1 do {
+    }
+  }
+}
+ spec M observes E1 {
+  start state Init {
+    on E1 do {
+      goto S;
+    }
+  }
+  state S {
+    entry (payload: int) { 
+      assert (payload == 1000), format ("Expected payload to be 1000, actual payload is {0}", payload);
+    }
+  }
+}
+
+test DefaultImpl [main=Main]: assert M in { Main };

Tst/RegressionTests/Feature2Stmts/StaticError/raise1/raise1.p

@@ -0,0 +1,16 @@
+/********************
+ * This example tests raise with payload on state machine
+ * ******************/
+
+ event E1: int;
+
+ machine Main {
+  start state Init {
+    entry {
+      raise E1;
+    }
+    on E1 do (payload: int) { 
+      assert (payload == 1000), format ("Expected payload to be 1000, actual payload is {0}", payload);
+    }
+  }
+}

Tst/RegressionTests/Feature2Stmts/StaticError/raise2/raise2.p

@@ -0,0 +1,28 @@
+/********************
+ * This example tests raise with payload on monitor
+ * ******************/
+
+ event E1;
+ event E2: int;
+
+ machine Main {
+  start state Init {
+    entry {
+      send this, E1;
+    }
+    on E1 do {
+    }
+  }
+}
+ spec M observes E1, E2 {
+  start state Init {
+    on E1 do {
+      raise E2;
+    }
+    on E2 do (payload: int) { 
+      assert (payload == 1000), format ("Expected payload to be 1000, actual payload is {0}", payload);
+    }
+  }
+}
+
+test DefaultImpl [main=Main]: assert M in { Main };