From b611e46695adba2807384dcfdfb5ae377cb55cc2 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Fri, 19 Apr 2024 19:43:55 +0000 Subject: [PATCH] [PExplicit] More reformatting --- .../pexplicit/runtime/PExplicitGlobal.java | 26 +++++++------------ .../pexplicit/runtime/logger/TextWriter.java | 2 +- .../pexplicit/runtime/machine/PMachine.java | 18 +++++-------- .../runtime/machine/PTestDriver.java | 2 +- .../runtime/scheduler/Scheduler.java | 10 +++---- .../explicit/ExplicitSearchScheduler.java | 13 +++------- 6 files changed, 26 insertions(+), 45 deletions(-) diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/PExplicitGlobal.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/PExplicitGlobal.java index df120e9a7..9e337faed 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/PExplicitGlobal.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/PExplicitGlobal.java @@ -12,34 +12,40 @@ * Represents global data structures represented with a singleton class */ public class PExplicitGlobal { + /** + * Mapping from machine type to list of all machine instances + */ + @Getter + private static final Map, List> machineListByType = new HashMap<>(); + /** + * Set of machines + */ + @Getter + private static final SortedSet machineSet = new TreeSet<>(); /** * PModel **/ @Getter @Setter private static PModel model = null; - /** * Global configuration **/ @Getter @Setter private static PExplicitConfig config = null; - /** * Scheduler **/ @Getter @Setter private static Scheduler scheduler = null; - /** * Status of the run **/ @Getter @Setter private static STATUS status = STATUS.INCOMPLETE; - /** * Result of the run **/ @@ -47,18 +53,6 @@ public class PExplicitGlobal { @Setter private static String result = "error"; - /** - * Mapping from machine type to list of all machine instances - */ - @Getter - private static final Map, List> machineListByType = new HashMap<>(); - - /** - * Set of machines - */ - @Getter - private static final SortedSet machineSet = new TreeSet<>(); - /** * Get a machine of a given type and index if exists, else return null. * diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/TextWriter.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/TextWriter.java index d358ea096..55a54efb6 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/TextWriter.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/logger/TextWriter.java @@ -8,10 +8,10 @@ import java.io.PrintWriter; public class TextWriter { + private static final int logIdx = 0; static PrintWriter log = null; @Getter static String fileName = ""; - private static final int logIdx = 0; public static void Initialize() { try { diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/PMachine.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/PMachine.java index 56773807c..109dc0a40 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/PMachine.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/PMachine.java @@ -29,31 +29,25 @@ public abstract class PMachine implements Serializable, Comparable { @Getter private static final Map nameToMachine = new HashMap<>(); protected static int globalMachineId = mainMachineId; - - @Getter - protected int instanceId; @Getter protected final int typeId; @Getter protected final String name; - private final Set states; private final State startState; - @Getter - private State currentState; - @Getter private final SenderQueue sendBuffer; private final DeferQueue deferQueue; - + @Getter + private final Map continuationMap = new TreeMap<>(); + @Getter + protected int instanceId; + @Getter + private State currentState; @Getter private boolean started = false; @Getter private boolean halted = false; - - @Getter - private final Map continuationMap = new TreeMap<>(); - private PContinuation blockedBy = null; @Getter private State blockedStateExit; diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/PTestDriver.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/PTestDriver.java index 39e151964..516bbb539 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/PTestDriver.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/machine/PTestDriver.java @@ -12,9 +12,9 @@ * Represents the base class for a P test driver. */ public abstract class PTestDriver implements Serializable { - public PMachine mainMachine; public final List monitorList; public final Map> observerMap; + public PMachine mainMachine; /** * Test driver constructor diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Scheduler.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Scheduler.java index e3eb4c5de..f57bba3ef 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Scheduler.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Scheduler.java @@ -22,17 +22,15 @@ * Represents the base class that all schedulers extend. */ public abstract class Scheduler implements SchedulerInterface { + /** + * Current schedule + */ + public final Schedule schedule; /** * Current step state */ @Getter protected StepState stepState = new StepState(); - - /** - * Current schedule - */ - public final Schedule schedule; - /** * Whether done with current iteration */ diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java index 24fac2dbf..808608a0e 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java @@ -27,34 +27,29 @@ * Represents the scheduler for performing explicit-state model checking */ public class ExplicitSearchScheduler extends Scheduler { + /** + * Map from state hash to iteration when first visited + */ + private final transient Map stateCache = new HashMap<>(); /** * Backtrack choice number */ @Getter private transient int backtrackChoiceNumber = 0; - /** * Whether done with all iterations */ private transient boolean isDoneIterating = false; - /** * Whether to skip liveness check (because of early schedule termination due to state caching) */ private transient boolean skipLiveness = false; - /** * Time of last status report */ @Getter @Setter private transient Instant lastReportTime = Instant.now(); - - /** - * Map from state hash to iteration when first visited - */ - private final transient Map stateCache = new HashMap<>(); - private transient StepState storedStep; /**