Information Technology Reference
In-Depth Information
identically named
variables. Therefore, the natural candidate for the concrete
observation is the tuple of values of the IO
C
variables.
Unfortunately, there is a dierence in the types of an
C
IO
Signal variable and
its corresponding
C
variable. While any
IO
signal
v 2 IO
may also assume the
value
?
, signifying that the signal
v
is absent in the current step, all
C
variables
are persistent and can never assume the value
?
. This implies that we have to
identify for every concrete step and every
IO
-variable
v
whether the abstract
version of
is present or absent in the current step.
Our decision was that an input variable
v
v
should be considered present in
the current step i a new value for
has been read during the current execution
of the loop's body. Similarly, an output variable
v
v
is considered present i the
variable
was written during the current step.
To detect these events, we have instrumented the given
v
C
program by adding
:v
for each output variable
2
. All these auxiliary variables are set to 0 (
false
)at
the beginning of the loop's body. After every
read
(
:v
v
a boolean variable
rd
for each input variable
, and a boolean variable
wr
v
) operation, we add the
assignment
rd
:v
:= 1, and after every
write
(
v
) operation, we add the assignment
wr
:v
:= 1.
In Fig. 1, we present the instrumented version of function DEC iterate().
logical DEC iterate()
f
rd :
FB
c
= F;
wr:
N
c
= F;
l0: h1
c
=TRUE;
l1: h2
c
=ZN
c
<
=1;
l2: if (h2
c
)
l2.1:
f
read(FB
c
);
rd :
FB
c
= T;
g
;
l3: if (h2
c
)
l3.1: N
c
=FB
c
;
else
l3.2: N
c
=ZN
c
−
1;
l4:
f
write(N
c
);
wr:
N
c
= T;
g
;
l5:
ZN
c
=N
c
;
return TRUE;
g
Fig. 1.
Instrumented version of function DEC iterate().
In Fig. 2, we present the composite
sts
corresponding to the instrumented
C
program. This presentation of the composite
sts
identies the concrete obser-
O
N
are dened in Fig. 2.
As can be seen in Fig. 2, the instrumented variables
rd
O
c
=(
O
FB
;O
N
), where
O
FB
and
vation function as
:
FB
c
and
wr
:
N
c
are
dened within
C
and then used in the denition of the observation function
O
c
. Therefore, it is possible to simplify the composite sts by substituting the
2
Our nal implementation does not really add these auxiliary variables but performs
an equivalent derivation. Introducing these variables simplies the explanation.
Search WWH ::
Custom Search