CLI Trace Explorer, Stage 4 - #393

. A clean model check with the generateSpecTE flag specified created a post-model-check exception and an aborted SpecTE file left on the filesystem; addressed this, as well as verbiage change due to -tool being implicitly set under this flag set condition.

[Feature][Tools]

tlatools/src/tlc2/TLC.java

@@ -438,6 +438,7 @@ public class TLC {
 							temporaryMCOutputStream.close();
 							haveClosedOutputStream = true;
 							
+							if (mcOutputConsumer.getError() != null) {
 								final File tempTLA = File.createTempFile("temp_tlc_tla_", ".tla");
 								tempTLA.deleteOnExit();
 								FileUtil.copyFile(specTETLAFile, tempTLA);
@@ -459,6 +460,7 @@ public class TLC {
 																 mcOutputConsumer.getSourceDirectory(),
 																 extendedModules, mcParserResults.getAllExtendedModules());
 								monolithCreator.copy();
+							}
 							
 							waitingOnGenerationCompletion.set(false);
 							synchronized(this) {
@@ -483,8 +485,7 @@ public class TLC {
 					
 					MP.printMessage(EC.GENERAL,
 									"Will generate a " + TLAConstants.TraceExplore.ERROR_STATES_MODULE_NAME
-										+ " file pair if error states are encountered and we are "
-										+ "being run with the '-tool' flag.");
+										+ " file pair if error states are encountered.");
 				} catch (final IOException ioe) {
 					printErrorMsg("Failed to set up piped output consumers; no potential "
 										+ TLAConstants.TraceExplore.ERROR_STATES_MODULE_NAME + " will be generated: "
@@ -1056,13 +1057,7 @@ public class TLC {
 					result = TLCGlobals.mainChecker.modelCheck();
                 }
 
-                if (mcOutputConsumer != null)  {
-                	if (mcOutputConsumer.getError() == null) {
-                		MP.printMessage(EC.GENERAL,
-                						"The model check run produced no usable error-state messages, "
-                										+ "so no " + TLAConstants.TraceExplore.ERROR_STATES_MODULE_NAME
-                										+ " was generated.");
-                	} else {
+                if ((mcOutputConsumer != null) && (mcOutputConsumer.getError() != null)) {
             		final SpecProcessor sp = tool.getSpecProcessor();
             		final ModelConfig mc = tool.getModelConfig();
             		final File sourceDirectory = mcOutputConsumer.getSourceDirectory();
@@ -1077,7 +1072,6 @@ public class TLC {
             		specTETLAFile = files[0];
                 }
             }
-            }
             return result;
         } catch (Throwable e)
         {