Hardware Reference
In-Depth Information
productAutomaton
( A; B;
limit
)
f
/* initialize the product automaton */
P =
newAutomaton
();
/* get initial states of the automata */
I
A
=
getInitialState
( A );
I
B
=
getInitialState
( B );
/* initialize the set of states to be explored with the initial product state */
S
Df
I
A
;I
B
g
;
/* explore states */
while ( S
¤;
)
f
/* extract one product state from the set of states to be explored */
f
s
A
;s
B
g
=
getOneState
( S ); S
D
S
nf
s
A
;s
B
g
;
/* iterate through the transitions from these component states */
for each state t
A
reachable from state s
A
in automaton A
f
for each state t
B
reachable from state s
B
in automaton B
f
/* transition conditions must agree on common support */
cond
.i /
D
cond
.i /
s
A
!
t
A
:
cond
.i /
s
B
!
t
B
;
if (
cond
.i /
D;
)
continue;
// if the new product state does not exist, add it for exploration
if (
stateIsNew
(P;
f
t
A
;t
B
g
))
f
S
D
S
[f
t
A
;t
B
g
;
/* set the acceptance attribute of the new product state */
if (
stateIsAccepting
(t
A
)and
stateIsAccepting
(t
B
))
setAttribute
(
f
t
A
;t
B
g
, “accepting” );
else
setAttribute
(
f
t
A
;t
B
g
, “non-accepting” );
/* record the transition */
addTransition
( P;
f
s
A
;s
B
g
;
f
t
A
;t
B
g
;
cond
.i / );
g
/* quit if the number of states exceeded the limit */
if (
getNumStates
.P /
limit
)
return NULL;
return P ;
g
Fig. 6.4
Product computation algorithm
empty, it is processed iteratively. Each iteration removes any state whose outgoing
transitions under some input are undefined. The iteration stops when the automaton
is not changed. This operation may return the empty automaton. Note that the subset
of the support variables that constitute the inputs must be specified as an input to
this procedure.
Search WWH ::
Custom Search