#!/bin/bash

################################################################################
# $Id: timenodes,v 1.1 2006/05/24 00:12:59 schuppan Exp $
#
# Name:    timenodes
# Version: 0.1
# Date:    29.10.2002
#
# Author:  Viktor Schuppan, ETH Zuerich
#
# Description:
# 
# Invokes scripts to generate and verify models from FAC
# paper. '-sequential' top iteration is on model checker, '-interleave'
# on no of nodes (small models first). '-nobmc' disables, '-bmc' enables
# bounded model checking. '-t timelimit' sets the wall clock limit.
#
# Command-line
#
# timenodes [-sequential|-interleave] [-nobmc|-bmc] [-t timelimit]
#
################################################################################



doit() {

  if [ $mc = csmv-bmc -a $bmc = false ]; then
    return
  fi

  if [ $nodes = 10 ]; then
    if [ $det != det -a $det != frn ]; then
      return
    fi
  fi

  if [ $mc = bsmv ]; then
    if [ $det = scfn -o $det = sn ]; then
      return
    fi
    if [ $det = det -o $det = frn ]; then
      if [ $nodes = 4 ]; then
        return
      fi
      if [ $ports = 2 ]; then
	return
      fi
      if [ $ports = 4 -a \( $nodes != 6 -a $nodes != 6nc \) ]; then
	return
      fi
      if [ $ports = 3 -a $nodes = 6 ]; then
        return
      fi
    fi
    if [ $nodes = 6nc -a ! \( $ports = 4 -a \( $det = det -o $det = frn \) \) ]; then
      return
    fi
    cd bsmv/run
    ../bin/timenode -n ${nodes} -p ${ports} -d ${det} -t ${tlimit}
    cd ../..
  fi                                                                       

  if [ $mc = csmv-symm ]; then
    if [ ${nodes} = 6nc -o ${nodes} = 10 ]; then
      return
    fi
    if [ $det = det -o $det = frn ]; then
      return
    fi
    cd csmv/runsymm
    ../bin/timenodesymm -n ${nodes} -p ${ports} -d ${det} -t ${tlimit}
    cd ../..
  fi                                                                       

  if [ $mc = csmv-bmc ]; then
    if [ $nodes = 4 ]; then
      return
    fi
    if [ $ports = 2 ]; then
      return
    fi
    if [ ! $det = det -a ! $det = n ]; then
      return
    fi
    if [ $ports = 4 -a \( $nodes != 6 -a $nodes != 6nc \) ]; then
      return
    fi
    if [ $ports = 3 -a \( $nodes = 6 -o $nodes = 6nc \) ]; then
      return
    fi
    if [ $det = n -a \( $nodes = 6 -o $nodes = 6nc \) ]; then
      return
    fi
    for rootcontits in 0 2; do
      cd csmv/runbmc
      ../bin/timenodebmc -n ${nodes} -p ${ports} -d ${det} -r ${rootcontits} -t ${tlimit}
      cd ../..
    done;
  fi
}

order=sequential
if [ ${1} = -sequential ]; then
  shift
  order=sequential
elif [ ${1} = -interleave ]; then
  shift
  order=interleave
fi

bmc=false
if [ ${1} = -nobmc ]; then
  shift
  bmc=false
elif [ ${1} = -bmc ]; then
  shift
  bmc=true
fi

tlimit=21600
if [ ${1} = -t ]; then
  shift
  tlimit=${1}
fi

if [ $order = sequential ]; then
  for mc in bsmv csmv-symm csmv-bmc; do \
    for nodes in 2 3 4 5 6 6nc 10; do \
      for ports in 2 3 4; do \
        for det in det frn cfn scfn n sn; do \
          doit
        done;
      done;
    done;
  done;
elif [ $order = interleave ]; then
  for nodes in 2 3 4 5 6 6nc 10; do \
    for ports in 2 3 4; do \
      for det in det frn cfn scfn n sn; do \
        for mc in bsmv csmv-symm csmv-bmc; do \
          doit
        done;
      done;
    done;
  done;
fi