Hardware Reference
In-Depth Information
nondeterministic finite automaton. In this, some behavior may be eliminated
(the resulting language is a subset of the original language). This is used when
the largest solution of a language equation is computed first, which contains all
possible solutions, whereas we only want one small solution. A discussion of the
use of
dcmin
can be found in Sect. 14.3.
Many verification problems in state-transition systems can be reduced to check-
ing language containment, which tests if the language of one automaton is contained
in that of another. The checking can be accomplished by the product and comple-
ment operations. In BALM, language containment checking is performed using
command
contain
, which will report if the two automata specified on the
command line are related by language containment (or are equivalent). If the
automata are not equivalent, a counter-example can be produced.
8.4
Appendix: Commands in BALM
BALM can be downloaded from the following site:
The following list contains a one line summary of all the commands available in
BALM.
Automata manipulation commands:
•
complement
: complement an automaton (a nondeterministic automaton will
be automatically determinized first)
•
complete
: complete an automaton by adding a don't-care state
•
contain
: check language containment of two automata (checking is automati-
cally aborted is at least one automaton is nondeterministic)
•
dcmin
: minimize the number of states by collapsing states whose transitions
into care states are compatible
•
determinize
: determinize an automaton
•
minimize
: minimize the number of states of a deterministic automaton
•
moore
: trim an automaton to contain Moore states only
•
prefix
: leave only accepting states that are reachable from initial states
•
product
: build the product of two automata
•
progressive
: leave only accepting and complete states that are reachable
from initial states
•
support
: change the input variables of an automaton
5
5
Two caveats about using
support
:
1. One must declare explicitly the number of values of input variables with more than two values.
2. It cannot handle an automaton with only one state; a work-around is to define an automaton
with two equivalent states.
Search WWH ::
Custom Search