#!/bin/sh
# Author: Ullrich Hustadt

USAGE='usage: ltl2snf+ls4 [options for ltl2snf] <file>
<file>                is a file containing a PLTL formula in the syntax accepted by ltl2snf
                      and must be the last argument given to this script
[options for ltl2snf] is a possibly empty list of options for ltl2snf that the script
                      will pass to ltl2snf; if no options are provided then -isnf -ple -simp
                      will be used
Modify LS4 and SNF before use'
LS4=<path to LS4>
SNF=<path to ltl2snf>
if [[ $# >  0 ]]; then
  IN="${@: -1}"
else
  echo "$USAGE"
  exit 1
fi
set -- "${@:1:$(($#-1))}"
RMFILES="/tmp/snf.$$"
trap '${RMFILES:+rm} ${RMFILES:+-f} $RMFILES 2> /dev/null ;
      exit 1' 0 1 2 3 15
if [[ $# > 0 ]]; then
  $SNF $@ -i $IN -o /tmp/snf.$$
else
  $SNF -isnf -ple -simp -i $IN -o /tmp/snf.$$
fi
$LS4 -no-verbose -no-model /tmp/snf.$$
trap 0
${RMFILES:+rm} ${RMFILES:+-f} $RMFILES 2> /dev/null