tlc_simulate
Randomly explore execution traces of TLA+ specifications to quickly test large state spaces. Use simulation mode for faster checks where exhaustive verification is impractical.
Instructions
Run TLC in simulation mode to randomly explore execution traces. Faster than exhaustive checking but not complete — useful for large state spaces or quick smoke tests.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| tla_file | Yes | Absolute path to the .tla specification file | |
| cfg_file | No | Path to .cfg file (defaults to same basename as tla_file with .cfg extension) | |
| depth | No | Maximum depth of each simulation trace (default 100) | |
| num_traces | No | Number of traces to generate | |
| seed | No | Random seed for reproducibility | |
| aril | No | Aril (adjusts the random seed) | |
| workers | No | Number of worker threads, or 'auto' for all cores | |
| deadlock | No | Check for deadlock (default true). Set false to disable deadlock checking. | |
| diff_trace | No | Show only changed variables between trace states | |
| extra_args | No | Additional raw arguments to pass to TLC |