tlc_coverage
Run the TLC model checker with action coverage reporting to identify under-explored parts of a specification by tracking how often each action is taken and how many distinct states it produces.
Instructions
Run TLC model checker with action coverage reporting. Shows how many times each action was taken and how many distinct states it produced, helping identify under-explored parts of the spec.
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) | |
| interval_minutes | No | Coverage reporting interval in minutes (default 1) | |
| workers | No | Number of worker threads, or 'auto' for all cores | |
| extra_args | No | Additional raw arguments to pass to TLC |