diff --git a/tlatools/src/tlc2/TLC.java b/tlatools/src/tlc2/TLC.java index d3d9101212320ee4e55a349697b892d4238a372d..9a283bbfbdc43a20c893b03c71c042bd9e0bdd91 100644 --- a/tlatools/src/tlc2/TLC.java +++ b/tlatools/src/tlc2/TLC.java @@ -35,6 +35,7 @@ import tlc2.input.MCParser; import tlc2.input.MCParserResults; import tlc2.output.EC; import tlc2.output.MP; +import tlc2.output.Messages; import tlc2.output.TLAMonolithCreator; import tlc2.output.TeeOutputStream; import tlc2.tool.DFIDModelChecker; @@ -66,6 +67,7 @@ import util.TLAConstants; import util.TLCRuntime; import util.ToolIO; import util.UniqueString; +import util.UsageGenerator; /** * Main TLC starter class. @@ -494,7 +496,7 @@ public class TLC { + ioe.getMessage()); mcOutputConsumer = null; } - } else if (args[index].equals("-help")) + } else if (args[index].equals("-help") || args[index].equals("-h")) { printUsage(); return false; @@ -1339,8 +1341,116 @@ public class TLC { */ private void printUsage() { - printWelcome(); - MP.printMessage(EC.TLC_USAGE); + final List<List<UsageGenerator.Argument>> commandVariants = new ArrayList<>(); + final List<UsageGenerator.Argument> sharedArguments = new ArrayList<>(); + + // N.B. alphabetical ordering is not required by the UsageGenerator, but introduced here to more easily + // find options when reading the code + sharedArguments.add(new UsageGenerator.Argument("-checkpoint", "minutes", + "interval between check point; defaults to 30", + true)); + sharedArguments.add(new UsageGenerator.Argument("-cleanup", "clean up the states directory", true)); + sharedArguments.add(new UsageGenerator.Argument("-config", "file", + "provide the configuration file; defaults to SPEC.cfg", true)); + sharedArguments.add(new UsageGenerator.Argument("-continue", + "continue running even when an invariant is violated; default\n" + + "behavior is to halt on first violation", true)); + sharedArguments.add(new UsageGenerator.Argument("-coverage", "minutes", + "interval between the collection of coverage information;\n" + + "if not specified, no coverage will be collected", true)); + sharedArguments.add(new UsageGenerator.Argument("-deadlock", + "if specified DO NOT CHECK FOR DEADLOCK; default\n" + + "behavior is to check for deadlock", true)); + sharedArguments.add(new UsageGenerator.Argument("-difftrace", + "show only the differences between successive states when\n" + + "printing trace information; defaults to printing\n" + + "full state descriptions", true)); + 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("-fp", "N", + "use the Nth irreducible polynomial from the list stored\n" + + "in the class FP64", true)); + sharedArguments.add(new UsageGenerator.Argument("-fpbits", "num", + "the number of MSB used by MultiFPSet to create nested\n" + + "FPSets; defaults to 1", true)); + sharedArguments.add(new UsageGenerator.Argument("-fpmem", "num", + "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", + "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)); + sharedArguments.add(new UsageGenerator.Argument("-gzip", + "control if gzip is applied to value input/output streams;\n" + + "defaults to 'off'", true)); + sharedArguments.add(new UsageGenerator.Argument("-h", "display these help instructions", true)); + sharedArguments.add(new UsageGenerator.Argument("-maxSetSize", "num", + "the size of the largest set which TLC will enumerate; defaults\n" + + "to 1000000 (10^6)", true)); + 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("-nowarning", + "disable all warnings; defaults to reporting warnings", true)); + sharedArguments.add(new UsageGenerator.Argument("-recover", "id", + "recover from the checkpoint with the specified id", true)); + sharedArguments.add(new UsageGenerator.Argument("-terse", + "do not expand values in Print statements; defaults to\n" + + "expanding values", true)); + sharedArguments.add(new UsageGenerator.Argument("-tool", + "run in 'tool' mode, surrounding output with message codes;\n" + + "if '-generateSpecTE' is specified, this is enabled\n" + + "automatically", true)); + sharedArguments.add(new UsageGenerator.Argument("-workers", "num", + "the number of TLC worker threads; defaults to 1", true)); + + sharedArguments.add(new UsageGenerator.Argument("SPEC", null)); + + + final List<UsageGenerator.Argument> modelCheckVariant = new ArrayList<>(sharedArguments); + modelCheckVariant.add(new UsageGenerator.Argument("-dfid", "num", + "run the model check in depth-first iterative deepening\n" + + "starting with an initial depth of 'num'", true)); + modelCheckVariant.add(new UsageGenerator.Argument("-view", + "apply VIEW (if provided) when printing out states", true)); + commandVariants.add(modelCheckVariant); + + + final List<UsageGenerator.Argument> simulateVariant = new ArrayList<>(sharedArguments); + simulateVariant.add(new UsageGenerator.Argument("-depth", "num", + "specifies the depth of random simulation; defaults to 100", + true)); + simulateVariant.add(new UsageGenerator.Argument("-seed", "num", + "provide the seed for random simulation; defaults to a\n" + + "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)); + commandVariants.add(simulateVariant); + + + final List<String> tips = new ArrayList<String>(); + tips.add("When using the '-generateSpecTE' you can version the generated specification by doing:\n\t" + + "./tla2tools.jar -generateSpecTE MySpec.tla && NAME=\"SpecTE-$(date +%s)\" && sed -e \"s/MODULE" + + " SpecTE/MODULE $NAME/g\" SpecTE.tla > $NAME.tla"); + tips.add("If, while checking a SpecTE created via '-generateSpecTE', you get an error message concerning\n" + + "CONSTANT declaration and you've previous used 'integers' as model values, rename your\n" + + "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. Until a 'disable monolith creation' flag is added to TLC, provide the tool\n" + + "output of your model checking to tlc2.TraceExplorer to have it generate a non-monolithic\n" + + "specification."); + + UsageGenerator.displayUsage(ToolIO.out, "TLC", TLCGlobals.versionOfTLC, + "provides model checking and simulation of TLA+ specifications", + Messages.getString("TLCDescription"), + commandVariants, tips, ' '); } FPSetConfiguration getFPSetConfiguration() { diff --git a/tlatools/src/tlc2/model/MCState.java b/tlatools/src/tlc2/model/MCState.java index dc92fc33b70eaeef9d6f3c70baee48bb6802526f..aa1af885eab94d9126af0437d2c2fc68812ef216 100644 --- a/tlatools/src/tlc2/model/MCState.java +++ b/tlatools/src/tlc2/model/MCState.java @@ -6,8 +6,6 @@ import tla2sany.st.Location; import util.TLAConstants; public class MCState { - private static final String ANSI_BOLD_CODE = "\033[1m"; - private static final String ANSI_RESET_CODE = "\033[0m"; private static final String BACK_TO_STATE = " " + TLAConstants.BACK_TO_STATE; public static MCState parseState(final String stateInputString) { @@ -237,7 +235,7 @@ public class MCState { result.append("/\\ "); if (var.isTraceExplorerExpression()) { if (ansiMarkup) { - result.append(ANSI_BOLD_CODE); + result.append(TLAConstants.ANSI.BOLD_CODE); } result.append(var.getSingleLineDisplayName()); @@ -248,7 +246,7 @@ public class MCState { result.append(" = ").append(var.getValueAsString()); if (var.isTraceExplorerExpression() && ansiMarkup) { - result.append(ANSI_RESET_CODE); + result.append(TLAConstants.ANSI.RESET_CODE); } result.append('\n'); diff --git a/tlatools/src/tlc2/output/EC.java b/tlatools/src/tlc2/output/EC.java index 322470816bb57226d4d9c9371498fbbf0d1d8079..46a1c307d75bd8533b495b28a5d8a6b2fb18d0ba 100644 --- a/tlatools/src/tlc2/output/EC.java +++ b/tlatools/src/tlc2/output/EC.java @@ -284,7 +284,6 @@ public interface EC public static final int TLC_ENABLED_WRONG_FORMULA = 2260; public static final int TLC_ENCOUNTERED_FORMULA_IN_PREDICATE = 2261; public static final int TLC_VERSION = 2262; - public static final int TLC_USAGE = 2263; public static final int TLC_COUNTER_EXAMPLE = 2264; public static final int TLC_INTEGER_TOO_BIG = 2265; diff --git a/tlatools/src/tlc2/output/MP.java b/tlatools/src/tlc2/output/MP.java index 504e98312b44006576fd435b1633f60b6fee771a..0f44b383a7707fce722659570f44ea6a5606c6aa 100644 --- a/tlatools/src/tlc2/output/MP.java +++ b/tlatools/src/tlc2/output/MP.java @@ -414,9 +414,6 @@ public class MP b.append("%1%\nUsage: java tlc2.Simulator [-option] inputfile"); break; /* ----------------------------------------------------------------- */ - case EC.TLC_USAGE: - b.append(Messages.getString("HelpMessage"));// $NON-NLS-1$ - break; case EC.TLC_VERSION: b.append("TLC2 %1%"); break; diff --git a/tlatools/src/tlc2/output/messages.properties b/tlatools/src/tlc2/output/messages.properties index 648e4c06b0491a31f0c33d698b38e77f4ba4e489..1c16a02df39fe3f7c864e727c1b90fa7852a453b 100644 --- a/tlatools/src/tlc2/output/messages.properties +++ b/tlatools/src/tlc2/output/messages.properties @@ -1,53 +1,5 @@ -VersionTag=Version 2.02 of 3 August 2009 -HelpMessage=The model checker (TLC) provides the functionalities of model\n\ -checking or simulation of TLA+ specifications. The syntax for this command is:\n\n\ -java tlc2.TLC [GENERAL-SWITCHES] [MODE-SWITCHES] SPEC\n\n\ -where SPEC is the name of the specification's root module\n\ -and the optional GENERAL-SWITCHES are:\n\ - -checkpoint num: interval between check point (in minutes)\n\ - \tDefaults 30 if not provided.\n\ - -cleanup: clean up the states directory\n\ - -config file: provide the config file.\n\ - \tDefaults to SPEC.cfg if not provided\n\ - -continue: continue running even when invariant is violated\n\ - \tDefaults to stop at the first violation if not specified\n\ - -coverage minutes: interval between collection of coverage information \n\ - \ton the spec in minutes. Defaults to no coverage if not specified\n\ - -deadlock: do not check for deadlock.\n\ - \tDefaults to check deadlock if not specified\n\ - -difftrace: show only the differences between successive states,\n\ - \twhen printing trace. Defaults to print full state descriptions\n\ - -debug: debugging information (not for production use)\n\ - -dump file: dump all the states into file\n\ - -fp num: use the num'th irreducible polynomial from the list \n\ - \tstored in the class FP64.\n\ - -gzip: control if gzip is applied to value input/output stream.\n\ - \tDefaults to off if not specified\n\ - -metadir path: store metadata in the directory at path\n\ - \tDefaults to SPEC-directory/states if not specified\n\ - -recover id: recover from the checkpoint with id\n\ - \tDefaults to scratch run if not specified\n\ - -terse: do not expand values in Print statement\n\ - \tDefaults to expand value if not specified\n\ - -tool: tool mode (put message codes on console)\n\ - -nowarning: disable all the warnings.\n\ - \tDefaults to report warnings if not specified\n\ - -workers num: the number of TLC worker threads. Defaults to 1.\n\n\ +TLCDescription=The model checker (TLC) provides the functionalities of model\n\ +checking or simulation of TLA+ specifications. It may be invoked from the\n\ +command line, or via the model checking functionality of the Toolbox.\n\n\ By default, TLC starts in the model checking mode using breadth-first\n\ -approach for the state space exploration. This can be changed using\n\ -the MODE-SWITCHES. In contrast to the GENERAL-SWITCHES these can be used \n\ -if applied in certain combinations only:\n\n\ -{[-dfid num][ -view]|-simulate[ -depth num][ -aril num][ -seed num]}\n\n\ - -modelcheck: run in model checking mode using breadth-first approach for the\n\ - \tstate space exploration (default)\n\ - -dfid num: run in model checking mode and use depth-first iterative deepening\n\ - \twith initial depth num\n\ - -view: apply VIEW (if provided) when printing out states.\n\ - -simulate: run in simulation mode\n\ - -depth num: specify the depth of random simulation\n\ - \tDefaults to 100 if not specified\n\ - -seed num: provide the seed for random simulation\n\ - \tDefaults to a random seed if not specified)\n\ - -aril num: Adjust the seed for random simulation\n\ - \tDefaults to 0 if not specified\n\ - \ No newline at end of file +approach for the state space exploration. diff --git a/tlatools/src/util/TLAConstants.java b/tlatools/src/util/TLAConstants.java index d4140196e0c088d3cb350bbd29e4de8ab11ecbaa..a8a4aaa1cae79d4bdd00da8a50ab447be472bf3a 100644 --- a/tlatools/src/util/TLAConstants.java +++ b/tlatools/src/util/TLAConstants.java @@ -4,6 +4,12 @@ package util; * A class of bits of keywords, operators, and bears. */ public final class TLAConstants { + public final class ANSI { + public static final String BOLD_CODE = "\033[1m"; + public static final String ITALIC_CODE = "\033[3m"; + public static final String RESET_CODE = "\033[0m"; + } + public final class BuiltInModules { public static final String TLC = "TLC"; public static final String TRACE_EXPRESSIONS = "Toolbox"; diff --git a/tlatools/src/util/UsageGenerator.java b/tlatools/src/util/UsageGenerator.java new file mode 100644 index 0000000000000000000000000000000000000000..ef40ac0a9e917c557b3a5f7518d34748898328d7 --- /dev/null +++ b/tlatools/src/util/UsageGenerator.java @@ -0,0 +1,320 @@ +package util; + +import java.io.PrintStream; +import java.util.ArrayList; +import java.util.Collections; +import java.util.Comparator; +import java.util.HashSet; +import java.util.List; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +/** + * A helper class to print usage text for a command-line-application in a motif reminiscent of manpages. + * + * In a world where we were not concerned with jar size, i would import Apache Commons CLI and take advantage + * of those classes. + */ +public class UsageGenerator { + private static final String NAME = "NAME"; + private static final String SYNOPSIS = "SYNOPSIS"; + private static final String DESCRIPTION = "DESCRIPTION"; + private static final String OPTIONS = "OPTIONS"; + private static final String TIPS = "TIPS"; + + private static Comparator<Argument> NAME_COMPARATOR = new Comparator<Argument>() { + @Override + public int compare(final Argument a, final Argument b) { + return a.getArgumentName().compareTo(b.getArgumentName()); + } + }; + + private static Comparator<Argument> NAME_DASH_COMPARATOR = new Comparator<Argument>() { + @Override + public int compare(final Argument a, final Argument b) { + final boolean aDash = a.isDashArgument(); + final boolean bDash = b.isDashArgument(); + + if (aDash != bDash) { + return aDash ? -1 : 1; + } + + return a.getArgumentName().compareTo(b.getArgumentName()); + } + }; + + + public static void displayUsage(final PrintStream ps, final String commandName, final String version, + final String commandShortSummary, final String commandDescription, + final List<List<Argument>> commandVariants, final List<String> tips, + final char valuedArgumentsSeparator) { + ps.println(); + ps.println(generateSectionHeader(NAME)); + ps.println('\t' + commandName + " - " + commandShortSummary + + ((version != null) ? (" - " + version) : "") + "\n\n"); + + + final String boldName = markupWord(commandName, true); + + + final HashSet<Argument> arguments = new HashSet<>(); + ps.println(generateSectionHeader(SYNOPSIS)); + for (final List<Argument> variant : commandVariants) { + ps.println("\t" + generateCommandForVariant(boldName, variant, arguments, valuedArgumentsSeparator)); + } + ps.println(); + + + final String commandNameRegex = commandName + "(\\)\\s|$)"; + final Pattern p = Pattern.compile(commandNameRegex); + final Matcher m = p.matcher(commandDescription); + final String markedUpDescription; + if (m.find()) { + final StringBuilder sb = new StringBuilder(); + + if (m.start() > 0) { + sb.append(commandDescription.substring(0, m.start())); + } + sb.append(boldName).append(m.group(1)); + + int lastEnd = m.end(); + while (m.find()) { + sb.append(commandDescription.substring(lastEnd, m.start())).append(boldName).append(m.group(1)); + lastEnd = m.end(); + } + sb.append(commandDescription.substring(lastEnd, commandDescription.length())); + + markedUpDescription = sb.toString(); + } else { + markedUpDescription = commandDescription; + } + + ps.println(generateSectionHeader(DESCRIPTION)); + ps.println("\t" + markedUpDescription.replaceAll("(\\r\\n|\\r|\\n)", "\n\t")); + ps.println(); + + + final List<Argument> orderedArguments = new ArrayList<>(arguments); + Collections.sort(orderedArguments, NAME_COMPARATOR); + ps.println(generateSectionHeader(OPTIONS)); + for (final Argument arg : orderedArguments) { + if (arg.expectsValue() || arg.isOptional() || (!arg.expectsValue() && arg.isDashArgument())) { + ps.println(generateOptionText(arg, valuedArgumentsSeparator)); + } + } + ps.println(); + + + if ((tips != null) && (tips.size() > 0)) { + ps.println(generateSectionHeader(TIPS)); + for (final String tip : tips) { + ps.println("\t" + tip.replaceAll("(\\r\\n|\\r|\\n)", "\n\t") + "\n"); + } + } + } + + private static String generateCommandForVariant(final String boldedCommandName, final List<Argument> variant, + final HashSet<Argument> arguments, + final char valuedArgumentsSeparator) { + final List<Argument> optionalSingleDashValueless = new ArrayList<>(); + final List<Argument> optionalDoubleDashValueless = new ArrayList<>(); + final List<Argument> optionalValued = new ArrayList<>(); + final List<Argument> requiredValued = new ArrayList<>(); + final List<Argument> requiredValueless = new ArrayList<>(); + + for (final Argument arg : variant) { + if (arg.expectsValue()) { + if (arg.isOptional()) { + optionalValued.add(arg); + } else { + requiredValued.add(arg); + } + } else { + if (arg.isOptional()) { + if (arg.isDashArgument()) { + optionalSingleDashValueless.add(arg); + } else if (arg.isDashDashArgument()) { + optionalDoubleDashValueless.add(arg); + } + } else { + requiredValueless.add(arg); + } + } + } + + Collections.sort(optionalSingleDashValueless, NAME_COMPARATOR); + Collections.sort(optionalDoubleDashValueless, NAME_COMPARATOR); + Collections.sort(optionalValued, NAME_COMPARATOR); + Collections.sort(requiredValued, NAME_COMPARATOR); + Collections.sort(requiredValueless, NAME_DASH_COMPARATOR); + + final StringBuilder sb = new StringBuilder(boldedCommandName); + + if (optionalSingleDashValueless.size() > 0) { + final StringBuilder concatenation = new StringBuilder("-"); + final List<Argument> nonShortArguments = new ArrayList<>(); + for (final Argument arg : optionalSingleDashValueless) { + if (arg.isShortArgument()) { + concatenation.append(arg.getDashlessArgumentName()); + } else { + nonShortArguments.add(arg); + } + } + if (concatenation.length() > 1) { + sb.append(" [").append(markupWord(concatenation.toString(), true)).append(']'); + } + + for (final Argument arg : nonShortArguments) { + sb.append(" [").append(markupWord(("-" + arg.getDashlessArgumentName()), true)).append(']'); + } + } + + if (optionalDoubleDashValueless.size() > 0) { + for (final Argument arg : optionalDoubleDashValueless) { + sb.append(" [").append(markupWord(arg.getArgumentName(), true)).append(']'); + } + } + + if (optionalValued.size() > 0) { + for (final Argument arg : optionalValued) { + sb.append(" [").append(markupWord(arg.getArgumentName(), true)).append(valuedArgumentsSeparator); + sb.append(markupWord(arg.getSampleValue(), false)).append(']'); + } + } + + if (requiredValued.size() > 0) { + for (final Argument arg : optionalValued) { + sb.append(" ").append(markupWord(arg.getArgumentName(), true)).append(valuedArgumentsSeparator); + sb.append(markupWord(arg.getSampleValue(), false)); + } + } + + if (requiredValueless.size() > 0) { + for (final Argument arg : requiredValueless) { + sb.append(" ").append(arg.getArgumentName()); + } + } + + arguments.addAll(variant); + + return sb.toString(); + } + + private static String generateOptionText(final Argument argument, final char valuedArgumentsSeparator) { + final StringBuilder sb = new StringBuilder("\t"); + + sb.append(markupWord(argument.getArgumentName(), true)); + if (argument.expectsValue()) { + sb.append(valuedArgumentsSeparator).append(markupWord(argument.getSampleValue(), false)); + } + sb.append("\n\t\t").append(argument.getDescription().replaceAll("(\\r\\n|\\r|\\n)", "\n\t\t")); + + return sb.toString(); + } + + private static String generateSectionHeader(final String title) { + final StringBuilder sb = new StringBuilder(markupWord(title, true)); + + sb.append('\n'); + + return sb.toString(); + } + + /** + * @param bold if true, the word will be bolded; false, the word will be italicized + */ + private static String markupWord(final String word, final boolean bold) { + final StringBuilder sb = new StringBuilder(bold ? TLAConstants.ANSI.BOLD_CODE : TLAConstants.ANSI.ITALIC_CODE); + + sb.append(word).append(TLAConstants.ANSI.RESET_CODE); + + return sb.toString(); + } + + + public static class Argument { + private final String argumentName; + private final String sampleValue; + private final String description; + private final boolean optional; + + /** + * This calls {@code this(key, optionDescription, false);} + * + * @param key + * @param optionDescription + */ + public Argument(final String key, final String optionDescription) { + this(key, optionDescription, false); + } + + public Argument(final String key, final String optionDescription, final boolean isOptional) { + this(key, null, optionDescription, isOptional); + } + + /** + * This calls {@code this(key, exampleValue, optionDescription, false);} + */ + public Argument(final String key, final String exampleValue, final String optionDescription) { + this(key, exampleValue, optionDescription, false); + } + + public Argument(final String key, final String exampleValue, final String optionDescription, + final boolean isOptional) { + argumentName = key; + sampleValue = exampleValue; + description = optionDescription; + optional = isOptional; + } + + public boolean isOptional() { + return optional; + } + + public boolean expectsValue() { + return (sampleValue != null); + } + + /** + * @return if the argument name starts with "-", but not "--", this returns true + */ + public boolean isDashArgument() { + return argumentName.startsWith("-") && !isDashDashArgument(); + } + + public boolean isDashDashArgument() { + return argumentName.startsWith("--"); + } + + /** + * @return true if the argument name is of length 1 (two if this is a dash argument) + */ + public boolean isShortArgument() { + return ((isDashArgument() && (argumentName.length() == 2)) || (argumentName.length() == 1)); + } + + public String getArgumentName() { + return argumentName; + } + + /** + * @return if {@link #isDashArgument()} returns true, this retuns the argument name without the prefacing dash, + * otherwise this returns the entire argument name + */ + public String getDashlessArgumentName() { + if (isDashArgument()) { + return argumentName.substring(1); + } + + return argumentName; + } + + public String getSampleValue() { + return sampleValue; + } + + public String getDescription() { + return description; + } + } +}