Go backward to Describing Programs with RTLA
Go up to Top
Go forward to TLA
Describing Programs with RTLA
- Init asserts initial condition.
- Action A asserts effect of first guarded command.
- Action A asserts effect of second guarded command.
- Action A asserts effect of non-deterministic composition.
- Formular Phi represents whole program:
- Init is true in first state.
- Every step is an A step.
Each equivalent formula is a valid representation of the program.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine