"-lncheck seqfinal" checks satisfiability branches of liveness checking

sequentially.

Multiple properties are usually split into individual branches that TLC
checks in parallel.  In memory constrained environments, running the
branches sequentially trades memory (space) for time.

[Feature][TLC]

tlatools/src/tlc2/TLCGlobals.java

@@ -52,7 +52,11 @@ public class TLCGlobals
 	public static String lnCheck = "default";
 	
 	public static boolean doLiveness() {
-		return !lnCheck.equals("final");
+		return !(lnCheck.equals("final") || lnCheck.equals("seqfinal"));
+	}
+
+	public static boolean doSequentialLiveness() {
+		return lnCheck.startsWith("seq");
 	}
 
 	public synchronized static void setNumWorkers(int n)

tlatools/src/tlc2/tool/liveness/LiveCheck.java

@@ -227,7 +227,7 @@ public class LiveCheck implements ILiveCheck {
 		 * a violation found by another LW. However, if any LW fails to check, we terminate
 		 * model checking after all LWs completed.
 		 */
-		final int wNum = Math.min(checker.length, TLCGlobals.getNumWorkers());
+		final int wNum = TLCGlobals.doSequentialLiveness() ? 1 : Math.min(checker.length, TLCGlobals.getNumWorkers());
 		final ExecutorService pool = Executors.newFixedThreadPool(wNum);
 		// CS is really just a container around the set of Futures returned by the pool. It saves us from
 		// creating a low-level array.