Merging PEvent with Event

p-org · Aug 22, 2024 · bcacbc7 · bcacbc7
1 parent 1567407
commit bcacbc7
Show file tree

Hide file tree

Showing 52 changed files with 196 additions and 216 deletions.
diff --git a/Src/PChecker/CheckerCore/PRuntime/PEvent.cs b/Src/PChecker/CheckerCore/PRuntime/PEvent.cs
diff --git a/Src/PChecker/CheckerCore/PRuntime/PMachine.cs b/Src/PChecker/CheckerCore/PRuntime/PMachine.cs
@@ -58,7 +58,7 @@ protected override OnExceptionOutcome OnException(Exception ex, string methodNam
                     : base.OnException(ex, methodName, e);
             }
 
-            return (ex as UnhandledEventException).UnhandledEvent is PHalt
+            return (ex as UnhandledEventException).UnhandledEvent is Halt
                 ? OnExceptionOutcome.Halt
                 : base.OnException(ex, methodName, e);
         }
@@ -182,7 +182,7 @@ public void Log(string message)
         public void Announce(Event ev, object payload = null)
         {
             Assert(ev != null, "Machine cannot announce a null event");
-            if (ev is PHalt)
+            if (ev is Halt)
             {
                 ev = HaltEvent.Instance;
             }
@@ -251,7 +251,7 @@ public object ToDict()
             }
         }
 
-        public class InitializeParametersEvent : PEvent
+        public class InitializeParametersEvent : Event
         {
             public InitializeParametersEvent(InitializeParameters payload) : base(payload)
             {

diff --git a/Src/PChecker/CheckerCore/StateMachines/Events/DefaultEvent.cs b/Src/PChecker/CheckerCore/StateMachines/Events/DefaultEvent.cs
@@ -21,7 +21,6 @@ public sealed class DefaultEvent : Event
         /// Initializes a new instance of the <see cref="DefaultEvent"/> class.
         /// </summary>
         private DefaultEvent()
-            : base()
         {
         }
     }

diff --git a/Src/PChecker/CheckerCore/StateMachines/Events/Event.cs b/Src/PChecker/CheckerCore/StateMachines/Events/Event.cs
@@ -1,15 +1,56 @@
-// Copyright (c) Microsoft Corporation.
-// Licensed under the MIT License.
-
-using System.Runtime.Serialization;
+using System;
+using PChecker.PRuntime.Values;
 
 namespace PChecker.StateMachines.Events
 {
-    /// <summary>
-    /// Abstract 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 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 Halt : Event
     {
+        public Halt(IPrtValue payload) : base(payload)
+        {
+        }
     }
 }
diff --git a/Src/PChecker/CheckerCore/StateMachines/Events/GotoStateEvent.cs b/Src/PChecker/CheckerCore/StateMachines/Events/GotoStateEvent.cs
@@ -22,7 +22,6 @@ internal sealed class GotoStateEvent : Event
         /// </summary>
         /// <param name="s">Type of the state.</param>
         public GotoStateEvent(Type s)
-            : base()
         {
             State = s;
         }

diff --git a/Src/PChecker/CheckerCore/StateMachines/Events/HaltEvent.cs b/Src/PChecker/CheckerCore/StateMachines/Events/HaltEvent.cs
@@ -20,7 +20,6 @@ public sealed class HaltEvent : Event
         /// Initializes a new instance of the <see cref="HaltEvent"/> class.
         /// </summary>
         private HaltEvent()
-            : base()
         {
         }
     }

diff --git a/Src/PChecker/CheckerCore/StateMachines/Events/WildcardEvent.cs b/Src/PChecker/CheckerCore/StateMachines/Events/WildcardEvent.cs
@@ -15,7 +15,6 @@ public sealed class WildCardEvent : Event
         /// Initializes a new instance of the <see cref="WildCardEvent"/> class.
         /// </summary>
         public WildCardEvent()
-            : base()
         {
         }
     }

