[PCover] Refactor and cleanup

Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/logger/ScheduleWriter.java

@@ -14,7 +14,6 @@
 import psym.utils.Assert;
 import psym.valuesummary.GuardedValue;
 import psym.valuesummary.PrimitiveVS;
-import psym.valuesummary.ValueSummary;
 
 public class ScheduleWriter {
     static PrintWriter log = null;

Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/Machine.java

@@ -24,8 +24,8 @@
 public abstract class Machine implements Serializable, Comparable<Machine> {
   @Getter
   private static final int mainMachineId = 2;
-  protected static int globalMachineId = mainMachineId;
   @Getter private static final Map<String, Machine> nameToMachine = new HashMap<>();
+  protected static int globalMachineId = mainMachineId;
   public final Map<
           String,
           SerializableFunction<

Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/events/Message.java

@@ -6,37 +6,20 @@
 import psym.runtime.machine.Machine;
 import psym.valuesummary.*;
 
-import javax.crypto.Mac;
-
 /** Represents a message in the sender buffer of a state machine */
 public class Message implements ValueSummary<Message> {
   @Getter
   /** Concrete hash used for hashing in explicit-state search */
   private final int concreteHash;
-
-  static class ConcreteMessage {
-    private final Machine target;
-    private final Event event;
-    private final Map<Event, Object> payload;
-
-    ConcreteMessage(Machine t, Event e, Map<Event, Object> p) {
-      target = t;
-      event = e;
-      payload = p;
-    }
-  }
-
   @Getter
   /** Concrete value used in explicit-state search */
   private final ConcreteMessage concreteValue;
-
   // the target machine to which the message is being sent
   private final PrimitiveVS<Machine> target;
   // the event sent to the target machine
   private final PrimitiveVS<Event> event;
   // the payload associated with the event
   private final Map<Event, UnionVS> payload;
-
   private Message(PrimitiveVS<Event> names, PrimitiveVS<Machine> machine, Map<Event, UnionVS> map) {
     assert (!machine.getValues().contains(null));
     this.event = names;
@@ -305,8 +288,8 @@ public int computeConcreteHash() {
 
   @Override
   public ConcreteMessage computeConcreteValue() {
-    Machine t = target == null ? null : (Machine) target.getConcreteValue();
-    Event e = event == null ? null : (Event) event.getConcreteValue();
+    Machine t = target == null ? null : target.getConcreteValue();
+    Event e = event == null ? null : event.getConcreteValue();
 
     Map<Event, Object> p = new HashMap<>();
     for (Map.Entry<Event, UnionVS> entry : payload.entrySet()) {
@@ -354,4 +337,16 @@ public String toStringDetailed() {
     out.append("]");
     return out.toString();
   }
+
+  static class ConcreteMessage {
+    private final Machine target;
+    private final Event event;
+    private final Map<Event, Object> payload;
+
+    ConcreteMessage(Machine t, Event e, Map<Event, Object> p) {
+      target = t;
+      event = e;
+      payload = p;
+    }
+  }
 }

Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/Scheduler.java

@@ -4,7 +4,6 @@
 import java.util.concurrent.TimeoutException;
 import java.util.function.Function;
 import java.util.stream.Collectors;
-
 import lombok.Getter;
 import psym.runtime.*;
 import psym.runtime.Program;
@@ -14,7 +13,6 @@
 import psym.runtime.machine.State;
 import psym.runtime.machine.events.Event;
 import psym.runtime.machine.events.Message;
-import psym.runtime.scheduler.search.symmetry.SymmetryMode;
 import psym.runtime.scheduler.search.symmetry.SymmetryTracker;
 import psym.runtime.statistics.SearchStats;
 import psym.utils.Assert;

Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/replay/ReplayScheduler.java

@@ -4,7 +4,6 @@
 import java.util.List;
 import java.util.concurrent.TimeoutException;
 import java.util.function.Function;
-
 import lombok.Getter;
 import org.apache.commons.lang3.NotImplementedException;
 import psym.runtime.PSymGlobal;

Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/explicit/ExplicitSymmetryTracker.java

@@ -1,7 +1,6 @@
 package psym.runtime.scheduler.search.explicit;
 
 import java.util.*;
-
 import lombok.Getter;
 import psym.runtime.PSymGlobal;
 import psym.runtime.machine.Machine;
@@ -187,9 +186,7 @@ public List<ValueSummary> getReducedChoices(List<ValueSummary> original, boolean
                 }
                 assert (machineRep != null);
 
-                if (!isData) {
-                  assert (!machineRep.getEventBuffer().isEmpty());
-                }
+                assert isData || (!machineRep.getEventBuffer().isEmpty());
                 pendingSummaries.add(machineRep);
               }
               added = true;

Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/symbolic/SymbolicSearchScheduler.java

@@ -20,7 +20,6 @@
 import psym.runtime.statistics.CoverageStats;
 import psym.runtime.statistics.SearchStats;
 import psym.runtime.statistics.SolverStats;
-import psym.utils.Assert;
 import psym.utils.monitor.MemoryMonitor;
 import psym.utils.monitor.TimeMonitor;
 import psym.valuesummary.Guard;

Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/symbolic/SymbolicSymmetryTracker.java

@@ -1,7 +1,6 @@
 package psym.runtime.scheduler.search.symbolic;
 
 import java.util.*;
-
 import psym.runtime.PSymGlobal;
 import psym.runtime.machine.Machine;
 import psym.runtime.machine.Monitor;

Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/symmetry/SymmetryTracker.java

@@ -2,9 +2,7 @@
 
 import java.io.Serializable;
 import java.util.*;
-import lombok.Setter;
 import psym.runtime.machine.Machine;
-import psym.runtime.scheduler.Scheduler;
 import psym.valuesummary.*;
 
 public abstract class SymmetryTracker implements Serializable {