Model Checking
TLA+
The TLA toolbox has the TLC model checking and TLAPS.
The properties that TLA+ checks:
- Doesn't produce a wrong answer
- Checks conditions on individual executions, not statistical conclusions
A step is a change of state.
An execution is a represented as a sequence of states.
TLA does not support generalizations
See how to import a model to another file. verify the counter
State Machine
Definded by:
- All possible initial states
- What next states can follow in any given state