In January 2021 we will introduce a 10 GB quota for project repositories. Higher limits for individual projects will be available on request. Please see https://doku.lrz.de/display/PUBLIC/GitLab for more information.

run_benchmarks.sh 3.96 KB
Newer Older
Stefan Jaax's avatar
Stefan Jaax committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
#!/bin/bash

benchmark_dir='.'
protocols_dir='protocols'
out_dir='out'
results_dir='results'

extension='pp'
executable_dir='../dist/build/peregrine'
executable='peregrine'
options='-i -v'

#1 hour
timelimit=$((1 * 3600))

16 17 18
properties=( 'termination' 'consensus' 'correctness' )
prop_options=( '--layered-termination' '--strong-consensus' '--correctness' )
prop_refinements=( 'Checking SAT of layered termination' 'Checking SAT of trap' 'Checking SAT of trap' )
19
structure_option='--structure'
Stefan Jaax's avatar
Stefan Jaax committed
20 21 22 23 24

mkdir -p $benchmark_dir/$out_dir
mkdir -p $benchmark_dir/$results_dir

>$benchmark_dir/$results_dir/results.csv
25
echo -n "protocol,file,states,transitions" >>$benchmark_dir/$results_dir/results.csv
Stefan Jaax's avatar
Stefan Jaax committed
26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52

for (( propi=0;propi<${#properties[@]};propi++)); do
    prop=${properties[$propi]}
    echo -n ",${prop}_result,${prop}_time,${prop}_refinements" >>$benchmark_dir/$results_dir/results.csv
    >$benchmark_dir/$results_dir/$prop.positive.list
    >$benchmark_dir/$results_dir/$prop.dontknow.list
    >$benchmark_dir/$results_dir/$prop.timeout.list
    >$benchmark_dir/$results_dir/$prop.error.list
done

echo >>$benchmark_dir/$results_dir/results.csv

for protocol_dir in $(find $benchmark_dir/$protocols_dir -mindepth 1 -maxdepth 1 -type d); do
    protocol=$(basename $protocol_dir)
    echo
    echo "Benchmarking $protocol protocol"
    echo

    mkdir -p $benchmark_dir/$out_dir/$protocol
    timeout_reached='false'
    for param in $(seq 1 1000); do
        if [ $timeout_reached == 'false' ]; then
            for filename in $(find $protocol_dir -mindepth 1 -maxdepth 1 -name "${protocol}_?${param}_*.$extension"); do
                file=$(basename $filename)
                echo -n "$protocol,$file" >>$benchmark_dir/$results_dir/results.csv

                (
53
                    $executable_dir/$executable $options $structure_option $filename 2>&1 | tee $benchmark_dir/$out_dir/$protocol/$file.out
Stefan Jaax's avatar
Stefan Jaax committed
54
                )
55 56
                n_states=$(grep -e '^States *: ' "$benchmark_dir/$out_dir/$protocol/$file.out" | sed -e 's/^.*: \([0-9]*\)$/\1/')
                n_transitions=$(grep -e '^Transitions *: ' "$benchmark_dir/$out_dir/$protocol/$file.out" | sed -e 's/^.*: \([0-9]*\)$/\1/')
57
                echo -n ",$n_states,$n_transitions" >>$benchmark_dir/$results_dir/results.csv
Stefan Jaax's avatar
Stefan Jaax committed
58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95

                for (( propi=0;propi<${#properties[@]};propi++)); do
                    prop=${properties[$propi]}
                    prop_option=${prop_options[$propi]}
                    prop_refinement=${prop_refinements[$propi]}
                    echo "Benchmarking $file with property $prop"
                    timing="$(date +%s%N)"
                    (
                        set -o pipefail

                        echo timeout $timelimit $executable_dir/$executable $options $prop_option $filename
                        timeout $timelimit $executable_dir/$executable $options $prop_option $filename 2>&1 | tee $benchmark_dir/$out_dir/$protocol/$file.$prop.out
                    )
                    result=$?
                    timing=$(($(date +%s%N)-timing))
                    if [[ result -eq 0 ]]; then
                        list='positive'
                    elif [[ result -eq 2 ]]; then
                        list='dontknow'
                    elif [[ result -eq 124 || result -eq 137 ]]; then
                        list='timeout'
                    else
                        list='error'
                    fi
                    # get number of refinement steps
                    n_refinements=$(grep -c -e "$prop_refinement" "$benchmark_dir/$out_dir/$protocol/$file.$prop.out")
                    echo "$file,$timing" >>$benchmark_dir/$results_dir/$prop.$list.list
                    echo -n ",$list,$timing,$n_refinements" >>$benchmark_dir/$results_dir/results.csv
                    if [ $list == 'timeout' ]; then
                        timeout_reached='true'
                    fi
                done

                echo >>$benchmark_dir/$results_dir/results.csv
            done
        fi
    done
done