The Software Package BALM - The Unknown Component Problem: Theory and Applications - page 138

out a resulting automaton in AUT format. In addition, there is a command
which extracts an equivalent automaton from a BLIF-MV file: the command is
extract aut . A typical script executing equation solving is the following:

read_blif_mv fixed.mv
extract_aut fixed.aut
complement spec.aut specc.aut
product fixed.aut specc.aut product.aut
support u product.aut product_supp.aut
complement product_supp.aut x.aut
progressive -i n x.aut xfsm.aut
minimize xfsm.aut xfsm_min.aut
Note that each command, except for read blif mv , reads in an automaton file
and writes out an automaton file. Here u is a list of support variables and n is the
number of inputs that the solution will have as an FSM.
If an automaton would be already available as fixed.aut (say written
directly in the AUT format ) then there would be no need to run first the
read blif mv and extract aut commands and the previous flow would
reduce to:

complement spec.aut specc.aut
product fixed.aut specc.aut product.aut
support u product.aut product_supp.aut
complement product_supp.aut x.aut
progressive -i n x.aut xfsm.aut
minimize xfsm.aut xfsm_min.aut

8.3.1 Some Specialized Automata Operations

In BALM, command print nd states checks if an automaton is determin-
istic. A nondeterministic automaton can be determinized using the command
determinize . This uses a subset construction.
Determinizing a nondeterministic automaton is a step usually performed before
complementation since complementing a deterministic automaton can be easily

achieved by inverting the acceptance condition of states. In BALM, an automaton

A

A
can be complemented using command complement where a determinization step
is automatically performed first if is nondeterministic.

A state is incomplete if there exists some input assignment, under which the next
state transition is undefined (i.e., there is no next state under that input assignment).
An automaton is said to be incomplete if it has at least one incomplete state.
An incomplete automaton can be completed by adding a single non-accepting
don't-care state with a self-loop transition under any input assignment (thus the
don't-care state is a sink state). All missing input assignments of an incomplete

A