Hardware Reference
In-Depth Information
Proposition 3.20.
FSM
M
B
is a solution of the equation
M
A
M
X
M
C
,where
M
A
and
M
C
are FSMs, iff
M
B
is a reduction of the FSM
M
S
associated
to
S
FSM
,
where
S
FSM
is obtained by applying Procedure
3.1.1
to
S
,where
S
D
A
C
.If
S
FSM
Df
g
then the trivial FSM is the only solution.
The largest complete FSM solution
M
Prog.S
FSM
/
is found, if it exists, by applying
Procedure
3.1.2
.
A complete FSM is a solution of
M
A
M
X
M
C
iff it is a reduction of the
largest complete solution
M
Prog.S
FSM
/
.
Given the largest (complete) solution
M
Prog.S
FSM
/
of the equation
M
A
M
X
M
C
,let
M
A
M
X
Š
M
C
.Then
M
Prog.S
FSM
/
is the largest (complete) solution of
the equation
M
A
M
X
Š
M
C
.
Example 3.21. (Variant of Example
3.16
)
Consider the FSMs M
A
Dh
S
A
;I
1
V; U
O
1
;T
A
;sa
i
and M
C
Dh
S
C
;U;V;T
C
;s1
i
with S
A
Df
sa
g
, T
A
Df
.01; sa; sa;
s00/, .00;
sa;
sa;
01/, .11;
sa;
sa;
10/, .10;
sa;
sa;
10/
g
, S
C
Df
s1
g
,
T
C
Df
.1; s1; s1; 1/, .0;s1;s1;0/
g
. The equation M
A
M
X
M
C
yields
Df
.01/
?
the language equation A
X
C with solution S
g
, i.e., the corresponding
FSM solution M
X
produces the set of strings of input/output pairs
f
.0=1/
?
g
,andso
the equation has no complete FSM solution.
Not every deterministic complete FSM M
SR
that is a reduction of the largest
solution M
S
is a solution of the equation M
A
M
X
Š
M
C
, as shown by the examples
in Example
3.22
.
Example 3.22.
Given the context FSM M
A
and the specification FSM M
C
shown
respectively in Fig.
3.6
a,b, consider the equation M
A
M
X
Š
M
C
, whose largest
solution M
S
is in Fig.
3.6
c (and obviously satisfies M
A
M
X
Š
M
C
,asshownin
Fig.
3.6
d). Then the deterministic complete FSM M
S1
in Fig.
3.6
e is not a solution
of M
A
M
X
Š
M
C
, whereas M
S2
in Fig.
3.6
g is a solution of M
A
M
X
Š
M
C
,
as shown respectively in Fig.
3.6
f and Fig.
3.6
h. Notice that both M
S1
and M
S2
are
reductions of the largest solution M
S
.
Given the context FSM M
A
and the specification FSM M
C
shown respectively
in Fig.
3.7
a,b, consider the equation M
A
M
X
Š
M
C
, whose largest solution M
S
is
in Fig.
3.7
c (and obviously satisfies M
A
M
X
Š
M
C
, as shown in Fig.
3.7
d). Then
a deterministic complete FSM that is a reduction of M
S
should choose at state s
either the transition
u
3
=
v
2
or
u
3
=
v
1
. Suppose to define the reduction M
S1
where at
state s we choose
u
3
=
v
2
instead of
u
3
=
v
1
,thenitisM
A
M
S1
6Š
M
C
, because in
the product at state 1 we cannot get the transition i
1
=o
1
that requires the selection
u
3
=
v
1
in M
S1
; similarly, if we define the reduction M
S2
where at state s we choose
u
3
=
v
1
instead of
u
3
=
v
2
.thenitisM
A
M
S1
6Š
M
C
, because in the product at state 1
we cannot get the transition i
3
=o
2
that requires the selection
u
3
=
v
2
in M
S2
.Sothere
is no deterministic complete FSM that is a reduction of the largest solution M
S
and
also solves the FSM equation M
A
M
X
Š
M
C
.
Another interesting example and related discussion can be found in Example 3.1
and Fig. 2 of [149], where by removing any transition from the largest solution M
S
we would miss some complete deterministic FSM reduction that is a solution.
Search WWH ::
Custom Search