[Cleanup] Merging PEvent with Event (#764)

Co-authored-by: Christine Zhou <[email protected]>

Src/PChecker/CheckerCore/PRuntime/PMachine.cs

@@ -251,7 +251,7 @@ public object ToDict()
             }
         }
 
-        public class InitializeParametersEvent : PEvent
+        public class InitializeParametersEvent : Event
         {
             public InitializeParametersEvent(InitializeParameters payload) : base(payload)
             {

Src/PChecker/CheckerCore/StateMachines/Events/Event.cs

@@ -1,15 +1,64 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
+using System;
 using System.Runtime.Serialization;
+using PChecker.PRuntime.Values;
 
 namespace PChecker.StateMachines.Events
 {
     /// <summary>
-    /// Abstract class representing an event.
+    /// Class representing an event.
     /// </summary>
     [DataContract]
-    public abstract class Event
+    public class Event: IPrtValue
     {
+        public Event()
+        {
+        }
+
+        public Event(IPrtValue payload)
+        {
+            Payload = payload;
+        }
+
+        public IPrtValue Payload { get; }
+
+        public bool Equals(IPrtValue other)
+        {
+            return other != null && GetType().FullName.Equals(other.GetType().FullName);
+        }
+
+        public virtual IPrtValue Clone()
+        {
+            throw new NotImplementedException();
+        }
+
+        public object ToDict()
+        {
+            return this.GetType().Name;
+        }
+
+        public override bool Equals(object obj)
+        {
+            return obj is Event other && Equals(other);
+        }
+
+        public override int GetHashCode()
+        {
+            return GetType().FullName.GetHashCode();
+        }
+
+        public override string ToString()
+        {
+            return GetType().Name;
+        }
+    }
+
+    public class PHalt : Event
+    {
+        public PHalt(IPrtValue payload) : base(payload)
+        {
+        }
     }
 }

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

@@ -75,7 +75,7 @@ private static string GetEventNameWithPayload(Event e)
                 return e.GetType().Name;
             }
 
-            var pe = (PEvent)(e);
+            var pe = (Event)(e);
             var payload = pe.Payload == null ? "null" : pe.Payload.ToEscapedString();
             var msg = pe.Payload == null ? "" : $" with payload ({payload})";
             return $"{GetShortName(e.GetType().Name)}{msg}";
@@ -93,7 +93,7 @@ private static object GetEventPayloadInJson(Event e)
                 return null;
             }
 
-            var pe = (PEvent)(e);
+            var pe = (Event)(e);
             return pe.Payload?.ToDict();
         }
 

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

@@ -42,7 +42,7 @@ private string GetEventNameWithPayload(Event e)
             {
                 return e.GetType().Name;
             }
-            var pe = (PEvent)(e);
+            var pe = (Event)(e);
             var payload = pe.Payload == null ? "null" : pe.Payload.ToEscapedString();
             var msg = pe.Payload == null ? "" : $" with payload ({payload})";
             return $"{GetShortName(e.GetType().Name)}{msg}";

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

