TLA+ | The way to specify

This tutorial describes the command line switches accepted by the console-based TLA+ Tools: SANY, TLC, and the PlusCal Translator. Most users will run the tools from the Toolbox, in which case the switches for SANY and TLC are irrelevant. When running the Toolbox, command line switches for the PlusCal translator can be provided in a specification’s Preferences menu. However, starting with Version 1.5 of the translator, the most useful options can be specified in the module containing the algorithm. (See the language manual.)

The command line switches are detected, by the fact that they begin with a ‘-’ character. Once the first command line element that is not a switch is encountered, the rest are presumed to be file names.

SANY, the Syntax Analyzer

java tla2sany.SANY [-S] [-L] [-D] [-STAT] FILES

where FILES is a list of modules separated by spaces and

• -S: disable semantic analysis
• -L: disable level checking
• -D: enable debugging
• -STAT: print statistics

The switches are useful for finding errors in SANY ony and are not providing particular helpful features for the user.

TLC, the Model Checker

The model checker (TLC) provides the following functionalities:

• Model checking of TLA+ specs
• Simulation of TLA+ specs

The program can be executed by typing the following to the console

java tlc2.TLC [GENERAL-SWITCHES] [MODE-SWITCHES] SPEC

where SPEC is the name of the specification’s root module (the .tla extension can be omitted) and the optional GENERAL-SWITCHES are:

• -cleanup: clean up the states directory
• -config file: provide the config file. Defaults to .cfg if not provided.
• -continue: continue running even when invariant is violated. Defaults to stop at the first violation if not specified.
• -coverage minutes: collect coverage information on the spec, print out the information every minutes. Defaults to no coverage if not specified.
• -deadlock: do not check for deadlock. Defaults to checking deadlock if not specified.
• -difftrace: when printing trace, show only the differences between successive states. Defaults to printing full state descriptions if not specified.
• -dump file: dump all the states into file
• -fp num: use the num’th irreducible polynomial from the list stored in the class FP64.
• -gzip: control if gzip is applied to value input/output stream. Defaults to use gzip.
• -metadir path: store metadata in the directory at path. Defaults to specdir/states if not specified.
• -nowarning: disable all the warnings. Defaults to report warnings if not specified
• -recover path: recover from the checkpoint at path. Defaults to scratch run if not specified.
• -terse: do not expand values in Print statement. Defaults to expand value if not specified.
• -workers num: the number of TLC worker threads. Defaults to 1.

By default TLC starts in the model checking mode using breadth-first approach for state space exploration. This can be changed using the MODE-SWITCHES. In contrast to the GENERAL-SWITCHES these can be used if applied in certain combinations only:

{[-dfid num][ -view]|-simulate[ -depth num][ -aril num][ -seed num]}

• -modelcheck: run model checking and explore the state space in breadth first manner. This is a default mode.
• -dfid num: run model checking and use depth-first iterative deepening with initial depth num
• -view: apply VIEW (if provided) when printing out states. Applicable only in model checking mode.
• -simulate: run simulation
• -depth num: specify the depth of random simulation. Defaults to 100 if not specified, relevant for simulation mode only.
• -seed num: provide the seed for random simulation. Defaults to a random seed if not specified, relevant for simulation mode only.
• -aril num: adjust the seed for random simulation. Defaults to 0 if not specified, relevant for simulation mode only.

PlusCal, the Translator

The PlusCal translator translates a PlusCal algorithm into a TLA+ specification. The translator is called by typing

java pcal.trans [SWITCHES] SPEC

where SPEC is a TLA+ file (the extension .tla need not be typed)
containing the algorithm. See the PlusCal manual for an explanation of
what the TLA+ file must contain. The possible options are

• -help: Prints out the usage instead of running the translator.
• -wf: Conjoin to formula Spec weak fairness of each process’s next-state action
• -sf: Conjoin to formula Spec strong fairness of each process’s next-state action
• -wfNext: Conjoin to formula Spec weak fairness of the entire next-state action
• -nof: Conjoin no fairness formula to Spec. This is the default, except when the -termination option is chosen.
• -termination: Add to the .cfg file the command PROPERTY Termination With this option, the default fairness option becomes -wf.
• -nocfg: Suppress writing of the .cfg file.
• -label: Tells the translator to add missing labels. This is the default only for a uniprocess algorithm in which the user has typed no labels.
• -reportLabels: True if the translator should print the names and locations of all labels it adds. Like -label, it tells the translator to add missing labels.
• -labelRoot name: If the translator adds missing labels, it names them name1, name2, etc. The default value is “Lbl_”.
• -unixEOL: Forces the use of Unix end-of-line convention, regardless of the system’s default. Without this, when run on Windows, the files it writes seem to have a “^M” at the end of every line when viewed with Emacs.
• -debug: This is useful only for maintainers of the program and has no effect on normal execution.
• -reportLabels: True if the translator should print the names and locations of all labels it adds. Like -label, it tells the translator to add missing labels.
• -lineWidth: The translation tries to perform the translation so lines have this maximum width. (It will often fail.) Default is 78, minimum value is 60.
• -version: The version of PlusCal for which this algorithm is written. If the language is ever changed to make algorithms written for earlier versions no longer legal, then the translator should do the appropriate thing when the earlier version number is specified.

Starting with Version 1.5, the following options no longer work. They can be used only if the -version 1.4 option is also used. Moreover, the -writeAST option does not work from the Toolbox. If there is any demand, these options may be made to work again in later versions.

• -spec name: Uses TLC and the TLA+ specification name.tla to do the translation. It copies the files name.tla and name.cfg from the directory containing the translator’s Java source files to the current directory; it writes in the current director the file AST.tla that defines `fairness’ to equal the fairness option and `ast’ to equal the the AST data structure representing the algorithm; and it runs TLC on name.tla to produce the translation.
• -myspec name: Like -spec, except it finds the files names.tla and names.cfg in the current directory, instead of writing them there.
• -spec2 name: Like -spec, except it uses TLC2 insead of the old version of TLC (aka TLC1).
• -myspec2 name: Like -myspec, except it uses TLC2 instead of TLC (aka TLC1).
• -writeAST: Writes the AST file as in the -spec option, but does not perform the translation.