unused.txt

active_nodes_always_identical
active_successors_are_live_nodes
adding_node_preserves_reachable
adding_nodes_did_not_affect_best_succ
adding_nodes_did_not_affect_dead_node
ahr_nodes
all_first_succs_correct_finds_pred
always_exists_live_node
always_forall_list_comm
always_possible_preds_lst
apply_handler_result_nodes
apply_handler_result_preserves_failed_nodes
apply_handler_result_preserves_nodes
at_most_one_request
at_most_one_request_in
best_first_succ_is_best_pred
best_pred_is_best_first_succ
best_succ_of
better_first_succ_bool_antisymmetric
better_pred_better_pred_bool_true
better_pred_better_succ
better_pred_bool_antisym'
better_pred_bool_antisymmetric
better_pred_bool_total'
better_pred_bool_trans
better_pred_bool_true_better_pred
better_pred_elim
better_pred_intro
better_pred_trans
better_succ_better_pred
better_succ_bool_false_not_better_succ
better_succ_bool_true_better_succ
between_ends_neq_unroll_between
between_rot_l
between_rot_r
between_swap_not
between_swap_not_xy
between_trans
between_trans'
Build_global_state
Build_occurrence
busy_response_exists
Chord:client_addr_dec
ChordCorrectPhaseTwo:live_node_preserved_by_recv_step
chord_fail_pre_post_strengthen_l
chord_fail_pre_post_weaken_l
chord_fail_pre_post_weaken_r
chord_init_invariant_weaken_l
chord_init_invariant_weaken_r
Chord:response_payload_dec
ChordSemantics:client_addr_dec
ChordSemantics:client_payload_dec
ChordSemantics:e_fail
ChordSemantics:label_eq_dec
ChordSemantics:payload_eq_dec
chord_start_pre_post_strengthen_l
ChordSystem:client_addr
ChordSystem:client_addr_dec
ChordSystem:_client_payload
ChordSystem:client_payload
ChordSystem:client_payload_dec
ChordSystem:CPGetBestPredecessor
ChordSystem:CPGetSuccList
ChordSystem:data_eq_dec
ChordSystem:empty_start_res
ChordSystem:find_pred
ChordSystem:find_succs
ChordSystem:id
ChordSystem:init_state_join
ChordSystem:init_state_preset
ChordSystem:is_safe
ChordSystem:label
ChordSystem:label_eq_dec
ChordSystem:label_input
ChordSystem:label_output
ChordSystem:pi
ChordSystem:start_handler
ChordSystem:timeout_effect_eq_dec
churn_between
CIdelayed
CInone
CIother
CIreq
CIres
client_addr_dec
client_payload_dec
coarse_best_succ_characterization
coarse_dead_node_characterization
coarse_live_node_characterization
coarse_reachable_characterization
Cons_lb_exec
correct_first_succ_unique
correct_pred_exists
correct_pred_exists'
correct_pred_unique
counting_opt_error_depends_on_live_addrs
counting_opt_error_inj
counting_opt_error_zero_implies_correct
CPGetBestPredecessor
CPGetSuccList
cur_request_join_not_joined
cur_request_preserved_by_do_delayed_queries
data_eq_dec
delay_query_adds_query
do_delayed_queries_busy_nop
do_delayed_queries_never_clears_Tick
do_rectify_never_clears_Tick
enabled_Tick_invariant
enabled_Tick_with_effect
eventual_exists_invariant_always_true
eventually_and_tl_comm
exists_filter_nonempty
exists_node_in_initial_st
Fail
fail_churn
failed_nodes_not_new
first_succ_error_continuously_nonincreasing
first_succ_improvement_suffices
first_succ_never_self
first_succs_correct_succ_right
forge_pointer
GetBestPredClearedPossible
global_state_eq_ext
gpred
gpred_and
handle_delayed_query_only_sends_responses
handle_msg_busy_is_handle_query_req_busy
handle_msg_never_clears_Tick
handle_query_req_busy_delays_query
handle_query_req_busy_never_clears
handle_query_req_busy_preserves_cur_request
handle_query_req_busy_sends_busy
handle_query_req_gives_response
handle_query_req_only_sends_responses
handle_query_res_info_from_changed_set_cur_request
handle_query_res_never_clears_Tick
has_dead_first_succ_intro
has_succs_intro
id_of_z
id_to_ascii
if_Timeout_enabled
Info: read file ../verdi-chord/systems/chord/chord_all.dpd
In_live_ptrs_live
in_nodes_sigma_some
input_not_lbl_loc
in_singleton_eq
intermediate_reachable_st
intReachableDelayedQueries
intReachableInit
intReachableStep
irrelevant_message_not_removed
is_request_same_as_request_payload
is_safe
join_churn
joined_preserved_by_handle_query_timeout
joined_preserved_by_timeout_handler_eff
KeepaliveTick_unconstrained
labeled_step_dynamic_is_step_dynamic_without_churn
labeled_step_dynamic_preserves_active_nodes
labeled_step_dynamic_timeout_enabled
labeled_step_preserves_state_existing
LDeliver_client
l_enabled_Timeout_In_timeouts
length_filter_by_cmp_same_eq
lift_gpred_to_ex
lift_gpred_to_occ
lift_pred_opt_elim
LiftPredOptNone
LiftPredOptSome
lift_pred_opt_Some_elim
LInput
live_addrs_not_empty
live_node_exists_after_simple_change
live_node_in_initial_st
live_node_preserved_by_recv_step
live_node_preserved_by_timeout_step
live_node_specificity
live_ptrs_not_empty
live_ptrs_possible_preds_lst
live_ptrs_with_states
live_with_state
local_drops_below_bound
ltb_correct
lt_false_ltb
lt_true_ltb
make_pointer_valid
make_request_query_request
map_empty
max_cmp
max_cmp_correct
max_cmp_empty
max_cmp_in
max_cmp_None_correct
max_cmp_ret
max_of_nats_zero_means_zero
merge_point_gone_improved_something
merge_point_wf
msg_eq_dec
msg_from_length
name_eq_dec
NoDup_two_diff
nonempty_filter_exists
not_between_between
not_between_between_bool_equiv
not_between_swap
notify_when_pred_dead_eventually_improves
notify_when_pred_worse_eventually_improves
occurred_is_step
open_request_from_better_pred_eventually_improves_error
open_stabilize_request
open_stabilize_request_to_open_request_to
output_not_lbl_loc
pair_GetBestPredecessor
pair_GetSuccList
pair_Ping
pending_query
phase_one_all_first_succs_best
phase_two_zero_error_has_first_succ
phase_two_zero_error_has_pred
pings_always_get_pongs_handle_msg
pings_always_get_pongs_recv_handler
possible_preds_lst
pred_changing_suffices
predecessors_are_live_nodes
pred_error_continuously_nonincreasing
pred_never_self
pred_preserved_by_do_delayed_queries
principal_not_failed
ptr_between_antisym'
ptr_between_antisym''
ptr_between_bool_antisym'
ptr_between_bool_trans
ptr_between_bool_trans'
query_delayed_at
reachable
reachableInit
reachable_intermediate_reachable
ReachableSucc
ReachableTrans
ReachableTransL
ReachableTransR
real_requests_get_busy_response
real_requests_get_queued
real_requests_get_queued_and_busy_response
real_requests_get_response_handle_query_req
real_requests_get_responses_handle_msg
real_requests_get_responses_recv_handler
reassembled_msg_still_eq
RectifyTick_unconstrained
recv_GetPredAndSuccs_busy_queues_request
recv_GetPredAndSuccs_causes_GotPredAndSuccs_eq
recv_GetPredAndSuccs_not_busy_causes_GotPredAndSuccs
recv_GotPredAndSuccs_causes_Notify_Some
recv_GotPredAndSuccs_with_a_after_p_causes_improvement
recv_GotPredAndSuccs_with_a_after_p_causes_Notify
recv_handler_adds_new_timeout_when_sending_request
recv_handler_GetPredAndSuccs_gives_GotPredAndSuccs
recv_handler_GotPredAndSuccs_response_accurate
recv_handler_keeps_timeouts_satisfying_constraint
recv_handler_never_clears_RectifyTick
recv_handler_never_clears_Tick
recv_handler_nodup_cts
recv_handler_nodup_nts
recv_handler_pre_strengthen_l
recv_handler_sends_request_when_adding_new_timeout
recv_handler_sets_cur_request_when_adding_new_timeout
recv_handler_small_cts
recv_implies_message_exists_after_timeout
recv_implies_node_in
recv_implies_node_not_failed
recv_implies_state_exists
recv_implies_state_exists_after_timeout
request_for_query
Request_has_message
request_in_transit
Request_messages_unique
Request_payload_has_response
request_response_mutually_exclusive
request_response_pair_dec
requests_are_always_responded_to
response_for_query
response_in_transit
responses_are_unique
ring_member
safe_msgs
sigma_apply_handler_result_diff
sigma_apply_handler_result_same
sigma_some_in_nodes
split_eq_singleton
Start
start_handler_valid_ptrs_state
start_query_cur_requests_timeouts_ok'
states_not_removed_by_recv_step
step_preserves_timeout_constraint
succ_error_means_merge_point
succs_joined
sufficient_principals_intro
timeout_handler_eff_never_removes_Tick
timeout_handler_eff_Tick_adds_Tick
timeout_implies_node_exists
timeout_implies_node_not_failed
timeout_means_active
timeout_means_active_inductive
timeout_means_active_invariant
timeouts_apply_handler_result_diff
timeouts_in_clear_rectify_with
timeouts_in_never_has_Tick
timeouts_in_Request
timeout_step_satisfies_constraint
unroll_between_neq_swap_false
unrolled_not_between_rot
unrolling_reflexive
unrolling_transitive
unsafe_msgs_not_safe_ones
update_determined_by_f
update_for_start_definition
update_for_start_nodes
update_for_start_nodes_eq
update_for_start_sigma_h_exists
update_for_start_sigma_h_n
valid_opt_ptr_elim
valid_opt_ptr_nodes
valid_opt_ptr_nodes_subset
valid_ptr_elim
valid_ptr_elim_hash
valid_ptr_elim_nodes
valid_ptr_in_nodes
valid_ptr_intro
valid_ptr_list_nodes
valid_ptr_list_nodes_subset
valid_ptr_nodes
valid_ptr_nodes_subset
valid_ptr_payload_nodes
valid_ptr_payload_nodes_subset
valid_ptrs_global_elim
valid_ptrs_global_intro
valid_ptrs_global_net
valid_ptrs_global_recv_handler
valid_ptrs_global_sigma
valid_ptrs_global_start_invariant
valid_ptrs_global_timeout_handler
valid_ptrs_global_timeouts
valid_ptrs_global_trace
valid_ptrs_net_elim_snd_snd
valid_ptrs_some_cur_request_elim
valid_ptrs_some_cur_request_elim_m
valid_ptrs_some_cur_request_elim_p
valid_ptrs_some_cur_request_elim_q
valid_ptrs_some_cur_request_intro
valid_ptrs_state_elim
valid_ptrs_state_intro
valid_ptrs_state_nodes_subset
valid_ptrs_timeouts_elim
valid_ptrs_timeouts_intro
valid_ptrs_timeouts_nodes_timeouts
valid_ptrs_timeouts_preserved
valid_ptrs_trace_intro
valid_ptr_timeout_nodes
VPBusy
VPEfail
VPErecv
VPEsend
VPEtimeout
VPGetBestPredecessor
VPGetPredAndSuccs
VPGetSuccList
VPGotBestPredecessor
VPGotPredAndSuccs
VPGotSuccList
VPNotify
VPPing
VPPong
VPQJoin
VPQJoin2
VPQRectify
VPQStabilize
VPQStabilize2
VPTick
VPTKeepaliveTick
VPTRequest
wf_ptr_dec
wf_ptr_hash_eq
when_apply_handler_result_preserves_live_node
when_Timeout_enabled
wrong_pred_not_correct_pred
z_of_id_inv