#!/bin/bash

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



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



for nodes in 2 3 4 5 6; do \
  for ports in 2 3 4; do \
    for det in cfn scfn n sn; do \

      if [ $det = det -o $det = frn ]; then
        if [ $nodes = 4 ]; then
          continue
        fi
        if [ $ports = 2 ]; then
          continue
        fi
        if [ $ports = 4 -a $nodes != 6 ]; then
          continue
        fi
        if [ $ports = 3 -a $nodes = 6 ]; then
          continue
        fi
      fi
      if [ $nodes = 10 ]; then
        if [ $det != det -a $det != frn ]; then
         continue
        fi
      fi                                                                       

      bmcdef=#undef
      sixnocycle=#undef
      rootcontits=0

      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
	nnodes=${nodes}
      else
	nnodes=6
      fi

      # cmd="memusage ${CSMV} -force -persist -together -f -r -rev"
      cmd="${CSMV} -force -persist -together -f -r -rev"

      basename=nodes_${nodes}_${ports}_${det}
      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

      cp ../lib/groups.in ${basename}.groups

      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;
