Hardware Reference
In-Depth Information
a
b
c
d
Fig. 2.5
Automata of communication system described in Sect.
2.3.2
.(
a
) Automaton of PS;
(
b
) automaton of PR;(
c
) automaton of PC;(
d
) automaton of SS
Figure
2.7
show
s yet another view of the largest prefix-closed solution S
D
PS
˘
PC
˘
PR
˘
SS
of the converter problem, with the
dc
state included and the
fail
state excluded.
Figure
2.8
shows the largest prefix-closed 2-bounded solution of the converter
problem, as an example of solution with bounded internal communication.
Figure
2.9
shows the composition
PS
˘
PC
˘
PR
\
S
*f
Acc;Del
g
of the com-
munication system
PS
˘
PC
˘
PR
and of the largest converter S .Thelargest
prefix-closed solution S is compositionally .I
?
O/-progressive and compositionally
prefix .U
[
V/-deadlock-free, but not compositionally prefix .U
[
V/-convergent.
This means that, even if we extract from the largest solution S a complete solution
S (i.e., S is defined for every internal input A; d 0cx;
d1cx
), the composition of S
with the context (
PS
˘
PC
˘
PR
may deadlock, i.e., the automata can exchange
internal actions without producing any output for the environment; this happens,
for instance, if S after the internal input
d0cx
always selects the internal output
a1cx
(and never selects D). In general the composition of any complete solution
that never produces the internal output D with the context has livelocks (loop
Search WWH ::
Custom Search