10.12., 9:00 - 11:00: Due to updates GitLab may be unavailable for some minutes between 09:00 and 11:00.

Commit 1920c90c authored by Philipp J. Meyer's avatar Philipp J. Meyer

Updated benchmark script for lola

parent 29918a87
#!/bin/bash #!/bin/bash
#benchmarks=( 'service-tech/ibm-soundness' 'service-tech/sap-reference' )
#benchmarks=( 'cav-benchmarks/mist' 'cav-benchmarks/wahl-kroening' 'cav-benchmarks/soter' 'cav-benchmarks/medical' 'cav-benchmarks/bug_tracking' )
benchmarks=( 'service-tech/ibm-soundness' ) benchmarks=( 'service-tech/ibm-soundness' )
#benchmarks=( 'service-tech/sap-reference' ) extensions=( 'lola' )
extensions=( 'pnet' 'tpn' 'lola' 'spec' )
properties=( 'safe' 'fin' )
tool='lola' tool='lola'
executable='/home/philipp/local/lola-2.0/src/lola' executable='lola'
options=''
#1 hour #1 hour
time_soft=$(expr 1 \* 3600) time_soft=$(expr 1 \* 3600)
time_hard=$(expr $time_soft + 60) time_hard=$(expr $time_soft + 60)
#2 gigabyte #8 gigabyte
mem_soft=$(expr 2 \* 1024 \* 1024) mem_soft=$(expr 8 \* 1024 \* 1024)
mem_hard=$(expr $mem_soft + 1024) mem_hard=$(expr $mem_soft + 1024)
properties=( 'safe' )
for benchmark in ${benchmarks[@]}; do for benchmark in ${benchmarks[@]}; do
benchmark_dir="$benchmark" benchmark_dir="$benchmark"
for prop in ${properties[@]}; do for prop in ${properties[@]}; do
...@@ -34,8 +32,8 @@ for benchmark in ${benchmarks[@]}; do ...@@ -34,8 +32,8 @@ for benchmark in ${benchmarks[@]}; do
ulimit -S -v $mem_soft ulimit -S -v $mem_soft
ulimit -H -v $mem_hard ulimit -H -v $mem_hard
set -o pipefail; set -o pipefail;
echo $executable -f $file.$prop.task1 $file.$prop echo $executable $options -f $file.$prop.task $file
$executable -f $file.$prop.task1 $file.$prop 2>&1 | tee $file.out $executable $options -f $file.$prop.task $file 2>&1 | tee $file.out
) )
result=$? result=$?
ryes=$(grep "result: yes" $file.out) ryes=$(grep "result: yes" $file.out)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment