#!/bin/bash

################################################################################
# $Id: timenodesbmc.in,v 1.1 2006/05/24 00:13:01 schuppan Exp $
#
# Name:    timenodesbmc
# Version: 0.1
# Date:    08.10.2002
#
# Author:  Viktor Schuppan, ETH Zuerich
#
# Description:
#
# Runs bounded model checker of Cadence SMV on models of the FireWire TIP
# protocol.
#
# Command-line
#
# timenodesbmc
#
################################################################################



#
# configurable parameters
#
CSMV=/usr/local/src/csmv/bin/smv
SED=/bin/sed



for det in det n; do \
  for rootcontits in 0 2; do \
    for nodes in 2 3 5 6 6nc 10; do \
      for ports in 3 4; do \

      if [ $ports = 4 -a \( $nodes != 6 -a $nodes != 6nc \) ]; then
         continue
      fi                                                                                                                                  
      if [ $ports = 3 -a \( $nodes = 6 -o $nodes = 6nc \) ]; then
         continue
      fi                                                                                                                                  
      if [ $det = n -a \( $nodes = 6 -o $nodes = 6nc \) ]; then
         continue
      fi                                                                                                                                  
      if [ $det = n -a $nodes = 10 ]; then
         continue
      fi                                                                                                                     
      bmcdef=#define

      if [ $det = det ]; then
        symmdef=#undef
        forcerootdet=#define
        configurationdet=#define
      elif [ $det = frn ]; then
        symmdef=#undef
        forcerootdet=#undef
        configurationdet=#define
      elif [ $det = cfn ]; then
        symmdef=#undef
        forcerootdet=#define
        configurationdet=#undef
      elif [ $det = scfn ]; then
        symmdef=#define
        forcerootdet=#define
        configurationdet=#undef
      elif [ $det = n ]; then
        symmdef=#undef
        forcerootdet=#undef
        configurationdet=#undef
      elif [ $det = sn ]; then
        symmdef=#define
        forcerootdet=#undef
        configurationdet=#undef
      fi
 
      src=../lib/nodes_bmc.smv.in

      if [ ! \( $nodes = 6nc -a $ports = 4 \) ]; then
        sixnocycle=#undef
	nnodes=${nodes}
      else
        sixnocycle=#define
	nnodes=6
      fi

      if [ $rootcontits = 0 ]; then
        if [ $nodes = 2 ]; then
            pathlength=20
        elif [ $nodes = 3 ]; then
            pathlength=25
        elif [ $nodes = 4 ]; then
            pathlength=29
        elif [ $nodes = 5 ]; then
            pathlength=34
        elif [ $nodes = 6 ]; then
            pathlength=38
        elif [ $nodes = 10 ]; then
            pathlength=56
        fi
      elif [ $rootcontits = 2 ]; then
        if [ $nodes = 2 ]; then
            pathlength=28
        elif [ $nodes = 3 ]; then
            pathlength=33
        elif [ $nodes = 4 ]; then
            pathlength=37
        elif [ $nodes = 5 ]; then
            pathlength=42
        elif [ $nodes = 6 ]; then
            pathlength=46
        elif [ $nodes = 10 ]; then
            pathlength=64
        fi
      fi

      # cmd="memusage ${CSMV} -force -bmc -l ${pathlength}"
      cmd="${CSMV} -force -bmc -l ${pathlength}"

      basename=nodes_${nodes}_${ports}_${det}_${rootcontits}
      dst=${basename}_results.txt

      echo -n "generating file ${basename}.smv... "
      ${SED} -e s/@numnodes@/${nnodes}/ \
          -e s/@numports@/${ports}/ \
          -e s/@symmetry@/${symmdef}/ \
          -e s/@bmc@/${bmcdef}/ \
          -e s/@rootcontits@/${rootcontits}/ \
          -e s/@forcerootdet@/${forcerootdet}/ \
          -e s/@configurationdet@/${configurationdet}/ \
          -e s/@sixnocycle@/${sixnocycle}/ \
          "${src}" > ${basename}.smv
      echo done

      echo -n "model checking file ${basename}.smv... "
      ulimit -St 21600
      ulimit -Sd unlimited
      if [ -f .smv_history ]; then rm .smv_history; fi
      if [ -f .smv_lock ]; then rm .smv_lock; fi
      if [ -f ${basename}.update ]; then rm ${basename}.update; fi
      if [ -f ${basename}.warn ]; then rm ${basename}.warn; fi
      if [ -f ${basename}.cnf ]; then rm ${basename}.cnf; fi
      if [ -f core ]; then rm core; fi
      echo $cmd > ${dst}
      $cmd ${basename}.smv >> ${dst} 2>&1
      ulimit -St unlimited
      ulimit -Sd unlimited
      if [ -f .smv_history ]; then rm .smv_history; fi
      if [ -f .smv_lock ]; then rm .smv_lock; fi
      if [ -f ${basename}.update ]; then rm ${basename}.update; fi
      if [ -f ${basename}.warn ]; then rm ${basename}.warn; fi
      if [ -f ${basename}.cnf ]; then rm ${basename}.cnf; fi                                                                              
      if [ -f core ]; then rm core; fi
      echo done

      done;
    done;
  done;
done;
