Skip to content

Commit

Permalink
[PExplicit] Reformat code
Browse files Browse the repository at this point in the history
  • Loading branch information
aman-goel committed Apr 19, 2024
1 parent 5c76a2d commit 9964710
Show file tree
Hide file tree
Showing 10 changed files with 33 additions and 30 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,7 @@ public static void logEndOfRun(ExplicitSearchScheduler scheduler, long timeSpent
}
log.info(String.format("..... Explored %d distinct schedules", SearchStatistics.iteration));
log.info(String.format("..... Number of steps explored: %d (min), %d (avg), %d (max).",
SearchStatistics.minSteps, (SearchStatistics.totalSteps/SearchStatistics.iteration), SearchStatistics.maxSteps));
SearchStatistics.minSteps, (SearchStatistics.totalSteps / SearchStatistics.iteration), SearchStatistics.maxSteps));
log.info(String.format("... Elapsed %d seconds and used %.1f GB", timeSpent, MemoryMonitor.getMaxMemSpent() / 1000.0));
log.info(String.format(".. Result: " + PExplicitGlobal.getResult()));
log.info(". Done");
Expand All @@ -106,7 +106,7 @@ public static void logEndOfRun(ExplicitSearchScheduler scheduler, long timeSpent
/**
* Print error trace
*
* @param e Exception object
* @param e Exception object
*/
public static void logStackTrace(Exception e) {
StringWriter sw = new StringWriter();
Expand Down Expand Up @@ -333,7 +333,7 @@ public static void logDequeueEvent(PMachine machine, PMessage message) {
public static void logStartReplay() {
if (verbosity > 0) {
log.info("--------------------");
log.info(String.format("Replaying schedule"));
log.info("Replaying schedule");
}
}
}
Original file line number Diff line number Diff line change
@@ -1,8 +1,5 @@
package pexplicit.runtime.logger;

import java.io.File;
import java.io.IOException;
import java.io.PrintWriter;
import lombok.Getter;
import pexplicit.runtime.PExplicitGlobal;
import pexplicit.runtime.machine.PMachine;
Expand All @@ -11,9 +8,14 @@
import pexplicit.values.PInt;
import pexplicit.values.PValue;

import java.io.File;
import java.io.IOException;
import java.io.PrintWriter;

public class ScheduleWriter {
static PrintWriter log = null;
@Getter static String fileName = "";
@Getter
static String fileName = "";
private static int logIdx = 0;

public static void Initialize() {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ public class TextWriter {
static PrintWriter log = null;
@Getter
static String fileName = "";
private static int logIdx = 0;
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 @@ -82,7 +82,6 @@ public void runAfter(PMachine machine) {
}
} else {
// blocked on a different continuation encountered when processing pending new state entry function, do nothing
return;
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,8 @@
import pexplicit.values.PValue;

import java.io.Serializable;
import java.util.*;
import java.util.ArrayList;
import java.util.List;

/**
* Represents a single (possibly partial) schedule.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -325,7 +325,7 @@ public void announce(PEvent event, PValue<?> payload) {
* Check for deadlock at the end of a completed schedule
*/
public void checkDeadlock() {
for (PMachine machine: stepState.getMachineSet()) {
for (PMachine machine : stepState.getMachineSet()) {
if (machine.canRun() && machine.isBlocked()) {
throw new DeadlockException(String.format("Deadlock detected. %s is waiting to receive an event, but no other controlled tasks are enabled.", machine));
}
Expand All @@ -336,7 +336,7 @@ public void checkDeadlock() {
* Check for liveness at the end of a completed schedule
*/
public void checkLiveness(boolean terminated) {
for (PMachine monitor: PExplicitGlobal.getModel().getMonitors()) {
for (PMachine monitor : PExplicitGlobal.getModel().getMonitors()) {
if (monitor.getCurrentState().isHotState()) {
if (terminated) {
throw new LivenessException(String.format("Monitor %s detected liveness bug in hot state %s at the end of program execution", monitor, monitor.getCurrentState()));
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ public class ExplicitSearchScheduler extends Scheduler {
/**
* Map from state hash to iteration when first visited
*/
private transient Map<Object, Integer> stateCache = new HashMap<>();
private final transient Map<Object, Integer> stateCache = new HashMap<>();

private transient StepState storedStep;

Expand Down Expand Up @@ -224,6 +224,7 @@ boolean skipRemainingSchedule() {

/**
* Get the hashing key corresponding to the current protocol state
*
* @return
*/
Object getCurrentStateKey() {
Expand All @@ -235,7 +236,7 @@ Object getCurrentStateKey() {
} else {
// use exact values from each machine vars
List<List<Object>> machineValues = new ArrayList<>();
for (PMachine machine: stepState.getMachineSet()) {
for (PMachine machine : stepState.getMachineSet()) {
machineValues.add(machine.getLocalVarValues());
}
stateKey = machineValues;
Expand Down Expand Up @@ -373,7 +374,7 @@ private void postIterationCleanup() {
backtrackChoiceNumber = cIdx;
int newStepNumber = 0;
if (PExplicitGlobal.getConfig().isStatefulBacktrackEnabled()) {
StepState choiceStep = choice.getChoiceStep();
StepState choiceStep = choice.getChoiceStep();
if (choiceStep != null) {
newStepNumber = choice.getChoiceStep().getStepNumber();
}
Expand Down Expand Up @@ -454,19 +455,19 @@ public void recordStats() {
}
StatWriter.log("steps-min", String.format("%d", SearchStatistics.minSteps));
StatWriter.log("steps-max", String.format("%d", SearchStatistics.maxSteps));
StatWriter.log("steps-avg", String.format("%d", SearchStatistics.totalSteps/SearchStatistics.iteration));
StatWriter.log("steps-avg", String.format("%d", SearchStatistics.totalSteps / SearchStatistics.iteration));
StatWriter.log("#-choices-unexplored", String.format("%d", schedule.getNumUnexploredChoices()));
StatWriter.log("%-choices-unexplored-data", String.format("%.1f", schedule.getUnexploredDataChoicesPercent()));
}

private void printCurrentStatus(double newRuntime) {

String s = "--------------------" +
String.format("\n Status after %.2f seconds:", newRuntime) +
String.format("\n Memory: %.2f MB", MemoryMonitor.getMemSpent()) +
String.format("\n Depth: %d", stepState.getStepNumber()) +
String.format("\n Schedules: %d", SearchStatistics.iteration) +
String.format("\n Unexplored: %d", schedule.getNumUnexploredChoices());
String.format("\n Status after %.2f seconds:", newRuntime) +
String.format("\n Memory: %.2f MB", MemoryMonitor.getMemSpent()) +
String.format("\n Depth: %d", stepState.getStepNumber()) +
String.format("\n Schedules: %d", SearchStatistics.iteration) +
String.format("\n Unexplored: %d", schedule.getNumUnexploredChoices());
if (PExplicitGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) {
s += String.format("\n DistinctStates: %d", SearchStatistics.totalDistinctStates);
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ public StepState copy() {
public void resetToZero() {
this.stepNumber = 0;
this.choiceNumber = 0;
for (PMachine machine: PExplicitGlobal.getMachineSet()) {
for (PMachine machine : PExplicitGlobal.getMachineSet()) {
machine.reset();
}
machineListByType.clear();
Expand All @@ -76,7 +76,7 @@ public void setTo(StepState input) {
machineLocalStates = input.machineLocalStates;

int i = 0;
for (PMachine machine: PExplicitGlobal.getMachineSet()) {
for (PMachine machine : PExplicitGlobal.getMachineSet()) {
MachineLocalState ms = machineLocalStates.get(i++);
if (ms == null) {
machine.reset();
Expand Down Expand Up @@ -161,7 +161,7 @@ public String toString() {
List<String> fields = machine.getLocalVarNames();
List<Object> values = machineLocalStates.get(i++).getLocals();
int j = 0;
for (String field: fields) {
for (String field : fields) {
Object val = values.get(j++);
s.append(String.format(" %s -> %s\n", field, val));
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ public static int getHashCode(SortedSet<PMachine> machines) {
int hashValue = 0x802CBBDB;
for (PMachine machine : machines) {
hashValue = hashValue ^ machine.hashCode();
for (Object value: machine.getLocalVarValues()) {
for (Object value : machine.getLocalVarValues()) {
hashValue = hashValue ^ Objects.hashCode(value);
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -230,9 +230,9 @@ Collection<DynamicTest> loadDataTypeTests() {
// return loadTests("../../../Tst/RegressionTests/Feature5ModuleSystem");
// }

@TestFactory
//@Timeout(value = 1, unit = TimeUnit.MILLISECONDS)
Collection<DynamicTest> loadLivenessTests() {
return loadTests("../../../Tst/RegressionTests/Liveness");
}
@TestFactory
//@Timeout(value = 1, unit = TimeUnit.MILLISECONDS)
Collection<DynamicTest> loadLivenessTests() {
return loadTests("../../../Tst/RegressionTests/Liveness");
}
}

0 comments on commit 9964710

Please sign in to comment.