TLC help text and nomonolith sub-option - #393

. Clarified help text for dump and simulate to include sub-options
. Moved '-nomonolith' to a sub-option ('nomonolith') of '-generateSpecTe', ammended help text
. Improved Usage Generator to accept and display sub-options

[Enhancement][Tools]

tlatools/src/tlc2/TLC.java

@@ -223,9 +223,8 @@ public class TLC {
      *  o -generateSpecTE: will generate SpecTE assets if error-states are
      *  				encountered during model checking; this will change
      *  				to tool mode regardless of whether '-tool' was
-     *  				explicitly specified.
-     *  o -nomonolith: if generating a SpecTE, do not generate the monolith
-     *  				version
+     *  				explicitly specified; add on 'nomonolith' to not
+     *  				embed the dependencies in the SpecTE
      *  o -checkpoint num: interval for check pointing (in minutes)
      *		Defaults to 30
      *  o -fpmem num: a value between 0 and 1, exclusive, representing the ratio
@@ -411,13 +410,15 @@ public class TLC {
             {
                 index++;
                 TLCGlobals.tool = true;
-            } else if (args[index].equals("-nomonolith")) {
-            	index++;
-            	avoidMonolithSpecTECreation = true;
             } else if (args[index].equals("-generateSpecTE")) {
                 index++;
             	
                 TLCGlobals.tool = true;
+                
+                if (args[index].equals("nomonolith")) {
+                	index++;
+                	avoidMonolithSpecTECreation = true;
+                }
 				try {
 					temporaryMCOutputLogFile = File.createTempFile("mcout_", ".out");
 					temporaryMCOutputLogFile.deleteOnExit();
@@ -544,7 +545,7 @@ public class TLC {
             } else if (args[index].equals("-dump"))
             {
                 index++; // consume "-dump".
-                if (index + 1 < args.length && args[index].startsWith("dot"))
+                if (((index + 1) < args.length) && args[index].startsWith("dot"))
                 {
                 	final String dotArgs = args[index].toLowerCase();
                 	index++; // consume "dot...".
@@ -1381,7 +1382,13 @@ public class TLC {
     	sharedArguments.add(new UsageGenerator.Argument("-debug",
 														"print various debugging information - not for production use\n",
 														true));
-    	sharedArguments.add(new UsageGenerator.Argument("-dump", "file", "dump all states into the specified file", true));
+    	sharedArguments.add(new UsageGenerator.Argument("-dump", "file",
+    													"dump all states into the specified file; this parameter takes\n"
+    														+ "optional parameters for dot graph generation. Specifying\n"
+    														+ "'dot' allows further options, comma delimited, of zero\n"
+    														+ "or more of 'actionlabels', 'colorize', 'snapshot' to be\n"
+    														+ "specified before the '.dot'-suffixed filename", true,
+    													"dot actionlabels,colorize,snapshot"));
     	sharedArguments.add(new UsageGenerator.Argument("-fp", "N",
     													"use the Nth irreducible polynomial from the list stored\n"
     														+ "in the class FP64", true));
@@ -1392,11 +1399,16 @@ public class TLC {
 														"a value in (0.0,1.0) representing the ratio of total\n"
 															+ "physical memory to devote to storing the fingerprints\n"
 															+ "of found states; defaults to 0.25", true));
-    	sharedArguments.add(new UsageGenerator.Argument("-generateSpecTE",
+    	sharedArguments.add(new UsageGenerator.Argument("-generateSpecTE", null,
 														"if errors are encountered during model checking, generate\n"
-															+ "a SpecTE tla/cfg file pair which encapsulates Init-\n"
-															+ "Next definitions to specify the state conditions\n"
-															+ "of the error state; this enables 'tool' mode", true));
+															+ "a SpecTE tla/cfg file pair which encapsulates Init-Next\n"
+															+ "definitions to specify the state conditions of the error\n"
+															+ "state; this enables 'tool' mode. The generated SpecTE\n"
+															+ "will include tool output as well as all non-Standard-\n"
+															+ "Modules dependencies embeded in the module. To prevent\n"
+															+ "the embedding of dependencies, add the parameter\n"
+															+ "'nomonolith' to this declaration", true,
+															"nomonolith"));
     	sharedArguments.add(new UsageGenerator.Argument("-gzip",
 														"control if gzip is applied to value input/output streams;\n"
 															+ "defaults to 'off'", true));
@@ -1407,12 +1419,6 @@ public class TLC {
     	sharedArguments.add(new UsageGenerator.Argument("-metadir", "path",
 														"specify the directory in which to store metadata; defaults to\n"
 															+ "SPEC-directory/states if not specified", true));
-    	sharedArguments.add(new UsageGenerator.Argument("-nomonolith",
-														"if -generateSpecTE was specified and a SpecTE is created due\n"
-    														+ "to errors encountered, this flag specifies not to create a\n"
-															+ "monolithic SpecTE that embeds all non-Standard-Module\n"
-    														+ "dependent TLA modules - rather, include them via a\n"
-															+ "complete EXTENDS list", true));
     	sharedArguments.add(new UsageGenerator.Argument("-nowarning",
 														"disable all warnings; defaults to reporting warnings", true));
     	sharedArguments.add(new UsageGenerator.Argument("-recover", "id",
@@ -1451,8 +1457,14 @@ public class TLC {
     														+ "random long pulled from a pseudo-RNG", true));
     	simulateVariant.add(new UsageGenerator.Argument("-aril", "num",
 														"adjust the seed for random simulation; defaults to 0", true));
-    	simulateVariant.add(new UsageGenerator.Argument("-simulate",
-													  	"run in simulation mode", false));
+    	simulateVariant.add(new UsageGenerator.Argument("-simulate", null,
+													  	"run in simulation mode; optional parameters may be specified\n"
+	    													+ "comma delimited: 'num=X' where X is the maximum number of\n"
+	    													+ "total traces to generate and/or 'file=Y' where Y is the\n"
+	    													+ "absolute-pathed prefix for trace file modules to be written\n"
+	    													+ "by the simulation workers; for example Y='/a/b/c/tr' would\n"
+	    													+ "produce, e.g, '/a/b/c/tr_1_15'", false,
+	    												"file=X,num=Y"));
     	commandVariants.add(simulateVariant);
 
     	
@@ -1465,7 +1477,8 @@ public class TLC {
     				+ "model values to start with a non-numeral and rerun the model check to generate a new SpecTE.");
     	tips.add("If, while checking a SpecTE created via '-generateSpecTE', you get a warning concerning\n"
 					+ "duplicate operator definitions, this is likely due to the 'monolith' specification\n"
-					+ "creation. Try re-running TLC adding the -nomonolith flag.");
+					+ "creation. Try re-running TLC adding the 'nomonolith' option to the '-generateSpecTE'\n"
+					+ "parameter.");
     	
     	UsageGenerator.displayUsage(ToolIO.out, "TLC", TLCGlobals.versionOfTLC,
     								"provides model checking and simulation of TLA+ specifications",

tlatools/src/util/UsageGenerator.java

@@ -166,19 +166,30 @@ public class UsageGenerator {
 			}
 			
 			for (final Argument arg : nonShortArguments) {
-				sb.append(" [").append(markupWord(("-" + arg.getDashlessArgumentName()), true)).append(']');
+				sb.append(" [").append(markupWord(("-" + arg.getDashlessArgumentName()), true));
+				if (arg.hasSubOptions()) {
+					sb.append(" [").append(arg.getSubOptions()).append("]");
+				}
+				sb.append(']');
 			}
 		}
 		
 		if (optionalDoubleDashValueless.size() > 0) {
 			for (final Argument arg : optionalDoubleDashValueless) {
-				sb.append(" [").append(markupWord(arg.getArgumentName(), true)).append(']');
+				sb.append(" [").append(markupWord(arg.getArgumentName(), true));
+				if (arg.hasSubOptions()) {
+					sb.append(" [").append(arg.getSubOptions()).append("]");
+				}
+				sb.append(']');
 			}
 		}
 		
 		if (optionalValued.size() > 0) {
 			for (final Argument arg : optionalValued) {
 				sb.append(" [").append(markupWord(arg.getArgumentName(), true)).append(valuedArgumentsSeparator);
+				if (arg.hasSubOptions()) {
+					sb.append("[").append(arg.getSubOptions()).append("] ");
+				}
 				sb.append(markupWord(arg.getSampleValue(), false)).append(']');
 			}
 		}
@@ -193,6 +204,9 @@ public class UsageGenerator {
 		if (requiredValueless.size() > 0) {
 			for (final Argument arg : requiredValueless) {
 				sb.append(" ").append(arg.getArgumentName());
+				if (arg.hasSubOptions()) {
+					sb.append(" [").append(arg.getSubOptions()).append("]");
+				}
 			}
 		}
 		
@@ -238,6 +252,7 @@ public class UsageGenerator {
 		private final String sampleValue;
 		private final String description;
 		private final boolean optional;
+		private final String subOptions;
 		
 		/**
 		 * This calls {@code this(key, optionDescription, false);}
@@ -262,10 +277,16 @@ public class UsageGenerator {
 		
 		public Argument(final String key, final String exampleValue, final String optionDescription,
 						final boolean isOptional) {
+			this(key, exampleValue, optionDescription, isOptional, null);
+		}
+		
+		public Argument(final String key, final String exampleValue, final String optionDescription,
+						final boolean isOptional, final String concatenatedSuboptions) {
 			argumentName = key;
 			sampleValue = exampleValue;
 			description = optionDescription;
 			optional = isOptional;
+			subOptions = concatenatedSuboptions;
 		}
 		
 		public boolean isOptional() {
@@ -294,6 +315,10 @@ public class UsageGenerator {
 			return ((isDashArgument() && (argumentName.length() == 2)) || (argumentName.length() == 1));
 		}
 		
+		public boolean hasSubOptions() {
+			return (subOptions != null);
+		}
+
 		public String getArgumentName() {
 			return argumentName;
 		}
@@ -318,6 +343,10 @@ public class UsageGenerator {
 			return description;
 		}
 		
+		public String getSubOptions() {
+			return subOptions;
+		}
+
 		@Override
 		public int hashCode() {
 			return Objects.hash(argumentName);