Hardware Reference
In-Depth Information
stgExtract ( network ; limit ) f
/* initialize the STG to be extracted */
STG = newSTG ();
/* get hold of the initial state of the network */
I = getInitialState ( network );
/* initialize the set of states to be explored with the initial states */
S = I ;
/* explore states */
while ( S ¤; ) f
/* extract one state from the set of states to be explored */
s = getOneState ( S ); S D S n s;
/* get the relation of the given state */
R.i; o; x/ = deriveStateRelation ( network , s );
/* enumerate next states reachable from the given state */
while ( R.i; o; x/ ¤; ) f
/* find one combination of variables from the state relation */
minterm .i;o;x/= getOneCombination ( R );
/* get the next state of this combination */
n.x/ D9 io minterm .i;o;x/;
/* get the IO predicate of this next state */
pred.i;o/ D9 x minterm .i;o;x/;
/* remove transition to this state from the relation */
R.i; o; x/ D R.i; o; x/ : Šn.x/;
/* if the state does not exist, schedule it for exploration */
if ( stateIsNew (STG;n))
S D S [ n;
/* record the transition */
addTransition ( STG;s;n;pred );
/* quit if the number of states exceeded the limit */
if ( getNumStates (STG) limit )
return NULL;
return STG;
g
Fig. 6.1
STG extraction algorithm
The internal procedures called from the STG extraction algorithm are the
following:
newSTG : Creates a new state transition graph.
getInitialState : Queries the network for its initial state.
getOneState : Extracts one state from the set.
deriveStateRelation : Traverses the network and derives the transition relation from
the given state as a BDD in terms of inputs, i , outputs, o, and next state variables, x.
Search WWH ::




Custom Search