Iteration on TLC wrapper script

[achamayou]

We have centralised some useful things in tlc.sh, but a lot of flags remain expanded inline in YAML, and tend to be copy-pasted per invocation. We then require extra descriptions, which can fall out of sync, to get readable CI steps. We also increasingly rely on environment variables, which are not necessarily validated nor discoverable.

tlc.py sets context-appropriate defaults, and exposes as CLI flags all options we currently use:

$ ./tlc.py --help
usage: tlc.py [-h] [-x] [-n] [--disable-cdot] [--workers WORKERS] [--checkpoint CHECKPOINT] [--lncheck {final,default}] [--jmx] [--dot]
              [--trace-name TRACE_NAME] [--config CONFIG]
              {mc,tv,sim} ... spec

TLC model checker wrapper for the CCF project

positional arguments:
  {mc,tv,sim}
    mc                  Model checking
    tv                  Trace validation
    sim                 Simulation
  spec                  Path to the TLA+ specification

optional arguments:
  -h, --help            show this help message and exit
  -x                    Print out command and environment before running
  -n                    Print out command and environment, but do not run
  --disable-cdot        Disable \cdot support
  --workers WORKERS     Number of workers to use, default is 'auto'
  --checkpoint CHECKPOINT
                        Checkpoint interval, default is 0
  --lncheck {final,default}
                        Liveness check, set to 'default' to run periodically or 'final' to run once at the end, default is final
  --jmx                 Enable JMX to allow monitoring, use echo 'get -b tlc2.tool:type=ModelChecker CurrentState' | jmxterm -l localhost:55449 -i to query
  --dot                 Generate a dot file for the state graph
  --trace-name TRACE_NAME
                        Name to give to the trace files, defaults to the config name if provided, otherwise to the base name of the spec
  --config CONFIG       Path to the TLA+ configuration, defaults to spec name

The following subcommands are available:

Model Checking

$ ./tlc.py mc --help
usage: tlc.py mc [-h] [--term-count TERM_COUNT] [--request-count REQUEST_COUNT] [--raft-configs RAFT_CONFIGS] [--disable-check-quorum]

optional arguments:
  -h, --help            show this help message and exit
  --term-count TERM_COUNT
                        Number of terms the nodes are allowed to advance through, defaults to 0
  --request-count REQUEST_COUNT
                        Number of requests the nodes are allowed to advance through, defaults to 3
  --raft-configs RAFT_CONFIGS
                        Raft configuration sequence, defaults to 1C2N
  --disable-check-quorum
                        Disable CheckQuorum action

Trace Validation

$ ./tlc.py tv --help
usage: tlc.py tv [-h] [--disable-dfs] [--ccf-raft-trace CCF_RAFT_TRACE]

optional arguments:
  -h, --help            show this help message and exit
  --disable-dfs         Set TLC to use depth-first search
  --ccf-raft-trace CCF_RAFT_TRACE
                        Path to a CCF Raft trace .ndjson file, for example produced by make_traces.sh

Simulation

$ ./tlc.py sim --help
usage: tlc.py sim [-h] [--num NUM] [--depth DEPTH] [--max-seconds MAX_SECONDS]

optional arguments:
  -h, --help            show this help message and exit
  --num NUM             Number of behaviours to simulate per worker thread
  --depth DEPTH         Set the depth of the simulation, defaults to 500
  --max-seconds MAX_SECONDS
                        Set the timeout of the simulation, defaults to 1200 seconds

This PR also includes some renaming to follow platform conventions, and remove the ambiguity caused by Limit variables with regards to the state space being explored.

[lemmy]

We also increasingly rely on environment variables, which are not necessarily validated nor discoverable

The .tla specifications validate the environment variables and define their valid values.

[achamayou]

We also increasingly rely on environment variables, which are not necessarily validated nor discoverable

The .tla specifications validate the environment variables and define their valid values.

They do for the values to some extent, but not the variables themselves, so if something is unset or mistyped, a default is picked, and it's easy to miss because the output is very verbose. There is also no way to --help and get a documented list.