TLC Model Checker

TLC is an explicit state model checker originally written by Yu et al. [1999] to verify TLA+ specifications. TLC can check a subset of TLA+ that is commonly needed to describe real-world systems, most notably finite systems.

To run it, you will need Java runtime environment version 11.

You can always download the latest stable release from the release page on github: https://github.com/tlaplus/tlaplus/releases/

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

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.

See https://docs.oracle.com/en/java/javase/20/gctuning/available-collectors.html#GUID-F215A508-9E58-40B4-90A5-74E29BF3BD3C

If (a) peak application performance is the first priority and (b) there are no pause-time requirements or pauses of one second or longer are acceptable, then let the VM select the collector or select the parallel collector with -XX:+UseParallelGC.

Simulation, nor Model Checking seem to work well with G1GC, but Trace Validation does not for some reason, and is much slower unless -XX:+UseParallelGC is used.

In all cases, pauses don’t matter, only throughput does.

java -XX:+UseParallelGC

You can always access the latest information by using

java -jar ./dist/tla2tools.jar -help

Not all options are exposed through it though. These are the options that are supported but missing from the -help:

• -lncheck: Check liveness properties at different times of model checking. Supported values are “default”, “final”, “seqfinal”. “default” will check liveness at every step, while final will search it only at the end of the exploration. “seqfinal” is anlias for “final”. -lncheck final option postpones the search of Strongly Connected Components in the behavior graph until after the safety check has been completed

These are all the options outputted from the cli 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.

Some flags can be set passing java parameters to tlc, they are mostly undocumented (for now) and can be found by searching for “Boolean.getBoolean” in the codebase.

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.