Go backward to The Raw Logic
Go up to Top
Go forward to Describing Programs with RTLA
Describing Programs with RTLA
- Program in guarded command language.
- var natural , = 0
do
<true -> := >
[]
<true -> := >
od
- Formula Phi
- Init
and
- A and
- A and
- A A or A
- Phi Init
and always A
- sigma[[Phi]] = true iff sigma represents possible
execution of program.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine