Update benchmarks

benchmarks/Makefile

+program: pp-print 
+	@echo 'Compiling pp-print'
+	@$(MAKE) -C pp-print
+
+peregrine:
+	@echo 'Compiling peregrine'
+	@$(MAKE) -C ..
+
+protocols: program
+	@./generate_protocols.sh
+
+results: protocols peregrine
+	@./run_benchmarks.sh
+
+table.tex: results
+	python3 make_table.py >table.tex
+
+pdf: table.tex
+	pdflatex main.tex
+
+clean:
+	@rm -f *.aux *.log *.pdf
+	@rm -rf results protocols out
+	@rm -f table.tex
+	@$(MAKE) clean -C pp-print

benchmarks/generate_protocols.sh

+#!/bin/bash
+
+benchmark_dir='.'
+executable='./pp-print/dist/build/pp-print/pp-print'
+protocols_dir='protocols'
+
+mkdir -p $benchmark_dir/$protocols_dir
+
+# majority
+echo "generating majority protocol"
+mkdir -p $benchmark_dir/$protocols_dir/majority
+$executable majorityPP >$benchmark_dir/$protocols_dir/majority/majority_m1_.pp
+
+# broadcast
+echo "generating broadcast protocol"
+mkdir -p $benchmark_dir/$protocols_dir/broadcast
+$executable broadCastPP >$benchmark_dir/$protocols_dir/broadcast/broadcast_m1_.pp
+
+# threshold
+echo "generating threshold protocols"
+mkdir -p $benchmark_dir/$protocols_dir/threshold
+for l in 2 3 4 5 6 7 8 9 10 11 12 13 14 15; do
+    for c in 1; do
+        $executable oldThresholdPP $l $c >$benchmark_dir/$protocols_dir/threshold/threshold_l${l}_c${c}_.pp
+    done
+done
+
+# modulo
+echo "generating modulo protocols"
+mkdir -p $benchmark_dir/$protocols_dir/modulo
+for m in 2 3 4 5 6 7 8 9 10 20 30 40 50 60 70 80 90 100 110 120 130 140 150; do
+    for c in 1; do
+        $executable moduloPP $m $c >$benchmark_dir/$protocols_dir/modulo/modulo_m${m}_c${c}_.pp
+    done
+done
+
+# flock of birds
+echo "generating flockofbirds protocols"
+mkdir -p $benchmark_dir/$protocols_dir/flockofbirds
+for c in 10 15 20 25 30 35 40 45 50 55 60 65 70 75 80 85 90 95 100; do
+    $executable flockOfBirdsPP $c >$benchmark_dir/$protocols_dir/flockofbirds/flockofbirds_c${c}_.pp
+done
+
+# new birds
+echo "generating newbirds protocols"
+mkdir -p $benchmark_dir/$protocols_dir/newbirds
+for c in 10 20 25 30 40 50 75 100 125 150 175 200 225 250 275 300 325 350; do
+    $executable newBirdsPP $c >$benchmark_dir/$protocols_dir/newbirds/newbirds_c${c}_.pp
+done

benchmarks/main.tex

+\documentclass{scrartcl}
+
+\usepackage[a4paper, top=1cm, bottom=1cm, left=1cm, right=1cm]{geometry}
+\usepackage[table]{xcolor}
+\usepackage{booktabs}
+\usepackage{longtable}
+\usepackage{multirow}
+
+\begin{document}
+
+\input{table.tex}
+
+\begin{tabular}{ll}
+    $|Q|$ & Number of states. \\
+    $|T|$ & Number of non-silent transitions. \\
+    termination & Time in seconds to prove layered termination. \\
+    $|\mathcal{P}|$ & Number of blocks in the partition for layered termination. \\
+    consensus & Time in seconds to prove strong consensus. \\
+    $|\mathcal{R}|$ & Number of refinement steps (i.e.\ number of traps or siphons) for strong consensus. \\
+    total & Time in seconds to prove layered termination and strong consensus. \\
+\end{tabular}
+
+\end{document}

benchmarks/make_table.py

