#!/bin/csh

set lemmas=(time_aux1 time_aux2 delivery_delay1 abstract_a1 abstract_a2 \
abstract_a3 abstract_a4 abstract_a5 abstract_a6)

set prfcmd="/project/sal/sal-2.2/bin/sal-inf-bmc -v 3 -d 1 -i --disable-traceability"

if ($# == 1) then 
   set tracefile=$1
else
   echo "Usage: $0 <trace_file>"
   exit 0
endif

if (-e $tracefile) then 
  echo "${tracefile}: file exists"
  exit 0
else if ({ cat /dev/null > $tracefile }) then
  set aux
  #
  # prove the lemmas, all by induction at depth 1
  #
  foreach lm ($lemmas)
    echo $prfcmd simple_startup2 $lm
    echo "\n=========== $lm ==========" >> $tracefile
    echo $prfcmd simple_startup2 $lm >> $tracefile
    echo "" >> $tracefile
    $prfcmd simple_startup2 $lm >>& $tracefile
    set aux="${aux} -l ${lm} "
  end
  #
  # main invariant: shows that the abstraction is correct
  #
  echo $prfcmd $aux simple_startup2 abstract_invar
  echo "\n=========== abstract_invar ==========" >> $tracefile
  echo $prfcmd $aux simple_startup2 abstract_invar >> $tracefile
  echo "" >> $tracefile  
  $prfcmd $aux simple_startup2 abstract_invar >>& $tracefile
  #
  # last step: safety property
  #
  echo $prfcmd -l abstract_invar simple_startup2 synchro
  echo "\n============ synchro ==========" >> $tracefile
  echo $prfcmd -l abstract_invar simple_startup2 synchro >> $tracefile
  echo "" >> $tracefile
  $prfcmd -l abstract_invar simple_startup2 synchro >>& $tracefile
else
  echo "error with $tracefile"
endif