Add tlc options

src/SUMMARY.md

@@ -24,11 +24,12 @@
     - [Pluscal]()
         - []()
     - [TLA+ Vs xxx](./learning/tla-comparisons.md)
+    - [Config files](./learning/config-file.md)
 - [Learning TLAP]()
 - [Tools](./using/intro.md)
     - [Vscode extension](./using/vscode.md)
     - [Toolbox](./using/toolbox.md)
-    - [TLC CLI](./using/tlc-cli.md)
+    - [TLA2Tools - CLI](./using/tla2tools-cli.md)
     - [Standard Library](./using/standard-lib.md)
     - [Community Modules](./using/community-modules.md)
     - [Debugger](./using/debugger.md)

src/learning/config-file.md

@@ -0,0 +1 @@
+# Config files

src/using/tla2tools-cli.md

@@ -0,0 +1,181 @@
+# TLA2Tools - CLI
+TLA tools contain all the tools related to tla+ and tlc:
+ * model checker
+ * SANY
+
+To run them, you will need Java runtime environment version 11.
+
+## Getting the latest stable release
+You can always download the latest stable release from the release page on github: https://github.com/tlaplus/tlaplus/releases/
+
+
+## Building TLC from sources
+You will need JDK 11 and ant.
+1. Download the repository from github: https://github.com/tlaplus/tlaplus
+2. Go to tlaplus/tlatools/org.lamport.tlatools and run: `ant -f customBuild.xml compile dist`
+
+You can then find the jar file inside tlaplus/tlatools/org.lamport.tlatools/dist/tla2tools.jar
+
+## Running the tla2tools.jar
+To run the TLC model checker:
+```
+java -jar ./dist/tla2tools.jar <MySpec.tla>
+```
+the cli will automatically use the config file called MySpec.cfg in that same directory, if present.
+
+## Parameters
+You can always access the latest information by using
+```
+java -jar ./dist/tla2tools.jar -help
+```
+These are all the options supported at the time of writing from master:
+```
+    -aril num
+            adjust the seed for random simulation; defaults to 0
+    -checkpoint minutes
+            interval between check point; defaults to 30
+    -cleanup
+            clean up the states directory
+    -config file
+            provide the configuration file; defaults to SPEC.cfg
+    -continue
+            continue running even when an invariant is violated; default
+            behavior is to halt on first violation
+    -coverage minutes
+            interval between the collection of coverage information;
+            if not specified, no coverage will be collected
+    -deadlock
+            if specified DO NOT CHECK FOR DEADLOCK. Setting the flag is
+            the same as setting CHECK_DEADLOCK to FALSE in config
+            file. When -deadlock is specified, config entry is
+            ignored; default behavior is to check for deadlocks
+    -debug
+            print various debugging information - not for production use
+            
+    -debugger nosuspend
+            run simulation or model-checking in debug mode such that TLC's
+            state-space exploration can be temporarily halted and variables
+            be inspected. The only debug front-end so far is the TLA+
+            VSCode extension, which has to be downloaded and configured
+            separately, though other front-ends could be implemeted via the
+            debug-adapter-protocol.
+            Specifying the optional parameter 'nosuspend' causes
+            TLC to start state-space exploration without waiting for a
+            debugger front-end to connect. Without 'nosuspend', TLC
+            suspends state-space exploration before the first ASSUME is
+            evaluated (but after constants are processed). With 'nohalt',
+            TLC does not halt state-space exploration when an evaluation
+            or runtime error is caught. Without 'nohalt', evaluation or
+            runtime errors can be inspected in the debugger before TLC
+            terminates. The optional parameter 'port=1274' makes the
+            debugger listen on port 1274 instead of on the standard
+            port 4712, and 'port=0' lets the debugger choose a port.
+            Multiple optional parameters must be comma-separated.
+            Specifying '-debugger' implies '-workers 1'.
+    -depth num
+            specifies the depth of random simulation; defaults to 100
+    -dfid num
+            run the model check in depth-first iterative deepening
+            starting with an initial depth of 'num'
+    -difftrace
+            show only the differences between successive states when
+            printing trace information; defaults to printing
+            full state descriptions
+    -dump file
+            dump all states into the specified file; this parameter takes
+            optional parameters for dot graph generation. Specifying
+            'dot' allows further options, comma delimited, of zero
+            or more of 'actionlabels', 'colorize', 'snapshot' to be
+            specified before the '.dot'-suffixed filename
+    -dumpTrace format file
+            in case of a property violation, formats the TLA+ error trace
+            as the given format and dumps the output to the specified
+            file.  The file is relative to the same directory as the
+            main spec. At the time of writing, TLC supports the "tla"
+            and the "json" formats.  To dump to multiple formats, the
+            -dumpTrace parameter may appear multiple times.
+            The git commits 1eb815620 and 386eaa19f show that adding new
+            formats is easy.
+            
+    -fp N
+            use the Nth irreducible polynomial from the list stored
+            in the class FP64
+    -fpbits num
+            the number of MSB used by MultiFPSet to create nested
+            FPSets; defaults to 1
+    -fpmem num
+            a value in (0.0,1.0) representing the ratio of total
+            physical memory to devote to storing the fingerprints
+            of found states; defaults to 0.25
+    -gzip
+            control if gzip is applied to value input/output streams;
+            defaults to 'off'
+    -h
+            display these help instructions
+    -maxSetSize num
+            the size of the largest set which TLC will enumerate; defaults
+            to 1000000 (10^6)
+    -metadir path
+            specify the directory in which to store metadata; defaults to
+            SPEC-directory/states if not specified
+    -noGenerateSpecTE
+            Whether to skip generating a trace exploration (TE) spec in
+            the event of TLC finding a state or behavior that does
+            not satisfy the invariants; TLC's default behavior is to
+            generate this spec.
+    -nowarning
+            disable all warnings; defaults to reporting warnings
+    -postCondition mod!oper
+            evaluate the given (constant-level) operator oper in the TLA+
+            module mod at the end of model-checking.
+    -recover id
+            recover from the checkpoint with the specified id
+    -seed num
+            provide the seed for random simulation; defaults to a
+            random long pulled from a pseudo-RNG
+    -simulate
+            run in simulation mode; optional parameters may be specified
+            comma delimited: 'num=X' where X is the maximum number of
+            total traces to generate and/or 'file=Y' where Y is the
+            absolute-pathed prefix for trace file modules to be written
+            by the simulation workers; for example Y='/a/b/c/tr' would
+            produce, e.g, '/a/b/c/tr_1_15'
+    -teSpecOutDir some-dir-name
+            Directory to which to output the TE spec if TLC generates
+            an error trace. Can be a relative (to root spec dir)
+            or absolute path. By default the TE spec is output
+            to the same directory as the main spec.
+    -terse
+            do not expand values in Print statements; defaults to
+            expanding values
+    -tool
+            run in 'tool' mode, surrounding output with message codes;
+            if '-generateSpecTE' is specified, this is enabled
+            automatically
+    -userFile file
+            an absolute path to a file in which to log user output (for
+            example, that which is produced by Print)
+    -view
+            apply VIEW (if provided) when printing out states
+    -workers num
+            the number of TLC worker threads; defaults to 1. Use 'auto'
+            to automatically select the number of threads based on the
+            number of available cores.
+```
+
+
+## Good to know:
+When using the  '-generateSpecTE' you can version the generated specification by doing:
+
+    ./tla2tools.jar -generateSpecTE MySpec.tla && NAME="SpecTE-$(date +%s)" && sed -e "s/MODULE SpecTE/MODULE $NAME/g" SpecTE.tla > $NAME.tla
+
+If, while checking a SpecTE created via '-generateSpecTE', you get an error message concerning
+CONSTANT declaration and you've previous used 'integers' as model values, rename your
+model values to start with a non-numeral and rerun the model check to generate a new SpecTE.
+
+If, while checking a SpecTE created via '-generateSpecTE', you get a warning concerning
+duplicate operator definitions, this is likely due to the 'monolith' specification
+creation. Try re-running TLC adding the 'nomonolith' option to the '-generateSpecTE'
+parameter.
+
+When using more than one worker, the reported depth might differ across runs. For small models, use a single worker. For large models, the diameter will almost always appear deterministic.