diff --git a/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogJsonFormatter.cs b/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();
         }
 

diff --git a/Src/PChecker/CheckerCore/StateMachines/Logging/PCheckerLogTextFormatter.cs b/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}";

diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs b/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 @event)
         {
             WriteNameSpacePrologue(context, output);
 
-            var declName = context.Names.GetNameForDecl(pEvent);
+            var declName = context.Names.GetNameForDecl(@event);
 
             // initialize the payload type
-            var payloadType = GetCSharpType(pEvent.PayloadType, true);
-            context.WriteLine(output, $"internal partial class {declName} : PEvent");
+            var payloadType = GetCSharpType(@event.PayloadType, true);
+            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;");
                 }
             }
@@ -1004,14 +1004,14 @@ private void WriteStmt(CompilationContext context, StringWriter output, Function
                     var eventName = context.Names.GetTemporaryName("recvEvent");
                     var eventTypeNames = receiveStmt.Cases.Keys.Select(evt => context.Names.GetNameForDecl(evt))
                         .ToHashSet();
-                    eventTypeNames.Add("PHalt"); // halt as a special case for receive
+                    eventTypeNames.Add("Halt"); // halt as a special case for receive
                     var recvArgs = string.Join(", ", eventTypeNames.Select(name => $"typeof({name})"));
                     context.WriteLine(output, $"var {eventName} = await currentMachine.TryReceiveEvent({recvArgs});");
                     context.WriteLine(output, $"switch ({eventName}) {{");
                     // add halt as a special case if doesnt exist
-                    if (receiveStmt.Cases.All(kv => kv.Key.Name != "PHalt"))
+                    if (receiveStmt.Cases.All(kv => kv.Key.Name != "Halt"))
                     {
-                        context.WriteLine(output,"case PHalt _hv: { currentMachine.TryRaiseEvent(_hv); break;} ");
+                        context.WriteLine(output,"case Halt _hv: { currentMachine.TryRaiseEvent(_hv); break;} ");
 
                     }
 
@@ -1386,7 +1386,7 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr p
                     switch (eventName)
                     {
                         case "Halt":
-                            context.Write(output, "new PHalt()");
+                            context.Write(output, "new Halt()");
                             break;
 
                         case "DefaultEvent":
@@ -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";

diff --git a/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpNameManager.cs b/Src/PCompiler/CompilerCore/Backend/CSharp/CSharpNameManager.cs
@@ -49,12 +49,12 @@ 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";
                     }
-                    return pEvent.IsHaltEvent ? "PHalt" : name;
+                    return pEvent.IsHaltEvent ? "Halt" : name;
 
 
                 case State pState:

diff --git a/Src/PCompiler/CompilerCore/Backend/Debugging/IrToPseudoP.cs b/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 ",

diff --git a/Src/PCompiler/CompilerCore/Backend/Java/Constants.cs b/Src/PCompiler/CompilerCore/Backend/Java/Constants.cs
@@ -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 PEventsClass = "prt.events.Event";
 
         #endregion
 

diff --git a/Src/PCompiler/CompilerCore/Backend/Java/EventGenerator.cs b/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,7 +43,7 @@ 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);

diff --git a/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs b/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)}";
 

diff --git a/Src/PCompiler/CompilerCore/Backend/Java/NameManager.cs b/Src/PCompiler/CompilerCore/Backend/Java/NameManager.cs
@@ -95,10 +95,10 @@ protected override string ComputeNameForDecl(IPDecl decl)
 
             switch (decl)
             {
-                case PEvent { IsNullEvent: true }:
+                case Event { IsNullEvent: true }:
                     return "DefaultEvent";
-                case PEvent { IsHaltEvent: true }:
-                    return "PHalt";
+                case Event { IsHaltEvent: true }:
+                    return "Halt";
                 case Interface i:
                     name = "I_" + i.Name;
                     break;

diff --git a/Src/PCompiler/CompilerCore/Backend/Java/TypeManager.cs b/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()
                 {