learning_tla/learn_tla/03_cli.md

3. Beyond toolbox: the CLI tools

Up-to-date list: https://github.com/tlaplus/tlaplus/blob/master/general/docs/current-tools.md

The CLI

SANY and Tla2tex

See https://lamport.azurewebsites.net/tla/current-tools.pdf

Limitations

\* When using TLC, replace
IM(x) == INSTANCE M
ISpec == IM(xbar)!Spec
\* by this equivalent notation
IM == INSTANCE M WITH x <- xbar
ISpec == IM!Spec

Enhanced replacement

The "definition override" feature of the Toolbox is available from the module CFG file:

• foo <- bar in a CFG file
• will replace foo by bar everywhere in the spec and its EXTEND imports,
• will NOT replace them in INSTANCE imports
• foo <- [Mod] bar in a CFG file
  • will replace foo by bar everywhere module Mod and its EXTEND imports only,
  • will NOT replace them in INSTANCE imports

Strings

• Strings are sequences in TLA+, not completely in TLC.
  • "ab" \o "c" = "abc", but Len is incorrect on strings with ""-escapes.

PlusCal translator

On the CLI, invoke like java -cp tla2tools.jar pcal.trans file.tla

• will create file.old as a backup. Cannot be avoided
• will rewrite file.cfg
  • regenerating everything above the line \* Add statements after this line.
  • preserving anything below it
  • won't do it when using the -nocfg flag

TLC2

Config file

Keyword and example	Max#	Multiple	Description
ACTION_CONSTRAINT AC1	n	?	Specifies action constraints to limit transitions
ALIAS SomeAlias	1	?	Replaces the error trace by the designated property, which must be a record
CHECK_DEADLOCK TRUE	1	N	Enables or disables deadlock checking
CONSTANT Const1 = Value1	n	?	Assigns values to constants declared in the TLA+ specification
CONSTRAINT Constraint1	n	?	Specifies state constraints to limit the state space
INIT InitPredicate	1	N	Specifies the initial state predicate or overrides it
INVARIANT Inv1	n	Y	Specifies an invariant that should hold in every reachable state
NEXT NextPredicate	1	N	Specifies the next-state relation or overrides it
PROPERTY Prop1	n	Y	Specifies temporal properties to be checked
SPECIFICATION Spec	1	N	Specifies the name of the specification to be checked
SYMMETRY SymmetrySet	n	?	Specifies symmetry sets to reduce the state space
Nat <- {1, 2, 3}	n	N	Overrides definitions or constants using <-

• SPECIFICATION
  • Use either SPECIFICATION or INIT+NEXT but not both.
  • The name of the specification is conventionally Spec, but it is not a requirement.
• INVARIANT
  • Unlike the toolbox, expression invariants are not supported: use named operators instead
  • That's what the toolbox really does in its semi-hidden MC spec+model
• CONSTANT values can be simple values, sets of such, but not functions or expression.
  • ... like 1..10
  • For model values, use CONSTANT foo = foo, bar = {baz, qux}
  • multiple constants are one-per-line, not comma-separated
• ALIAS directives accepts a record only,
  • they will display it in the error trace as a replacement of the default output.
  • See example in topic2_alias
  • In the Toolbox, this is achieved by adding expressions to the "Error-Trace exploration panel".

TLC Options

Use tlc2.TLC -help, not tlc2.TLC -h for the complete list:

Selected flags:

• -continue: do not stop on first error
• -dump <outfile>: writes all the reached states, unordered. The format looks like:

State 1:
/\ counter = 0
/\ lock = NULL
/\ pc = <<"GetLock", "GetLock">>
/\ tmp = <<0, 0>>

State 2:
/\ counter = 0
/\ lock = 1
/\ pc = <<"GetCounter", "GetLock">>
/\ tmp = <<0, 0>>

\* ...etc...

• -workers <num>|auto: the CLI defaults to 1 worker. Pass auto to use as many workers as cores
• -fpmem 0.xx: fraction of the system memory to use for model checking, defaulting to 0.25