#!/bin/sh

# $Id: configure,v 1.1 2006/05/24 00:12:59 schuppan Exp $

#
# set path of Bwolen Yang's and/or Cadence SMV here
# other paths can be set by replacing `which ...` further down if necessary
#
bsmv=
csmv=

cd `dirname ${0}`

if [ -f .configured ]; then
  echo
  echo "Old configuration exists and might get overwritten. Remove .configure manually if this is desired."
  echo
  exit 1
fi

force=0
if [ "${1}" = "-force" ]; then
  force=1
fi

echo "Checking for make..."
make=`which make`
if [ -x "${make}" ]; then
  echo " make found. Using ${make}."
else
  echo " make not found."
fi

echo "Checking for bash..."
bash=`which bash`
if [ -x "${bash}" ]; then
  echo " bash found. Using ${bash}."
else
  echo " bash not found."
fi

echo "Checking for sed..."
sed=`which sed`
if [ -x "${sed}" ]; then
  echo " sed found. Using ${sed}."
else
  echo " sed not found."
fi

echo "Checking for cpp..."
cpp=`which cpp`
if [ -x "${cpp}" ]; then
  echo " cpp found. Using ${cpp}."
else
  echo " cpp not found."
fi

echo "Checking for Bwolen Yang's SMV..."
if [ -x "${bsmv}" ]; then
  echo " Bwolen Yang's SMV specified by user. Using ${bsmv}."
else
  for f in /usr/local/bin/smv-2.4b /usr/local/src/smv-2.4b/bin/smv-2.4b `which bsmv` ; do
    if [ -x ${f} ]; then
       (${f} | tail -n 113 > bsmv.out) 2> /dev/null
       (diff bsmv.out lib/bsmv.test 2>&1 > /dev/null) && bsmv=${f}
       rm -f bsmv.out
    fi
  done
  if [ -x "${bsmv}" ]; then
    echo " Bwolen Yang's SMV found. Using ${bsmv}." 
  else
    echo " Bwolen Yang's SMV not found." 
  fi
fi

echo "Checking for Cadence SMV..."
if [ -x "${csmv}" ]; then
  echo " Cadence SMV specified by user. Using ${csmv}."
else
  for f in /usr/local/bin/smv /usr/local/bin/csmv /usr/local/src/smv/bin/smv /usr/local/src/csmv/bin/smv `which smv` `which csmv` ; do
    if [ -x ${f} ]; then
       (${f} lib/csmv.test | head -n 1 > csmv.out) 2> /dev/null
       (diff csmv.out lib/csmv.test 2>&1 > /dev/null) && csmv=${f}
       rm -f csmv.out
    fi
  done
  if [ -x "${csmv}" ]; then
    echo " Cadence SMV found. Using ${csmv}." 
  else
    echo " Cadence SMV not found." 
  fi
fi

if [ ! -x "${bsmv}" ]; then
  if [ -x "${csmv}" ]; then
    bsmv=${csmv}
    echo "Bwolen Yang's SMV not found. Using Cadence SMV instead."
  fi
fi

if [ ! -x "${bsmv}" ]; then
  bsmv=`which NuSMV`
  if [ -x "${bsmv}" ]; then
    echo "Bwolen Yang's SMV not found. Using ${bsmv} instead."
  else
    bsmv=`which smv`
    if [ -x "${bsmv}" ]; then
      echo "Bwolen Yang's SMV not found. Using ${bsmv} instead."
    fi
  fi
fi

err=0
sederr=0

if [ ! -x "${make}" ]; then
  echo "Error: make not found. Please provide path of make in configure script explicitely and run again or execute commands from Makefile(s) by hand."
  err=1
fi

if [ ! -x "${bash}" ]; then
  echo "Error: bash not found. Please provide path of bash in configure script explicitely and run again. No guarantee that shell scripts work with other shells."
  err=1
fi

if [ ! -x "${sed}" ]; then
  echo "Error: sed not found. Please provide path of sed in configure script explicitely and run again. Most shell scripts won't work otherwise."
  err=1
  sederr=1
fi

if [ ! -x "${bsmv}" ]; then
  echo "Error: Bwolen Yang's SMV not found. Please provide path explicitely in configure script and run again."
  err=1
fi

if [ ! -x "${cpp}" ]; then
  echo "Error: cpp not found. Please provide path of cpp in configure script explicitely and run again. The models for Bwolen Yang's SMV require a C-Preprocessor."
  err=1
fi

if [ ! -x "${csmv}" ]; then
  echo "Error: Cadence SMV not found. Please provide path explicitely in configure script and run again."
  err=1
fi

if [ "${err}" -eq 0 -o "${force}" -eq 1 -a "${sederr}" -eq 0 ]; then
  for f in bsmv/bin/timenode csmv/bin/timenodebmc csmv/bin/timenodesymm; do
    ${sed} -e "s,^SED=\/bin\/sed,SED=${sed},
	       s,^BSMV=\/usr\/local\/bin\/smv-2\.4b,BSMV=${bsmv},
	       s,^CSMV=\/usr\/local\/src\/csmv\/bin\/smv,CSMV=${csmv},
	       s,^CPP=\/usr\/bin\/cpp,CPP=${cpp}," ./lib/${f}.in > ./${f}
    chmod 755 ./${f}
  done
  touch .configured
  echo
  echo "Configured sucessfully."
  echo
else
  echo
  echo "An error occurred, configuration was not written. Use -force to enforce writing."
  echo
fi