diff --git a/Src/PChecker/CheckerCore/PRuntime/PMachine.cs b/Src/PChecker/CheckerCore/PRuntime/PMachine.cs index 7555973f9..d778d186e 100644 --- a/Src/PChecker/CheckerCore/PRuntime/PMachine.cs +++ b/Src/PChecker/CheckerCore/PRuntime/PMachine.cs @@ -14,7 +14,6 @@ namespace PChecker.PRuntime public class PMachine : StateMachine { public List creates = new List(); - protected IPrtValue gotoPayload; private string interfaceName; public List receives = new List(); public PMachineValue self; @@ -104,13 +103,6 @@ public Task TryReceiveEvent(params Type[] events) return ReceiveEventAsync(events); } - public void TryGotoState(IPrtValue payload = null) where T : State - { - gotoPayload = payload; - RaiseGotoStateEvent(); - throw new PNonStandardReturnException { ReturnKind = NonStandardReturn.Goto }; - } - public int TryRandomInt(int maxValue) { return RandomInteger(maxValue); diff --git a/Src/PChecker/CheckerCore/StateMachines/StateMachine.cs b/Src/PChecker/CheckerCore/StateMachines/StateMachine.cs index f3e9c036c..a95eaffdc 100644 --- a/Src/PChecker/CheckerCore/StateMachines/StateMachine.cs +++ b/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. /// protected JsonWriter JsonLogger => Runtime.JsonLogger; + + protected IPrtValue gotoPayload; + /// /// Initializes a new instance of the 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. /// /// Type of the state. - protected void RaiseGotoStateEvent() - where S : State => + public void RaiseGotoStateEvent(IPrtValue payload = null) where S : State + { + gotoPayload = payload; RaiseGotoStateEvent(typeof(S)); + throw new PNonStandardReturnException { ReturnKind = NonStandardReturn.Goto }; + } /// /// Raise a special event that performs a goto state operation at the end of the current action. diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs index 05e3c942a..3143c83b4 100644 --- a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs +++ b/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; diff --git a/Tst/RegressionTests/Feature2Stmts/Correct/goto2/goto2.p b/Tst/RegressionTests/Feature2Stmts/Correct/goto2/goto2.p new file mode 100644 index 000000000..db886ff2a --- /dev/null +++ b/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); + } + } +} \ No newline at end of file diff --git a/Tst/RegressionTests/Feature2Stmts/Correct/goto3/goto3.p b/Tst/RegressionTests/Feature2Stmts/Correct/goto3/goto3.p new file mode 100644 index 000000000..4bc5da285 --- /dev/null +++ b/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 }; \ No newline at end of file diff --git a/Tst/RegressionTests/Feature2Stmts/Correct/raise1/raise1.p b/Tst/RegressionTests/Feature2Stmts/Correct/raise1/raise1.p new file mode 100644 index 000000000..234e066ee --- /dev/null +++ b/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); + } + } +} \ No newline at end of file diff --git a/Tst/RegressionTests/Feature2Stmts/Correct/raise2/raise2.p b/Tst/RegressionTests/Feature2Stmts/Correct/raise2/raise2.p new file mode 100644 index 000000000..a433e06b1 --- /dev/null +++ b/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 }; \ No newline at end of file diff --git a/Tst/RegressionTests/Feature2Stmts/DynamicError/goto2/goto2.p b/Tst/RegressionTests/Feature2Stmts/DynamicError/goto2/goto2.p new file mode 100644 index 000000000..ca3fe4497 --- /dev/null +++ b/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); + } + } +} \ No newline at end of file diff --git a/Tst/RegressionTests/Feature2Stmts/DynamicError/goto3/goto3.p b/Tst/RegressionTests/Feature2Stmts/DynamicError/goto3/goto3.p new file mode 100644 index 000000000..1d94e778c --- /dev/null +++ b/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 }; \ No newline at end of file diff --git a/Tst/RegressionTests/Feature2Stmts/DynamicError/raise1/raise1.p b/Tst/RegressionTests/Feature2Stmts/DynamicError/raise1/raise1.p new file mode 100644 index 000000000..ca4ccfc7c --- /dev/null +++ b/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); + } + } +} \ No newline at end of file diff --git a/Tst/RegressionTests/Feature2Stmts/DynamicError/raise2/raise2.p b/Tst/RegressionTests/Feature2Stmts/DynamicError/raise2/raise2.p new file mode 100644 index 000000000..6fc6d66e1 --- /dev/null +++ b/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 }; \ No newline at end of file diff --git a/Tst/RegressionTests/Feature2Stmts/StaticError/goto2/goto2.p b/Tst/RegressionTests/Feature2Stmts/StaticError/goto2/goto2.p new file mode 100644 index 000000000..f93a37aef --- /dev/null +++ b/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); + } + } +} \ No newline at end of file diff --git a/Tst/RegressionTests/Feature2Stmts/StaticError/goto3/goto3.p b/Tst/RegressionTests/Feature2Stmts/StaticError/goto3/goto3.p new file mode 100644 index 000000000..0fba8eb29 --- /dev/null +++ b/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 }; \ No newline at end of file diff --git a/Tst/RegressionTests/Feature2Stmts/StaticError/raise1/raise1.p b/Tst/RegressionTests/Feature2Stmts/StaticError/raise1/raise1.p new file mode 100644 index 000000000..5173e279d --- /dev/null +++ b/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); + } + } +} \ No newline at end of file diff --git a/Tst/RegressionTests/Feature2Stmts/StaticError/raise2/raise2.p b/Tst/RegressionTests/Feature2Stmts/StaticError/raise2/raise2.p new file mode 100644 index 000000000..7ebba5c6b --- /dev/null +++ b/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 }; \ No newline at end of file