#!/bin/bash

################################################################################
# $Id: timenodes.in,v 1.1 2006/05/24 00:13:01 schuppan Exp $
#
# Name:    timenodes
# Version: 0.1
# Date:    08.10.2002
#
# Author:  Viktor Schuppan, ETH Zuerich
#
# Description:
#
# Runs Bwolen Yang's version of SMV on models of the FireWire TIP protocol.
# Invokes C-preprocessor to build final models from several modules.
#
# Command-line
#
# timenodes
#
################################################################################



#
# configurable parameters
#
CPP=/usr/bin/cpp
BSMV=/usr/local/bin/smv-2.4b



for nodes in 2 3 4 5 6 6nc 10; do \
  for ports in 2 3 4; do \
    for det in det frn cfn n; 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 -a $nodes != 6nc \) ]; then
	  continue
        fi
	if [ $ports = 3 -a $nodes = 6 ]; then
	  continue
	fi
      fi
      if [ $nodes = 6nc -a ! \( $ports = 4 -a \( $det = det -o $det = frn \) \) ]; then
        continue
      fi
      if [ $nodes = 10 ]; then
        if [ $det != det -a $det != frn ]; then
	 continue
        fi
      fi                                                                       

      if [ $det = det ]; then
        basename=nodes_${nodes}_${ports}_0
      elif [ $det = frn ]; then
        basename=nodes_${nodes}_${ports}_1
      elif [ $det = cfn ]; then
        basename=nodes_${nodes}_${ports}_2
      elif [ $det = n ]; then
        basename=nodes_${nodes}_${ports}_3
      fi
 
      dst=${basename}_results.txt
      pre="${CPP} obj/${basename}.smv"
      # cmd="memusage ${BSMV} -f ${basename}_tmp.smv"
      cmd="${BSMV} -f ${basename}_tmp.smv"

      echo -n "model checking file ${basename}.smv... "
      ulimit -St 21600     #note cmd
      #ulimit -Sd 1048576 #note cmd
      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}
      $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}.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;
