107 lines
4.5 KiB
Markdown
107 lines
4.5 KiB
Markdown
# 3. Beyond toolbox: the CLI tools
|
|
|
|
Up-to-date list: https://github.com/tlaplus/tlaplus/blob/master/general/docs/current-tools.md
|
|
|
|
## The CLI
|
|
|
|
### SANY and Tla2tex
|
|
|
|
See https://lamport.azurewebsites.net/tla/current-tools.pdf
|
|
|
|
### Limitations
|
|
|
|
```tla+ code fragment
|
|
\* When using TLC, replace
|
|
IM(x) == INSTANCE M
|
|
ISpec == IM(xbar)!Spec
|
|
\* by this equivalent notation
|
|
IM == INSTANCE M WITH x <- xbar
|
|
ISpec == IM!Spec
|
|
```
|
|
|
|
### Enhanced replacement
|
|
|
|
The "definition override" feature of the Toolbox is available from the module CFG file:
|
|
|
|
- `foo <- bar` in a CFG file
|
|
- will replace `foo` by `bar` everywhere in the spec and its `EXTEND` imports,
|
|
- will NOT replace them in `INSTANCE` imports
|
|
- `foo <- [Mod] bar` in a CFG file
|
|
- will replace `foo` by `bar` everywhere module `Mod` and its `EXTEND` imports only,
|
|
- will NOT replace them in `INSTANCE` imports
|
|
|
|
### Strings
|
|
|
|
- Strings are sequences in TLA+, not completely in TLC.
|
|
- `"ab" \o "c" = "abc"`, but `Len` is incorrect on strings with "\"-escapes.
|
|
|
|
## PlusCal translator
|
|
|
|
On the CLI, invoke like `java -cp tla2tools.jar pcal.trans file.tla`
|
|
|
|
- will create `file.old` as a backup. Cannot be avoided
|
|
- will rewrite `file.cfg`
|
|
- regenerating everything above the line `\* Add statements after this line.`
|
|
- preserving anything below it
|
|
- won't do it when using the `-nocfg` flag
|
|
|
|
## TLC2
|
|
|
|
### Config file
|
|
|
|
| Keyword and example | Max# | Multiple | Description |
|
|
|----------------------------|:----:|:--------:|-----------------------------------------------------------------------------|
|
|
| `ACTION_CONSTRAINT AC1` | n | ? | Specifies action constraints to limit transitions |
|
|
| `ALIAS SomeAlias` | 1 | ? | Replaces the error trace by the designated property, which must be a record |
|
|
| `CHECK_DEADLOCK TRUE` | 1 | N | Enables or disables deadlock checking |
|
|
| `CONSTANT Const1 = Value1` | n | ? | Assigns values to constants declared in the TLA+ specification |
|
|
| `CONSTRAINT Constraint1` | n | ? | Specifies state constraints to limit the state space |
|
|
| `INIT InitPredicate` | 1 | N | Specifies the initial state predicate or overrides it |
|
|
| `INVARIANT Inv1` | n | Y | Specifies an invariant that should hold in every reachable state |
|
|
| `NEXT NextPredicate` | 1 | N | Specifies the next-state relation or overrides it |
|
|
| `PROPERTY Prop1` | n | Y | Specifies temporal properties to be checked |
|
|
| `SPECIFICATION Spec` | 1 | N | Specifies the name of the specification to be checked |
|
|
| `SYMMETRY SymmetrySet` | n | ? | Specifies symmetry sets to reduce the state space |
|
|
| `Nat <- {1, 2, 3}` | n | N | Overrides definitions or constants using `<-` |
|
|
|
|
- `SPECIFICATION`
|
|
- Use either `SPECIFICATION` or `INIT`+`NEXT` but not both.
|
|
- The name of the specification is conventionally `Spec`, but it is not a requirement.
|
|
- `INVARIANT`
|
|
- Unlike the toolbox, expression invariants are not supported: use named operators instead
|
|
- That's what the toolbox really does in its semi-hidden `MC` spec+model
|
|
- `CONSTANT` values can be simple values, sets of such, but not functions or expression.
|
|
- ... like 1..10
|
|
- For model values, use `CONSTANT foo = foo, bar = {baz, qux}`
|
|
- multiple constants are one-per-line, not comma-separated
|
|
- `ALIAS` directives accepts a **record** only,
|
|
- they will display it in the error trace as a replacement of the default output.
|
|
- See example in [topic2_alias](topics2_alias.tla)
|
|
- In the Toolbox, this is achieved by adding expressions to the "Error-Trace exploration panel".
|
|
|
|
## TLC Options
|
|
|
|
Use `tlc2.TLC -help`, not `tlc2.TLC -h` for the complete list:
|
|
|
|
Selected flags:
|
|
|
|
- `-continue`: do not stop on first error
|
|
- `-dump <outfile>`: writes all the reached states, unordered. The format looks like:
|
|
```
|
|
State 1:
|
|
/\ counter = 0
|
|
/\ lock = NULL
|
|
/\ pc = <<"GetLock", "GetLock">>
|
|
/\ tmp = <<0, 0>>
|
|
|
|
State 2:
|
|
/\ counter = 0
|
|
/\ lock = 1
|
|
/\ pc = <<"GetCounter", "GetLock">>
|
|
/\ tmp = <<0, 0>>
|
|
|
|
\* ...etc...
|
|
```
|
|
|
|
- `-workers <num>|auto`: the CLI defaults to 1 worker. Pass `auto` to use as many workers as cores
|
|
- `-fpmem 0.xx`: fraction of the system memory to use for model checking, defaulting to 0.25
|