[Cleanup] Remove GodMachine, reformat PChecker folder, add assert fal…

…se after raise test case

Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogJsonFormatter.cs → Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogJsonFormatter.cs

@@ -114,11 +114,6 @@ public void OnAssertionFailure(string error)
         /// <inheritdoc/>
         public void OnCreateStateMachine(StateMachineId id, string creatorName, string creatorType)
         {
-            if (id.Name.Contains("GodMachine") || creatorName.Contains("GodMachine"))
-            {
-                return;
-            }
-
             var source = creatorName ?? $"task '{Task.CurrentId}'";
             var log = $"{id} was created by {source}.";
 
@@ -147,11 +142,6 @@ public void OnDefaultEventHandler(StateMachineId id, string stateName)
 
         public void OnDequeueEvent(StateMachineId id, string stateName, Event e)
         {
-            if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine"))
-            {
-                return;
-            }
-
             var eventName = GetEventNameWithPayload(e);
             var log = stateName is null
                 ? $"'{id}' dequeued event '{eventName}'."
@@ -221,11 +211,6 @@ public void OnExecuteAction(StateMachineId id, string handlingStateName, string
         /// <inheritdoc />
         public void OnGotoState(StateMachineId id, string currentStateName, string newStateName)
         {
-            if (currentStateName.Contains("__InitState__") || id.Name.Contains("GodMachine"))
-            {
-                return;
-            }
-
             currentStateName = GetShortName(currentStateName);
             newStateName = GetShortName(newStateName);
 
@@ -304,8 +289,7 @@ public void OnRaiseEvent(StateMachineId id, string stateName, Event e)
             stateName = GetShortName(stateName);
             string eventName = GetEventNameWithPayload(e);
 
-            if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine") ||
-                eventName.Contains("GotoStateEvent"))
+            if (eventName.Contains("GotoStateEvent"))
             {
                 return;
             }
@@ -371,11 +355,6 @@ public void OnSendEvent(StateMachineId targetStateMachineId, string senderName,
         /// <inheritdoc />
         public void OnStateTransition(StateMachineId id, string stateName, bool isEntry)
         {
-            if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine"))
-            {
-                return;
-            }
-
             stateName = GetShortName(stateName);
             var direction = isEntry ? "enters" : "exits";
             var log = $"{id} {direction} state '{stateName}'.";

Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogTextFormatter.cs → Src/PChecker/CheckerCore/PRuntime/StateMachines/Logging/PCheckerLogTextFormatter.cs

@@ -57,10 +57,6 @@ public void OnAssertionFailure(string error)
         /// <inheritdoc/>
         public void OnCreateStateMachine(StateMachineId id, string creatorName, string creatorType)
         {
-            if (id.Name.Contains("GodMachine") || creatorName.Contains("GodMachine"))
-            {
-                return;
-            }
             var source = creatorName ?? $"task '{Task.CurrentId}'";
             var text = $"<CreateLog> {id} was created by {source}.";
             Logger.WriteLine(text);
@@ -69,11 +65,6 @@ public void OnCreateStateMachine(StateMachineId id, string creatorName, string c
         /// <inheritdoc/>
         public void OnStateTransition(StateMachineId id, string stateName, bool isEntry)
         {
-            if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine"))
-            {
-                return;
-            }
-
             var direction = isEntry ? "enters" : "exits";
             var text = $"<StateLog> {id} {direction} state '{stateName}'.";
             Logger.WriteLine(text);
@@ -188,11 +179,6 @@ public void OnMonitorProcessEvent(string monitorType, string stateName, string s
         /// <inheritdoc/>
         public void OnDequeueEvent(StateMachineId id, string stateName, Event e)
         {
-            if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine"))
-            {
-                return;
-            }
-
             stateName = GetShortName(stateName);
             var eventName = GetEventNameWithPayload(e);
             string text = null;
@@ -213,7 +199,7 @@ public void OnRaiseEvent(StateMachineId id, string stateName, Event e)
         {
             stateName = GetShortName(stateName);
             var eventName = GetEventNameWithPayload(e);
-            if (stateName.Contains("__InitState__") || id.Name.Contains("GodMachine") || eventName.Contains("GotoStateEvent"))
+            if (eventName.Contains("GotoStateEvent"))
             {
                 return;
             }
@@ -277,11 +263,6 @@ public void OnSendEvent(StateMachineId targetStateMachineId, string senderName,
         /// <inheritdoc/>
         public void OnGotoState(StateMachineId id, string currStateName, string newStateName)
         {
-            if (currStateName.Contains("__InitState__") || id.Name.Contains("GodMachine"))
-            {
-                return;
-            }
-
             var text = $"<GotoLog> {id} is transitioning from state '{currStateName}' to state '{newStateName}'.";
             Logger.WriteLine(text);
         }

Src/PChecker/CheckerCore/StateMachines/StateMachine.cs → Src/PChecker/CheckerCore/PRuntime/StateMachines/StateMachine.cs

@@ -966,6 +966,7 @@ public void RaiseEvent(Event e)
             Assert(e != null, "{0} is raising a null event.", Id);
             CheckDanglingTransition();
             PendingTransition = new Transition(Transition.Type.RaiseEvent, default, e);
+            throw new PNonStandardReturnException { ReturnKind = NonStandardReturn.Raise };
         }
 
         /// <summary>

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

@@ -395,7 +395,7 @@ private void WriteTestFunction(CompilationContext context, StringWriter output,
             context.WriteLine(output, "InitializeMonitorMap(runtime);");
             context.WriteLine(output, "InitializeMonitorObserves();");
             context.WriteLine(output,
-                $"runtime.CreateStateMachine(typeof(_GodMachine), new _GodMachine.Config(typeof({main})));");
+                $"runtime.CreateStateMachine(typeof({main}), \"{main}\");");
             context.WriteLine(output, "}");
         }
 

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

@@ -8,6 +8,7 @@
   start state Init {
     entry {
       raise E1, 1000;
+      assert false;
     }
     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

@@ -18,6 +18,7 @@
   start state Init {
     on E1 do {
       raise E2, 1000;
+      assert false;
     }
     on E2 do (payload: int) { 
       assert (payload == 1000), format ("Expected payload to be 1000, actual payload is {0}", payload);