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