+import sys
+import pandas as pd
+
+benchmark_dir='.'
+results_dir='results'
+
+properties = [ 'termination', 'consensus' ]
+prop_steps = [ '$|\mathcal{P}|$', '$|R|$' ]
+
+max_params = 2
+
+long_table = True
+short_table = True
+if len(sys.argv) >= 2:
+    long_table = False
+    short_table = False
+    for arg in sys.argv[1:]:
+        if arg == '-s':
+            short_table = True
+        elif arg == '-l':
+            long_table = True
+        else:
+            print("unknown argument: %s" % arg, file=sys.stderr)
+            sys.exit(-1)
+
+# long table
+
+if long_table:
+    results_file='results.csv'
+
+    results = pd.read_csv(benchmark_dir + '/' + results_dir + '/' + results_file)
+
+    alignrow = "\\begin{longtable}{l"
+    for i in range(max_params):
+        alignrow += 'l'
+    alignrow += 'rr'
+    for prop in properties:
+        alignrow += 'rr'
+    alignrow += 'r}'
+    print(alignrow)
+    print("\\toprule")
+
+    headerrow = "protocol & \\multicolumn{%d}{c}{params} & $|Q|$ & $|T|$" % max_params
+    for prop, prop_step in zip(properties, prop_steps):
+        headerrow +=  " & %s & %s" % (prop, prop_step)
+    headerrow += " & total \\\\"
+    print(headerrow)
+
+    last_protocol = ''
+    last_params = []
+    for i in range(max_params):
+        last_params.append('')
+
+    for result in results.iterrows():
+        row = result[1]
+        row_string = ''
+
+        protocol = row['protocol']
+        filename = row['file']
+
+        protocol_changed = False
+        if protocol != last_protocol:
+            protocol_changed = True
+            print("\\midrule")
+            row_string = "%s" % protocol
+            last_protocol = protocol
+            for i in range(max_params):
+                last_params[i] = ''
+        else:
+            row_string = ""
+
+        params = [ p for p in filename[len(protocol):][:-5].split('_') if len(p) >= 2 ]
+
+        for i in range(len(params)):
+            var = params[i][0]
+            val = params[i][1:]
+            param_string = "$%s = %s$" % (var, val)
+            if last_params[i] != param_string:
+                #if i == 0 and len(params) > 1 and not protocol_changed:
+                #    print("\\cline{2-%d}" % (4 + max_params + 2*len(properties)))
+                last_params[i] = param_string
+                row_string += " & %s" % param_string
+                for j in range(i+1, max_params):
+                    last_params[j] = ''
+            else:
+                row_string += " &"
+        for i in range(len(params), max_params):
+            row_string += " &"
+
+        n_places = row['places']
+        n_transitions = row['transitions']
+        row_string += ' & %d & %d' % (n_places, n_transitions)
+
+        total_time = 0.0
+        total_timeout = False
+
+        for prop in properties:
+            prop_result = row[prop + '_result']
+            prop_time = row[prop + '_time'] / 10**9
+            prop_refinements = row[prop + '_refinements']
+            prop_string = ''
+            if prop_result == 'positive':
+                prop_string = "%.2f" % prop_time
+            elif prop_result == 'dontknow':
+                prop_string = "%.2f (?)" % prop_time
+            elif prop_result == 'timeout':
+                prop_string = 'timeout'
+                total_timeout = True
+            else:
+                prop_string = 'error'
+            try:
+                refinement_string = str(int(prop_refinements))
+            except ValueError:
+                refinement_string ='-'
+            row_string += " & %s & %s" % (prop_string, refinement_string)
+            total_time += prop_time
+
+        row_string += " & "
+        if total_timeout:
+            row_string += "timeout"
+        else:
+            row_string += "%.2f" % total_time
+        row_string += " \\\\"
+
+        print(row_string)
+
+    print("\\bottomrule")
+    print("\\end{longtable}")
+
+# short table
+
+if short_table:
+    results_file='results-short.csv'
+
+    results = pd.read_csv(benchmark_dir + '/' + results_dir + '/' + results_file)
+
+    last_protocol = ''
+    last_params = []
+    for i in range(max_params):
+        last_params.append('')
+
+    for result in results.iterrows():
+        row = result[1]
+        row_string = ''
+
+        protocol = row['protocol']
+        filename = row['file']
+
+        protocol_changed = False
+        if protocol != last_protocol:
+            protocol_changed = True
+            if last_protocol != '':
+                print("\\bottomrule")
+                print("\\end{tabular}")
+            last_protocol = protocol
+            print("\\begin{tabular}{rrrr}")
+            print("\\toprule")
+            print("\multicolumn{3}{c}{%s} \\\\" % protocol)
+            print("\\midrule")
+            print("$m$ & $|Q|$ & $|T|$ & Time\,(s) \\\\")
+            print("\\midrule")
+
+        params = [ p for p in filename[len(protocol):][:-5].split('_') if len(p) >= 2 ]
+
+        if len(params) > 0:
+            val = params[0][1:]
+            row_string += "%s " % val
+
+        n_places = row['places']
+        n_transitions = row['transitions']
+        row_string += ' & %d & %d' % (n_places, n_transitions)
+
+        total_time = 0.0
+        total_timeout = False
+        total_error = False
+
+        for prop in properties:
+            prop_result = row[prop + '_result']
+            if prop_result == 'positive':
+                prop_time = row[prop + '_time'] / 10**9
+                total_time += prop_time
+            elif prop_result == 'timeout':
+                total_timeout = True
+            else:
+                total_error = True
+
+        row_string += " & "
+        if total_timeout:
+            row_string += "timeout"
+        elif total_error:
+            row_string += "error"
+        else:
+            row_string += "%.1f" % total_time
+        row_string += " \\\\"
+
+        print(row_string)
+
+    if last_protocol != '':
+        print("\\bottomrule")
+        print("\\end{tabular}")
+

benchmarks/run_benchmarks.sh

+#!/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