#!/bin/csh
#
# Proof commands for abstract5.sal
#
# Usage: abstract5 <trace_file>
#

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

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

# proofs: <lemmas> <goal>

set proofs
set proofs=($proofs time_aux1)
set proofs=($proofs time_aux2)
set proofs=($proofs time_aux3)
set proofs=($proofs abstract_b)
set proofs=($proofs -l time_aux1 -l time_aux2 -l time_aux3 -l abstract_b abstract_hub_invar)
set proofs=($proofs -l abstract_hub_invar time_aux4)
set proofs=($proofs hub_listen)
set proofs=($proofs -l time_aux2 -l hub_listen hub_transmission)
set proofs=($proofs -l hub_transmission frame_aux1)
set proofs=($proofs -l hub_listen -l hub_transmission frame_aux2 )
set proofs=($proofs -l hub_transmission frame_aux3)
set proofs=($proofs -l hub_transmission frame_aux4)
set proofs=($proofs frame_aux5)
set proofs=($proofs -l frame_aux5 frame_aux6 )
set proofs=($proofs frame_aux7)
set proofs=($proofs -l time_aux3 frame_aux8)
set proofs=($proofs faulty_id)
set proofs=($proofs abstract_a)
set proofs=($proofs -l time_aux1 -l time_aux2 -l time_aux3 -l time_aux4 \
 -l frame_aux1 -l frame_aux2 -l frame_aux3 -l frame_aux4 \
 -l frame_aux5 -l frame_aux6 -l frame_aux7 -l frame_aux8 \
 -l hub_transmission -l faulty_id -l abstract_a abstract_invar)
set proofs=($proofs -l frame_aux8 -l hub_transmission -l abstract_a -l abstract_invar synchro)

if (-e $tracefile) then 
  echo "${tracefile}: file exists"
  exit 0
else if ({ cat /dev/null > $tracefile }) then
  set lemmas goal lm
  foreach word ($proofs)
    if ("${word}" == "-l") then
       set lm=lemma
    else if ("${lm}" == "lemma") then
       set lemmas=($lemmas "-l" $word)
       set lm
    else 
       set goal=$word
       echo $prfcmd $lemmas $context $goal
       echo "\n=========== ${goal} ==========" >> $tracefile
       echo $prfcmd $lemmas $context $goal >> $tracefile
       echo "" >> $tracefile
       $prfcmd $lemmas $context $goal >>& $tracefile
       set lemmas goal lm
    endif
  end
else
  echo "error with $tracefile"
endif