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
1
)
and
SF
w
(
A
2
)
Init
Psi
<=>
(
pc
1
= "a")
and
(
pc
2
= "a")
and
(
x=0
)
and
(
y=0
)
and
(
sem
=1)
w
<=>
<
x
,
y
,
sem
,
pc
1
,
pc
2
>
A
<=>
A
1
or
A
2
A
1
<=>
alpha
1
or
beta
1
or
gamma
1
A
2
<=>
alpha
2
or
beta
2
or
gamma
2
alpha
1
<=>
(
pc
1
= "a")
and
(0
<
sem
)
and
pc
1
' = "b"
and
sem
' =
sem
-1
and
Unchanged
<
x
,
y
,
pc
2
>
beta
1
<=>
pc
1
= "b"
and
pc
1
' = "g"
and
x'
=
x+1
and
Unchanged
<
x
,
y
,
pc
2
>
gamma
1
<=>
pc
1
= "g"
and
pc
1
' = "a"
and
sem
' =
sem
+1
and
Unchanged
<
x
,
y
,
pc
2
>
alpha
2
<=>
...,
beta
2
<=>
...,
gamma
2
<=>
...
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998