Loading benchmarks/Makefile +5 −3 Original line number Diff line number Diff line all: main.pdf program: pp-print @echo 'Compiling pp-print' @$(MAKE) -C pp-print Loading @@ -9,13 +11,13 @@ peregrine: protocols: program @./generate_protocols.sh results: protocols peregrine results/results.csv: protocols peregrine @./run_benchmarks.sh table.tex: results table.tex: results/results.csv python3 make_table.py >table.tex pdf: table.tex main.pdf: table.tex pdflatex main.tex clean: Loading benchmarks/main.tex +1 −1 Original line number Diff line number Diff line Loading @@ -14,7 +14,7 @@ $|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. \\ $|\mathcal{P}|$ & Number of layers 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. \\ Loading benchmarks/make_table.py +6 −5 Original line number Diff line number Diff line Loading @@ -10,7 +10,8 @@ prop_steps = [ '$|\mathcal{P}|$', '$|R|$' ] max_params = 2 long_table = True short_table = True short_table = False if len(sys.argv) >= 2: long_table = False short_table = False Loading Loading @@ -87,9 +88,9 @@ if long_table: for i in range(len(params), max_params): row_string += " &" n_places = row['places'] n_states = row['states'] n_transitions = row['transitions'] row_string += ' & %d & %d' % (n_places, n_transitions) row_string += ' & %d & %d' % (n_states, n_transitions) total_time = 0.0 total_timeout = False Loading Loading @@ -166,9 +167,9 @@ if short_table: val = params[0][1:] row_string += "%s " % val n_places = row['places'] n_states = row['states'] n_transitions = row['transitions'] row_string += ' & %d & %d' % (n_places, n_transitions) row_string += ' & %d & %d' % (n_states, n_transitions) total_time = 0.0 total_timeout = False Loading benchmarks/run_benchmarks.sh +3 −3 Original line number Diff line number Diff line Loading @@ -21,7 +21,7 @@ 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 echo -n "protocol,file,states,transitions" >>$benchmark_dir/$results_dir/results.csv for (( propi=0;propi<${#properties[@]};propi++)); do prop=${properties[$propi]} Loading Loading @@ -51,9 +51,9 @@ for protocol_dir in $(find $benchmark_dir/$protocols_dir -mindepth 1 -maxdepth 1 ( $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_states=$(grep -e 'Number of states' "$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 echo -n ",$n_states,$n_transitions" >>$benchmark_dir/$results_dir/results.csv for (( propi=0;propi<${#properties[@]};propi++)); do prop=${properties[$propi]} Loading Loading
benchmarks/Makefile +5 −3 Original line number Diff line number Diff line all: main.pdf program: pp-print @echo 'Compiling pp-print' @$(MAKE) -C pp-print Loading @@ -9,13 +11,13 @@ peregrine: protocols: program @./generate_protocols.sh results: protocols peregrine results/results.csv: protocols peregrine @./run_benchmarks.sh table.tex: results table.tex: results/results.csv python3 make_table.py >table.tex pdf: table.tex main.pdf: table.tex pdflatex main.tex clean: Loading
benchmarks/main.tex +1 −1 Original line number Diff line number Diff line Loading @@ -14,7 +14,7 @@ $|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. \\ $|\mathcal{P}|$ & Number of layers 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. \\ Loading
benchmarks/make_table.py +6 −5 Original line number Diff line number Diff line Loading @@ -10,7 +10,8 @@ prop_steps = [ '$|\mathcal{P}|$', '$|R|$' ] max_params = 2 long_table = True short_table = True short_table = False if len(sys.argv) >= 2: long_table = False short_table = False Loading Loading @@ -87,9 +88,9 @@ if long_table: for i in range(len(params), max_params): row_string += " &" n_places = row['places'] n_states = row['states'] n_transitions = row['transitions'] row_string += ' & %d & %d' % (n_places, n_transitions) row_string += ' & %d & %d' % (n_states, n_transitions) total_time = 0.0 total_timeout = False Loading Loading @@ -166,9 +167,9 @@ if short_table: val = params[0][1:] row_string += "%s " % val n_places = row['places'] n_states = row['states'] n_transitions = row['transitions'] row_string += ' & %d & %d' % (n_places, n_transitions) row_string += ' & %d & %d' % (n_states, n_transitions) total_time = 0.0 total_timeout = False Loading
benchmarks/run_benchmarks.sh +3 −3 Original line number Diff line number Diff line Loading @@ -21,7 +21,7 @@ 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 echo -n "protocol,file,states,transitions" >>$benchmark_dir/$results_dir/results.csv for (( propi=0;propi<${#properties[@]};propi++)); do prop=${properties[$propi]} Loading Loading @@ -51,9 +51,9 @@ for protocol_dir in $(find $benchmark_dir/$protocols_dir -mindepth 1 -maxdepth 1 ( $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_states=$(grep -e 'Number of states' "$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 echo -n ",$n_states,$n_transitions" >>$benchmark_dir/$results_dir/results.csv for (( propi=0;propi<${#properties[@]};propi++)); do prop=${properties[$propi]} Loading
