run_benchmarks.sh 3.87 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
16
17
18
19
20
21
22
23
24
25
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
53
54
55
56
57
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
#!/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))

properties=( 'termination' 'consensus' )
prop_options=( '--layered-termination' '--strong-consensus' )
prop_refinements=( 'Checking SAT of layered termination' 'Checking SAT of trap' )

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

>$benchmark_dir/$results_dir/results.csv
echo -n "protocol,file,places,transitions" >>$benchmark_dir/$results_dir/results.csv

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

                (
                    $executable_dir/$executable $options $filename 2>&1 | tee $benchmark_dir/$out_dir/$protocol/$file.out
                )
                n_places=$(grep -e 'Number of places' "$benchmark_dir/$out_dir/$protocol/$file.out" | sed -e 's/^.*: \([0-9]*\)$/\1/')
                n_transitions=$(grep -e 'Number of transitions' "$benchmark_dir/$out_dir/$protocol/$file.out" | sed -e 's/^.*: \([0-9]*\)$/\1/')
                echo -n ",$n_places,$n_transitions" >>$benchmark_dir/$results_dir/results.csv

                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