Rename PEvent to Event, Handle PrimitiveType.Null in GetDefaultValue

Author: Aishwarya Jagarapu

Src/PCompiler/CompilerCore/Backend/PEx/PExCodeGenerator.cs

@@ -1926,9 +1926,9 @@ private string GetPExType(PLanguageType type)
             case EnumType enumType:
                 return "PEnum";
             case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Event):
-                return "PEvent";
+                return "Event";
             case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Null):
-                return "void";
+                return "PValue";
             case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Any):
                 return "PValue<?>";
             default:
@@ -2006,6 +2006,7 @@ private string GetDefaultValue(PLanguageType type)
 
                 return $"new {GetPExType(type)}(\"{enumType.OriginalRepresentation}\", \"{minName}\", {minValue})";
             }
+            case PrimitiveType nullType when nullType.IsSameTypeAs(PrimitiveType.Null):
             case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Event):
                 return "null";
             case PrimitiveType primitiveType when primitiveType.IsSameTypeAs(PrimitiveType.Any):

Src/PRuntimes/PExRuntime/pom.xml

@@ -148,7 +148,7 @@
                         <schedules/>
                         <max.steps/>
                     </systemPropertyVariables>
-                    <systemProperties>
+                    <systemPropertyVariables>
                         <property>
                             <name>mode</name>
                             <value/>
@@ -157,7 +157,7 @@
                             <name>pex.args</name>
                             <value/>
                         </property>
-                    </systemProperties>
+                    </systemPropertyVariables>
                 </configuration>
             </plugin>
             <plugin>

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/logger/SchedulerLogger.java

@@ -20,7 +20,7 @@
 import pex.runtime.scheduler.explicit.strategy.SearchTask;
 import pex.runtime.scheduler.replay.ReplayScheduler;
 import pex.values.ComputeHash;
-import pex.values.PEvent;
+import pex.values.Event;
 import pex.values.PMessage;
 import pex.values.PValue;
 
@@ -354,7 +354,7 @@ public void logStateExit(PMachine machine) {
         }
     }
 
