diff --git a/Src/PCompiler/CompilerCore/Backend/PExplicit/PExplicitCodeGenerator.cs b/Src/PCompiler/CompilerCore/Backend/PExplicit/PExplicitCodeGenerator.cs index e23847801..b0e0f1fef 100644 --- a/Src/PCompiler/CompilerCore/Backend/PExplicit/PExplicitCodeGenerator.cs +++ b/Src/PCompiler/CompilerCore/Backend/PExplicit/PExplicitCodeGenerator.cs @@ -344,6 +344,18 @@ private void WriteMachineFields(CompilationContext context, StringWriter output, context.WriteLine(output, "}"); context.WriteLine(output); + context.WriteLine(output, "@Generated"); + context.WriteLine(output, "@Override"); + context.WriteLine(output, "public List copyLocalVarValues() {"); + context.WriteLine(output, " List result = super.copyLocalVarValues();"); + foreach (var field in machine.Fields) + { + context.WriteLine(output, $" result.add({CompilationContext.GetVar(field.Name)});"); + } + context.WriteLine(output, " return result;"); + context.WriteLine(output, "}"); + context.WriteLine(output); + context.WriteLine(output, "@Generated"); context.WriteLine(output, "@Override"); context.WriteLine(output, "protected int setLocalVarValues(List values) {"); diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java index 39a8675b7..baf410702 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java @@ -94,7 +94,7 @@ private static void process(boolean resume) throws Exception { throw new Exception("MEMOUT", e); } catch (BugFoundException e) { PExplicitGlobal.setStatus(STATUS.BUG_FOUND); - PExplicitGlobal.setResult(String.format("found cex of length %d", scheduler.currentStep.getStepNumber())); + PExplicitGlobal.setResult(String.format("found cex of length %d", scheduler.getStepState().getStepNumber())); PExplicitLogger.logStackTrace(e); ReplayScheduler replayer = new ReplayScheduler(scheduler.schedule); 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 b5471ef8f..7003f4014 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 @@ -171,6 +171,30 @@ public List getLocalVarValues() { result.add(currentState); + result.add(sendBuffer.getElements()); + result.add(deferQueue.getElements()); + + result.add(started); + result.add(halted); + + result.add(blockedBy); + result.add(blockedStateExit); + result.add(blockedNewStateEntry); + result.add(blockedNewStateEntryPayload); + + return result; + } + + /** + * Copy values of local variables as an ordered list + * + * @return List of values + */ + public List copyLocalVarValues() { + List result = new ArrayList<>(); + + result.add(currentState); + result.add(new ArrayList<>(sendBuffer.getElements())); result.add(new ArrayList<>(deferQueue.getElements())); @@ -210,8 +234,8 @@ protected int setLocalVarValues(List values) { return idx; } - public MachineState getMachineState() { - return new MachineState(getLocalVarValues()); + public MachineState copyMachineState() { + return new MachineState(copyLocalVarValues()); } public void setMachineState(MachineState input) { diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Choice.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Choice.java index 2f6afb0ce..612140655 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Choice.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Choice.java @@ -32,28 +32,6 @@ public class Choice implements Serializable { public Choice() { } - /** - * Copy-constructor for Choice - * - * @param old The choice to copy - */ - private Choice(Choice old) { - currentScheduleChoice = old.currentScheduleChoice; - currentDataChoice = old.currentDataChoice; - unexploredScheduleChoices = new ArrayList<>(old.unexploredScheduleChoices); - unexploredDataChoices = new ArrayList<>(old.unexploredDataChoices); - choiceStep = old.choiceStep; - } - - /** - * Copy the Choice - * - * @return A new cloned copy of the Choice - */ - public Choice getCopy() { - return new Choice(this); - } - /** * Check if this choice has an unexplored choice remaining. * diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java index 30032c23c..af451d48d 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Schedule.java @@ -21,6 +21,13 @@ public class Schedule implements Serializable { @Setter private List choices = new ArrayList<>(); + /** + * Step state at the start of a scheduler step. + * Used in stateful backtracking + */ + @Setter + private StepState stepBeginState = null; + /** * Constructor */ @@ -140,9 +147,9 @@ public void setUnexploredScheduleChoices(List machines, int idx) { choices.get(idx).setUnexploredScheduleChoices(machines); if (PExplicitGlobal.getConfig().isBacktrackingEnabled() && !machines.isEmpty() - && PExplicitGlobal.getScheduler().currentStep != null - && PExplicitGlobal.getScheduler().currentStep.getStepNumber() != 0) { - choices.get(idx).setChoiceStep(PExplicitGlobal.getScheduler().currentStep.copy()); + && stepBeginState != null + && stepBeginState.getStepNumber() != 0) { + choices.get(idx).setChoiceStep(stepBeginState.copy()); } } @@ -159,9 +166,9 @@ public void setUnexploredDataChoices(List> values, int idx) { choices.get(idx).setUnexploredDataChoices(values); if (PExplicitGlobal.getConfig().isBacktrackingEnabled() && !values.isEmpty() - && PExplicitGlobal.getScheduler().currentStep != null - && PExplicitGlobal.getScheduler().currentStep.getStepNumber() != 0) { - choices.get(idx).setChoiceStep(PExplicitGlobal.getScheduler().currentStep.copy()); + && stepBeginState != null + && stepBeginState.getStepNumber() != 0) { + choices.get(idx).setChoiceStep(stepBeginState.copy()); } } 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 f81110f23..3b6a56fea 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 @@ -25,7 +25,8 @@ public abstract class Scheduler implements SchedulerInterface { /** * Current step state */ - public StepState currentStep = new StepState(); + @Getter + protected StepState stepState = new StepState(); /** * Current schedule @@ -205,7 +206,7 @@ public void startMachine(PMachine machine) { } // add machine to schedule - currentStep.makeMachine(machine); + stepState.makeMachine(machine); // run create machine event processCreateEvent(new PMessage(PEvent.createMachine, machine, null)); @@ -222,20 +223,20 @@ public void executeStep(PMachine sender) { if (!msg.getEvent().isCreateMachineEvent()) { // update step number - currentStep.setStepNumber(currentStep.getStepNumber() + 1); + stepState.setStepNumber(stepState.getStepNumber() + 1); } // reset number of logs in current step stepNumLogs = 0; // log start step - PExplicitLogger.logStartStep(currentStep.getStepNumber(), sender, msg); + PExplicitLogger.logStartStep(stepState.getStepNumber(), sender, msg); // process message processDequeueEvent(sender, msg); // update done stepping flag - isDoneStepping = (currentStep.getStepNumber() >= PExplicitGlobal.getConfig().getMaxStepBound()); + isDoneStepping = (stepState.getStepNumber() >= PExplicitGlobal.getConfig().getMaxStepBound()); } /** @@ -249,7 +250,7 @@ public PMachine allocateMachine( Class machineType, Function constructor) { // get machine count for given type from schedule - int machineCount = currentStep.getMachineCount(machineType); + int machineCount = stepState.getMachineCount(machineType); PMachine machine = PExplicitGlobal.getGlobalMachine(machineType, machineCount); if (machine == null) { @@ -259,7 +260,7 @@ public PMachine allocateMachine( } // add machine to schedule - currentStep.makeMachine(machine); + stepState.makeMachine(machine); return machine; } @@ -324,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: currentStep.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)); } 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 cd2047d15..b2ae1b935 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 @@ -79,11 +79,13 @@ public void run() throws TimeoutException { printProgressHeader(true); } isDoneIterating = false; - start(); while (!isDoneIterating) { SearchStatistics.iteration++; - PExplicitLogger.logStartIteration(SearchStatistics.iteration, currentStep.getStepNumber()); + PExplicitLogger.logStartIteration(SearchStatistics.iteration, stepState.getStepNumber()); + if (stepState.getStepNumber() == 0) { + start(); + } runIteration(); postProcessIteration(); } @@ -105,12 +107,12 @@ protected void runIteration() throws TimeoutException { } printProgress(false); - SearchStatistics.totalSteps += currentStep.getStepNumber(); - if (SearchStatistics.minSteps == -1 || currentStep.getStepNumber() < SearchStatistics.minSteps) { - SearchStatistics.minSteps = currentStep.getStepNumber(); + SearchStatistics.totalSteps += stepState.getStepNumber(); + if (SearchStatistics.minSteps == -1 || stepState.getStepNumber() < SearchStatistics.minSteps) { + SearchStatistics.minSteps = stepState.getStepNumber(); } - if (SearchStatistics.maxSteps == -1 || currentStep.getStepNumber() > SearchStatistics.maxSteps) { - SearchStatistics.maxSteps = currentStep.getStepNumber(); + if (SearchStatistics.maxSteps == -1 || stepState.getStepNumber() > SearchStatistics.maxSteps) { + SearchStatistics.maxSteps = stepState.getStepNumber(); } if (scheduleTerminated) { @@ -123,7 +125,7 @@ protected void runIteration() throws TimeoutException { } Assert.fromModel( - !PExplicitGlobal.getConfig().isFailOnMaxStepBound() || (currentStep.getStepNumber() < PExplicitGlobal.getConfig().getMaxStepBound()), + !PExplicitGlobal.getConfig().isFailOnMaxStepBound() || (stepState.getStepNumber() < PExplicitGlobal.getConfig().getMaxStepBound()), "Step bound of " + PExplicitGlobal.getConfig().getMaxStepBound() + " reached."); if (PExplicitGlobal.getConfig().getMaxSchedules() > 0) { @@ -150,10 +152,15 @@ protected void runStep() throws TimeoutException { scheduleTerminated = false; skipLiveness = true; isDoneStepping = true; - PExplicitLogger.logFinishedIteration(currentStep.getStepNumber()); + PExplicitLogger.logFinishedIteration(stepState.getStepNumber()); return; } + if (PExplicitGlobal.getConfig().isBacktrackingEnabled()) { + stepState.storeMachinesState(); + schedule.setStepBeginState(stepState); + } + // get a scheduling choice as sender machine PMachine sender = getNextScheduleChoice(); @@ -162,14 +169,10 @@ protected void runStep() throws TimeoutException { scheduleTerminated = true; skipLiveness = false; isDoneStepping = true; - PExplicitLogger.logFinishedIteration(currentStep.getStepNumber()); + PExplicitLogger.logFinishedIteration(stepState.getStepNumber()); return; } - if (PExplicitGlobal.getConfig().isBacktrackingEnabled()) { - currentStep.storeMachinesState(); - } - // execute a step from message in the sender queue executeStep(sender); } @@ -182,7 +185,7 @@ protected void runStep() throws TimeoutException { boolean skipRemainingSchedule() { if (PExplicitGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) { // perform state caching only if beyond backtrack choice number - if (currentStep.getChoiceNumber() > backtrackChoiceNumber) { + if (stepState.getChoiceNumber() > backtrackChoiceNumber) { // increment state count SearchStatistics.totalStates++; @@ -226,12 +229,12 @@ Object getCurrentStateKey() { Object stateKey = null; if (PExplicitGlobal.getConfig().getStateCachingMode() == StateCachingMode.Fingerprint) { // use fingerprinting by hashing values from each machine vars - int fingerprint = ComputeHash.getHashCode(currentStep.getMachineSet()); + int fingerprint = ComputeHash.getHashCode(stepState.getMachineSet()); stateKey = fingerprint; } else { // use exact values from each machine vars List> machineValues = new ArrayList<>(); - for (PMachine machine: currentStep.getMachineSet()) { + for (PMachine machine: stepState.getMachineSet()) { machineValues.add(machine.getLocalVarValues()); } stateKey = machineValues; @@ -256,46 +259,46 @@ protected void reset() { public PMachine getNextScheduleChoice() { PMachine result; - if (currentStep.getChoiceNumber() < backtrackChoiceNumber) { + if (stepState.getChoiceNumber() < backtrackChoiceNumber) { // pick the current schedule choice - result = schedule.getCurrentScheduleChoice(currentStep.getChoiceNumber()); - PExplicitLogger.logRepeatScheduleChoice(result, currentStep.getStepNumber(), currentStep.getChoiceNumber()); + result = schedule.getCurrentScheduleChoice(stepState.getChoiceNumber()); + PExplicitLogger.logRepeatScheduleChoice(result, stepState.getStepNumber(), stepState.getChoiceNumber()); - currentStep.setChoiceNumber(currentStep.getChoiceNumber() + 1); + stepState.setChoiceNumber(stepState.getChoiceNumber() + 1); return result; } // get existing unexplored choices, if any - List choices = schedule.getUnexploredScheduleChoices(currentStep.getChoiceNumber()); + List choices = schedule.getUnexploredScheduleChoices(stepState.getChoiceNumber()); if (choices.isEmpty()) { // no existing unexplored choices, so try generating new choices choices = getNewScheduleChoices(); if (choices.size() > 1) { // log new choice - PExplicitLogger.logNewScheduleChoice(choices, currentStep.getStepNumber(), currentStep.getChoiceNumber()); + PExplicitLogger.logNewScheduleChoice(choices, stepState.getStepNumber(), stepState.getChoiceNumber()); } if (choices.isEmpty()) { // no unexplored choices remaining - currentStep.setChoiceNumber(currentStep.getChoiceNumber() + 1); + stepState.setChoiceNumber(stepState.getChoiceNumber() + 1); return null; } } // pick the first choice result = choices.get(0); - schedule.setCurrentScheduleChoice(result, currentStep.getChoiceNumber()); - PExplicitLogger.logCurrentScheduleChoice(result, currentStep.getStepNumber(), currentStep.getChoiceNumber()); + schedule.setCurrentScheduleChoice(result, stepState.getChoiceNumber()); + PExplicitLogger.logCurrentScheduleChoice(result, stepState.getStepNumber(), stepState.getChoiceNumber()); // remove the first choice from unexplored choices choices.remove(0); // set unexplored choices - schedule.setUnexploredScheduleChoices(choices, currentStep.getChoiceNumber()); + schedule.setUnexploredScheduleChoices(choices, stepState.getChoiceNumber()); // increment choice number - currentStep.setChoiceNumber(currentStep.getChoiceNumber() + 1); + stepState.setChoiceNumber(stepState.getChoiceNumber() + 1); return result; } @@ -309,18 +312,18 @@ public PMachine getNextScheduleChoice() { public PValue getNextDataChoice(List> input_choices) { PValue result; - if (currentStep.getChoiceNumber() < backtrackChoiceNumber) { + if (stepState.getChoiceNumber() < backtrackChoiceNumber) { // pick the current data choice - result = schedule.getCurrentDataChoice(currentStep.getChoiceNumber()); + result = schedule.getCurrentDataChoice(stepState.getChoiceNumber()); assert (input_choices.contains(result)); - PExplicitLogger.logRepeatDataChoice(result, currentStep.getStepNumber(), currentStep.getChoiceNumber()); + PExplicitLogger.logRepeatDataChoice(result, stepState.getStepNumber(), stepState.getChoiceNumber()); - currentStep.setChoiceNumber(currentStep.getChoiceNumber() + 1); + stepState.setChoiceNumber(stepState.getChoiceNumber() + 1); return result; } // get existing unexplored choices, if any - List> choices = schedule.getUnexploredDataChoices(currentStep.getChoiceNumber()); + List> choices = schedule.getUnexploredDataChoices(stepState.getChoiceNumber()); assert (input_choices.containsAll(choices)); if (choices.isEmpty()) { @@ -328,29 +331,29 @@ public PValue getNextDataChoice(List> input_choices) { choices = input_choices; if (choices.size() > 1) { // log new choice - PExplicitLogger.logNewDataChoice(choices, currentStep.getStepNumber(), currentStep.getChoiceNumber()); + PExplicitLogger.logNewDataChoice(choices, stepState.getStepNumber(), stepState.getChoiceNumber()); } if (choices.isEmpty()) { // no unexplored choices remaining - currentStep.setChoiceNumber(currentStep.getChoiceNumber() + 1); + stepState.setChoiceNumber(stepState.getChoiceNumber() + 1); return null; } } // pick the first choice result = choices.get(0); - schedule.setCurrentDataChoice(result, currentStep.getChoiceNumber()); - PExplicitLogger.logCurrentDataChoice(result, currentStep.getStepNumber(), currentStep.getChoiceNumber()); + schedule.setCurrentDataChoice(result, stepState.getChoiceNumber()); + PExplicitLogger.logCurrentDataChoice(result, stepState.getStepNumber(), stepState.getChoiceNumber()); // remove the first choice from unexplored choices choices.remove(0); // set unexplored choices - schedule.setUnexploredDataChoices(choices, currentStep.getChoiceNumber()); + schedule.setUnexploredDataChoices(choices, stepState.getChoiceNumber()); // increment choice number - currentStep.setChoiceNumber(currentStep.getChoiceNumber() + 1); + stepState.setChoiceNumber(stepState.getChoiceNumber() + 1); return result; } @@ -369,14 +372,16 @@ private void postIterationCleanup() { backtrackChoiceNumber = cIdx; int newStepNumber = 0; if (PExplicitGlobal.getConfig().isBacktrackingEnabled()) { - newStepNumber = choice.getChoiceStep().getStepNumber(); + StepState choiceStep = choice.getChoiceStep(); + if (choiceStep != null) { + newStepNumber = choice.getChoiceStep().getStepNumber(); + } } PExplicitLogger.logBacktrack(cIdx, newStepNumber); if (newStepNumber == 0) { - currentStep.resetToZero(); - start(); + stepState.resetToZero(); } else { - currentStep.setTo(choice.getChoiceStep()); + stepState.setTo(choice.getChoiceStep()); } return; } else { @@ -388,7 +393,7 @@ private void postIterationCleanup() { private List getNewScheduleChoices() { // prioritize create machine events - for (PMachine machine : currentStep.getMachineSet()) { + for (PMachine machine : stepState.getMachineSet()) { if (machine.getSendBuffer().nextIsCreateMachineMsg()) { return new ArrayList<>(Collections.singletonList(machine)); } @@ -397,7 +402,7 @@ private List getNewScheduleChoices() { // now there are no create machine events remaining List choices = new ArrayList<>(); - for (PMachine machine : currentStep.getMachineSet()) { + for (PMachine machine : stepState.getMachineSet()) { if (machine.getSendBuffer().nextHasTargetRunning()) { choices.add(machine); } @@ -458,7 +463,7 @@ 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", currentStep.getStepNumber()) + + 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) { @@ -514,7 +519,7 @@ protected void printProgress(boolean forcePrint) { s.append(StringUtils.center(String.format("%s", runtimeHms), 11)); s.append( StringUtils.center(String.format("%.1f GB", MemoryMonitor.getMemSpent() / 1024), 9)); - s.append(StringUtils.center(String.format("%d", currentStep.getStepNumber()), 7)); + s.append(StringUtils.center(String.format("%d", stepState.getStepNumber()), 7)); s.append(StringUtils.center(String.format("%d", SearchStatistics.iteration), 12)); s.append( diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/StepState.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/StepState.java index 0e133b7dd..bacc9252a 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/StepState.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/StepState.java @@ -86,7 +86,7 @@ public void setTo(StepState input) { public void storeMachinesState() { machineStates.clear(); for (PMachine machine : machineSet) { - MachineState ms = machine.getMachineState(); + MachineState ms = machine.copyMachineState(); machineStates.add(ms); } } @@ -139,4 +139,21 @@ public PMachine getMachine(Class type, int idx) { public int getMachineCount(Class type) { return machineListByType.getOrDefault(type, new ArrayList<>()).size(); } + + @Override + public String toString() { + StringBuilder s = new StringBuilder(); + int i = 0; + for (PMachine machine : machineSet) { + s.append(String.format("%s::\n", machine)); + List fields = machine.getLocalVarNames(); + List values = machineStates.get(i++).getLocals(); + int j = 0; + for (String field: fields) { + Object val = values.get(j++); + s.append(String.format(" %s -> %s\n", field, val)); + } + } + return s.toString(); + } } diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/replay/ReplayScheduler.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/replay/ReplayScheduler.java index 4f621b323..9207eeea8 100644 --- a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/replay/ReplayScheduler.java +++ b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/replay/ReplayScheduler.java @@ -25,7 +25,7 @@ public void run() throws TimeoutException, InterruptedException { // log run test PExplicitLogger.logRunTest(); - currentStep.resetToZero(); + stepState.resetToZero(); start(); runIteration(); } @@ -51,7 +51,7 @@ protected void runIteration() throws TimeoutException { checkLiveness(scheduleTerminated); Assert.fromModel( - !PExplicitGlobal.getConfig().isFailOnMaxStepBound() || (currentStep.getStepNumber() < PExplicitGlobal.getConfig().getMaxStepBound()), + !PExplicitGlobal.getConfig().isFailOnMaxStepBound() || (stepState.getStepNumber() < PExplicitGlobal.getConfig().getMaxStepBound()), "Step bound of " + PExplicitGlobal.getConfig().getMaxStepBound() + " reached."); } @@ -64,7 +64,7 @@ protected void runStep() throws TimeoutException { // done with this schedule scheduleTerminated = true; isDoneStepping = true; - PExplicitLogger.logFinishedIteration(currentStep.getStepNumber()); + PExplicitLogger.logFinishedIteration(stepState.getStepNumber()); return; } @@ -79,36 +79,36 @@ protected void reset() { @Override protected PMachine getNextScheduleChoice() { - if (currentStep.getChoiceNumber() >= schedule.size()) { + if (stepState.getChoiceNumber() >= schedule.size()) { return null; } // pick the current schedule choice - PMachine result = schedule.getCurrentScheduleChoice(currentStep.getChoiceNumber()); + PMachine result = schedule.getCurrentScheduleChoice(stepState.getChoiceNumber()); if (result == null) { return null; } ScheduleWriter.logScheduleChoice(result); - PExplicitLogger.logRepeatScheduleChoice(result, currentStep.getStepNumber(), currentStep.getChoiceNumber()); + PExplicitLogger.logRepeatScheduleChoice(result, stepState.getStepNumber(), stepState.getChoiceNumber()); - currentStep.setChoiceNumber(currentStep.getChoiceNumber() + 1); + stepState.setChoiceNumber(stepState.getChoiceNumber() + 1); return result; } @Override protected PValue getNextDataChoice(List> input_choices) { - if (currentStep.getChoiceNumber() >= schedule.size()) { + if (stepState.getChoiceNumber() >= schedule.size()) { return null; } // pick the current data choice - PValue result = schedule.getCurrentDataChoice(currentStep.getChoiceNumber()); + PValue result = schedule.getCurrentDataChoice(stepState.getChoiceNumber()); assert (input_choices.contains(result)); ScheduleWriter.logDataChoice(result); - PExplicitLogger.logRepeatDataChoice(result, currentStep.getStepNumber(), currentStep.getChoiceNumber()); + PExplicitLogger.logRepeatDataChoice(result, stepState.getStepNumber(), stepState.getChoiceNumber()); - currentStep.setChoiceNumber(currentStep.getChoiceNumber() + 1); + stepState.setChoiceNumber(stepState.getChoiceNumber() + 1); return result; } }