Go backward to State Functions and Predicates
Go up to Top
Go forward to Predicates as Actions
- Action = boolean-valued expression.
- Variables, primed variables, constant symbols.
- , in .
- Relation between old state and new state.
- Unprimed variables refer to old state.
- Primed variables refer to new state.
- Representation of atomic operation of concurrent program.
- Formalization of A
- [[A]] in St -> S
- [[A]] in Bool.
- Old state , new state .
- [[A]] A(forall ': []/,
- [] = ([] = []+1).
- is an A step iff [[A]] =
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine