#!/bin/bash

################################################################################
# $Id: timenodesymm.in,v 1.1 2006/05/24 00:13:01 schuppan Exp $
#
# Name:    timenodesymm
# Version: 0.1
# Date:    27.10.2002
#
# Author:  Viktor Schuppan, ETH Zuerich
#
# Description:
#
# Runs Cadence SMV with/without symmetry reduction on a single model of
# the FireWire TIP protocol.
#
# Command-line
#
# timenodessymm -n nodes -p ports -d determinism -t timelimit
#
################################################################################



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



usage() {
  echo "usage: ${0} -n nodes -p ports -d determinism -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 ]; 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} != cfn -a ${1} != scfn -a  ${1} != n  -a  ${1} != sn ]; then
    echo "${0}: illegal determinism"
    exit 1
  else
    det=${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=#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="${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 with timelimit ${tlimit}... "
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                                                                                                                           
