Skip to content

Commit

Permalink
[Cleanup] Merging PMonitor with Monitor (#766)
Browse files Browse the repository at this point in the history 
Co-authored-by: Christine Zhou <zhouchrs@amazon.com>
  • Loading branch information
@ChristineZh0u
ChristineZh0u and Christine Zhou committed Aug 29, 2024
1 parent aa5e50b commit 51b41ec
Show file tree
Hide file tree
Showing 4 changed files with 53 additions and 79 deletions.
54 changes: 0 additions & 54 deletions Src/PChecker/CheckerCore/PRuntime/PMonitor.cs
View file

This file was deleted.

47 changes: 40 additions & 7 deletions Src/PChecker/CheckerCore/Specifications/Monitor.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ namespace PChecker.Specifications.Monitors
/// See <see href="/coyote/learn/core/specifications">Specifications Overview</see>
/// for more information.
/// </remarks>
public abstract class Monitor
public class Monitor
{
/// <summary>
/// Map from monitor types to a set of all possible states types.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
/// </remarks>
/// <param name="e">The event to raise.</param>
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);
}

/// <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>
/// Raise a special event that performs a goto state operation at the end of the current action.
/// </summary>
Expand All @@ -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.
/// </remarks>
/// <typeparam name="S">Type of the state.</typeparam>
protected void RaiseGotoStateEvent<S>()
where S : State =>
public void RaiseGotoStateEvent<S>(object payload = null) where S : State
{
gotoPayload = payload;
RaiseGotoStateEvent(typeof(S));
}

/// <summary>
/// Raise a special event that performs a goto state operation at the end of the current action.
Expand All @@ -238,7 +271,7 @@ protected void RaiseGotoStateEvent<S>()
/// An Assert is raised if you accidentally try and do two of these operations in a single action.
/// </remarks>
/// <param name="state">Type of the state.</param>
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)),
Expand All @@ -250,7 +283,7 @@ protected void RaiseGotoStateEvent(Type state)
/// <summary>
/// Checks if the assertion holds, and if not, throws an <see cref="AssertionFailureException"/> exception.
/// </summary>
protected void Assert(bool predicate)
public void Assert(bool predicate)
{
if (!predicate)
{
Expand All @@ -262,7 +295,7 @@ protected void Assert(bool predicate)
/// <summary>
/// Checks if the assertion holds, and if not, throws an <see cref="AssertionFailureException"/> exception.
/// </summary>
protected void Assert(bool predicate, string s, params object[] args)
public void Assert(bool predicate, string s, params object[] args)
{
if (!predicate)
{
Expand Down
12 changes: 6 additions & 6 deletions Src/PChecker/CheckerCore/StateMachines/StateMachine.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -213,30 +213,30 @@ protected void Monitor(Type type, Event e)
/// <summary>
/// Checks if the assertion holds, and if not, throws an <see cref="AssertionFailureException"/> exception.
/// </summary>
protected void Assert(bool predicate) => Runtime.Assert(predicate);
public void Assert(bool predicate) => Runtime.Assert(predicate);

/// <summary>
/// Checks if the assertion holds, and if not, throws an <see cref="AssertionFailureException"/> exception.
/// </summary>
protected void Assert(bool predicate, string s, object arg0) =>
public void Assert(bool predicate, string s, object arg0) =>
Runtime.Assert(predicate, s, arg0);

/// <summary>
/// Checks if the assertion holds, and if not, throws an <see cref="AssertionFailureException"/> exception.
/// </summary>
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);

/// <summary>
/// Checks if the assertion holds, and if not, throws an <see cref="AssertionFailureException"/> exception.
/// </summary>
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);

/// <summary>
/// Checks if the assertion holds, and if not, throws an <see cref="AssertionFailureException"/> exception.
/// </summary>
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);

/// <summary>
Expand Down Expand Up @@ -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.
/// </remarks>
/// <param name="e">The event to raise.</param>
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);
Expand Down
19 changes: 7 additions & 12 deletions Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;");
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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: \" + ");
Expand Down Expand Up @@ -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;

Expand All @@ -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;} ");

}

Expand Down

0 comments on commit 51b41ec

Please sign in to comment.