[Cleanup] Merging PMonitor with Monitor

Src/PChecker/CheckerCore/Specifications/Monitor.cs

@@ -91,6 +91,16 @@ public abstract class Monitor
         /// liveness bug has been found.
         /// </summary>
         private int LivenessTemperature;
+
+        /// <summary>
+        /// List containing all the event types that are observed by this monitor.
+        /// </summary>
+        public static List<string> observes = new List<string>();
+
+        /// <summary>
+        /// Temporarily holds data that might be needed during a state transition.
+        /// </summary>
+        public object gotoPayload;
 
         /// <summary>
         /// Gets the name of this monitor.
@@ -177,6 +187,17 @@ internal void Initialize(ControlledRuntime runtime)
         {
             Runtime = runtime;
         }
+
+        /// <summary>
+        /// Checks if the event is null, and calls <see cref="Monitor.RaiseEvent"/>.
+        /// </summary>
+        public void TryRaiseEvent(Event ev, object payload = null)
+        {
+            Assert(!(ev is DefaultEvent), "Monitor cannot raise a null event");
+            var oneArgConstructor = ev.GetType().GetConstructors().First(x => x.GetParameters().Length > 0);
+            var @event = (Event)oneArgConstructor.Invoke(new[] { payload });
+            RaiseEvent(@event);
+        }
 
         /// <summary>
         /// Raises the specified <see cref="Event"/> at the end of the current action.
@@ -196,6 +217,36 @@ protected void RaiseEvent(Event e)
             PendingTransition = new Transition(Transition.Type.Raise, default, e);
         }
 
+        /// <summary>
+        /// Writes PrintLog messages to logger.
+        /// </summary>
+        public void LogLine(string message)
+        {
+            Logger.WriteLine($"<PrintLog> {message}");
+
+            // Log message to JSON output
+            JsonLogger.AddLogType(JsonWriter.LogType.Print);
+            JsonLogger.AddLog(message);
+            JsonLogger.AddToLogs(updateVcMap: false);
+        }
+
+        /// <summary>
+        /// Writes message to logger.
+        /// </summary>
+        public void Log(string message)
+        {
+            Logger.Write($"{message}");
+        }
+
+        /// <summary>
+        /// Stores payload temperarily, and calls <see cref="Monitor.RaiseGotoStateEvent"/>.
+        /// </summary>
+        public void TryGotoState<T>(object payload = null) where T : State
+        {
+            gotoPayload = payload;
+            RaiseGotoStateEvent<T>();
+        }
+
         /// <summary>
         /// Raise a special event that performs a goto state operation at the end of the current action.
         /// </summary>

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

@@ -263,7 +263,7 @@ private void WriteMonitor(CompilationContext context, StringWriter output, Machi
             WriteNameSpacePrologue(context, output);
 
             var declName = context.Names.GetNameForDecl(machine);
-            context.WriteLine(output, $"internal partial class {declName} : PMonitor");
+            context.WriteLine(output, $"internal partial class {declName} : PChecker.Specifications.Monitors.Monitor");
             context.WriteLine(output, "{");
 
             foreach (var field in machine.Fields)
@@ -737,7 +737,7 @@ private void WriteFunction(CompilationContext context, StringWriter output, Func
                 // for monitor
                 if (!(function.CanCreate == true || function.CanSend == true || function.IsNondeterministic == true || function.CanReceive == true))
                 {
-                    var functionParameters_monitor = functionParameters + string.Concat(seperator, "PMonitor currentMachine");
+                    var functionParameters_monitor = functionParameters + string.Concat(seperator, "Monitor currentMachine");
                     context.WriteLine(output,
                         $"public {staticKeyword}{asyncKeyword}{returnType} {functionName}({functionParameters_monitor})");
                     WriteFunctionBody(context, output, function);
@@ -806,7 +806,7 @@ private void WriteStmt(CompilationContext context, StringWriter output, Function
                     break;
 
                 case AssertStmt assertStmt:
-                    context.Write(output, "currentMachine.TryAssert(");
+                    context.Write(output, "currentMachine.Assert(");
                     WriteExpr(context, output, assertStmt.Assertion);
                     context.Write(output, ",");
                     context.Write(output, $"\"Assertion Failed: \" + ");