@@ -206,7 +206,7 @@ private void WriteDecl(CompilationContext context, StringWriter output, IPDecl d
 
                     break;
 
-                case PEvent pEvent:
+                case Event pEvent:
                     if (!pEvent.IsBuiltIn)
                     {
                         WriteEvent(context, output, pEvent);
@@ -472,15 +472,15 @@ private void WriteInitializeLinkMap(CompilationContext context, StringWriter out
             context.WriteLine(output);
         }
 
-        private void WriteEvent(CompilationContext context, StringWriter output, PEvent pEvent)
+        private void WriteEvent(CompilationContext context, StringWriter output, Event pEvent)
         {
             WriteNameSpacePrologue(context, output);
 
             var declName = context.Names.GetNameForDecl(pEvent);
 
             // initialize the payload type
             var payloadType = GetCSharpType(pEvent.PayloadType, true);
-            context.WriteLine(output, $"internal partial class {declName} : PEvent");
+            context.WriteLine(output, $"internal partial class {declName} : Event");
             context.WriteLine(output, "{");
             context.WriteLine(output, $"public {declName}() : base() {{}}");
             context.WriteLine(output, $"public {declName} ({payloadType} payload): base(payload)" + "{ }");
@@ -506,7 +506,7 @@ private void WriteMachine(CompilationContext context, StringWriter output, Machi
 
             //create the constructor event
             var cTorType = GetCSharpType(machine.PayloadType, true);
-            context.Write(output, "public class ConstructorEvent : PEvent");
+            context.Write(output, "public class ConstructorEvent : Event");
             context.Write(output, "{");
             context.Write(output, $"public ConstructorEvent({cTorType} val) : base(val) {{ }}");
             context.WriteLine(output, "}");
@@ -680,7 +680,7 @@ private void WriteNamedFunctionWrapper(CompilationContext context, StringWriter
                 context.WriteLine(output, $"{context.Names.GetNameForDecl(function.Owner)} currentMachine = this;");
             }
 
-            var parameter = function.Signature.Parameters.Any() ? $"({GetCSharpType(function.Signature.ParameterTypes.First())})((PEvent)currentMachine_dequeuedEvent).Payload" : "";
+            var parameter = function.Signature.Parameters.Any() ? $"({GetCSharpType(function.Signature.ParameterTypes.First())})((Event)currentMachine_dequeuedEvent).Payload" : "";
             context.WriteLine(output, $"{awaitMethod}{functionName}({parameter});");
             context.WriteLine(output, "}");
         }
@@ -769,7 +769,7 @@ private void WriteFunctionBody(CompilationContext context, StringWriter output,
                 {
                     var param = function.Signature.Parameters.First();
                     context.WriteLine(output,
-                        $"{GetCSharpType(param.Type)} {context.Names.GetNameForDecl(param)} = ({GetCSharpType(param.Type)})(gotoPayload ?? ((PEvent)currentMachine_dequeuedEvent).Payload);");
+                        $"{GetCSharpType(param.Type)} {context.Names.GetNameForDecl(param)} = ({GetCSharpType(param.Type)})(gotoPayload ?? ((Event)currentMachine_dequeuedEvent).Payload);");
                     context.WriteLine(output, "this.gotoPayload = null;");
                 }
             }
@@ -795,7 +795,7 @@ private void WriteStmt(CompilationContext context, StringWriter output, Function
             {
                 case AnnounceStmt announceStmt:
                     context.Write(output, "currentMachine.Announce((Event)");
-                    WriteExpr(context, output, announceStmt.PEvent);
+                    WriteExpr(context, output, announceStmt.Event);
                     if (announceStmt.Payload != null)
                     {
                         context.Write(output, ", ");
@@ -989,7 +989,7 @@ private void WriteStmt(CompilationContext context, StringWriter output, Function
                 case RaiseStmt raiseStmt:
                     //last statement
                     context.Write(output, "currentMachine.TryRaiseEvent((Event)");
-                    WriteExpr(context, output, raiseStmt.PEvent);
+                    WriteExpr(context, output, raiseStmt.Event);
                     if (raiseStmt.Payload.Any())
                     {
                         context.Write(output, ", ");
@@ -1579,7 +1579,7 @@ private string GetCSharpType(PLanguageType type, bool isVar = false)
                     return "PrtString";
 
                 case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Event):
-                    return "PEvent";
+                    return "Event";
 
                 case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Machine):
                     return "PMachineValue";

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

@@ -49,7 +49,7 @@ protected override string ComputeNameForDecl(IPDecl decl)
 #pragma warning disable CCN0002 // Non exhaustive patterns in switch block
             switch (decl)
             {
-                case PEvent pEvent:
+                case Event pEvent:
                     if (pEvent.IsNullEvent)
                     {
                         return "DefaultEvent";

Src/PCompiler/CompilerCore/Backend/Debugging/IrToPseudoP.cs

@@ -147,7 +147,7 @@ private void WriteTree(IPAST tree)
                         " };");
                     break;
 
-                case PEvent pEvent:
+                case Event pEvent:
                     WriteStmt("event ",
                         pEvent,
                         " assert ",
@@ -168,7 +168,7 @@ private void WriteTree(IPAST tree)
                     break;
 
                 case AnnounceStmt announceStmt:
-                    WriteStmt("announce ", announceStmt.PEvent, ", ", announceStmt.Payload, ";");
+                    WriteStmt("announce ", announceStmt.Event, ", ", announceStmt.Payload, ";");
                     break;
 
                 case AssertStmt assertStmt:
@@ -235,7 +235,7 @@ private void WriteTree(IPAST tree)
                     break;
 
                 case RaiseStmt raiseStmt:
-                    WriteStmt("raise ", raiseStmt.PEvent, ", ", raiseStmt.Payload, ";");
+                    WriteStmt("raise ", raiseStmt.Event, ", ", raiseStmt.Payload, ";");
                     break;
 
                 case ReceiveStmt receiveStmt:

Src/PCompiler/CompilerCore/Backend/IRTransformer.cs

@@ -338,7 +338,7 @@ private List<IPStmt> SimplifyStatement(IPStmt statement)
                 case null:
                     throw new ArgumentNullException(nameof(statement));
                 case AnnounceStmt announceStmt:
-                    (var annEvt, var annEvtDeps) = SimplifyExpression(announceStmt.PEvent);
+                    (var annEvt, var annEvtDeps) = SimplifyExpression(announceStmt.Event);
                     (IExprTerm annPayload, List<IPStmt> annPayloadDeps) = announceStmt.Payload == null
                         ? (null, new List<IPStmt>())
                         : SimplifyExpression(announceStmt.Payload);
@@ -477,7 +477,7 @@ private List<IPStmt> SimplifyStatement(IPStmt statement)
                     return deps.Concat(new[] { new PrintStmt(location, newMessage) }).ToList();
 
                 case RaiseStmt raiseStmt:
-                    (var raiseEvent, var raiseEventDeps) = SimplifyExpression(raiseStmt.PEvent);
+                    (var raiseEvent, var raiseEventDeps) = SimplifyExpression(raiseStmt.Event);
                     (var raiseEventTmp, var raiseEventTempDep) = SaveInTemporary(new CloneExpr(raiseEvent));
 
                     (var raiseArgs, var raiseArgDeps) = SimplifyArgPack(raiseStmt.Payload);

Src/PCompiler/CompilerCore/Backend/Java/Constants.cs

@@ -52,7 +52,7 @@ internal static IEnumerable<string> ImportStatements()
 
         #region Event source generation
 
-        public static readonly string EventNamespaceName = "PEvents";
+        public static readonly string EventNamespaceName = "Events";
         public static readonly string EventDefnFileName = $"{EventNamespaceName}.java";
 
         #endregion
@@ -227,9 +227,9 @@ internal static string AsFFIComment(string line)
         internal static readonly string PValueClass = "prt.values.PValue";
 
         /// <summary>
-        /// The fully-qualified class name of the Java P runtime's PEvent class.
+        /// The fully-qualified class name of the Java P runtime's Event class.
         /// </summary>
-        internal static readonly string PEventsClass = "prt.events.PEvent";
+        internal static readonly string EventsClass = "prt.events.Event";
 
         #endregion
 

Src/PCompiler/CompilerCore/Backend/Java/EventGenerator.cs

@@ -28,9 +28,9 @@ protected override void GenerateCodeImpl()
         }
 
 
-        private IEnumerable<PEvent> monitoredEvents(IEnumerable<Machine> machines)
+        private IEnumerable<Event> monitoredEvents(IEnumerable<Machine> machines)
         {
-            var events = new HashSet<PEvent>();
+            var events = new HashSet<Event>();
 
             foreach (var m in machines.Where(m => m.IsSpec))
             {
@@ -43,15 +43,15 @@ private IEnumerable<PEvent> monitoredEvents(IEnumerable<Machine> machines)
             return events;
         }
 
-        private void WriteEventDecl(PEvent e)
+        private void WriteEventDecl(Event e)
         {
             var eventName = Names.GetNameForDecl(e);
             var argType = Types.JavaTypeFor(e.PayloadType);
 
             var payloadType = argType.TypeName;
             var payloadRefType = argType.ReferenceTypeName;
 
-            WriteLine($"public static class {eventName} extends {Constants.PEventsClass}<{payloadRefType}> implements Serializable {{");
+            WriteLine($"public static class {eventName} extends {Constants.EventsClass}<{payloadRefType}> implements Serializable {{");
 
             var hasPayload = !(argType is TypeManager.JType.JVoid);
             if (hasPayload)

Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs

@@ -316,7 +316,7 @@ private void WriteStateBuilderEntryHandler(Function f)
             WriteLine($".withEntry(this::{fname})");
         }
 
-        private void WriteStateBuilderEventHandler(PEvent e, IStateAction a)
+        private void WriteStateBuilderEventHandler(Event e, IStateAction a)
         {
             var ename = $"{Constants.EventNamespaceName}.{Names.GetNameForDecl(e)}";
 
@@ -492,7 +492,7 @@ private void WriteStmt(IPStmt stmt)
 
                 case RaiseStmt raiseStmt:
                     Write($"{Constants.TryRaiseEventMethodName}(new ");
-                    WriteExpr(raiseStmt.PEvent);
+                    WriteExpr(raiseStmt.Event);
                     Write("(");
                     foreach (var (sep, expr) in raiseStmt.Payload.WithPrefixSep(", "))
                     {

Src/PCompiler/CompilerCore/Backend/Java/NameManager.cs

@@ -95,9 +95,9 @@ protected override string ComputeNameForDecl(IPDecl decl)
 
             switch (decl)
             {
-                case PEvent { IsNullEvent: true }:
+                case Event { IsNullEvent: true }:
                     return "DefaultEvent";
-                case PEvent { IsHaltEvent: true }:
+                case Event { IsHaltEvent: true }:
                     return "PHalt";
                 case Interface i:
                     name = "I_" + i.Name;

Src/PCompiler/CompilerCore/Backend/Java/TypeManager.cs

@@ -102,7 +102,7 @@ internal string ReferenceTypeName
 
             internal class JAny : JType
             {
-                /// A JAny can either be a PEvent, a PValue, or a collection type like ArrayList, HashSet, etc.
+                /// A JAny can either be a Event, a PValue, or a collection type like ArrayList, HashSet, etc.
                 /// For a complete list, see the implementation of `deepEquals()` and `deepClone` in the P java runtime:
                 internal JAny()
                 {
@@ -304,7 +304,7 @@ internal class JEvent : JType
             {
                 internal JEvent()
                 {
-                    _unboxedType = $"{Constants.PEventsClass}<?>";
+                    _unboxedType = $"{Constants.EventsClass}<?>";
                 }
                 internal override bool IsPrimitive => false;
             }