[PEx] Adds writing buggy trace in file

Adds serializing buggy trace in file

Minor renaming

Author: aman-goel

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java

@@ -100,6 +100,10 @@ private static void process(boolean resume) throws Exception {
             PExplicitGlobal.setResult(String.format("found cex of length %d", scheduler.getStepNumber()));
             PExplicitLogger.logStackTrace(e);
 
+            String schFile = PExplicitGlobal.getConfig().getOutputFolder() + "/" + PExplicitGlobal.getConfig().getProjectName() + "_0_0.schedule";
+            PExplicitLogger.logInfo(String.format("Writing buggy trace in %s", schFile));
+            scheduler.schedule.writeToFile(schFile);
+
             ReplayScheduler replayer = new ReplayScheduler(scheduler.schedule);
             PExplicitGlobal.setScheduler(replayer);
             try {

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/PExplicitLogger.java

@@ -13,6 +13,7 @@
 import pexplicit.runtime.machine.PMonitor;
 import pexplicit.runtime.machine.State;
 import pexplicit.runtime.machine.events.PContinuation;
+import pexplicit.runtime.scheduler.Schedule;
 import pexplicit.runtime.scheduler.choice.ScheduleSearchUnit;
 import pexplicit.runtime.scheduler.choice.SearchUnit;
 import pexplicit.runtime.scheduler.explicit.ExplicitSearchScheduler;
@@ -167,6 +168,17 @@ public static void logNewTasks(List<SearchTask> tasks) {
         }
     }
 
+    /**
+     * Log when serializing a schedule
+     *
+     * @param schedule Schedule to serialize
+     * @param szBytes Bytes written
+     */
+    public static void logSerializeSchedule(Schedule schedule, String fileName, long szBytes) {
+        if (verbosity > 1) {
+        }
+    }
+
     /**
      * Log when serializing a task
      *

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/ScheduleWriter.java

@@ -21,7 +21,7 @@ public class ScheduleWriter {
     public static void Initialize() {
         try {
             // get new file name
-            fileName = PExplicitGlobal.getConfig().getOutputFolder() + "/" + PExplicitGlobal.getConfig().getProjectName() + "_0_0.schedule";
+            fileName = PExplicitGlobal.getConfig().getOutputFolder() + "/" + PExplicitGlobal.getConfig().getProjectName() + "_0_0.steps";
             // Define new file printer
             File schFile = new File(fileName);
             schFile.getParentFile().mkdirs();

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java

@@ -3,6 +3,7 @@
 import lombok.Getter;
 import lombok.Setter;
 import pexplicit.runtime.PExplicitGlobal;
+import pexplicit.runtime.logger.PExplicitLogger;
 import pexplicit.runtime.machine.PMachineId;
 import pexplicit.runtime.scheduler.choice.Choice;
 import pexplicit.runtime.scheduler.choice.DataChoice;
@@ -11,7 +12,12 @@
 import pexplicit.runtime.scheduler.explicit.StepState;
 import pexplicit.values.PValue;
 
+import java.io.FileOutputStream;
+import java.io.IOException;
+import java.io.ObjectOutputStream;
 import java.io.Serializable;
+import java.nio.file.Files;
+import java.nio.file.Paths;
 import java.util.ArrayList;
 import java.util.List;
 
@@ -146,4 +152,14 @@ public void clear() {
     public int size() {
         return choices.size();
     }
+
+    public void writeToFile(String fileName) {
+        try {
+            FileOutputStream fos = new FileOutputStream(fileName);
+            ObjectOutputStream oos = new ObjectOutputStream(fos);
+            oos.writeObject(this);
+        } catch (IOException e) {
+            throw new RuntimeException("Failed to write schedule in file " + fileName, e);
+        }
+    }
 }

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java

@@ -475,7 +475,7 @@ private void setChildTask(SearchUnit unit, int choiceNum, SearchTask parentTask,
             newTask.addPrefixChoice(schedule.getChoice(i));
         }
 
-        newTask.serializeTask();
+        newTask.writeToFile();
         parentTask.addChild(newTask);
         searchStrategy.addNewTask(newTask);
     }

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchStrategy.java

@@ -76,7 +76,7 @@ public SearchTask setNextTask() {
         }
 
         SearchTask nextTask = popNextTask();
-        nextTask.deserializeTask();
+        nextTask.readFromFile();
         setCurrTask(nextTask);
 
         return nextTask;

Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/strategy/SearchTask.java

@@ -239,7 +239,7 @@ public static void Cleanup() {
         }
     }
 
-    public void serializeTask() {
+    public void writeToFile() {
         assert (serializeFile == null);
         assert (prefixChoices != null);
         assert (searchUnits != null);
@@ -260,7 +260,7 @@ public void serializeTask() {
         searchUnits = null;
     }
 
-    public void deserializeTask() {
+    public void readFromFile() {
         assert (serializeFile != null);
         assert (prefixChoices == null);
         assert (searchUnits == null);