#!/bin/bash

################################################################################
# $Id: timenodebmc.in,v 1.1 2006/05/24 00:13:01 schuppan Exp $
#
# Name:    timenodebmc
# Version: 0.1
# Date:    27.10.2002
#
# Author:  Viktor Schuppan, ETH Zuerich
#
# Description:
#
# Runs bounded model checker of Cadence SMV on single model of the FireWire TIP
# protocol.
#
# Command-line
#
# timenodesbmc -n nodes -p ports -d determinism -r rootcontits -t timelimit
#
################################################################################



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



usage() {
  echo "usage: ${0} -n nodes -p ports -d determinism -r rootcontits -t timelimit"
  exit 1
}

nodes=
if [ ! ${1} ]; then
  usage
elif [ ! ${1} = "-n" ]; then
  usage
else
  shift
  if [ ${1} != 2 -a ${1} != 3 -a ${1} != 4 -a ${1} != 5 -a ${1} != 6 -a ${1} != 6nc -a ${1} != 10 ]; then
    echo "${0}: illegal number of nodes"
    exit 1
  else
    nodes=${1}
    shift
  fi
fi

ports=
if [ ! ${1} ]; then
  usage
elif [ ! ${1} = "-p" ]; then
  usage
else
  shift
  if [ ${1} != 2 -a ${1} != 3 -a  ${1} != 4 ]; then
    echo "${0}: illegal number of ports"
    exit 1
  else
    ports=${1}
    shift
  fi
fi

det=
if [ ! ${1} ]; then
  usage
elif [ ! ${1} = "-d" ]; then
  usage
else
  shift
  if [ ${1} != det -a ${1} != frn -a  ${1} != cfn  -a  ${1} != n ]; then
    echo "${0}: illegal determinism"
    exit 1
  else
    det=${1}
    shift
  fi
fi

rootcontits=
if [ ! ${1} ]; then
  usage
elif [ ! ${1} = "-r" ]; then
  usage
else
  shift
  if [ ${1} != 0 -a ${1} != 2 ]; then
    echo "${0}: illegal rootcontits"
    exit 1
  else
    rootcontits=${1}
    shift
  fi
fi

tlimit=
if [ ! ${1} ]; then
  usage
elif [ ! ${1} = "-t" ]; then
  usage
else
  shift
  if [ ! ${1} ]; then
    echo "${0}: illegal timelimit"
    exit 1
  else
    tlimit=${1}
    shift
  fi
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 [ $nnodes = 2 ]; then
    pathlength=20
  elif [ $nnodes = 3 ]; then
    pathlength=25
  elif [ $nnodes = 4 ]; then
    pathlength=29
  elif [ $nnodes = 5 ]; then
    pathlength=34
  elif [ $nnodes = 6 ]; then
    pathlength=38
  elif [ $nnodes = 10 ]; then
    pathlength=56
  fi
elif [ $rootcontits = 2 ]; then
  if [ $nnodes = 2 ]; then
    pathlength=28
  elif [ $nnodes = 3 ]; then
    pathlength=33
  elif [ $nnodes = 4 ]; then
    pathlength=37
  elif [ $nnodes = 5 ]; then
    pathlength=42
  elif [ $nnodes = 6 ]; then
    pathlength=46
  elif [ $nnodes = 10 ]; then
    pathlength=64
  fi
fi

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 ${tlimit}
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}.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}.cnf ]; then rm ${basename}.cnf; fi                                                                              
if [ -f core ]; then rm core; fi
echo done
