#!/bin/bash

################################################################################
# $Id: timenode.in,v 1.1 2006/05/24 00:13:01 schuppan Exp $
#
# Name:    timenode
# Version: 0.1
# Date:    29.10.2002
#
# Author:  Viktor Schuppan, ETH Zuerich
#
# Description:
#
# Runs Bwolen Yang's version of SMV on single user-specified model of
# the FireWire TIP protocol. Invokes C-preprocessor to build final
# models from several modules.
#
# Command-line
#
# timenode -n nodes -p ports -d determinism -t timelimit
#
################################################################################



#
# configurable parameters
#
SED=/bin/sed
CPP=/usr/bin/cpp
BSMV=/usr/local/bin/bsmv



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 -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

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

if [ ! $nodes = 6nc ]; then
  gencmd="../bin/genall -n ${nodes} -p ${ports}"
else
  gencmd="../bin/genall -n 6 -p ${ports}"
fi
if [ $det = det ]; then
  basename=nodes_${nodes}_${ports}_0
  gencmd="${gencmd}"
elif [ $det = frn ]; then
  basename=nodes_${nodes}_${ports}_1
  gencmd="${gencmd} -frn"
elif [ $det = cfn ]; then
  basename=nodes_${nodes}_${ports}_2
  gencmd="${gencmd} -cfn"
elif [ $det = n ]; then
  basename=nodes_${nodes}_${ports}_3
  gencmd="${gencmd} -frn -cfn"
fi

dst=${basename}_results.txt

echo -n "generating modules for ${basename}.smv... "
${gencmd} > ${dst} 2>&1
if [ $nodes = 6nc ]; then
  if [ $det = det ]; then
    ${SED} -e "s/nodes_6_4_0\.smv/nodes_6nc_4_0\.smv/
      s/#include \"\.\.\/lib\/config_6_4_0\.smv\"/#include \"\.\.\/lib\/config_6nc_4_0\.smv\"/
      " obj/nodes_6_4_0.smv >obj/nodes_6nc_4_0.smv
  elif [ $det = frn ]; then
    ${SED} -e "s/nodes_6_4_1\.smv/nodes_6nc_4_1\.smv/
      s/#include \"\.\.\/lib\/config_6_4_1\.smv\"/#include \"\.\.\/lib\/config_6nc_4_1\.smv\"/
      " obj/nodes_6_4_1.smv >obj/nodes_6nc_4_1.smv
  fi
fi
echo done

pre="${CPP} -P obj/${basename}.smv"
cmd="${BSMV} -f ${basename}_tmp.smv"

if [ ! -f obj/${basename}.smv ]; then
  echo "${0}: source file obj/${basename}.smv not found"
  exit 1
fi

echo -n "model checking file ${basename}.smv with timelimit ${tlimit}... "
ulimit -St ${tlimit}
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}
$pre > ${basename}_tmp.smv
$cmd >> ${dst} 2>&1
ulimit -St unlimited
ulimit -Sv 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                                                                                                                           
