Go backward to Reasoning about Composed Systems
Go up to Top
Go forward to Interleaving Representations
- Canconical TLA specification form:
- exists : and always [A] and .
- Initialization predicate .
- Variable vector .
- Fairness conditions .
- There exists a sequence of values for such that Init is true
in the initial state, every step of the behavior is an A step or
leaves state function unchanged and holds.
- Example: GCD
- () and ()
A (() and () and ())
or (() and () and ())
Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine