diff --git a/Src/PChecker/CheckerCore/PRuntime/PMonitor.cs b/Src/PChecker/CheckerCore/PRuntime/PMonitor.cs deleted file mode 100644 index 439542238..000000000 --- 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 b8e2020d4..7c81cd433 100644 --- a/Src/PChecker/CheckerCore/Specifications/Monitor.cs +++ b/Src/PChecker/CheckerCore/Specifications/Monitor.cs @@ -27,7 +27,7 @@ namespace PChecker.Specifications.Monitors /// See Specifications Overview /// for more information. /// - public abstract class Monitor + public class Monitor { /// /// Map from monitor types to a set of all possible states types. @@ -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. @@ -189,13 +199,34 @@ internal void Initialize(ControlledRuntime runtime) /// An Assert is raised if you accidentally try and do two of these operations in a single action. /// /// The event to raise. - protected void RaiseEvent(Event e) + public void RaiseEvent(Event e) { Assert(e != null, "{0} is raising a null event.", GetType().FullName); CheckDanglingTransition(); 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}"); + } + /// /// Raise a special event that performs a goto state operation at the end of the current action. /// @@ -215,9 +246,11 @@ protected 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(object payload = null) where S : State + { + gotoPayload = payload; RaiseGotoStateEvent(typeof(S)); + } /// /// Raise a special event that performs a goto state operation at the end of the current action. @@ -238,7 +271,7 @@ protected void RaiseGotoStateEvent() /// 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(Type state) + public void RaiseGotoStateEvent(Type state) { // If the state is not a state of the monitor, then report an error and exit. Assert(StateTypeMap[GetType()].Any(val => val.DeclaringType.Equals(state.DeclaringType) && val.Name.Equals(state.Name)), @@ -250,7 +283,7 @@ protected void RaiseGotoStateEvent(Type state) /// /// Checks if the assertion holds, and if not, throws an exception. /// - protected void Assert(bool predicate) + public void Assert(bool predicate) { if (!predicate) { @@ -262,7 +295,7 @@ protected void Assert(bool predicate) /// /// Checks if the assertion holds, and if not, throws an exception. /// - protected void Assert(bool predicate, string s, params object[] args) + public void Assert(bool predicate, string s, params object[] args) { if (!predicate) { diff --git a/Src/PChecker/CheckerCore/StateMachines/StateMachine.cs b/Src/PChecker/CheckerCore/StateMachines/StateMachine.cs index 241a112a1..f3e9c036c 100644 --- a/Src/PChecker/CheckerCore/StateMachines/StateMachine.cs +++ b/Src/PChecker/CheckerCore/StateMachines/StateMachine.cs @@ -213,30 +213,30 @@ protected void Monitor(Type type, Event e) /// /// Checks if the assertion holds, and if not, throws an exception. /// - protected void Assert(bool predicate) => Runtime.Assert(predicate); + public void Assert(bool predicate) => Runtime.Assert(predicate); /// /// Checks if the assertion holds, and if not, throws an exception. /// - protected void Assert(bool predicate, string s, object arg0) => + public void Assert(bool predicate, string s, object arg0) => Runtime.Assert(predicate, s, arg0); /// /// Checks if the assertion holds, and if not, throws an exception. /// - protected void Assert(bool predicate, string s, object arg0, object arg1) => + public void Assert(bool predicate, string s, object arg0, object arg1) => Runtime.Assert(predicate, s, arg0, arg1); /// /// Checks if the assertion holds, and if not, throws an exception. /// - protected void Assert(bool predicate, string s, object arg0, object arg1, object arg2) => + public void Assert(bool predicate, string s, object arg0, object arg1, object arg2) => Runtime.Assert(predicate, s, arg0, arg1, arg2); /// /// Checks if the assertion holds, and if not, throws an exception. /// - protected void Assert(bool predicate, string s, params object[] args) => + public void Assert(bool predicate, string s, params object[] args) => Runtime.Assert(predicate, s, args); /// @@ -814,7 +814,7 @@ private protected static class UserCallbackType /// An Assert is raised if you accidentally try and do two of these operations in a single action. /// /// The event to raise. - protected void RaiseEvent(Event e) + public void RaiseEvent(Event e) { Assert(CurrentStatus is Status.Active, "{0} invoked RaiseEvent while halting.", Id); Assert(e != null, "{0} is raising a null event.", Id); diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs index 51e770b0f..647fa735b 100644 --- a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs @@ -154,6 +154,7 @@ private void WriteSourcePrologue(CompilationContext context, StringWriter output context.WriteLine(output, "using PChecker.StateMachines.Events;"); context.WriteLine(output, "using PChecker.Runtime;"); context.WriteLine(output, "using PChecker.Specifications;"); + context.WriteLine(output, "using Monitor = PChecker.Specifications.Monitors.Monitor;"); context.WriteLine(output, "using System;"); context.WriteLine(output, "using System.Runtime;"); context.WriteLine(output, "using System.Collections.Generic;"); @@ -263,7 +264,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} : Monitor"); context.WriteLine(output, "{"); foreach (var field in machine.Fields) @@ -737,7 +738,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 +807,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: \" + "); @@ -988,15 +989,9 @@ private void WriteStmt(CompilationContext context, StringWriter output, Function case RaiseStmt raiseStmt: //last statement - context.Write(output, "currentMachine.TryRaiseEvent((Event)"); + context.Write(output, "currentMachine.RaiseEvent("); WriteExpr(context, output, raiseStmt.Event); - if (raiseStmt.Payload.Any()) - { - context.Write(output, ", "); - WriteExpr(context, output, raiseStmt.Payload.First()); - } - - context.WriteLine(output, ");"); + context.Write(output, ");"); context.WriteLine(output, "return;"); break; @@ -1011,7 +1006,7 @@ private void WriteStmt(CompilationContext context, StringWriter output, Function // add halt as a special case if doesnt exist if (receiveStmt.Cases.All(kv => kv.Key.Name != "PHalt")) { - context.WriteLine(output,"case PHalt _hv: { currentMachine.TryRaiseEvent(_hv); break;} "); + context.WriteLine(output,"case PHalt _hv: { currentMachine.RaiseEvent(_hv); break;} "); }