Information Technology Reference
In-Depth Information
3.4
The Transition Relation and Its Properties
The composition
j
of
Signal
programs corresponds to logical conjunction. Thus,
the transition relation
will be a conjunction of assertions where each
Signal
statement gives rise to a conjunct in
Signal
and present for each of them the conjunct it contributes to the transition relation.
. Below, we list the statements of
v
f
u
1
;:::;u
n
), where
f
Consider the Signal
statement
:=
(
is a state-
function. This statement contributes to
the following conjunct:
u
0
1
)
u
0
n
)
clk
(
::: clk
(
^ v
0
=
if
u
0
1
)
then
u
0
1
;:::;u
0
n
)
else
clk
(
f
(
?
This formula requires that the signals
v;u
1
;:::;u
n
are present at precisely
the same time instants, and that at these instants
v
=
f
(
u
1
;:::;u
n
).
The statement
r
:=
v
$ init
w
0
contributes to
the conjunct:
m:r
0
= f
v
0
)then
v
0
else
clk
(
m:r
^ r
0
v
0
)then
= f
clk
(
m:r
else
?
This denition introduces a memorization variable
m:r
which stores the last
(including the present) non-bottom value of
v
. Variable
m:r
is initialized
in the initial condition
to
w
0
. From now on we refer to flows
r
that are
dened by this type of statement as
register flows
. Variables in an
sts
which
represent register flows will typically be denoted by
r
, and the corresponding
memorization variables by
m:r
. Note that unlike the other system variables
in the constructed
sts
, memorization variables are
persistent
.
The statement
v
:=
u
when
b
contributes to
the conjunct:
v
0
=if
b
0
=Tthen
u
0
else
?:
The statement
w
:=
u
default
v
contributes to
the conjunct:
w
0
=if
u
0
)then
u
0
else
v
0
:
clk
(
According to the above explanations, the
Signal
program DEC is represented
by the following
sts
A
=(
V
a
;
a
;
a
).
Search WWH ::
Custom Search