1.7 KiB
1.7 KiB
2. Using the toolbox
Model configuration (selected, not exhaustive)
State/action constraints
Using the TLC CLI, state constraints are declared using CONSTRAINT <property>,
where the property is a boolean in the spec.
See topics2_contraint for an example
Definition override
LearnTLA+ says it is possible to override definitions, like Int <- 1..10,
but that appears to be a specific feature to the Toolbox, since plain CFG files
do not support the .. operator anyway, and it is unclear when such overrides
are really possible. This may be a consequence of the toolbox generating a
semi-hidden "MC" spec and config on each run, enabling features like this,
which combine TLA+ and TLC CFG capabilities.
Additional TLC options (selected)
- There are options for #threads, RAM, etc: see tlc2 --help
VIEWoverrides the way TLC distinguishes states using variables- a reduced view may make the run more efficient
- but it may "wreck your spec" by merging states that should be different
- described a dark magic
- depth-first
- By default, TLC uses a breadth-first search, but this can be overridden
- This is useful for invariants that can only be triggered deep in the behaviour
- Enables specifying a maximum depth of search, which is useful for unbound models
- simulation mode disables liveness checks
- it never stops, even when the state space is exhausted, so needs to be killed manually
- profiling is available at two levels
- "Action enablement" counts action calls and shows it in statistics
- An action never being enabled means there is an error in the spec.
- "On" counts more, to help optimizing models:
- operator calls
- expression branch uses
- operator costs
- "Action enablement" counts action calls and shows it in statistics