# algorithms for mutual exclusion
# Robert Meolic, July 2005

#without request signals (wor)
#this is useful for equivalence checking, only
#set type "_wor"
#set actions "enter1 exit1 enter2 exit2"

#with request signals
#this is needed for model checking
set type ""
set actions "request1 request2 enter1 exit1 enter2 exit2"

# known model checker's settings
global mc_diagnostic
global mc_explain
global mc_tracepath
global mc_automaton
global mc_minimize
global mc_progress

pa_read_process "me.dat"

pa_encode_process "EMPTY$type"
pa_encode_process "B1 B2 K N1 N2 N1PLUS N2PLUS NPLUS"
pa_encode_process "P1DEKKER P2DEKKER"
pa_encode_process "P1HYMAN P2HYMAN"
pa_encode_process "P1PETERSON P2PETERSON"
pa_encode_process "P1BAKERY P2BAKERY P1BENARI P2BENARI P1STEP P2STEP"

outline ""
outline "########################################################"
outline ""
outline "DEKKER'S ALGORITHM"

versis_compose 1 DEKKER \
   "EMPTY$type P1DEKKER P2DEKKER B1 B2 K" \
   $actions

outline ""
outline "STATISTICS"
outline "pa_comp_state_number = [pa_comp_state_number DEKKER]"
outline "pa_comp_transition_number = [pa_comp_transition_number DEKKER]"
outline "pa_comp_transition_visible = [pa_comp_transition_visible DEKKER]"

outline ""
mc_check_actl_file 1 DEKKER "me.actl"

outline "########################################################"
outline ""
outline "HYMAN'S ALGORITHM"

versis_compose 1 HYMAN \
   "EMPTY$type P1HYMAN P2HYMAN B1 B2 K" \
   $actions

outline ""
outline "STATISTICS"
outline "pa_comp_state_number = [pa_comp_state_number HYMAN]"
outline "pa_comp_transition_number = [pa_comp_transition_number HYMAN]"
outline "pa_comp_transition_visible = [pa_comp_transition_visible HYMAN]"

outline ""
mc_check_actl_file 1 HYMAN "me.actl"

outline "########################################################"
outline ""
outline "COUNTEREXAMPLE FOR HYMAN"

mc_check_actl 1 HYMAN "me_F3" [expr $mc_diagnostic |  $mc_explain | $mc_tracepath]

outline "########################################################"
outline ""
outline "PETERSON'S ALGORITHM"

versis_compose 1 PETERSON \
   "EMPTY$type P1PETERSON P2PETERSON B1 B2 K" \
   $actions

outline ""
outline "STATISTICS"
outline "pa_comp_state_number = [pa_comp_state_number PETERSON]"
outline "pa_comp_transition_number = [pa_comp_transition_number PETERSON]"
outline "pa_comp_transition_visible = [pa_comp_transition_visible PETERSON]"

outline ""
mc_check_actl_file 1 PETERSON "me.actl"

outline "########################################################"
outline ""
outline "LAMPORT'S BAKERY ALGORITHM"

versis_compose 1 BAKERY \
   "EMPTY$type P1BAKERY P2BAKERY B1 B2 N1 N2 N1PLUS N2PLUS" \
   $actions

outline ""
outline "STATISTICS"
outline "pa_comp_state_number = [pa_comp_state_number BAKERY]"
outline "pa_comp_transition_number = [pa_comp_transition_number BAKERY]"
outline "pa_comp_transition_visible = [pa_comp_transition_visible BAKERY]"

outline ""
mc_check_actl_file 1 BAKERY "me.actl"

outline "########################################################"
outline ""
outline "BEN-ARI'S VARIANT OF BAKERY ALGORITHM"

versis_compose 1 BENARI \
   "EMPTY$type P1BENARI P2BENARI N1 N2 N1PLUS N2PLUS" \
   $actions

outline ""
outline "STATISTICS"
outline "pa_comp_state_number = [pa_comp_state_number BENARI]"
outline "pa_comp_transition_number = [pa_comp_transition_number BENARI]"
outline "pa_comp_transition_visible = [pa_comp_transition_visible BENARI]"

outline ""
mc_check_actl_file 1 BENARI "me.actl"

outline "########################################################"
outline ""
outline "THE STeP VARIANT OF BAKERY ALGORITHM"

versis_compose 1 STEP \
   "EMPTY$type P1STEP P2STEP N1 N2 N1PLUS N2PLUS" \
   $actions

outline ""
outline "STATISTICS"
outline "pa_comp_state_number = [pa_comp_state_number STEP]"
outline "pa_comp_transition_number = [pa_comp_transition_number STEP]"
outline "pa_comp_transition_visible = [pa_comp_transition_visible STEP]"

outline ""
mc_check_actl_file 1 STEP "me.actl"

outline "########################################################"
outline ""
outline "THE STeP VARIANT OF BAKERY ALGORITHM - ATOMIC INCREMENTATION"

versis_compose 1 STEP2 \
   "EMPTY$type P1STEP P2STEP N1 N2 NPLUS" \
   $actions

outline ""
outline "STATISTICS"
outline "pa_comp_state_number = [pa_comp_state_number STEP2]"
outline "pa_comp_transition_number = [pa_comp_transition_number STEP2]"
outline "pa_comp_transition_visible = [pa_comp_transition_visible STEP2]"

outline ""
mc_check_actl_file 1 STEP2 "me.actl"

outline "########################################################"
outline ""
outline "COUNTEREXAMPLE FOR STEP"

mc_check_actl 1 STEP "me_F3" [expr $mc_diagnostic |  $mc_explain | $mc_tracepath]

outline "########################################################"
outline "COMPARISON OF DIFFERENT VARIANTS OF BAKERY ALGORITHM"

versis_trace_equivalence 1 STEP 1 STEP2
versis_testing_equivalence 1 STEP 1 STEP2

versis_trace_equivalence 1 STEP 1 BENARI
versis_trace_equivalence 1 STEP 1 BAKERY
versis_trace_equivalence 1 BENARI 1 BAKERY

versis_testing_equivalence 1 STEP 1 BENARI
versis_testing_equivalence 1 STEP 1 BAKERY
versis_testing_equivalence 1 BENARI 1 BAKERY

outline ""
outline "########################################################"
outline ""
outline "LAMPORTS'S (not Bakery) ALGORITHM"

versis_compose 1 LAMPORT \
   "EMPTY$type P1LAMPORT P2LAMPORT B1 B2" \
   $actions

outline ""
outline "STATISTICS"
outline "pa_comp_state_number = [pa_comp_state_number LAMPORT]"
outline "pa_comp_transition_number = [pa_comp_transition_number LAMPORT]"
outline "pa_comp_transition_visible = [pa_comp_transition_visible LAMPORT]"

outline ""
mc_check_actl_file 1 LAMPORT "me.actl"

outline "########################################################"
outline ""
outline "ONEBIT ALGORITHM"

versis_compose 1 ONEBIT \
   "EMPTY$type P1ONEBIT P2ONEBIT B1 B2" \
   $actions

outline ""
outline "STATISTICS"
outline "pa_comp_state_number = [pa_comp_state_number ONEBIT]"
outline "pa_comp_transition_number = [pa_comp_transition_number ONEBIT]"
outline "pa_comp_transition_visible = [pa_comp_transition_visible ONEBIT]"

outline ""
mc_check_actl_file 1 ONEBIT "me.actl"

outline "########################################################"
outline ""
outline "FISCHER'S ALGORITHM"

versis_compose 1 FISCHER \
   "EMPTYFISCHER$type P1FISCHER P2FISCHER REALCLOCK X NOP" \
   $actions

outline ""
outline "STATISTICS"
outline "pa_comp_state_number = [pa_comp_state_number FISCHER]"
outline "pa_comp_transition_number = [pa_comp_transition_number FISCHER]"
outline "pa_comp_transition_visible = [pa_comp_transition_visible FISCHER]"

outline ""
mc_check_actl_file 1 FISCHER "me.actl"