-    public void logRaiseEvent(PMachine machine, PEvent event) {
+    public void logRaiseEvent(PMachine machine, Event event) {
         PExGlobal.getScheduler().updateLogNumber();
         if (typedLogEnabled()) {
             typedLog(LogType.RaiseLog, String.format("%s raised event %s in state %s.", machine, event, machine.getCurrentState()));
@@ -372,7 +372,7 @@ public void logReceive(PMachine machine, PContinuation continuation) {
         PExGlobal.getScheduler().updateLogNumber();
         if (typedLogEnabled()) {
             typedLog(LogType.ReceiveLog, String.format("%s is waiting to dequeue an event of type %s or %s in state %s.",
-                    machine, continuation.getCaseEvents(), PEvent.haltEvent, machine.getCurrentState()));
+                    machine, continuation.getCaseEvents(), Event.haltEvent, machine.getCurrentState()));
         }
     }
 

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/PMachine.java

@@ -10,7 +10,7 @@
 import pex.utils.exceptions.BugFoundException;
 import pex.utils.misc.Assert;
 import pex.utils.serialize.SerializableBiFunction;
-import pex.values.PEvent;
+import pex.values.Event;
 import pex.values.PMachineValue;
 import pex.values.PMessage;
 import pex.values.PValue;
@@ -87,7 +87,7 @@ public PMachine(String name, int id, State startState, State... states) {
 
         // register create machine handler
         startState.registerHandlers(
-                new EventHandler(PEvent.createMachine) {
+                new EventHandler(Event.createMachine) {
                     @Override
                     public void handleEvent(PMachine target, PValue<?> payload) {
                         assert (!target.isStarted());
@@ -364,7 +364,7 @@ public PMachineValue create(
             PValue<?> payload) {
         Class<? extends PMachine> trueMachineType = PExGlobal.getModel().getTestDriver().interfaceMap.getOrDefault(machineType, machineType);
         PMachine machine = PExGlobal.getScheduler().allocateMachine(trueMachineType);
-        PMessage msg = new PMessage(PEvent.createMachine, machine, payload);
+        PMessage msg = new PMessage(Event.createMachine, machine, payload);
         sendBuffer.add(msg);
         return new PMachineValue(machine);
     }
@@ -384,10 +384,10 @@ public PMachineValue create(
      * Send an event to a target machine
      *
      * @param target  Target machine
-     * @param event   PEvent to send
+     * @param event   Event to send
      * @param payload Payload corresponding to the event
      */
-    public void sendEvent(PMachineValue target, PEvent event, PValue<?> payload) {
+    public void sendEvent(PMachineValue target, Event event, PValue<?> payload) {
         if (PValue.isEqual(target, null)) {
             throw new BugFoundException("Machine in send event cannot be null.");
         }
@@ -481,7 +481,7 @@ public void clearBlocked() {
         blockedBy = null;
     }
 
-    public boolean isDeferred(PEvent event) {
+    public boolean isDeferred(Event event) {
         if (currentState.isDeferred(event)) {
             return true;
         }
@@ -553,7 +553,7 @@ void processEvent(PMessage message) {
      * @param message Message to process
      */
     void runEvent(PMessage message) {
-        PEvent event = message.getEvent();
+        Event event = message.getEvent();
         if (isBlocked()) {
             PContinuation currBlockedBy = this.blockedBy;
             clearBlocked();
@@ -583,7 +583,7 @@ void runEvent(PMessage message) {
      * @param event   Event to raise
      * @param payload Payload
      */
-    public void raiseEvent(PEvent event, PValue<?> payload) {
+    public void raiseEvent(Event event, PValue<?> payload) {
         // do nothing if already halted
         if (isHalted()) {
             return;
@@ -610,7 +610,7 @@ public void raiseEvent(PEvent event, PValue<?> payload) {
      *
      * @param event Event to raise
      */
-    public void raiseEvent(PEvent event) {
+    public void raiseEvent(Event event) {
         raiseEvent(event, null);
     }
 
@@ -676,7 +676,7 @@ public void enterNewState(State newState, PValue<?> payload) {
         newState.entry(this, payload);
     }
 
-    private void addObservedEvent(PEvent newEvent) {
+    private void addObservedEvent(Event newEvent) {
         for (String happenedBeforeEvent : observedEvents) {
             happensBeforePairs.add(String.format("(%s,%s)", happenedBeforeEvent, newEvent));
         }

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/PTestDriver.java

@@ -1,6 +1,6 @@
 package pex.runtime.machine;
 
-import pex.values.PEvent;
+import pex.values.Event;
 
 import java.io.Serializable;
 import java.util.ArrayList;
@@ -15,7 +15,7 @@ public abstract class PTestDriver implements Serializable {
     // TODO: pex parallel - make fields thread safe
     public final Map<Class<? extends PMachine>, Class<? extends PMachine>> interfaceMap;
     public final List<Class<? extends PMachine>> monitorList;
-    public final Map<PEvent, List<Class<? extends PMachine>>> observerMap;
+    public final Map<Event, List<Class<? extends PMachine>>> observerMap;
     public Class<? extends PMachine> mainMachine;
 
     /**
@@ -52,7 +52,7 @@ public List<Class<? extends PMachine>> getMonitors() {
      *
      * @return Map from event to list of monitors listening/observing that event
      */
-    public Map<PEvent, List<Class<? extends PMachine>>> getListeners() {
+    public Map<Event, List<Class<? extends PMachine>>> getListeners() {
         return observerMap;
     }
 

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/State.java

@@ -5,7 +5,7 @@
 import pex.runtime.machine.eventhandlers.IgnoreEventHandler;
 import pex.runtime.machine.events.StateEvents;
 import pex.utils.misc.Assert;
-import pex.values.PEvent;
+import pex.values.Event;
 import pex.values.PMessage;
 import pex.values.PValue;
 
@@ -86,7 +86,7 @@ public void registerHandlers(EventHandler... eventHandlers) {
      * @param event Event to check
      * @return true if event is ignored in this state, else false
      */
-    public boolean isIgnored(PEvent event) {
+    public boolean isIgnored(Event event) {
         return stateEvents.ignored.contains(event);
     }
 
@@ -96,7 +96,7 @@ public boolean isIgnored(PEvent event) {
      * @param event Event to check
      * @return true if event is deferred in this state, else false
      */
-    public boolean isDeferred(PEvent event) {
+    public boolean isDeferred(Event event) {
         return stateEvents.deferred.contains(event);
     }
 

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/buffer/EventBuffer.java

@@ -1,7 +1,7 @@
 package pex.runtime.machine.buffer;
 
 import pex.runtime.machine.PMachine;
-import pex.values.PEvent;
+import pex.values.Event;
 import pex.values.PValue;
 
 /**
@@ -15,5 +15,5 @@ public interface EventBuffer {
      * @param event   Event
      * @param payload Event payload
      */
-    void send(PMachine target, PEvent event, PValue<?> payload);
+    void send(PMachine target, Event event, PValue<?> payload);
 }

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/buffer/SenderQueue.java

@@ -2,7 +2,7 @@
 
 import pex.runtime.machine.PMachine;
 import pex.utils.exceptions.NotImplementedException;
-import pex.values.PEvent;
+import pex.values.Event;
 import pex.values.PValue;
 
 import java.io.Serializable;
@@ -28,7 +28,7 @@ public SenderQueue(PMachine owner) {
      * @param eventName Event
      * @param payload   Event payload
      */
-    public void send(PMachine target, PEvent eventName, PValue<?> payload) {
+    public void send(PMachine target, Event eventName, PValue<?> payload) {
         throw new NotImplementedException();
     }
 

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/eventhandlers/DeferEventHandler.java

@@ -3,7 +3,7 @@
 
 import pex.runtime.machine.PMachine;
 import pex.utils.exceptions.NotImplementedException;
-import pex.values.PEvent;
+import pex.values.Event;
 import pex.values.PValue;
 
 /**
@@ -16,7 +16,7 @@ public class DeferEventHandler extends EventHandler {
      *
      * @param event Event to defer
      */
-    public DeferEventHandler(PEvent event) {
+    public DeferEventHandler(Event event) {
         super(event);
     }
 

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/eventhandlers/EventHandler.java

@@ -1,7 +1,7 @@
 package pex.runtime.machine.eventhandlers;
 
 import pex.runtime.machine.PMachine;
-import pex.values.PEvent;
+import pex.values.Event;
 import pex.values.PValue;
 
 import java.io.Serializable;
@@ -10,14 +10,14 @@
  * Represents the base class for all event handlers
  */
 public abstract class EventHandler implements Serializable {
-    public final PEvent event;
+    public final Event event;
 
     /**
      * Constructor
      *
      * @param event Event corresponding to the handler
      */
-    protected EventHandler(PEvent event) {
+    protected EventHandler(Event event) {
         this.event = event;
     }
 

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/eventhandlers/GotoEventHandler.java

@@ -2,7 +2,7 @@
 
 import pex.runtime.machine.PMachine;
 import pex.runtime.machine.State;
-import pex.values.PEvent;
+import pex.values.Event;
 import pex.values.PValue;
 
 /**
@@ -17,7 +17,7 @@ public class GotoEventHandler extends EventHandler {
      * @param event Event
      * @param dest  Destination state
      */
-    public GotoEventHandler(PEvent event, State dest) {
+    public GotoEventHandler(Event event, State dest) {
         super(event);
         this.gotoState = dest;
     }

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/eventhandlers/IgnoreEventHandler.java

@@ -1,7 +1,7 @@
 package pex.runtime.machine.eventhandlers;
 
 import pex.runtime.machine.PMachine;
-import pex.values.PEvent;
+import pex.values.Event;
 import pex.values.PValue;
 
 /**
@@ -14,7 +14,7 @@ public class IgnoreEventHandler extends EventHandler {
      *
      * @param event Event
      */
-    public IgnoreEventHandler(PEvent event) {
+    public IgnoreEventHandler(Event event) {
         super(event);
     }
 

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/events/PContinuation.java

@@ -4,7 +4,7 @@
 import pex.runtime.machine.PMachine;
 import pex.runtime.machine.State;
 import pex.utils.serialize.SerializableBiFunction;
-import pex.values.PEvent;
+import pex.values.Event;
 import pex.values.PMessage;
 import pex.values.PValue;
 
@@ -53,7 +53,7 @@ public void clearVars() {
         }
     }
 
-    public boolean isDeferred(PEvent event) {
+    public boolean isDeferred(Event event) {
         return !event.isHaltMachineEvent() && !caseEvents.contains(event.toString());
     }
 

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/events/StateEvents.java

@@ -1,7 +1,7 @@
 package pex.runtime.machine.events;
 
 import pex.runtime.machine.eventhandlers.EventHandler;
-import pex.values.PEvent;
+import pex.values.Event;
 
 import java.io.Serializable;
 import java.util.HashMap;
@@ -13,9 +13,9 @@
  * Stores details about all events corresponding to a state
  */
 public class StateEvents implements Serializable {
-    public final Map<PEvent, EventHandler> eventHandlers;
-    public final Set<PEvent> ignored;
-    public final Set<PEvent> deferred;
+    public final Map<Event, EventHandler> eventHandlers;
+    public final Set<Event> ignored;
+    public final Set<Event> deferred;
 
     /**
      * Constructor

Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/scheduler/Scheduler.java

@@ -236,7 +236,7 @@ public void startMachine(Class<? extends PMachine> machineType) {
         PMachine machine = allocateMachine(machineType);
 
         // run create machine event
-        processCreateEvent(new PMessage(PEvent.createMachine, machine, null));
+        processCreateEvent(new PMessage(Event.createMachine, machine, null));
     }
 
     /**
@@ -380,7 +380,7 @@ public void processDequeueEvent(PMachine sender, PMessage message) {
      * @param event   Event to announce
      * @param payload Event payload
      */
-    public void announce(PEvent event, PValue<?> payload) {
+    public void announce(Event event, PValue<?> payload) {
         if (event == null) {
             throw new NotImplementedException("Machine cannot announce a null event");
         }