Go backward to The Raw LogicGo up to TopGo forward to Describing Programs with RTLA |

- Program in guarded command language.
**var natural***x*,*y*= 0**do**

<**true**->*x*:=*x+1*>

[]

<**true**->*y*:=*y+1*>**od**

- Formula
`Phi``Init`_{Phi}*<=>**(x=0)**and**(y=0)*`A`_{1}*<=>**(x' = x+1)**and**(y' = y)*`A`_{2}*<=>**(y' = y+1)**and**(x' = x)*`A`*<=>*`A`_{1}*or*`A`_{2}`Phi`*<=>*`Init`_{Phi}*and*`always``A`

`sigma`[[`Phi`]] =**true**iff`sigma`represents possible execution of program.

Author: Wolfgang Schreiner

Last Modification: May 14, 1998