Hardware Reference
In-Depth Information
and say
n
.n
1
;n
2
;n
3
/ (say that n
1
;n
2
;n
3
are the next states under input i
1
), finally
suppose that n
1
;n
2
;n
3
are exactly the next states also under input i
3
, then it will be
pred
.i
1
;i
3
/.
The transition relation R.i; x/ is reduced by removing the transitions to n.x/
under predicate
pred(i)
. If state
subset n(x)
is new, it is scheduled for exploration by
the proposed algorithm. Finally, transition from s to n under input
pred
is added to
the automaton B under construction.
6.2.4
Complementation
Complementation
of a deterministic finite automaton is performed by exchanging
the set of accepting and non-accepting states. This is done by enumerating all states
of the automaton to be complemented and flipping the acceptance attribute of each
state.
If the automaton is not deterministic, it must be processed by the determinization
algorithm first.
6.2.5
Support
Support
is an operation, which resets the support of the automaton to be equal to the
given ordered list of variables. The following three situations may occur:
•
If a listed variable is not currently in the support, it is added to the resulting
support and the domain of all transition predicates is expanded to include
this variable. Since the predicates are represented implicitly using BDDs, the
manager is expanded to include the new variable, while the BDDs of the
predicates do not have to be modified, because they do not depend on the new
variable.
•
If a variable already exists in the support, it is simply moved to its new position
in the given order. This does not affect BDD ordering, so BDDs do not change,
however it changes the mapping function that matches the ordered list of support
variables and the internal BDD variables.
•
If a variable that is currently present in the support is not listed for inclusion in
the resulting support, it is removed from the support. This is done by quantifying
it existentially from all the predicates enabling the transitions of the given
automaton.
In the end, when the new variable order is defined, the variable map of the BDDs
representing all predicates is updated while the predicates remain unchanged. The
resulting automaton is returned.
Search WWH ::
Custom Search