Go backward to Another Example
Go up to Top
Go forward to The Next-State Relation

The Formula `Psi`

Psi $<=>$ Init_Psi and always [A]_w and SF_w(A₁) and SF_w(A₂)
Init_Psi $<=>$ (pc₁ = "a") and (pc₂ = "a")
and ( $x=0$ ) and ( $y=0$ ) and (sem=1)
$w$ $<=>$ < $x$ , $y$ , sem, pc₁, pc₂>
A $<=>$ A₁ or A₂
A₁ $<=>$ alpha₁ or beta₁ or gamma₁
A₂ $<=>$ alpha₂ or beta₂ or gamma₂
alpha₁ $<=>$ (pc₁ = "a") and (0 $<$ sem)
and pc₁' = "b" and sem' = sem-1
and Unchanged < $x$ , $y$ , pc₂>
beta₁ $<=>$ pc₁ = "b"
and pc₁' = "g" and $x'$ = $x+1$
and Unchanged < $x$ , $y$ , pc₂>
gamma₁ $<=>$ pc₁ = "g"
and pc₁' = "a" and sem' = sem+1
and Unchanged < $x$ , $y$ , pc₂>
alpha₂ $<=>$ ..., beta₂ $<=>$ ..., gamma₂ $<=>$ ...

Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine

The Formula Psi