1#!/bin/csh 2 3# 4# Run a set of otter jobs ($1/*.in) and compare the 5# results existing outputs. 6# 7# If $2 is given, it is assumed to be the Otter binary to use. 8# 9# If $3 is given, it is the filename extension for output files. 10# 11 12set base=out 13 14if ($#argv == 0) then 15 echo "usage: Run_all directory [otter] [extension]" 16 exit 1 17endif 18 19if ($#argv >= 2) then 20 set OTTER=$2 21else 22 set OTTER=../../bin/otter 23endif 24 25if ($#argv >= 3) then 26 set OUT=$3 27else 28 set OUT=out$$ 29endif 30 31cd $1 32set errors=0 33foreach i (*.in) 34 echo "Running $1/$i ..." 35 $OTTER < $i >& $i:r.$OUT 36 if (-e $i:r.$base) then 37 set genold=`grep "clauses generated" $i:r.$base | awk '{gen+=$3} END {print gen}'` 38 set gennew=`grep "clauses generated" $i:r.$OUT | awk '{gen+=$3} END {print gen}'` 39 if ($gennew != $genold) then 40 echo "There is a problem: your computer generated $gennew, $OUT generated $genold" 41 set errors=1 42 else 43 echo "Okay, it seems to have run correctly." 44 endif 45 else 46 echo "Okay, but there's no file for comparison." 47 set errors=1 48 endif 49end 50 51echo "" 52 53if (! $errors && $1 != split) then 54 set timeold=`grep "CPU time" *.$base | awk '{sum += $4} END {print sum}'` 55 set timenew=`grep "CPU time" *.$OUT | awk '{sum += $4} END {print sum}'` 56 set speedup=`awk "END {print $timeold / $timenew}" /dev/null` 57 echo "timenew=$timenew, timeold=$timeold." 58 echo "The new ($OUT) times are about $speedup times as fast as the old ($base) times." 59 set too_slow=`awk "END {if ($speedup < .1) print 1}" /dev/null` 60 if ($too_slow) then 61 echo "If this seems way too slow, edit source/Makefile," 62 echo "including -DTP_NO_CLOCKS on the DFLAGS line," 63 echo "then make clean; make otter." 64 endif 65endif 66 67echo "The output files have been left in $1/*.$OUT." 68echo "" 69 70cd .. 71