Add correctness check to benchmarks

benchmarks/make_table.py

@@ -4,8 +4,8 @@ import pandas as pd
 benchmark_dir='.'
 results_dir='results'
 
-properties = [ 'termination', 'consensus' ]
-prop_steps = [ '$|\mathcal{P}|$', '$|R|$' ]
+properties = [ 'termination', 'consensus', 'correctness' ]
+prop_steps = [ '$|\mathcal{P}|$', '$|R|$', '$|R|$' ]
 
 max_params = 2
 

benchmarks/run_benchmarks.sh

@@ -13,9 +13,9 @@ 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' )
+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' )
 
 mkdir -p $benchmark_dir/$out_dir
 mkdir -p $benchmark_dir/$results_dir