#!/bin/sh

# Path for OCaml compiler
OCAML=ocamlopt

# Path for ProVerif analyzer
PROVERIF=../proverif/analyzer

# Path for time binary
TIME=time

# Grep key for output of $TIME
# (Try TIMEKEY=elapsed if the following does not work.)
TIMEKEY=real

# Bound on max_rev 
# (Large values may exhaust memory; try N = 4 on 2GB machines, N = 5 on 4GB machines.)
N=2

echo Compiling plutusgen.ml
$OCAML plutusgen.ml -o plutusgen.exe
echo Compiling plutusgenSVW.ml
$OCAML plutusgenSVW.ml -o plutusgenSVW.exe

(

n=1
while [ $n -le $N ]
do
 
echo max_rev = $n

# Without server verified writes
# (To leave out any of the following options, comment out the relevant <for ...> <do> ... <done> loop.)

for corr in "" -corrected 
do

for signenc in "" -signhashwithoutenc
do

for lockbox in "" -detailedlockbox
do

filebase=plutus${corr}${signenc}${lockbox}-$n
echo PROTOCOL ${filebase}

./plutusgen.exe $corr $signenc $lockbox $n > ${filebase}.PV
$TIME $PROVERIF -in pi ${filebase}.PV > ${filebase}.RES 2>&1
grep RESULT ${filebase}.RES
grep $TIMEKEY ${filebase}.RES

done
done
done

# With server verified writes 
# (To leave out any of the following options, comment out the relevant <for ...> <do> ... <done> loop.)

for corr in "" -corrected 
do

for signenc in "" -signhashwithoutenc
do

for lockbox in "" -detailedlockbox
do

for privrfs in "" -privatereadfs
do

filebase=plutusSVW${corr}${signenc}${lockbox}${privrfs}-$n
echo PROTOCOL ${filebase}

./plutusgenSVW.exe $corr $signenc $lockbox $privrfs $n > ${filebase}.PV
$TIME $PROVERIF -in pi ${filebase}.PV > ${filebase}.RES 2>&1
grep RESULT ${filebase}.RES
grep $TIMEKEY ${filebase}.RES

done
done
done
done

n=`expr $n + 1` 

done

) | tee results