#!/bin/sh

sif2sr $1

SMVFILEBASE=`dirname $1`/`basename $1 .sif`

echo > $2

$COSPANDIR/bin/cospan $SIFCOSPANOPTS ${SMVFILEBASE}.sr 2>&1 | tee cospansif.trans

failed_prop=`grep "No transition enabled" cospansif.trans | sed -e 's/^.*No transition enabled.* \._\.//' | sed -e 's/_test.*$//'`

failed_prop=`echo $failed_prop | sed -e 's/ .*$//'`

if test "$failed_prop" = ""
then  	

  if test "`grep \"Task performed\" cospansif.trans`" = ""
  then
    echo Cospan did not return result >&2
    exit 1
  else
    for prop in `grep monitor ${SMVFILEBASE}.sr | sed -e 's/monitor //' | sed -e 's/_test :.*$//'`; do
        echo '{ "" {' >> $2
        echo $prop >> $2
        echo '} 1 0 0 {' >> $2
        echo '}}' >>$2
    done
  fi

else 

  echo '{ "" {' > $2
  echo $failed_prop >> $2
  echo '} 0 0 0 {' >> $2
  cospanT2smv < ${SMVFILEBASE}.T >> $2
  echo '}}' >>$2

fi

echo $failed_prop
