Go backward to State Functions and Predicates
Go up to Top
Go forward to Predicates as Actions

Actions

Action = boolean-valued expression.
- Variables, primed variables, constant symbols.
- $x'+y = y$ , $x-1$ in $z'$ .
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 -> Bool
- $s$ [[A]] $t$ in Bool.
- Old state $s$ , new state $t$ .
- $s$ [[A]] $t$ $<=>$ A(forall ' $v$ : $s$ [[ $v$ ]]/ $v$ , $t$ [[ $v$ ]]/ $v'$ ).
- $s$ [[ $y = x'+1$ ]] $t$ = ( $s$ [[ $y$ ]] = $t$ [[ $x$ ]]+1).
- $s,t$ is an A step iff $s$ [[A]] $t$ = true.

Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine