#!/bin/sh
#                ,,,
#               (o o)
#  ####=====oOO--(_)--OOO========================================####
#  ##                                                              ##
#  ##  This file is part of FPT : A Formal Proof Toolkit           ##
#  ##  (C) 1996, MASI, CAO-VLSI Team                               ##
#  ##                                                              ##
#  ##  Shell script to run yeap on a lot of files...              ##
#  ##                                                              ##
#  ##  File            :  testfsm                                  ##
#  ##  Author          :  Olivier SIROL                            ##
#  ##  Date            :  Apr 1996                                 ##
#  ##                                                              ##
#  ##  E-mail support  :  sirol@ecoledoc.ibp.fr                    ##
#  ##                                                              ##
#  ####==========================================================####
#
#
#  $Id: testfsm,v 1.3 1997/05/23 14:27:36 sirol Exp $
#
#
echo "START TIME : `date`" > ERRORLOG

for NB_OUT in 4 8 16 32
do

for NB_IN in 4 8 16 32
do

echo "numreg;total;abl;bdd;proof;topnodes" > PROFILE${NB_IN}x${NB_OUT}

for NB_ETA in 10 20 30 40 60 80 100 120 140 180 
do
echo "===============> FSM a $NB_ETA etats, $NB_IN entrees, $NB_OUT sorties"

mkfsm $NB_ETA $NB_IN $NB_OUT
if [ $? != 0 ] ; then echo "ERROR : mkfsm prof${NB_IN}x${NB_OUT}_${NB_ETA}" >> ERRORLOG ; fi
 
syf -a -CEV prof${NB_IN}x${NB_OUT}_${NB_ETA}
if [ $? != 0 ] ; then echo "ERROR : syfa prof${NB_IN}x${NB_OUT}_${NB_ETA}" >> ERRORLOG ; fi

 
syf -o -CEV prof${NB_IN}x${NB_OUT}_${NB_ETA}
if [ $? != 0 ] ; then echo "ERROR : syfo prof${NB_IN}x${NB_OUT}_${NB_ETA}" >> ERRORLOG ; fi


echo -n "${NB_ETA};" >>  PROFILE${NB_IN}x${NB_OUT}
 
yeap -v prof${NB_IN}x${NB_OUT}_${NB_ETA}o prof${NB_IN}x${NB_OUT}_${NB_ETA}a | tee `tty` | gawk '
/Total elapsed time/        { printf("%s;", $(NF-1) );}
/Time Making Abl/           { printf("%s;", $(NF-1) );}
/Time Making Bdds/          { printf("%s;", $(NF-1) );}
/Time Running Proof/        { printf("%s;", $(NF-1) );}
/Time Max Bdd Node/         { printf("%s\n", $(NF-1) );}
' >>  PROFILE${NB_IN}x${NB_OUT} 

if [ $? != 0 ] ; then echo "ERROR : yeap prof${NB_IN}x${NB_OUT}_${NB_ETA}" >> ERRORLOG ; fi

done
done
done

echo "STOP TIME : `date`" >> ERRORLOG

