Commit 85d7db33 authored by Philipp Meyer's avatar Philipp Meyer

Preliminary results for positive/negative termination

parent 0e10c59e
......@@ -20,7 +20,7 @@ our_tool=slapnet
#benchmark_dirs=( 'service-tech/ibm-soundness' 'service-tech/sap-reference' )
benchmark_dirs=( 'cav-benchmarks/mist' 'cav-benchmarks/wahl-kroening' 'cav-benchmarks/soter' )
benchmark_tools=( 'sara' 'sara' 'sara ') # TODO: use positive/negative lists
benchmark_tools=( 'sara' 'sara' 'sara' ) # TODO: use positive/negative lists
for (( benchmark=0;benchmark<${#benchmark_dirs[@]};benchmark++)); do
benchmark_dir=${benchmark_dirs[$benchmark]}
other_tool=${benchmark_tools[$benchmark]}
......
cav-benchmarks/mist/PN/MultiME
cav-benchmarks/mist/PN/basicME
cav-benchmarks/mist/PN/bingham_h150
cav-benchmarks/mist/PN/bingham_h25
cav-benchmarks/mist/PN/bingham_h250
cav-benchmarks/mist/PN/bingham_h250_attic
cav-benchmarks/mist/PN/bingham_h50
cav-benchmarks/mist/PN/csm
cav-benchmarks/mist/PN/fms
cav-benchmarks/mist/PN/fms_attic
cav-benchmarks/mist/PN/kanban
cav-benchmarks/mist/PN/leabasicapproach
cav-benchmarks/mist/PN/mesh2x2
cav-benchmarks/mist/PN/mesh3x2
cav-benchmarks/mist/PN/multipool
cav-benchmarks/mist/PN/pingpong
cav-benchmarks/mist/PN/pncsacover
cav-benchmarks/mist/PN/pncsasemiliv
cav-benchmarks/mist/boundedPN/kanban
cav-benchmarks/mist/boundedPN/lamport
cav-benchmarks/mist/boundedPN/newdekker
cav-benchmarks/mist/boundedPN/newrtp
cav-benchmarks/mist/boundedPN/peterson
cav-benchmarks/mist/boundedPN/read_write
cav-benchmarks/mist/PN/extendedread_write
cav-benchmarks/mist/PN/extendedread_write_smallconsts
cav-benchmarks/mist/PN/manufacturing
cav-benchmarks/soter/concdb__single_client_writes__depth_0
cav-benchmarks/soter/concdb__single_client_writes__depth_1
cav-benchmarks/soter/concdb__single_client_writes__depth_2
cav-benchmarks/soter/pipe__single_message_in_mailbox__depth_1
cav-benchmarks/soter/pipe__single_message_in_mailbox__depth_2
cav-benchmarks/soter/reslockbeh__critical__depth_0
cav-benchmarks/soter/reslockbeh__critical__depth_1
cav-benchmarks/soter/reslockbeh__critical__depth_2
cav-benchmarks/soter/ring__single_message_in_mailbox__depth_0
cav-benchmarks/soter/ring__single_message_in_mailbox__depth_1
cav-benchmarks/soter/ring__single_message_in_mailbox__depth_2
cav-benchmarks/soter/sieve__single_message_in_counter_mailbox__depth_0
cav-benchmarks/soter/sieve__single_message_in_counter_mailbox__depth_1
cav-benchmarks/soter/sieve__single_message_in_counter_mailbox__depth_2
cav-benchmarks/soter/sieve__single_message_in_filter_mailbox__depth_0
cav-benchmarks/soter/sieve__single_message_in_sieve_mailbox__depth_0
cav-benchmarks/soter/state_factory__after_receive_if_no_mail__depth_0
cav-benchmarks/soter/state_factory__single_message_in_mailbox__depth_0
cav-benchmarks/soter/state_factory__single_message_in_mailbox__depth_1
cav-benchmarks/soter/pipe__single_message_in_mailbox__depth_0
cav-benchmarks/soter/stutter__we_abhorr_as__depth_0
cav-benchmarks/soter/stutter__we_abhorr_as__depth_1
cav-benchmarks/soter/stutter__we_abhorr_as__depth_2
cav-benchmarks/soter/finite_leader__single_leader__depth_0
cav-benchmarks/soter/finite_leader__single_leader__depth_1
cav-benchmarks/soter/finite_leader__single_leader__depth_2
cav-benchmarks/soter/firewall__no_pred_called_with_zero__depth_0
cav-benchmarks/soter/firewall__no_pred_called_with_zero__depth_1
cav-benchmarks/soter/firewall__no_pred_called_with_zero__depth_2
cav-benchmarks/soter/howait__all_workers_finished_if_wait_over__depth_0
cav-benchmarks/soter/howait__all_workers_finished_if_wait_over__depth_1
cav-benchmarks/soter/howait__all_workers_finished_if_wait_over__depth_2
cav-benchmarks/soter/parikh__should_already_be_initialized__depth_0
cav-benchmarks/soter/parikh__should_already_be_initialized__depth_1
cav-benchmarks/soter/parikh__should_already_be_initialized__depth_2
cav-benchmarks/soter/reslock__critical__depth_0
cav-benchmarks/soter/reslock__critical__depth_1
cav-benchmarks/soter/reslock__critical__depth_2
cav-benchmarks/soter/safe_send__sending_to_non_pid_1__depth_1
cav-benchmarks/soter/safe_send__sending_to_non_pid_1__depth_2
cav-benchmarks/soter/safe_send__sending_to_non_pid_2__depth_1
cav-benchmarks/soter/safe_send__sending_to_non_pid_2__depth_2
cav-benchmarks/soter/safe_send__sending_to_non_pid_3__depth_1
cav-benchmarks/soter/safe_send__sending_to_non_pid_3__depth_2
cav-benchmarks/soter/safe_send__sending_to_non_pid_4__depth_1
cav-benchmarks/soter/safe_send__sending_to_non_pid_4__depth_2
cav-benchmarks/soter/safe_send__sending_to_non_pid__depth_0
cav-benchmarks/soter/unsafe_send__sending_to_non_pid__depth_0
cav-benchmarks/soter/unsafe_send__sending_to_non_pid__depth_1
cav-benchmarks/soter/unsafe_send__sending_to_non_pid__depth_2
cav-benchmarks/wahl-kroening/Boop_simple_vf_satabs.2/main
cav-benchmarks/wahl-kroening/Function_Pointer3_vs_satabs.2/main
cav-benchmarks/wahl-kroening/Function_Pointer3_vs_satabs.3/main
cav-benchmarks/wahl-kroening/dekker_vs_satabs.1/main
cav-benchmarks/wahl-kroening/dekker_vs_satabs.2/main
cav-benchmarks/wahl-kroening/double_lock_p1_vs_satabs.1/main
cav-benchmarks/wahl-kroening/double_lock_p1_vs_satabs.2/main
cav-benchmarks/wahl-kroening/double_lock_p1_vs_satabs.3/main
cav-benchmarks/wahl-kroening/double_lock_p2_vs_satabs.1/main
cav-benchmarks/wahl-kroening/double_lock_p2_vs_satabs.2/main
cav-benchmarks/wahl-kroening/double_lock_p3_vs_satabs.2/main
cav-benchmarks/wahl-kroening/double_lock_p3_vs_satabs.3/main
cav-benchmarks/wahl-kroening/lu-fig2_fixed_vs_satabs.2/main
cav-benchmarks/wahl-kroening/lu-fig2_fixed_vs_satabs.3/main
cav-benchmarks/wahl-kroening/peterson_vs_satabs.2/main
cav-benchmarks/wahl-kroening/pthread5_vs_satabs.1/main
cav-benchmarks/wahl-kroening/pthread5_vs_satabs.2/main
cav-benchmarks/wahl-kroening/rand_lock_p0_vs_satabs.2/main
cav-benchmarks/wahl-kroening/rand_lock_p0_vs_satabs.3/main
cav-benchmarks/wahl-kroening/simple_loop5_vs_satabs.1/main
cav-benchmarks/wahl-kroening/spin2003_vs_satabs.2/main
cav-benchmarks/wahl-kroening/stack_cas_p0_vs_satabs.2/main
cav-benchmarks/wahl-kroening/stack_cas_p0_vs_satabs.3/main
cav-benchmarks/wahl-kroening/stack_lock_p0_vs_satabs.1/main
cav-benchmarks/wahl-kroening/szymanski_vs_satabs.1/main
cav-benchmarks/wahl-kroening/szymanski_vs_satabs.2/main
cav-benchmarks/wahl-kroening/Boop_simple_vf_satabs.1/main
cav-benchmarks/wahl-kroening/Function_Pointer3_vs_satabs.1/main
cav-benchmarks/wahl-kroening/buggy_spaghetti_vf_satabs.1/main
cav-benchmarks/wahl-kroening/buggy_spaghetti_vf_satabs.2/main
cav-benchmarks/wahl-kroening/conditionals_vs_satabs.1/main
cav-benchmarks/wahl-kroening/conditionals_vs_satabs.2/main
cav-benchmarks/wahl-kroening/constants_vf_satabs.1/main
cav-benchmarks/wahl-kroening/double_lock_p3_vs_satabs.1/main
cav-benchmarks/wahl-kroening/lu-fig2_fixed_vs_satabs.1/main
cav-benchmarks/wahl-kroening/peterson_vs_satabs.1/main
cav-benchmarks/wahl-kroening/pthread5_vs_satabs.3/main
cav-benchmarks/wahl-kroening/pthread5_vs_satabs.4/main
cav-benchmarks/wahl-kroening/rand_cas_vs_satabs.1/main
cav-benchmarks/wahl-kroening/rand_cas_vs_satabs.2/main
cav-benchmarks/wahl-kroening/rand_lock_p0_vs_satabs.1/main
cav-benchmarks/wahl-kroening/simple_loop5_vs_satabs.2/main
cav-benchmarks/wahl-kroening/spin2003_vs_satabs.1/main
cav-benchmarks/wahl-kroening/stack_cas_p0_vs_satabs.1/main
cav-benchmarks/wahl-kroening/stack_lock_p0_vs_satabs.2/main
cav-benchmarks/wahl-kroening/constants_vf_satabs.2/main
......@@ -16,7 +16,7 @@ for benchmark in ${benchmarks[@]}; do
T="$(date +%s%N)"
(
set -o pipefail;
$executable -f $file.df.task1 $file.df --markinglimit=10000000 2>&1 | tee $file.out
$executable -f $file.terminating.task1 $file.terminating --markinglimit=1000000 2>&1 | tee $file.out
)
result=$?
ryes=$(grep "result: yes" $file.out)
......
......@@ -16,7 +16,7 @@ for benchmark in ${benchmarks[@]}; do
T="$(date +%s%N)"
(
set -o pipefail;
timeout 60 $executable --$ext --no-refinement --deadlock-free-unless-final $file | tee $file.out
timeout 60 $executable --no-given-properties --terminating --$ext $file 2>&1 | tee $file.out
)
result=$?
T=$(($(date +%s%N)-T))
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment