From 09f2e17622beecb5ab0bc286dbfd473856617ef8 Mon Sep 17 00:00:00 2001 From: Christine Zhou Date: Tue, 27 Aug 2024 16:56:05 -0700 Subject: [PATCH] [Cleanup] Merging PMonitor with Monitor --- Src/PChecker/CheckerCore/PRuntime/PMonitor.cs | 54 ------------------- .../CheckerCore/Specifications/Monitor.cs | 51 ++++++++++++++++++ .../Backend/CSharp/CSharpCodeGenerator.cs | 6 +-- 3 files changed, 54 insertions(+), 57 deletions(-) delete mode 100644 Src/PChecker/CheckerCore/PRuntime/PMonitor.cs diff --git a/Src/PChecker/CheckerCore/PRuntime/PMonitor.cs b/Src/PChecker/CheckerCore/PRuntime/PMonitor.cs deleted file mode 100644 index 4395422385..0000000000 --- a/Src/PChecker/CheckerCore/PRuntime/PMonitor.cs +++ /dev/null @@ -1,54 +0,0 @@ -using System.Collections.Generic; -using System.Linq; -using PChecker.StateMachines.Events; -using PChecker.StateMachines.Logging; -using PChecker.Specifications.Monitors; - -namespace PChecker.PRuntime -{ - public class PMonitor : Monitor - { - public static List observes = new List(); - - public object gotoPayload; - - 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); - } - - public void TryGotoState(object payload = null) where T : State - { - gotoPayload = payload; - RaiseGotoStateEvent(); - } - - public void TryAssert(bool predicate) - { - Assert(predicate); - } - - public void TryAssert(bool predicate, string s, params object[] args) - { - Assert(predicate, s, args); - } - - public void LogLine(string message) - { - Logger.WriteLine($" {message}"); - - // Log message to JSON output - JsonLogger.AddLogType(JsonWriter.LogType.Print); - JsonLogger.AddLog(message); - JsonLogger.AddToLogs(updateVcMap: false); - } - - public void Log(string message) - { - Logger.Write($"{message}"); - } - } -} \ No newline at end of file diff --git a/Src/PChecker/CheckerCore/Specifications/Monitor.cs b/Src/PChecker/CheckerCore/Specifications/Monitor.cs index b8e2020d4c..d51e2bc11a 100644 --- a/Src/PChecker/CheckerCore/Specifications/Monitor.cs +++ b/Src/PChecker/CheckerCore/Specifications/Monitor.cs @@ -91,6 +91,16 @@ public abstract class Monitor /// liveness bug has been found. /// private int LivenessTemperature; + + /// + /// List containing all the event types that are observed by this monitor. + /// + public static List observes = new List(); + + /// + /// Temporarily holds data that might be needed during a state transition. + /// + public object gotoPayload; /// /// Gets the name of this monitor. @@ -177,6 +187,17 @@ internal void Initialize(ControlledRuntime runtime) { Runtime = runtime; } + + /// + /// Checks if the event is null, and calls . + /// + 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); + } /// /// Raises the specified at the end of the current action. @@ -196,6 +217,36 @@ protected void RaiseEvent(Event e) PendingTransition = new Transition(Transition.Type.Raise, default, e); } + /// + /// Writes PrintLog messages to logger. + /// + public void LogLine(string message) + { + Logger.WriteLine($" {message}"); + + // Log message to JSON output + JsonLogger.AddLogType(JsonWriter.LogType.Print); + JsonLogger.AddLog(message); + JsonLogger.AddToLogs(updateVcMap: false); + } + + /// + /// Writes message to logger. + /// + public void Log(string message) + { + Logger.Write($"{message}"); + } + + /// + /// Stores payload temperarily, and calls . + /// + public void TryGotoState(object payload = null) where T : State + { + gotoPayload = payload; + RaiseGotoStateEvent(); + } + /// /// 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 51e770b0fd..1afc013898 100644 --- a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs +++ b/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: \" + ");