Hardware Reference
In-Depth Information
D
A
A, d
0
cx
d
1
cx
D, d
0
cx
d
1
cx
A, d
0
cx
d
1
cx
d
0
cx
a
0
xc
A, a
0
xc
a
1
xc, d
0
cx
A, a
0
xc
dc
a
1
xc, d
1
cx
d
1
cx
D, d
o
cx
d
1
cx
A, d
0
cx
d
1
cx
A, d
o
cx
d
1
cx
a
1
xc
A
D
Fig. 2.8
Largest prefix-closed 2-bounded solution of the converter problem of Sect.
2.3.2
Problems
2.1.
Consider the traffic controller example described in [12]. For ease of reference
we show in Figs.
2.10
and
2.11
respectively the context automaton A and the
specification automaton C derived from it.
Notice that the inputs of A are two binary variables
v
1
;
v
2
, and the multi-valued
variable
colours
that can assume the values
green, red, yellow
. The inputs of C are
two multi-valued variables i
1
;i
2
that can assume each one of the three values 1; 2; 3,
and again the multi-valued variable
colours
.
Find the largest solution of the equation A
X
C , where the input variables
of X are i
1
;i
2
and
v
1
;
v
2
. This is a series topology where X feeds A,andthe
composition of X and A yields C .
Repeat the problem assuming that X has one more input: the variable
colours
of
automaton A, as in the controller's topology.
Hint.
The largest solution automaton of the series-topology equation is shown in
Fig.
2.12
.
If the reader will find too cumbersome carrying on by the hand the computations,
it will be one more reason to appreciate the automatica tool BALM presented in the
second part of the topic.
Df
i0;i1
g
, V
Df
v
0;
v
1
g
, O
Df
o0; o1
g
,andthe
2.2.
Consider the alphabets I
Dh
S
A
;˙
A
;
A
;r
A
;Q
A
i
Dh
S
C
;˙
C
;
C
;r
C
;Q
C
i
.Letthe
automata A
and C
D
Df
sa; sb
g
, ˙
A
D
O,
A
D
automata be defined as follows: S
A
Q
A
V
f
.
v
0 o1; s a; s b /, .
v
1 o0; sa; sb/, .
v
0 o1; s b; s b /, .
v
1 o1; s b; s a/, r
A
D
sa,
Search WWH ::
Custom Search