Skip to content

Commit

Permalink
[PExplicit] More reformatting
Browse files Browse the repository at this point in the history
  • Loading branch information
aman-goel committed Apr 19, 2024
1 parent 9964710 commit b611e46
Show file tree
Hide file tree
Showing 6 changed files with 26 additions and 45 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -12,53 +12,47 @@
* 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<Class<? extends PMachine>, List<PMachine>> machineListByType = new HashMap<>();
/**
* Set of machines
*/
@Getter
private static final SortedSet<PMachine> 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
**/
@Getter
@Setter
private static String result = "error";

/**
* Mapping from machine type to list of all machine instances
*/
@Getter
private static final Map<Class<? extends PMachine>, List<PMachine>> machineListByType = new HashMap<>();

/**
* Set of machines
*/
@Getter
private static final SortedSet<PMachine> machineSet = new TreeSet<>();

/**
* Get a machine of a given type and index if exists, else return null.
*
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -29,31 +29,25 @@ public abstract class PMachine implements Serializable, Comparable<PMachine> {
@Getter
private static final Map<String, PMachine> 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<State> states;
private final State startState;
@Getter
private State currentState;

@Getter
private final SenderQueue sendBuffer;
private final DeferQueue deferQueue;

@Getter
private final Map<String, PContinuation> 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<String, PContinuation> continuationMap = new TreeMap<>();

private PContinuation blockedBy = null;
@Getter
private State blockedStateExit;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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<PMonitor> monitorList;
public final Map<PEvent, List<PMonitor>> observerMap;
public PMachine mainMachine;

/**
* Test driver constructor
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
*/
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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<Object, Integer> 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<Object, Integer> stateCache = new HashMap<>();

private transient StepState storedStep;

/**
Expand Down

0 comments on commit b611e46

Please sign in to comment.