[Bugfix] Check liveness regardless of checkpointing. Up to now, the

checkpointing interval would - as a side effect - also be the liveness
checking interval essentially turning the nextLiveCheck logic into dead
code. From now on, liveness checking is run when the amount of current
states in the fingerprint set has reached nextLiveCheck (which is
probably what was initially intended).

Note that deactivating checkpointing (with "-checkpoint 0") used to
deactivate partial liveness checking too. In this case liveness was only
checked finally at the end of model checking.

tlatools/src/tlc2/tool/AbstractChecker.java

@@ -256,14 +256,11 @@ public abstract class AbstractChecker implements Cancelable
         // added condition to run in the cycle
         // while (true) {
         while (!this.cancellationFlag)
-        {
-            if (TLCGlobals.doCheckPoint())
         {
             if (!this.doPeriodicWork())
             {
                 return false;
             }
-            }
             synchronized (this)
             {
                 if (!this.done)

tlatools/src/tlc2/tool/DFIDModelChecker.java

@@ -630,6 +630,7 @@ public class DFIDModelChecker extends AbstractChecker
                 nextLiveCheck = (stateNum < 600000) ? stateNum * 2 : stateNum + 200000;
             }
 
+            if (TLCGlobals.doCheckPoint()) {
             	// Checkpoint:
             	MP.printMessage(EC.TLC_CHECKPOINT_START, this.metadir);
             	// start checkpointing:
@@ -649,6 +650,7 @@ public class DFIDModelChecker extends AbstractChecker
             	UniqueString.internTbl.commitChkpt(this.metadir);
             	MP.printMessage(EC.TLC_CHECKPOINT_END);
             }
+        }
         return true;
     }
 

tlatools/src/tlc2/tool/ModelChecker.java

@@ -658,6 +658,7 @@ public class ModelChecker extends AbstractChecker
                 nextLiveCheck = (stateNum <= 640000) ? stateNum * 2 : stateNum + 640000;
             }
 
+            if (TLCGlobals.doCheckPoint()) {
             	// Checkpoint:
             	MP.printMessage(EC.TLC_CHECKPOINT_START, this.metadir);
             	
@@ -681,6 +682,10 @@ public class ModelChecker extends AbstractChecker
             		liveCheck.commitChkpt();
             	}
             	MP.printMessage(EC.TLC_CHECKPOINT_END);
+            } else {
+				// Just resume worker threads when checkpointing is skipped
+            	this.theStateQueue.resumeAll();
+            }
         }
         return true;
     }