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

and the specification automaton mc defined by the following BLIF-MV description:

.model mc
.inputs i o
.outputs Acc

.mv CS, NS 2 s1 s2
.mv i 2 i1 i2
.mv o 3 o1 o2 o3

.latch NS CS
.reset CS
s1

.table CS -> Acc
.default 1

.table i o CS -> NS
i1 o2 s1 s1
i1 o3 s1 s1
i2 o2 s1 s1

i1 o1 s1 s2

i1 o3 s2 s2
i2 o1 s2 s2

i1 o2 s2 s1
i2 o2 s2 s1

.end
Use BALM to solve the equation u .

Compute the following operations, invoking the appropriate commands in BALM,
and at each step plot the resulting automaton:

ma mx mc ,where mx has support v ;

1. Compute mc comp , the complement of mc .

2. Compute ma .mc comp / prod , the product of ma and mc comp .

3. Compute ma .mc comp / prod supp , the projection to the support v ; u of the

previous automaton ma .mc comp / prod .

4. Compute mx , the complement of the previous automaton ma .mc c omp /

prod supp , i.e., the largest automaton solution of the equation ( mxD .ma mc/ ).

8.2. Perform using the appropriate commands of BALM the following operations,
and at each step plot the resulting automaton:

1. Compute mx prog , the largest progressive automaton contained in mx .

2. Compute mx prog min , the automaton obtained by the (state) minimization of

mx prog .