Hardware Reference
In-Depth Information
[
V/
?
Definition 3.4.2.
A solution B of (
3.8
)isA
-compositionally prefix
I.U
O
-progressive
if
Pref
..IO/
?
/
*
U
[
V
Pref
.A/
*
I
2
[
O
2
\
Pref
.B/
*
I
1
[
O
1
\
is I.U
[
V/
?
O-progressive.
A compositionally prefix I.U
[
V/
?
O-progressive solution yields a composition
that allows .
u
[
v
/
?
cycles without exit, yet every sequence in I.U
[
V/
?
O followed
by an input in I must be followed by a .
u
[
v
/
?
cycle that can be exited (by an
output).
Definition 3.4.3.
A solution B of (
3.8
)isA
-compositionally prefix
.U
[
V/
-
deadlock-free
if
Pref
..IO/
?
/
*
U
[
V
Pref
.A/
*
I
2
[
O
2
\
Pref
.B/
*
I
1
[
O
1
\
is .U
[
V/-deadlock-free.
A compositionally prefix .U
[
V/-deadlock-free solution yields a composition that
has no .
u
[
v
/
?
cycles without exit.
Definition 3.4.4.
A solution B of (
3.8
)isA
-compositionally prefix
.U
[
V/
-
convergent
if
Pref
..IO/
?
/
*
U
[
V
Pref
.A/
*
I
2
[
O
2
\
Pref
.B/
*
I
1
[
O
1
\
is .U
[
V/-convergent.
A compositionally prefix .U
[
V/-convergent solution yields a composition
v
/
?
that has no .
u
[
cycles, i.e., it is livelock-free. A compositionally prefix
.U
[
V/-deadlock-free
solution
does
not
need
to
be
compositionally
prefix
.U
[
V/-convergent.
Example 3.31.
Consider the equation M
A
˘
M
X
M
C
, where FSMs M
A
and M
C
and the largest solution M
B
are shown in Fig.
3.13
a-c. Fig.
3.13
d,e shows the related
automata A and B
*
I
1
[
O
1
D
B
*f
i
g[f
o
g
, whereas Fig.
3.13
f,g portrays the automata
representing the languages A
*
I
2
[
O
2
\
.IO/
?
*
U
[
V
\
B
*
I
1
[
O
1
D
A
\
B
*f
i
g[f
o
g
\
.IO/
?
*f
u
g[f
v
g
P ref ..IO/
?
/
*
U
[
V
and Pref.A/
*
I
2
[
O
2
\
Pref.B/
*
I
1
[
O
1
\
D
Pref.A/
\
Pref.B/
*f
i
g[f
o
g
\
P ref ..IO/
?
/
*f
u
g[f
v
g
.
If FSM M
A
answers by
u
to the external input i then FSMs M
A
and M
B
fall into an infinite dialog, so we would like to classify their composition as
neither .U
[
V/-convergent nor .U
[
V/-deadlock-free. However the language
A
\
B
*f
i
g[f
o
g
\
.IO/
?
*f
u
g[f
v
g
Df
.i o/
?
g
is both .U
[
V/-convergent and .U
[
V/-
deadlock-free. To overcome this modeling problem, we introduce the operator
Pref (guarantees prefix-closure) and rewrite the previous language composition
as Pref.A/
\
Pref.B/
*f
i
g[f
o
g
\
P ref ..IO/
?
/
*f
u
g[f
v
g
. The latter language is
Search WWH ::
Custom Search