diff --git a/tlatools/src/tlc2/tool/AbstractChecker.java b/tlatools/src/tlc2/tool/AbstractChecker.java index 5115e6a3e5b84d4683c1a5ab1ce62e1fe2f2fe7a..86c1246e9dbfd16f7af651b728c84995d6307ded 100644 --- a/tlatools/src/tlc2/tool/AbstractChecker.java +++ b/tlatools/src/tlc2/tool/AbstractChecker.java @@ -257,12 +257,9 @@ public abstract class AbstractChecker implements Cancelable // while (true) { while (!this.cancellationFlag) { - if (TLCGlobals.doCheckPoint()) + if (!this.doPeriodicWork()) { - if (!this.doPeriodicWork()) - { - return false; - } + return false; } synchronized (this) { diff --git a/tlatools/src/tlc2/tool/DFIDModelChecker.java b/tlatools/src/tlc2/tool/DFIDModelChecker.java index de5506dcbace63b4a07121f0ce173b2d2bdc9fd0..3f26db5849d3e8c37018a1453017a72aafffc405 100644 --- a/tlatools/src/tlc2/tool/DFIDModelChecker.java +++ b/tlatools/src/tlc2/tool/DFIDModelChecker.java @@ -630,24 +630,26 @@ public class DFIDModelChecker extends AbstractChecker nextLiveCheck = (stateNum < 600000) ? stateNum * 2 : stateNum + 200000; } - // Checkpoint: - MP.printMessage(EC.TLC_CHECKPOINT_START, this.metadir); - // start checkpointing: - this.theFPSet.beginChkpt(); - if (this.checkLiveness) - { - liveCheck.beginChkpt(); - } - UniqueString.internTbl.beginChkpt(this.metadir); - - // Commit checkpoint: - this.theFPSet.commitChkpt(); - if (this.checkLiveness) - { - liveCheck.commitChkpt(); + if (TLCGlobals.doCheckPoint()) { + // Checkpoint: + MP.printMessage(EC.TLC_CHECKPOINT_START, this.metadir); + // start checkpointing: + this.theFPSet.beginChkpt(); + if (this.checkLiveness) + { + liveCheck.beginChkpt(); + } + UniqueString.internTbl.beginChkpt(this.metadir); + + // Commit checkpoint: + this.theFPSet.commitChkpt(); + if (this.checkLiveness) + { + liveCheck.commitChkpt(); + } + UniqueString.internTbl.commitChkpt(this.metadir); + MP.printMessage(EC.TLC_CHECKPOINT_END); } - UniqueString.internTbl.commitChkpt(this.metadir); - MP.printMessage(EC.TLC_CHECKPOINT_END); } return true; } diff --git a/tlatools/src/tlc2/tool/ModelChecker.java b/tlatools/src/tlc2/tool/ModelChecker.java index 3db3f98192e99245b5e31b837f6167a0945ec055..bff94e3d073c76b957ac98ccf40726a84f786f33 100644 --- a/tlatools/src/tlc2/tool/ModelChecker.java +++ b/tlatools/src/tlc2/tool/ModelChecker.java @@ -658,29 +658,34 @@ public class ModelChecker extends AbstractChecker nextLiveCheck = (stateNum <= 640000) ? stateNum * 2 : stateNum + 640000; } - // Checkpoint: - MP.printMessage(EC.TLC_CHECKPOINT_START, this.metadir); - - // start checkpointing: - this.theStateQueue.beginChkpt(); - this.trace.beginChkpt(); - this.theFPSet.beginChkpt(); - this.theStateQueue.resumeAll(); - UniqueString.internTbl.beginChkpt(this.metadir); - if (this.checkLiveness) - { - liveCheck.beginChkpt(); - } - // commit checkpoint: - this.theStateQueue.commitChkpt(); - this.trace.commitChkpt(); - this.theFPSet.commitChkpt(); - UniqueString.internTbl.commitChkpt(this.metadir); - if (this.checkLiveness) - { - liveCheck.commitChkpt(); + if (TLCGlobals.doCheckPoint()) { + // Checkpoint: + MP.printMessage(EC.TLC_CHECKPOINT_START, this.metadir); + + // start checkpointing: + this.theStateQueue.beginChkpt(); + this.trace.beginChkpt(); + this.theFPSet.beginChkpt(); + this.theStateQueue.resumeAll(); + UniqueString.internTbl.beginChkpt(this.metadir); + if (this.checkLiveness) + { + liveCheck.beginChkpt(); + } + // commit checkpoint: + this.theStateQueue.commitChkpt(); + this.trace.commitChkpt(); + this.theFPSet.commitChkpt(); + UniqueString.internTbl.commitChkpt(this.metadir); + if (this.checkLiveness) + { + liveCheck.commitChkpt(); + } + MP.printMessage(EC.TLC_CHECKPOINT_END); + } else { + // Just resume worker threads when checkpointing is skipped + this.theStateQueue.resumeAll(); } - MP.printMessage(EC.TLC_CHECKPOINT_END); } return true; }