Hardware Reference
In-Depth Information
eliminate another input alphabet and so on. In particular, when testing for an input
I
k
we detect and remove so-called forbidden states that depend essentially on I
k
:
if the initial state is a forbidden state, the FSM depends essentially on input I
k
.
Definition 14.4.1.
Given an FSM M
D
.S; I
1
I
l
;O
1
O
r
;T;r/
over the input alphabet I
1
I
l
,astates
2
S is I
k
-forbidden
if for some
.i
1
;:::;i
k
1
; i
k
C
1
;:::;i
l
/
2
I
1
I
k
1
I
k
C
1
I
l
there does not exist
o
1
o
r
2
O
1
O
r
such that for each i
2
I
k
there exists s
0
2
S for which
..i
1
;:::;i
k
1
;i;i
k
1
;:::;i
l
/; s; s
0
;o
1
o
r
/
2
T .
The meaning is that the behavior of each reduction of an FSM M in a I
k
-forbidden
state depends essentially on alphabet I
k
, and thus such state cannot be included into
a solution that does not depend on alphabet I
k
.
Therefore first we delete iteratively all the forbidden states and all transitions
to such states. If the initial state is deleted too, then each reduction of the FSM
M depends essentially on alphabet I
k
. If the initial state is not deleted, we check
whether the conditions of Proposition
14.4
hold. If they do, then the communication
wires corresponding to alphabet I
k
can be deleted from the initial composition by a
projection with respect to I
k
.
Definition 14.4.2.
GivenanFSMM over input alphabet I
1
I
l
and output
alphabet O
1
O
r
, an FSM M
P;k
over input alphabet I
1
I
k
1
I
k
C
1
I
l
such that the language of FSM M
P;k
lifted to the set
f
I
1
;:::;I
l
;O
1
;:::;O
r
g
is
contained in the language of M is a
full
I
k
-projection
of the FSM M to the set
I
1
I
k
1
I
k
C
1
I
l
.
Otherwise (when the conditions of Proposition
14.4
do not hold), each reduction of
the FSM M depends essentially on input alphabet I
k
, i.e., the communication wires
corresponding to alphabet I
k
cannot be deleted from the initial composition. We try
all input alphabets and derive the largest solution that depends on a minimal number
of input alphabets.
We propose next an algorithm for deriving the largest solution that depends on a
minimal number of input alphabets.
Procedure 14.4.1.
Input: FSM equation
M
Context
M
X
Š
M
Spec
,where
M
X
is
defined over the input alphabets
f
I
1
;:::;I
l
g
; Output: Largest FSM solution
M
P
defined on a minimal subset of input alphabets
f
I
1
;:::;I
l
g
; reduction
M
B
of
M
P
that satisfies Proposition
14.4
.
1. Find the largest solution M
S
over the input alphabets
f
I
1
;:::;I
l
g
of the FSM
equation M
Context
M
X
Š
M
Spec
.
Set I
i
;i
D
1.
2. Iteratively delete from M
S
all I
i
-forbidden states and transitions to these states.
If the initial state is deleted
f
/* any reduction of M
S
depends essentially on the alphabet I
i
*/
If there are untried input alphabets, try the next one (i
D
i
C
1) and go to 2.,
otherwise set M
P
D
M
S
;M
B
D
M
S
and exit.
g
else
f
Search WWH ::
Custom Search