Computation of Flexibility in Sequential Networks - The Unknown Component Problem: Theory and Applications - page 165

111-1
1--11
.table x r2 R2
.default 0
111
.table x y r3 R3
.default 0
1-11
-1-1
.end
We adapt the K&N script to this example:
K&N script - example MA.mv MB.mv
read_blif_mv MA.mv
extract_aut MA.aut
support x,y MA.aut MAs.aut
complete MAs.aut MAsc.aut
determinize MAsc.aut MAd.aut
minimize MAd.aut MAd_min.aut
read_blif_mv MB.mv
extract_aut MB.aut
product MB.aut MAd_min.aut MBi.aut
prefix MBi.aut MBifsm.aut
We obtain the automaton shown in Fig. 10.2 , which is reduced to two states by state
minimization with STAMINA.
In contrast, we can solve for the largest FSM solution of the component M B of
this example. We take the specification in spec.mv to be the FSM composed of
M A M B with inputs a; b; c; d; e and output o . We use the following script:
Largest solution script - example spec.mv MA.mv
read_blif_mv spec.mv
extract_aut spec.aut
complement spec.aut specc.aut
read_blif_mv MA.mv
extract_aut MA.aut
product MA.aut specc.aut p.aut
support x,y,o p.aut ps.aut
complement ps.aut x.aut
progressive -i 2 x.aut xfsm.aut
minimize xfsm.aut temp.aut
prefix temp.aut xfsm_min.aut
We obtain the solution xfsm min.aut shown in Fig. 10.3 , which is again reduced
to two states by state minimization with STAMINA.
One can check that MBifsm.aut is contained in xfsm min.aut using the
command contain MBifsm.aut xfsm min.aut .