38 lines
1.7 KiB
Markdown
38 lines
1.7 KiB
Markdown
# 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](topics2_constraint.cfg) 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
|
|
- `VIEW` overrides 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
|