Go backward to Rigid Variables and Quantifiers
Go up to Top
Go forward to Simple Temporal Logic
The Enabled Predicate
- Enabled A
- True for iff it is possible to take an A step starting in
.
- [[Enabled A]] exists in St:
[[A]]
- Syntactic definition
- all (flexible) variables in A.
- Enabled A
exists c, ..., c:
A(c/, ..., c/).
- Enabled( = ()+n) =
exists c: = c+n
- If A represents actomic operation, Enabled A is
true for those states in which it is possible to perform the operation.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine