vr_foldl
vr_foldl_wf
vr_foldr
vr_foldr_wf
vr_upd_lst_ks
vr_upd_lst_ks_wf
vr_base4
vr_base4-ext
base4-rep
base4-rep_wf
vr_baseK
vr_add_ge_zero
vr_divK
vr_divKplus
vr_natInd4
vr_sub_eq
vr_rsub_to_sub
vr_req_to_ieq
vr_test2
vr_exists_uni
vr_exists_uni_wf
vr_sub-rel
vr_sub-rel_wf
vr_AC
vr_AC_wf
vr_AC_r
vr_parmAC
vr_parmAC_wf
vr_parmEXT
vr_parmEXT_wf
vr_RAC
vr_RAC_wf
vr_RAC_r
vr_AC1
vr_AC1_wf
vr_AC1p
vr_AC1p_wf
vr_PEM
vr_PEM_wf
vr_equi-pred
vr_equi-pred_wf
vr_ExtFun
vr_ExtFun_wf
vr_EXT
vr_EXT_wf
vr_PEXT
vr_PEXT_wf
vr_EXTtoPEXT
vr_PEXT_implies_A_eq_AimpA
vr_PEXT_implies_retract
vr_PEXT_implies_fixpoint
vr_BOOLDI
vr_BOOLDI_wf
vr_BOOLDI_r
vr_PEXT_implies_t_eq_f
vr_PEXT_implies_inconsistent
vr_notPEXT
vr_SURJ
vr_SURJ_wf
vr_RINV
vr_RINV_wf
vr_SURJ_implies_RINV
vr_PROOF_IRREL
vr_PROOF_IRREL_wf
vr_PEXT_implies_PROOF_IRREL
vr_GRAC
vr_GRAC_wf
vr_RAC_and_PROOF_IRREL_implies_GRAC
vr_RAC2_implies_GRAC
vr_PROOF_IRREL_implies_GRAC
vr_AC_bool_subset_to_bool
vr_COMP
vr_COMP_wf
vr_COMP_r
vr_AC1toPEM
vr_AC1ptoPEM
vr_test_abs1
vr_test_abs1_wf
vr_test_abs2
vr_test_abs2_wf
vr_test_abs3
vr_test_abs3_wf
vr_test_length_ext
vr_test_length_ext2
tid
tid_wf
norep2_req'base
norep2_req'base_wf
norep2_req'base_nlp
norep2_handle'base
norep2_handle'base_wf
norep2_handle'base_nlp
norep2_handle'send
norep2_handle'send_wf
norep2_handle'broadcast
norep2_handle'broadcast_wf
norep2_ok'base
norep2_ok'base_wf
norep2_ok'base_nlp
norep2_ok'send
norep2_ok'send_wf
norep2_ok'broadcast
norep2_ok'broadcast_wf
norep2_acc'send
norep2_acc'send_wf
norep2_acc'broadcast
norep2_acc'broadcast_wf
norep2_onHandle
norep2_onHandle_wf
norep2_StoreState
norep2_StoreState_wf
norep2_StoreState_nlp
norep2_ok
norep2_ok_wf
norep2_Store
norep2_Store_wf
norep2_Store_nlp
norep2_okfor
norep2_okfor_wf
norep2_OkFor
norep2_OkFor_wf
norep2_OkFor_nlp
norep2_accept
norep2_accept_wf
norep2_Handler
norep2_Handler_wf
norep2_Handler_nlp
norep2_Leader
norep2_Leader_wf
norep2_Leader_nlp
norep2_main
norep2_main_wf
norep2_main_nlp
norep2_main_programmable
norep2_headers
norep2_headers_wf
norep2_headers_no_inputs
norep2_headers_no_inputs_wf
norep2_stdma
norep2_stdma_wf
norep2_message-constraint
norep2_message-constraint_wf
norep2_messages-delivered
norep2_messages-delivered_wf
sc_agreement
sc_agreement_wf
sc_validity
sc_validity_wf
sc_internal-caused
sc-decided-round1
sc-retry-round1
sc-decided-round
sc-retry-round
sc-vote+1-round
SimpleConsensus_main_nlp-ext
SimpleConsensus_main_nlp-ext
RSC_Vote
RSC_Vote_wf
RSC_Vote_nlp
RSC_voteMSGSto
RSC_voteMSGSto_wf
RSC_Retry
RSC_Retry_wf
RSC_Retry_nlp
RSC_retryMSGto
RSC_retryMSGto_wf
RSC_Decided
RSC_Decided_wf
RSC_Decided_nlp
RSC_dcdMSGto
RSC_dcdMSGto_wf
RSC_notifyMSGS
RSC_notifyMSGS_wf
RSC_Propose
RSC_Propose_wf
RSC_Propose_nlp
RSC_roundout
RSC_roundout_wf
RSC_init
RSC_init_wf
RSC_thr_out
RSC_thr_out_wf
RSC_newvote
RSC_newvote_wf
RSC_addvote
RSC_addvote_wf
RSC_Quorum
RSC_Quorum_wf
RSC_Quorum_nlp
RSC_Round
RSC_Round_wf
RSC_Round_nlp
RSC_vote2retry
RSC_vote2retry_wf
RSC_RoundInfo
RSC_RoundInfo_wf
RSC_RoundInfo_nlp
RSC_round_increase
RSC_round_increase_wf
RSC_incround
RSC_incround_wf
RSC_NewRounds
RSC_NewRounds_wf
RSC_NewRounds_nlp
RSC_Decision
RSC_Decision_wf
RSC_Notify
RSC_Notify_wf
RSC_Notify_nlp
RSC_Voter
RSC_Voter_wf
RSC_Voter_nlp
RSC_onnewpropose
RSC_onnewpropose_wf
RSC_vote2prop
RSC_vote2prop_wf
RSC_Proposal
RSC_Proposal_wf
RSC_Proposal_nlp
RSC_new_proposal
RSC_new_proposal_wf
RSC_NewVoters
RSC_NewVoters_wf
RSC_NewVoters_nlp
RSC_Replica
RSC_Replica_wf
RSC_Replica_nlp
RSC_main
RSC_main_wf
RSC_main_nlp
RSC_main_programmable
RSC_headers
RSC_headers_wf
RSC_headers_no_inputs
RSC_headers_no_inputs_wf
RSC_stdma
RSC_stdma_wf
RSC_message-constraint
RSC_message-constraint_wf
RSC_messages-delivered
RSC_messages-delivered_wf
RSC-ilf-hide
RSC-ilf
RSC_vote
RSC_retry
RSC_decided
RSC_ReplicaState
RSC_ReplicaState_wf
RSC_VoterState
RSC_VoterState_wf
RSC_agreement
RSC_agreement_wf
RSC_validity
RSC_validity_wf
RSC_non_blocking
RSC_non_blocking_wf
sq_stable__RSC_validity
RSC_Proposal-single-val
RSC_ReplicaState-single-val
RSC_ReplicaState-prop1
RSC_ReplicaState-prop2
RSC_VoterState-single-val
RSC_VoterState-inv
RSC_PrVoterState-inv
RSC_VoterState-trans
RSC_VoterState-trans2
RSC_VotesInRound-single-val
RSC_VotesInRound-inv
RSC_votes-from-locs
RSC_voter_start_unique
RSC-votes-consistent
RSC-decided-property
RSC-retry-property
RSC-retry-property2
RSC-agreement-property
RSC_validity_property
RSC_progress
RSC-slow-round
RSC-slow-round_wf
rsc3_vote'base
rsc3_vote'base_wf
rsc3_vote'base_nlp
rsc3_vote'send
rsc3_vote'send_wf
rsc3_vote'broadcast
rsc3_vote'broadcast_wf
rsc3_retry'base
rsc3_retry'base_wf
rsc3_retry'base_nlp
rsc3_retry'send
rsc3_retry'send_wf
rsc3_retry'broadcast
rsc3_retry'broadcast_wf
rsc3_decided'base
rsc3_decided'base_wf
rsc3_decided'base_nlp
rsc3_decided'send
rsc3_decided'send_wf
rsc3_decided'broadcast
rsc3_decided'broadcast_wf
rsc3_notify'send
rsc3_notify'send_wf
rsc3_notify'broadcast
rsc3_notify'broadcast_wf
rsc3_propose'base
rsc3_propose'base_wf
rsc3_propose'base_nlp
rsc3_roundout
rsc3_roundout_wf
rsc3_init
rsc3_init_wf
rsc3_newvote
rsc3_newvote_wf
rsc3_addvote
rsc3_addvote_wf
rsc3_add_to_quorum
rsc3_add_to_quorum_wf
rsc3_when_quorum
rsc3_when_quorum_wf
rsc3_QuorumState
rsc3_QuorumState_wf
rsc3_QuorumState_nlp
rsc3_Quorum
rsc3_Quorum_wf
rsc3_Quorum_nlp
rsc3_Round
rsc3_Round_wf
rsc3_Round_nlp
rsc3_vote2retry
rsc3_vote2retry_wf
rsc3_RoundInfo
rsc3_RoundInfo_wf
rsc3_RoundInfo_nlp
rsc3_update_round
rsc3_update_round_wf
rsc3_when_new_round
rsc3_when_new_round_wf
rsc3_NewRoundsState
rsc3_NewRoundsState_wf
rsc3_NewRoundsState_nlp
rsc3_NewRounds
rsc3_NewRounds_wf
rsc3_NewRounds_nlp
rsc3_decision
rsc3_decision_wf
rsc3_Notify
rsc3_Notify_wf
rsc3_Notify_nlp
rsc3_Voter
rsc3_Voter_wf
rsc3_Voter_nlp
rsc3_onnewpropose
rsc3_onnewpropose_wf
rsc3_vote2prop
rsc3_vote2prop_wf
rsc3_Proposal
rsc3_Proposal_wf
rsc3_Proposal_nlp
rsc3_update_replica
rsc3_update_replica_wf
rsc3_when_new_proposal
rsc3_when_new_proposal_wf
rsc3_ReplicaState
rsc3_ReplicaState_wf
rsc3_ReplicaState_nlp
rsc3_NewVoters
rsc3_NewVoters_wf
rsc3_NewVoters_nlp
rsc3_Replica
rsc3_Replica_wf
rsc3_Replica_nlp
rsc3_main
rsc3_main_wf
rsc3_main_nlp
rsc3_main_programmable
rsc3_headers
rsc3_headers_wf
rsc3_headers_no_inputs
rsc3_headers_no_inputs_wf
rsc3_stdma
rsc3_stdma_wf
rsc3_message-constraint
rsc3_message-constraint_wf
rsc3_messages-delivered
rsc3_messages-delivered_wf
rsc2_vote'base
rsc2_vote'base_wf
rsc2_vote'base_nlp
rsc2_vote'send
rsc2_vote'send_wf
rsc2_vote'broadcast
rsc2_vote'broadcast_wf
rsc2_retry'base
rsc2_retry'base_wf
rsc2_retry'base_nlp
rsc2_retry'send
rsc2_retry'send_wf
rsc2_retry'broadcast
rsc2_retry'broadcast_wf
rsc2_decided'base
rsc2_decided'base_wf
rsc2_decided'base_nlp
rsc2_decided'send
rsc2_decided'send_wf
rsc2_decided'broadcast
rsc2_decided'broadcast_wf
rsc2_notify'send
rsc2_notify'send_wf
rsc2_notify'broadcast
rsc2_notify'broadcast_wf
rsc2_propose'base
rsc2_propose'base_wf
rsc2_propose'base_nlp
rsc2_roundout
rsc2_roundout_wf
rsc2_init
rsc2_init_wf
rsc2_thr_out
rsc2_thr_out_wf
rsc2_newvote
rsc2_newvote_wf
rsc2_addvote
rsc2_addvote_wf
rsc2_Quorum
rsc2_Quorum_wf
rsc2_Quorum_nlp
rsc2_Round
rsc2_Round_wf
rsc2_Round_nlp
rsc2_vote2retry
rsc2_vote2retry_wf
rsc2_RoundInfo
rsc2_RoundInfo_wf
rsc2_RoundInfo_nlp
rsc2_round_increase
rsc2_round_increase_wf
rsc2_incround
rsc2_incround_wf
rsc2_NewRounds
rsc2_NewRounds_wf
rsc2_NewRounds_nlp
rsc2_decision
rsc2_decision_wf
rsc2_Notify
rsc2_Notify_wf
rsc2_Notify_nlp
rsc2_Voter
rsc2_Voter_wf
rsc2_Voter_nlp
rsc2_onnewpropose
rsc2_onnewpropose_wf
rsc2_vote2prop
rsc2_vote2prop_wf
rsc2_Proposal
rsc2_Proposal_wf
rsc2_Proposal_nlp
rsc2_new_proposal
rsc2_new_proposal_wf
rsc2_NewVoters
rsc2_NewVoters_wf
rsc2_NewVoters_nlp
rsc2_Replica
rsc2_Replica_wf
rsc2_Replica_nlp
rsc2_main
rsc2_main_wf
rsc2_main_nlp
rsc2_main_programmable
rsc2_headers
rsc2_headers_wf
rsc2_headers_no_inputs
rsc2_headers_no_inputs_wf
rsc2_stdma
rsc2_stdma_wf
rsc2_message-constraint
rsc2_message-constraint_wf
rsc2_messages-delivered
rsc2_messages-delivered_wf
rsc2-ilf-part1
rsc2-clause6
rsc4_vote'base
rsc4_vote'base_wf
rsc4_vote'base_nlp
rsc4_vote'send
rsc4_vote'send_wf
rsc4_vote'broadcast
rsc4_vote'broadcast_wf
rsc4_retry'base
rsc4_retry'base_wf
rsc4_retry'base_nlp
rsc4_retry'send
rsc4_retry'send_wf
rsc4_retry'broadcast
rsc4_retry'broadcast_wf
rsc4_decided'base
rsc4_decided'base_wf
rsc4_decided'base_nlp
rsc4_decided'send
rsc4_decided'send_wf
rsc4_decided'broadcast
rsc4_decided'broadcast_wf
rsc4_notify'send
rsc4_notify'send_wf
rsc4_notify'broadcast
rsc4_notify'broadcast_wf
rsc4_propose'base
rsc4_propose'base_wf
rsc4_propose'base_nlp
rsc4_roundout
rsc4_roundout_wf
rsc4_init
rsc4_init_wf
rsc4_newvote
rsc4_newvote_wf
rsc4_addvote
rsc4_addvote_wf
rsc4_add_to_quorum
rsc4_add_to_quorum_wf
rsc4_when_quorum
rsc4_when_quorum_wf
rsc4_QuorumState
rsc4_QuorumState_wf
rsc4_QuorumState_nlp
rsc4_Quorum
rsc4_Quorum_wf
rsc4_Quorum_nlp
rsc4_Round
rsc4_Round_wf
rsc4_Round_nlp
rsc4_vote2retry
rsc4_vote2retry_wf
rsc4_RoundInfo
rsc4_RoundInfo_wf
rsc4_RoundInfo_nlp
rsc4_update_round
rsc4_update_round_wf
rsc4_when_new_round
rsc4_when_new_round_wf
rsc4_NewRoundsState
rsc4_NewRoundsState_wf
rsc4_NewRoundsState_nlp
rsc4_NewRounds
rsc4_NewRounds_wf
rsc4_NewRounds_nlp
rsc4_decision
rsc4_decision_wf
rsc4_Notify
rsc4_Notify_wf
rsc4_Notify_nlp
rsc4_Voter
rsc4_Voter_wf
rsc4_Voter_nlp
rsc4_onnewpropose
rsc4_onnewpropose_wf
rsc4_vote2prop
rsc4_vote2prop_wf
rsc4_Proposal
rsc4_Proposal_wf
rsc4_Proposal_nlp
rsc4_update_replica
rsc4_update_replica_wf
rsc4_when_new_proposal
rsc4_when_new_proposal_wf
rsc4_ReplicaState
rsc4_ReplicaState_wf
rsc4_ReplicaState_nlp
rsc4_NewVoters
rsc4_NewVoters_wf
rsc4_NewVoters_nlp
rsc4_positive_max
rsc4_increasing_max
rsc4_Replica
rsc4_Replica_wf
rsc4_Replica_nlp
rsc4_main
rsc4_main_wf
rsc4_main_nlp
rsc4_main_programmable
rsc4_headers
rsc4_headers_wf
rsc4_headers_no_inputs
rsc4_headers_no_inputs_wf
rsc4_stdma
rsc4_stdma_wf
rsc4_message-constraint
rsc4_message-constraint_wf
rsc4_messages-delivered
rsc4_messages-delivered_wf
rsc4_vote'msg
rsc4_vote'msg_wf
rsc4-ilf-hide
rsc4-ilf
rsc4-vote
rsc4-vote2
rsc4-retry
rsc4-decided
rsc4-notify
rsc4_pos_rounds
rsc4_strict_inc_rounds
rsc4_increasing_rounds
rsc4_rounds_state_mem
rsc4_pos_max_missing
rsc4_increasing_max
rsc4_replica_state_mem
rsc4_quorum_invariant
rsc4_voter_start_unique
rsc4-votes-consistent
rsc4-decided-property
rsc4-retry-property
rsc4-agreement-property
rsc4-validity-property
rsc4-agreement
rsc4-validity
rsc5_vote'base
rsc5_vote'base_wf
rsc5_vote'base_nlp
rsc5_vote'send
rsc5_vote'send_wf
rsc5_vote'broadcast
rsc5_vote'broadcast_wf
rsc5_retry'base
rsc5_retry'base_wf
rsc5_retry'base_nlp
rsc5_retry'send
rsc5_retry'send_wf
rsc5_retry'broadcast
rsc5_retry'broadcast_wf
rsc5_decided'base
rsc5_decided'base_wf
rsc5_decided'base_nlp
rsc5_decided'send
rsc5_decided'send_wf
rsc5_decided'broadcast
rsc5_decided'broadcast_wf
rsc5_notify'send
rsc5_notify'send_wf
rsc5_notify'broadcast
rsc5_notify'broadcast_wf
rsc5_propose'base
rsc5_propose'base_wf
rsc5_propose'base_nlp
rsc5_init
rsc5_init_wf
rsc5_newvote
rsc5_newvote_wf
rsc5_possmajstep
rsc5_possmajstep_wf
rsc5_roundout
rsc5_roundout_wf
rsc5_when_quorum
rsc5_when_quorum_wf
rsc5_addvote
rsc5_addvote_wf
rsc5_add_to_quorum
rsc5_add_to_quorum_wf
rsc5_QuorumState
rsc5_QuorumState_wf
rsc5_QuorumState_nlp
rsc5_Quorum
rsc5_Quorum_wf
rsc5_Quorum_nlp
rsc5_quorum_inv
rsc5_quorum_progress
rsc5_Round
rsc5_Round_wf
rsc5_Round_nlp
rsc5_vote2retry
rsc5_vote2retry_wf
rsc5_RoundInfo
rsc5_RoundInfo_wf
rsc5_RoundInfo_nlp
rsc5_update_round
rsc5_update_round_wf
rsc5_when_new_round
rsc5_when_new_round_wf
rsc5_NewRoundsState
rsc5_NewRoundsState_wf
rsc5_NewRoundsState_nlp
rsc5_NewRounds
rsc5_NewRounds_wf
rsc5_NewRounds_nlp
rsc5_rounds_inv
rsc5_strict_rounds_progress
rsc5_rounds_progress
rsc5_rounds_mem
rsc5_Halt
rsc5_Halt_wf
rsc5_Halt_nlp
rsc5_Voter
rsc5_Voter_wf
rsc5_Voter_nlp
rsc5_vote2prop
rsc5_vote2prop_wf
rsc5_Proposal
rsc5_Proposal_wf
rsc5_Proposal_nlp
rsc5_update_replica
rsc5_update_replica_wf
rsc5_when_new_proposal
rsc5_when_new_proposal_wf
rsc5_ReplicaState
rsc5_ReplicaState_wf
rsc5_ReplicaState_nlp
rsc5_NewVoters
rsc5_NewVoters_wf
rsc5_NewVoters_nlp
rsc5_pos_max_missing
rsc5_increasing_max
rsc5_replica_mem
rsc5_Replica
rsc5_Replica_wf
rsc5_Replica_nlp
rsc5_main
rsc5_main_wf
rsc5_main_nlp
rsc5_main_programmable
rsc5_headers
rsc5_headers_wf
rsc5_headers_no_inputs
rsc5_headers_no_inputs_wf
rsc5_stdma
rsc5_stdma_wf
rsc5_message-constraint
rsc5_message-constraint_wf
rsc5_messages-delivered
rsc5_messages-delivered_wf
rsc5-ilf
mem_test_int'base
mem_test_int'base_wf
mem_test_int'base_nlp
mem_test_int'send
mem_test_int'send_wf
mem_test_int'broadcast
mem_test_int'broadcast_wf
mem_test_Maximum
mem_test_Maximum_wf
mem_test_Maximum_nlp
mem_test_pos_max
mem_test_ord_max
mem_test_inc_max
mem_test_mem_max
mem_test_start'base
mem_test_start'base_wf
mem_test_start'base_nlp
mem_test_inc'base
mem_test_inc'base_wf
mem_test_inc'base_nlp
mem_test_inc'send
mem_test_inc'send_wf
mem_test_inc'broadcast
mem_test_inc'broadcast_wf
mem_test_obs'base
mem_test_obs'base_wf
mem_test_obs'base_nlp
mem_test_obs'send
mem_test_obs'send_wf
mem_test_obs'broadcast
mem_test_obs'broadcast_wf
mem_test_Input
mem_test_Input_wf
mem_test_Input_nlp
mem_test_IncState
mem_test_IncState_wf
mem_test_IncState_nlp
mem_test_Increment
mem_test_Increment_wf
mem_test_Increment_nlp
mem_test_Obs
mem_test_Obs_wf
mem_test_Obs_nlp
mem_test_Out
mem_test_Out_wf
mem_test_Out_nlp
mem_test_main
mem_test_main_wf
mem_test_main_nlp
mem_test_main_programmable
mem_test_headers
mem_test_headers_wf
mem_test_headers_no_inputs
mem_test_headers_no_inputs_wf
mem_test_stdma
mem_test_stdma_wf
mem_test_message-constraint
mem_test_message-constraint_wf
mem_test_messages-delivered
mem_test_messages-delivered_wf
max_exch_int'base
max_exch_int'base_wf
max_exch_int'base_nlp
max_exch_exchange'base
max_exch_exchange'base_wf
max_exch_exchange'base_nlp
max_exch_exchange'send
max_exch_exchange'send_wf
max_exch_exchange'broadcast
max_exch_exchange'broadcast_wf
max_exch_Input
max_exch_Input_wf
max_exch_Input_nlp
max_exch_Maximum
max_exch_Maximum_wf
max_exch_Maximum_nlp
max_exch_Exchange
max_exch_Exchange_wf
max_exch_Exchange_nlp
max_exch_pos_max
max_exch_ord_max
max_exch_inc_nax
max_exch_mem_max
max_exch_main
max_exch_main_wf
max_exch_main_nlp
max_exch_main_programmable
max_exch_headers
max_exch_headers_wf
max_exch_headers_no_inputs
max_exch_headers_no_inputs_wf
max_exch_stdma
max_exch_stdma_wf
max_exch_message-constraint
max_exch_message-constraint_wf
max_exch_messages-delivered
max_exch_messages-delivered_wf
max1-ilf
ohc_v1_proposal'base
ohc_v1_proposal'base_wf
ohc_v1_proposal'base_nlp
ohc_v1_proposal'send
ohc_v1_proposal'send_wf
ohc_v1_proposal'broadcast
ohc_v1_proposal'broadcast_wf
ohc_v1_vote'base
ohc_v1_vote'base_wf
ohc_v1_vote'base_nlp
ohc_v1_vote'send
ohc_v1_vote'send_wf
ohc_v1_vote'broadcast
ohc_v1_vote'broadcast_wf
ohc_v1_retry'base
ohc_v1_retry'base_wf
ohc_v1_retry'base_nlp
ohc_v1_retry'send
ohc_v1_retry'send_wf
ohc_v1_retry'broadcast
ohc_v1_retry'broadcast_wf
ohc_v1_decided'base
ohc_v1_decided'base_wf
ohc_v1_decided'base_nlp
ohc_v1_decided'send
ohc_v1_decided'send_wf
ohc_v1_decided'broadcast
ohc_v1_decided'broadcast_wf
ohc_v1_notify'send
ohc_v1_notify'send_wf
ohc_v1_notify'broadcast
ohc_v1_notify'broadcast_wf
ohc_v1_initial'base
ohc_v1_initial'base_wf
ohc_v1_initial'base_nlp
ohc_v1_init
ohc_v1_init_wf
ohc_v1_newvote
ohc_v1_newvote_wf
ohc_v1_addvote
ohc_v1_addvote_wf
ohc_v1_add_to_quorum
ohc_v1_add_to_quorum_wf
ohc_v1_roundout1
ohc_v1_roundout1_wf
ohc_v1_when_quorum1
ohc_v1_when_quorum1_wf
ohc_v1_Quorum1State
ohc_v1_Quorum1State_wf
ohc_v1_Quorum1State_nlp
ohc_v1_Quorum1
ohc_v1_Quorum1_wf
ohc_v1_Quorum1_nlp
ohc_v1_quorum1_inv
ohc_v1_prune_off_units
ohc_v1_prune_off_units_wf
ohc_v1_roundout2
ohc_v1_roundout2_wf
ohc_v1_when_quorum2
ohc_v1_when_quorum2_wf
ohc_v1_Quorum2State
ohc_v1_Quorum2State_wf
ohc_v1_Quorum2State_nlp
ohc_v1_Quorum2
ohc_v1_Quorum2_wf
ohc_v1_Quorum2_nlp
ohc_v1_quorum2_inv
ohc_v1_SendVotes
ohc_v1_SendVotes_wf
ohc_v1_SendVotes_nlp
ohc_v1_SendProposals
ohc_v1_SendProposals_wf
ohc_v1_SendProposals_nlp
ohc_v1_Phase2
ohc_v1_Phase2_wf
ohc_v1_Phase2_nlp
ohc_v1_Phase1
ohc_v1_Phase1_wf
ohc_v1_Phase1_nlp
ohc_v1_prop2retry
ohc_v1_prop2retry_wf
ohc_v1_RoundInfo
ohc_v1_RoundInfo_wf
ohc_v1_RoundInfo_nlp
ohc_v1_update_round
ohc_v1_update_round_wf
ohc_v1_when_new_round
ohc_v1_when_new_round_wf
ohc_v1_NewRoundsState
ohc_v1_NewRoundsState_wf
ohc_v1_NewRoundsState_nlp
ohc_v1_NewRounds
ohc_v1_NewRounds_wf
ohc_v1_NewRounds_nlp
ohc_v1_pos_rounds
ohc_v1_inc_rounds
ohc_v1_strict_inc_rounds
ohc_v1_mem_rounds
ohc_v1_Halt
ohc_v1_Halt_wf
ohc_v1_Halt_nlp
ohc_v1_Voter
ohc_v1_Voter_wf
ohc_v1_Voter_nlp
ohc_v1_prop2init
ohc_v1_prop2init_wf
ohc_v1_Initial
ohc_v1_Initial_wf
ohc_v1_Initial_nlp
ohc_v1_update_replica
ohc_v1_update_replica_wf
ohc_v1_when_new_init
ohc_v1_when_new_init_wf
ohc_v1_ReplicaState
ohc_v1_ReplicaState_wf
ohc_v1_ReplicaState_nlp
ohc_v1_NewVoters
ohc_v1_NewVoters_wf
ohc_v1_NewVoters_nlp
ohc_v1_pos_max
ohc_v1_increasing_max
ohc_v1_mem_rep
ohc_v1_Replica
ohc_v1_Replica_wf
ohc_v1_Replica_nlp
ohc_v1_main
ohc_v1_main_wf
ohc_v1_main_nlp
ohc_v1_main_programmable
ohc_v1_headers
ohc_v1_headers_wf
ohc_v1_headers_no_inputs
ohc_v1_headers_no_inputs_wf
ohc_v1_stdma
ohc_v1_stdma_wf
ohc_v1_message-constraint
ohc_v1_message-constraint_wf
ohc_v1_messages-delivered
ohc_v1_messages-delivered_wf
ohc_v1-ilf-part1
ohc_v1-ilf-quorum1
ohc_v1-ilf-quorum2
ohc_v2_proposal'base
ohc_v2_proposal'base_wf
ohc_v2_proposal'base_nlp
ohc_v2_proposal'send
ohc_v2_proposal'send_wf
ohc_v2_proposal'broadcast
ohc_v2_proposal'broadcast_wf
ohc_v2_vote'base
ohc_v2_vote'base_wf
ohc_v2_vote'base_nlp
ohc_v2_vote'send
ohc_v2_vote'send_wf
ohc_v2_vote'broadcast
ohc_v2_vote'broadcast_wf
ohc_v2_retry'base
ohc_v2_retry'base_wf
ohc_v2_retry'base_nlp
ohc_v2_retry'send
ohc_v2_retry'send_wf
ohc_v2_retry'broadcast
ohc_v2_retry'broadcast_wf
ohc_v2_decided'base
ohc_v2_decided'base_wf
ohc_v2_decided'base_nlp
ohc_v2_decided'send
ohc_v2_decided'send_wf
ohc_v2_decided'broadcast
ohc_v2_decided'broadcast_wf
ohc_v2_notify'send
ohc_v2_notify'send_wf
ohc_v2_notify'broadcast
ohc_v2_notify'broadcast_wf
ohc_v2_initial'base
ohc_v2_initial'base_wf
ohc_v2_initial'base_nlp
ohc_v2_init
ohc_v2_init_wf
ohc_v2_newvote
ohc_v2_newvote_wf
ohc_v2_addvote
ohc_v2_addvote_wf
ohc_v2_add_to_quorum
ohc_v2_add_to_quorum_wf
ohc_v2_roundout1
ohc_v2_roundout1_wf
ohc_v2_when_quorum1
ohc_v2_when_quorum1_wf
ohc_v2_Quorum1State
ohc_v2_Quorum1State_wf
ohc_v2_Quorum1State_nlp
ohc_v2_Quorum1
ohc_v2_Quorum1_wf
ohc_v2_Quorum1_nlp
ohc_v2_quorum1_inv
ohc_v2_roundout2
ohc_v2_roundout2_wf
ohc_v2_when_quorum2
ohc_v2_when_quorum2_wf
ohc_v2_Quorum2State
ohc_v2_Quorum2State_wf
ohc_v2_Quorum2State_nlp
ohc_v2_Quorum2
ohc_v2_Quorum2_wf
ohc_v2_Quorum2_nlp
ohc_v2_quorum2_inv
ohc_v2_SendVotes
ohc_v2_SendVotes_wf
ohc_v2_SendVotes_nlp
ohc_v2_SendProposals
ohc_v2_SendProposals_wf
ohc_v2_SendProposals_nlp
ohc_v2_Phase2
ohc_v2_Phase2_wf
ohc_v2_Phase2_nlp
ohc_v2_Phase1
ohc_v2_Phase1_wf
ohc_v2_Phase1_nlp
ohc_v2_prop2retry
ohc_v2_prop2retry_wf
ohc_v2_RoundInfo
ohc_v2_RoundInfo_wf
ohc_v2_RoundInfo_nlp
ohc_v2_update_round
ohc_v2_update_round_wf
ohc_v2_when_new_round
ohc_v2_when_new_round_wf
ohc_v2_NewRoundsState
ohc_v2_NewRoundsState_wf
ohc_v2_NewRoundsState_nlp
ohc_v2_NewRounds
ohc_v2_NewRounds_wf
ohc_v2_NewRounds_nlp
ohc_v2_pos_rounds
ohc_v2_inc_rounds
ohc_v2_strict_inc_rounds
ohc_v2_mem_rounds
ohc_v2_Halt
ohc_v2_Halt_wf
ohc_v2_Halt_nlp
ohc_v2_Voter
ohc_v2_Voter_wf
ohc_v2_Voter_nlp
ohc_v2_prop2init
ohc_v2_prop2init_wf
ohc_v2_Initial
ohc_v2_Initial_wf
ohc_v2_Initial_nlp
ohc_v2_update_replica
ohc_v2_update_replica_wf
ohc_v2_when_new_init
ohc_v2_when_new_init_wf
ohc_v2_ReplicaState
ohc_v2_ReplicaState_wf
ohc_v2_ReplicaState_nlp
ohc_v2_NewVoters
ohc_v2_NewVoters_wf
ohc_v2_NewVoters_nlp
ohc_v2_pos_max
ohc_v2_increasing_max
ohc_v2_mem_rep
ohc_v2_Replica
ohc_v2_Replica_wf
ohc_v2_Replica_nlp
ohc_v2_main
ohc_v2_main_wf
ohc_v2_main_nlp
ohc_v2_main_programmable
ohc_v2_headers
ohc_v2_headers_wf
ohc_v2_headers_no_inputs
ohc_v2_headers_no_inputs_wf
ohc_v2_stdma
ohc_v2_stdma_wf
ohc_v2_message-constraint
ohc_v2_message-constraint_wf
ohc_v2_messages-delivered
ohc_v2_messages-delivered_wf
rotate-ring
rotate-ring_wf
rotate-ring-property1
rotate-ring-step
rotate-ring-property2
rotate-ring-eq-sets
id_in_bag_in_list
fun_exp_set_l_member
l_eqset
l_eqset_wf
bag-member-l_eqset
list-eq-in-bag-if-l_eqset-and-no_repeats
ma-ring
ma-ring_wf
ma-ring-property1
ma-ring-all-in-remove-repeats-steps1
ma-ring-all-in-remove-repeats-steps2
ma-ring-remove-repeats-eq-set-listify
remove-repeats-length-no-repeats
remove-repeats-length-leq
remove-repeats-length-no-repeats-iff
l_contains-eq_set-no_repeats
ma-ring-no-repeats-listify
ma-ring-diff
ma-ring-diff-circle
ma-ring-remove-repeats-id
ma-ring-id
ma-ring-id-or-diff
ma-ring-id-or-diff2
ma-ring-property2
imax-imax-list-left
listify-append
listify-append-last
ler_Config
ler_Config_wf
ler_Config_nlp
ler_send_leader
ler_send_leader_wf
ler_Choose
ler_Choose_wf
ler_Choose_nlp
ler_Propose
ler_Propose_wf
ler_Propose_nlp
ler_send_propose
ler_send_propose_wf
ler_dumEpoch
ler_dumEpoch_wf
ler_Nbr
ler_Nbr_wf
ler_Nbr_nlp
ler_ProposeReply
ler_ProposeReply_wf
ler_ProposeReply_nlp
ler_ChooseReply
ler_ChooseReply_wf
ler_ChooseReply_nlp
ler_leader_ring_main
ler_leader_ring_main_wf
ler_leader_ring_main_nlp
ler_leader_ring_main_programmable
ler_leader_ring_headers
ler_leader_ring_headers_wf
ler_leader_ring_headers_no_inputs
ler_leader_ring_headers_no_inputs_wf
ler_leader_ring_stdma
ler_leader_ring_stdma_wf
ler_leader_ring_message-constraint
ler_leader_ring_message-constraint_wf
ler_leader_ring_messages-delivered
ler_leader_ring_messages-delivered_wf
SpLeaderRing-ilf
ler_Leader
ler_Leader_wf
ler-ilf
ler_Leader_ilf
ler_Propose_ilf
ler_Leader_from_Propose
ler_Propose_from_Propose_or_Choose
ler_Nbr_from_Config
ler_Propose_from_Choose
ler_non_dummy_configuration
ler_non_dummy_configuration_wf
ler_non_dummy_configuration+
ler_non_dummy_configuration+_wf
ler_consistent_configuration
ler_consistent_configuration_wf
ler_non_decreasing_configuration
ler_non_decreasing_configuration_wf
ler_non_dummy_request
ler_non_dummy_request_wf
ler_ring_setup
ler_ring_setup_wf
ler_ring_sub_setup
ler_ring_sub_setup_wf
ler_ring_setup_non_reconf
ler_ring_setup_non_reconf_wf
ler_ring_strong_setup
ler_ring_strong_setup_wf
ler_ring_strong_setup_sub
ler_ring_strong_setup_sub_wf
ler_ring_strong_setup_sub+
ler_ring_strong_setup_sub+_wf
ler_list_Propose
ler_leader_max
ler_leader_max_sub
ler_unique_Leader
ler_unique_Leader_sub
ler_inc_Config
ler_eq_Config
ler_Config_to_Nbr
ler_Config_to_Nbr2
ler_propose_all_nodes
ler_propose_all_nodes2
ler_propose_all_nodes2_sub
ler_propose_all_max
ler_propose_all_max2
ler_propose_all_max2_sub
ler_propose_all_max+
ler_propose_all_max+2
ler_propose_all_max+2_sub
ler_liveness_prop
ler_liveness_prop2
ler_liveness_prop2_sub
ler2_config'base
ler2_config'base_wf
ler2_config'base_nlp
ler2_leader'send
ler2_leader'send_wf
ler2_leader'broadcast
ler2_leader'broadcast_wf
ler2_choose'base
ler2_choose'base_wf
ler2_choose'base_nlp
ler2_propose'base
ler2_propose'base_wf
ler2_propose'base_nlp
ler2_propose'send
ler2_propose'send_wf
ler2_propose'broadcast
ler2_propose'broadcast_wf
ler2_new_conf
ler2_new_conf_wf
ler2_Nbr
ler2_Nbr_wf
ler2_Nbr_nlp
ler2_positive_epoch
ler2_ProposeReply
ler2_ProposeReply_wf
ler2_ProposeReply_nlp
ler2_ChooseReply
ler2_ChooseReply_wf
ler2_ChooseReply_nlp
ler2_main
ler2_main_wf
ler2_main_nlp
ler2_main_programmable
ler2_headers
ler2_headers_wf
ler2_headers_no_inputs
ler2_headers_no_inputs_wf
ler2_stdma
ler2_stdma_wf
ler2_message-constraint
ler2_message-constraint_wf
ler2_messages-delivered
ler2_messages-delivered_wf
ler2-ilf
ler2_leader'base
ler2_leader'base_wf
ler2_propose-ilf
ler2_leader-ilf
ler2_nbr-ilf
ler2_leader_from_propose
ler2_propose_from_propose_or_choose
ler2_nbr_from_config
ler2_propose_from_choose
ler2_consistent_configuration
ler2_consistent_configuration_wf
ler2_non_dummy_configuration
ler2_non_dummy_configuration_wf
ler2_non_dummy_request
ler2_non_dummy_request_wf
ping_Start
ping_Start_wf
ping_Start_nlp
ping_ping
ping_ping_wf
ping_Ping
ping_Ping_wf
ping_Ping_nlp
ping_pong
ping_pong_wf
ping_Pong
ping_Pong_wf
ping_Pong_nlp
ping_out
ping_out_wf
ping_cout
ping_cout_wf
ping_Handler
ping_Handler_wf
ping_Handler_nlp
ping_Subs
ping_Subs_wf
ping_Subs_nlp
ping_P
ping_P_wf
ping_P_nlp
ping_Reply
ping_Reply_wf
ping_Reply_nlp
ping_main
ping_main_wf
ping_main_nlp
ping_main_programmable
ping_headers
ping_headers_wf
ping_headers_no_inputs
ping_headers_no_inputs_wf
ping_stdma
ping_stdma_wf
ping_message-constraint
ping_message-constraint_wf
ping_messages-delivered
ping_messages-delivered_wf
ping-ilf
m_ping_pong_Start
m_ping_pong_Start_wf
m_ping_pong_Start_nlp
m_ping_pong_Ping
m_ping_pong_Ping_wf
m_ping_pong_Ping_nlp
m_ping_pong_ping
m_ping_pong_ping_wf
m_ping_pong_Pong
m_ping_pong_Pong_wf
m_ping_pong_Pong_nlp
m_ping_pong_pong
m_ping_pong_pong_wf
m_ping_pong_Alive
m_ping_pong_Alive_wf
m_ping_pong_Alive_nlp
m_ping_pong_alive
m_ping_pong_alive_wf
m_ping_pong_out
m_ping_pong_out_wf
m_ping_pong_ReplyToPong
m_ping_pong_ReplyToPong_wf
m_ping_pong_ReplyToPong_nlp
m_ping_pong_SendPing
m_ping_pong_SendPing_wf
m_ping_pong_SendPing_nlp
m_ping_pong_Handler
m_ping_pong_Handler_wf
m_ping_pong_Handler_nlp
m_ping_pong_MemState
m_ping_pong_MemState_wf
m_ping_pong_MemState_nlp
m_ping_pong_Mem
m_ping_pong_Mem_wf
m_ping_pong_Mem_nlp
m_ping_pong_P
m_ping_pong_P_wf
m_ping_pong_P_nlp
m_ping_pong_ReplyToPing
m_ping_pong_ReplyToPing_wf
m_ping_pong_ReplyToPing_nlp
m_ping_pong_main
m_ping_pong_main_wf
m_ping_pong_main_nlp
m_ping_pong_main_programmable
m_ping_pong_headers
m_ping_pong_headers_wf
m_ping_pong_headers_no_inputs
m_ping_pong_headers_no_inputs_wf
m_ping_pong_stdma
m_ping_pong_stdma_wf
m_ping_pong_message-constraint
m_ping_pong_message-constraint_wf
m_ping_pong_messages-delivered
m_ping_pong_messages-delivered_wf
mu_ex_v4_Request
mu_ex_v4_Request_wf
mu_ex_v4_Request_nlp
mu_ex_v4_send_request
mu_ex_v4_send_request_wf
mu_ex_v4_Token
mu_ex_v4_Token_wf
mu_ex_v4_Token_nlp
mu_ex_v4_send_token
mu_ex_v4_send_token_wf
mu_ex_v4_LeaveCS
mu_ex_v4_LeaveCS_wf
mu_ex_v4_LeaveCS_nlp
mu_ex_v4_send_leave_cs
mu_ex_v4_send_leave_cs_wf
mu_ex_v4_EnterCS
mu_ex_v4_EnterCS_wf
mu_ex_v4_EnterCS_nlp
mu_ex_v4_send_enter_cs
mu_ex_v4_send_enter_cs_wf
mu_ex_v4_Exec
mu_ex_v4_Exec_wf
mu_ex_v4_Exec_nlp
mu_ex_v4_send_exec
mu_ex_v4_send_exec_wf
mu_ex_v4_UseCS
mu_ex_v4_UseCS_wf
mu_ex_v4_UseCS_nlp
mu_ex_v4_send_busy
mu_ex_v4_send_busy_wf
mu_ex_v4_otherProc
mu_ex_v4_otherProc_wf
mu_ex_v4_onRequest
mu_ex_v4_onRequest_wf
mu_ex_v4_onToken
mu_ex_v4_onToken_wf
mu_ex_v4_onUseCS
mu_ex_v4_onUseCS_wf
mu_ex_v4_onLeaveCS
mu_ex_v4_onLeaveCS_wf
mu_ex_v4_initState
mu_ex_v4_initState_wf
mu_ex_v4_State
mu_ex_v4_State_wf
mu_ex_v4_State_nlp
mu_ex_v4_PrState
mu_ex_v4_PrState_wf
mu_ex_v4_PrState_nlp
mu_ex_v4_PrToken
mu_ex_v4_PrToken_wf
mu_ex_v4_PrToken_nlp
mu_ex_v4_HandleRequests
mu_ex_v4_HandleRequests_wf
mu_ex_v4_HandleRequests_nlp
mu_ex_v4_HandleUseCS
mu_ex_v4_HandleUseCS_wf
mu_ex_v4_HandleUseCS_nlp
mu_ex_v4_HandleToken
mu_ex_v4_HandleToken_wf
mu_ex_v4_HandleToken_nlp
mu_ex_v4_HandleLeaveCS
mu_ex_v4_HandleLeaveCS_wf
mu_ex_v4_HandleLeaveCS_nlp
mu_ex_v4_P
mu_ex_v4_P_wf
mu_ex_v4_P_nlp
mu_ex_v4_CS
mu_ex_v4_CS_wf
mu_ex_v4_CS_nlp
mu_ex_v4_main
mu_ex_v4_main_wf
mu_ex_v4_main_nlp
mu_ex_v4_main_programmable
mu_ex_v4_headers
mu_ex_v4_headers_wf
mu_ex_v4_headers_no_inputs
mu_ex_v4_headers_no_inputs_wf
mu_ex_v4_stdma
mu_ex_v4_stdma_wf
mu_ex_v4_message-constraint
mu_ex_v4_message-constraint_wf
mu_ex_v4_messages-delivered
mu_ex_v4_messages-delivered_wf
mu_ex_v4-ilf
mu_ex_v4_main-ilf
mu_ex_v4_Token-ilf
mu_ex_v4_Request-ilf
mu_ex_v4_LeaveCS-ilf
mu_ex_v4_EnterCS-ilf
mu_ex_v4_Exec-ilf
mu_ex_v4_Token-other
mu_ex_v4_main-single-val
mu_ex_v5_Request
mu_ex_v5_Request_wf
mu_ex_v5_Request_nlp
mu_ex_v5_send_request
mu_ex_v5_send_request_wf
mu_ex_v5_Token
mu_ex_v5_Token_wf
mu_ex_v5_Token_nlp
mu_ex_v5_send_token
mu_ex_v5_send_token_wf
mu_ex_v5_LeaveCS
mu_ex_v5_LeaveCS_wf
mu_ex_v5_LeaveCS_nlp
mu_ex_v5_send_enter_cs
mu_ex_v5_send_enter_cs_wf
mu_ex_v5_UseSR
mu_ex_v5_UseSR_wf
mu_ex_v5_UseSR_nlp
mu_ex_v5_send_busy
mu_ex_v5_send_busy_wf
mu_ex_v5_getOtherProc
mu_ex_v5_getOtherProc_wf
mu_ex_v5_getMachine
mu_ex_v5_getMachine_wf
mu_ex_v5_onRequest
mu_ex_v5_onRequest_wf
mu_ex_v5_onToken
mu_ex_v5_onToken_wf
mu_ex_v5_onUseSR
mu_ex_v5_onUseSR_wf
mu_ex_v5_onLeaveCS
mu_ex_v5_onLeaveCS_wf
mu_ex_v5_initState
mu_ex_v5_initState_wf
mu_ex_v5_State
mu_ex_v5_State_wf
mu_ex_v5_State_nlp
mu_ex_v5_PrState
mu_ex_v5_PrState_wf
mu_ex_v5_PrState_nlp
mu_ex_v5_HandleRequests
mu_ex_v5_HandleRequests_wf
mu_ex_v5_HandleRequests_nlp
mu_ex_v5_HandleUseSR
mu_ex_v5_HandleUseSR_wf
mu_ex_v5_HandleUseSR_nlp
mu_ex_v5_HandleToken
mu_ex_v5_HandleToken_wf
mu_ex_v5_HandleToken_nlp
mu_ex_v5_HandleLeaveCS
mu_ex_v5_HandleLeaveCS_wf
mu_ex_v5_HandleLeaveCS_nlp
mu_ex_v5_P
mu_ex_v5_P_wf
mu_ex_v5_P_nlp
mu_ex_v5_main
mu_ex_v5_main_wf
mu_ex_v5_main_nlp
mu_ex_v5_main_programmable
mu_ex_v5_headers
mu_ex_v5_headers_wf
mu_ex_v5_headers_no_inputs
mu_ex_v5_headers_no_inputs_wf
mu_ex_v5_stdma
mu_ex_v5_stdma_wf
mu_ex_v5_message-constraint
mu_ex_v5_message-constraint_wf
mu_ex_v5_messages-delivered
mu_ex_v5_messages-delivered_wf
mu_ex_v5-ilf
mu_ex_v5_main-ilf
mu_ex_v5_Token-ilf
mu_ex_v5_Request-ilf
mu_ex_v5_EnterCS
mu_ex_v5_EnterCS_wf
mu_ex_v5_EnterCS-ilf
mu_ex_v5_cs-constraint
mu_ex_v5_cs-constraint_wf
mu_ex_v5_strong-message-constraint
mu_ex_v5_strong-message-constraint_wf
mu_ex_v5_no_repeats_headers_no_inputs
mu_ex_v5_State-exists
mu_ex_v5_State-single-val
mu_ex_v5_State-prior-single-val
mu_ex_v5_State-use
mu_ex_v5_State-token
mu_ex_v5_State-request
mu_ex_v5_State-leave-cs
mu_ex_v5_token-implies-state
mu_ex_v5_observe-unit
mu_ex_v5_send-token-not-token
mu_ex_v5_send-token-had-token
mu_ex_v5_send-token-state
mu_ex_v5_send-token-received-or-born
mu_ex_v5_send-token-from-same-loc
mu_ex_v5_send-token-to-same-loc
mu_ex_v5_send-token-to-same-loc2
mu_ex_v5_send-token-unit
mu_ex_v5_send-token-dec
mu_ex_v5_token-between-2sends
mu_ex_v5_decidable-prior-token
mu_ex_v5_initial-send
mu_ex_v5_tok-dec
mu_ex_v5_tok-dec_wf
mu_ex_v5_assert-tok-dec
mu_ex_v5_closest-send-token
mu_ex_v5_closest-send-token2
mu_ex_v5_send-at-most-one
mu_ex_v5_send-single
mu_ex_v5_main-single-val
mu_ex_v5_not-send-token
mu_ex_v5_ZigZag
mu_ex_v6_request'base
mu_ex_v6_request'base_wf
mu_ex_v6_request'base_nlp
mu_ex_v6_request'send
mu_ex_v6_request'send_wf
mu_ex_v6_request'broadcast
mu_ex_v6_request'broadcast_wf
mu_ex_v6_token'base
mu_ex_v6_token'base_wf
mu_ex_v6_token'base_nlp
mu_ex_v6_token'send
mu_ex_v6_token'send_wf
mu_ex_v6_token'broadcast
mu_ex_v6_token'broadcast_wf
mu_ex_v6_leaveCS'base
mu_ex_v6_leaveCS'base_wf
mu_ex_v6_leaveCS'base_nlp
mu_ex_v6_enterCS'send
mu_ex_v6_enterCS'send_wf
mu_ex_v6_enterCS'broadcast
mu_ex_v6_enterCS'broadcast_wf
mu_ex_v6_useSR'base
mu_ex_v6_useSR'base_wf
mu_ex_v6_useSR'base_nlp
mu_ex_v6_busy'send
mu_ex_v6_busy'send_wf
mu_ex_v6_busy'broadcast
mu_ex_v6_busy'broadcast_wf
mu_ex_v6_getOtherProc
mu_ex_v6_getOtherProc_wf
mu_ex_v6_getMachine
mu_ex_v6_getMachine_wf
mu_ex_v6_onRequest
mu_ex_v6_onRequest_wf
mu_ex_v6_onToken
mu_ex_v6_onToken_wf
mu_ex_v6_onUseSR
mu_ex_v6_onUseSR_wf
mu_ex_v6_onLeaveCS
mu_ex_v6_onLeaveCS_wf
mu_ex_v6_initState
mu_ex_v6_initState_wf
mu_ex_v6_State
mu_ex_v6_State_wf
mu_ex_v6_State_nlp
mu_ex_v6_Handle
mu_ex_v6_Handle_wf
mu_ex_v6_Handle_nlp
mu_ex_v6_handleRequest
mu_ex_v6_handleRequest_wf
mu_ex_v6_handleUseSR
mu_ex_v6_handleUseSR_wf
mu_ex_v6_handleToken
mu_ex_v6_handleToken_wf
mu_ex_v6_handleLeaveCS
mu_ex_v6_handleLeaveCS_wf
mu_ex_v6_P
mu_ex_v6_P_wf
mu_ex_v6_P_nlp
mu_ex_v6_main
mu_ex_v6_main_wf
mu_ex_v6_main_nlp
mu_ex_v6_main_programmable
mu_ex_v6_headers
mu_ex_v6_headers_wf
mu_ex_v6_headers_no_inputs
mu_ex_v6_headers_no_inputs_wf
mu_ex_v6_stdma
mu_ex_v6_stdma_wf
mu_ex_v6_message-constraint
mu_ex_v6_message-constraint_wf
mu_ex_v6_messages-delivered
mu_ex_v6_messages-delivered_wf
PV2_test1
pv8_p1_leq_bnum'
pv8_p1_leq_bnum'_wf
pv8_p1_leq_bnum
pv8_p1_leq_bnum_wf
pv8_p1_lt_bnum'
pv8_p1_lt_bnum'_wf
pv8_p1_lt_bnum
pv8_p1_lt_bnum_wf
pv8_p1_max_bnum
pv8_p1_max_bnum_wf
pv8_p1_pmax
pv8_p1_pmax_wf
pv8_p1_update_proposals
pv8_p1_update_proposals_wf
pv8_p1_in_domain
pv8_p1_in_domain_wf
pv8_p1_same_command
pv8_p1_same_command_wf
pv8_p1_same_proposal
pv8_p1_same_proposal_wf
pv8_p1_same_pvalue
pv8_p1_same_pvalue_wf
pv8_p1_add_if_new
pv8_p1_add_if_new_wf
pv8_p1_append_news
pv8_p1_append_news_wf
pv8_p1_threshold
pv8_p1_threshold_wf
pv8_p1_p1a'base
pv8_p1_p1a'base_wf
pv8_p1_p1a'base_nlp
pv8_p1_p1a'send
pv8_p1_p1a'send_wf
pv8_p1_p1a'broadcast
pv8_p1_p1a'broadcast_wf
pv8_p1_p1b'base
pv8_p1_p1b'base_wf
pv8_p1_p1b'base_nlp
pv8_p1_p1b'send
pv8_p1_p1b'send_wf
pv8_p1_p1b'broadcast
pv8_p1_p1b'broadcast_wf
pv8_p1_p2a'base
pv8_p1_p2a'base_wf
pv8_p1_p2a'base_nlp
pv8_p1_p2a'send
pv8_p1_p2a'send_wf
pv8_p1_p2a'broadcast
pv8_p1_p2a'broadcast_wf
pv8_p1_p2b'base
pv8_p1_p2b'base_wf
pv8_p1_p2b'base_nlp
pv8_p1_p2b'send
pv8_p1_p2b'send_wf
pv8_p1_p2b'broadcast
pv8_p1_p2b'broadcast_wf
pv8_p1_preempted'base
pv8_p1_preempted'base_wf
pv8_p1_preempted'base_nlp
pv8_p1_preempted'send
pv8_p1_preempted'send_wf
pv8_p1_preempted'broadcast
pv8_p1_preempted'broadcast_wf
pv8_p1_adopted'base
pv8_p1_adopted'base_wf
pv8_p1_adopted'base_nlp
pv8_p1_adopted'send
pv8_p1_adopted'send_wf
pv8_p1_adopted'broadcast
pv8_p1_adopted'broadcast_wf
pv8_p1_propose'base
pv8_p1_propose'base_wf
pv8_p1_propose'base_nlp
pv8_p1_decision'send
pv8_p1_decision'send_wf
pv8_p1_decision'broadcast
pv8_p1_decision'broadcast_wf
pv8_p1_dummy_ballot
pv8_p1_dummy_ballot_wf
pv8_p1_init_accepted
pv8_p1_init_accepted_wf
pv8_p1_init_acceptor
pv8_p1_init_acceptor_wf
pv8_p1_init_slot_num
pv8_p1_init_slot_num_wf
pv8_p1_init_proposals
pv8_p1_init_proposals_wf
pv8_p1_init_pvalues
pv8_p1_init_pvalues_wf
pv8_p1_init_scout
pv8_p1_init_scout_wf
pv8_p1_init_ballot_num
pv8_p1_init_ballot_num_wf
pv8_p1_init_active
pv8_p1_init_active_wf
pv8_p1_init_leader
pv8_p1_init_leader_wf
pv8_p1_on_p1a
pv8_p1_on_p1a_wf
pv8_p1_on_p2a
pv8_p1_on_p2a_wf
pv8_p1_AcceptorState
pv8_p1_AcceptorState_wf
pv8_p1_AcceptorState_nlp
pv8_p1_AcceptorsP1a
pv8_p1_AcceptorsP1a_wf
pv8_p1_AcceptorsP1a_nlp
pv8_p1_AcceptorsP2a
pv8_p1_AcceptorsP2a_wf
pv8_p1_AcceptorsP2a_nlp
pv8_p1_Acceptor
pv8_p1_Acceptor_wf
pv8_p1_Acceptor_nlp
pv8_p1_CommanderNotify
pv8_p1_CommanderNotify_wf
pv8_p1_CommanderNotify_nlp
pv8_p1_on_p2b
pv8_p1_on_p2b_wf
pv8_p1_CommanderState
pv8_p1_CommanderState_wf
pv8_p1_CommanderState_nlp
pv8_p1_CommanderOutput
pv8_p1_CommanderOutput_wf
pv8_p1_CommanderOutput_nlp
pv8_p1_Commander
pv8_p1_Commander_wf
pv8_p1_Commander_nlp
pv8_p1_ScoutNotify
pv8_p1_ScoutNotify_wf
pv8_p1_ScoutNotify_nlp
pv8_p1_on_p1b
pv8_p1_on_p1b_wf
pv8_p1_ScoutState
pv8_p1_ScoutState_wf
pv8_p1_ScoutState_nlp
pv8_p1_ScoutOutput
pv8_p1_ScoutOutput_wf
pv8_p1_ScoutOutput_nlp
pv8_p1_Scout
pv8_p1_Scout_wf
pv8_p1_Scout_nlp
pv8_p1_on_propose
pv8_p1_on_propose_wf
pv8_p1_when_adopted
pv8_p1_when_adopted_wf
pv8_p1_when_preempted
pv8_p1_when_preempted_wf
pv8_p1_LeaderState
pv8_p1_LeaderState_wf
pv8_p1_LeaderState_nlp
pv8_p1_LeaderPropose
pv8_p1_LeaderPropose_wf
pv8_p1_LeaderPropose_nlp
pv8_p1_LeaderAdopted
pv8_p1_LeaderAdopted_wf
pv8_p1_LeaderAdopted_nlp
pv8_p1_LeaderPreempted
pv8_p1_LeaderPreempted_wf
pv8_p1_LeaderPreempted_nlp
pv8_p1_SpawnFirstScout
pv8_p1_SpawnFirstScout_wf
pv8_p1_SpawnFirstScout_nlp
pv8_p1_Leader
pv8_p1_Leader_wf
pv8_p1_Leader_nlp
pv8_p1_main
pv8_p1_main_wf
pv8_p1_main_nlp
pv8_p1_main_programmable
pv8_p1_headers
pv8_p1_headers_wf
pv8_p1_headers_no_inputs
pv8_p1_headers_no_inputs_wf
pv8_p1_stdma
pv8_p1_stdma_wf
pv8_p1_message-constraint
pv8_p1_message-constraint_wf
pv8_p1_messages-delivered
pv8_p1_messages-delivered_wf
pv8_p2_same_command
pv8_p2_same_command_wf
pv8_p2_same_proposal
pv8_p2_same_proposal_wf
pv8_p2_diff_proposal
pv8_p2_diff_proposal_wf
pv8_p2_greater_proposal
pv8_p2_greater_proposal_wf
pv8_p2_add_if_new
pv8_p2_add_if_new_wf
pv8_p2_out_tr
pv8_p2_out_tr_wf
pv8_p2_iterate_tr
pv8_p2_iterate_tr_wf
pv8_p2_request'base
pv8_p2_request'base_wf
pv8_p2_request'base_nlp
pv8_p2_propose'send
pv8_p2_propose'send_wf
pv8_p2_propose'broadcast
pv8_p2_propose'broadcast_wf
pv8_p2_decision'base
pv8_p2_decision'base_wf
pv8_p2_decision'base_nlp
pv8_p2_response'send
pv8_p2_response'send_wf
pv8_p2_response'broadcast
pv8_p2_response'broadcast_wf
pv8_p2_init_slot_num
pv8_p2_init_slot_num_wf
pv8_p2_init_proposals
pv8_p2_init_proposals_wf
pv8_p2_init_decisions
pv8_p2_init_decisions_wf
pv8_p2_init_latest_decision
pv8_p2_init_latest_decision_wf
pv8_p2_init_replica
pv8_p2_init_replica_wf
pv8_p2_first_unoccupied
pv8_p2_first_unoccupied_wf
pv8_p2_propose
pv8_p2_propose_wf
pv8_p2_perform
pv8_p2_perform_wf
pv8_p2_inner_tr
pv8_p2_inner_tr_wf
pv8_p2_on_decision
pv8_p2_on_decision_wf
pv8_p2_ReplicaState
pv8_p2_ReplicaState_wf
pv8_p2_ReplicaState_nlp
pv8_p2_Replica
pv8_p2_Replica_wf
pv8_p2_Replica_nlp
pv8_p2_main
pv8_p2_main_wf
pv8_p2_main_nlp
pv8_p2_main_programmable
pv8_p2_headers
pv8_p2_headers_wf
pv8_p2_headers_no_inputs
pv8_p2_headers_no_inputs_wf
pv8_p2_stdma
pv8_p2_stdma_wf
pv8_p2_message-constraint
pv8_p2_message-constraint_wf
pv8_p2_messages-delivered
pv8_p2_messages-delivered_wf
vr_test_echo'base
vr_test_echo'base_wf
vr_test_echo'base_nlp
vr_test_forward'base
vr_test_forward'base_wf
vr_test_forward'base_nlp
vr_test_forward'send
vr_test_forward'send_wf
vr_test_forward'broadcast
vr_test_forward'broadcast_wf
vr_test_ackn'base
vr_test_ackn'base_wf
vr_test_ackn'base_nlp
vr_test_ackn'send
vr_test_ackn'send_wf
vr_test_ackn'broadcast
vr_test_ackn'broadcast_wf
vr_test_Forward
vr_test_Forward_wf
vr_test_Forward_nlp
vr_test_Ackn
vr_test_Ackn_wf
vr_test_Ackn_nlp
vr_test_main
vr_test_main_wf
vr_test_main_nlp
vr_test_main_programmable
vr_test_headers
vr_test_headers_wf
vr_test_headers_no_inputs
vr_test_headers_no_inputs_wf
vr_test_stdma
vr_test_stdma_wf
vr_test_message-constraint
vr_test_message-constraint_wf
vr_test_messages-delivered
vr_test_messages-delivered_wf
Home
Index