Dynamic Predicates: history/1 forward_history/1 current_state_id/1 current_options/1 packed_visited_expression/2 not_invariant_checked/1 not_interesting/1 max_reached_for_node/1 time_out_for_node/3 use_no_timeout/1 time_out_for_invariant/1 time_out_for_assertions/1 transition/4 transition_info/2 operation_not_yet_covered/1 state_error/3 saved_nested_context_state/2 hash_to_id/2 id_to_marker/2 hash_to_nauty_id/2 specialized_inv/2 op_trace_ids/1 state_space_version_in_file/1 not_all_z_saved/1 not_all_transitions_added_saved/1 bind_skeleton/2 stored_value/2 stored_value_hash_to_id/2 next_value_id/1 max_nr_of_new_nodes/1 equivalent/2 echange/0 counterexample_node/1 counterexample_op/1

1253 Lines

160 Predicates

Imported Modules: lists self_check error_manager gensym preferences tools module_information state_space_open_nodes_c state_packing hashing

129 Exports

34 specified Imports

Imports	Exports
Name: counter_init/0 Module: counter/counter Name: new_counter/1 Module: counter/counter Name: get_counter/2 Module: counter/counter Name: inc_counter/1 Module: counter/counter Name: inc_counter/2 Module: counter/counter Name: inc_counter_by/2 Module: counter/counter Name: reset_counter/1 Module: counter/counter Name: set_counter/2 Module: counter/counter Name: state_corresponds_to_initialised_b_machine/1 Module: specfile Name: state_corresponds_to_fully_setup_b_machine/1 Module: specfile Name: state_corresponds_to_set_up_constants/1 Module: specfile Name: between/3 Module: between Name: formatsilent/2 Module: debug Name: b_top_level_operation/1 Module: bmachine Name: debug_println/1 Module: debug Name: channel/2 Module: haskell_csp Name: print_error/1 Module: tools_printing Name: format_error_with_nl/2 Module: tools_printing Name: print_error_span/1 Module: error_manager Name: find_identifier_uses/3 Module: bsyntaxtree Name: ord_member/2 Module: ordsets Name: translate_error_term/3 Module: translate Name: register_event_listener/3 Module: eventhandling Name: translate_event_with_src_and_target_id/5 Module: translate Name: debug_mode/1 Module: debug Name: print_dynamic_fact/2 Module: tools_printing Name: print_dynamic_pred/4 Module: tools_printing Name: my_term_hash/2 Module: hashing Name: safe_on_exception/3 Module: tools_meta Name: compute_all_transitions_if_necessary/2 Module: tcltk_interface Name: b_or_z_mode/0 Module: specfile Name: csp_mode/0 Module: specfile Name: csp_with_bz_mode/0 Module: specfile Name: animation_mode/1 Module: specfile	Name: get_state_space_stats/3 Name: get_state_space_stats/4 Name: gen_new_state_id/1 Name: history/1 Name: forward_history/1 Name: get_action_trace/1 Name: get_action_trace_with_limit/2 Name: get_action_term_trace/1 Name: op_trace_ids/1 Name: add_to_op_trace_ids/1 Name: remove_from_op_trace_ids/1 Name: reset_op_trace_ids/0 Name: get_state_id_trace/1 Name: current_state_id/1 Name: current_expression/2 Name: set_current_state_id/1 Name: current_options/1 Name: set_current_options/1 Name: get_current_predecessor_state_id/1 Name: add_id_at_front/1 Name: add_id_at_end/1 Name: add_id_random/1 Name: add_id_with_weight/2 Name: add_id_to_process/3 Name: pop_id_from_front/1 Name: pop_id_from_end/1 Name: pop_id_oldest/1 Name: retract_open_node/1 Name: open_ids_empty/0 Name: top_front_id/1 Name: top_front_weight/1 Name: visited_expression/3 Name: visited_expression/2 Name: visited_expression_id/1 Name: find_hashed_packed_visited_expression/3 Name: retract_visited_expression/2 Name: not_all_transitions_added/1 Name: not_invariant_checked/1 Name: set_invariant_checked/1 Name: invariant_not_yet_checked/1 Name: invariant_still_to_be_checked/1 Name: not_interesting/1 Name: mark_as_not_interesting/1 Name: max_reached_for_node/1 Name: max_reached_or_timeout_for_node/1 Name: use_no_timeout/1 Name: time_out_for_node/1 Name: time_out_for_node/3 Name: hash_to_id/2 Name: id_to_marker/2 Name: hash_to_nauty_id/2 Name: invariant_violated/1 Name: time_out_for_invariant/1 Name: time_out_for_assertions/1 Name: set_invariant_violated/1 Name: state_error_exists/0 Name: state_error/3 Name: store_state_error/3 Name: set_context_state/1 Name: set_context_state/2 Name: update_context_state/1 Name: clear_context_state/0 Name: get_current_context_state/1 Name: store_error_for_context_state/2 Name: copy_current_errors_to_state/2 Name: store_abort_error_for_context_state_if_possible/4 Name: abort_error_exists_in_context_state/1 Name: transition/3 Name: transition/4 Name: any_transition/3 Name: store_transition/4 Name: deadlocked_state/1 Name: is_initial_state_id/1 Name: is_concrete_constants_state_id/1 Name: multiple_concrete_constants_exist/0 Name: get_constants_state_for_id/2 Name: get_constants_state_id_for_id/2 Name: try_get_unique_constants_state/1 Name: get_constants_id_for_state_id/2 Name: get_variables_state_for_id/2 Name: out_degree/2 Name: operation_not_yet_covered/1 Name: operation_name_not_yet_covered/1 Name: get_operation_name_coverage_infos/4 Name: mark_operation_as_covered/1 Name: initialise_operation_not_yet_covered/0 Name: transition_info/2 Name: store_transition_infos/2 Name: keep_transition_info/1 Name: compute_transitions_if_necessary/1 Name: state_space_initialise/0 Name: state_space_initialise_with_stats/0 Name: state_space_reset/0 Name: state_space_add/2 Name: state_space_packed_add/2 Name: delete_node/1 Name: current_state_corresponds_to_initialised_b_machine/0 Name: current_state_corresponds_to_fully_setup_b_machine/0 Name: current_state_corresponds_to_setup_constants_b_machine/0 Name: visited_state_corresponds_to_initialised_b_machine/1 Name: visited_state_corresponds_to_setup_constants_b_machine/1 Name: specialized_inv/2 Name: assert_max_reached_for_node/1 Name: assert_time_out_for_node/3 Name: assert_time_out_for_invariant/1 Name: assert_time_out_for_assertions/1 Name: set_max_nr_of_new_impl_trans_nodes/1 Name: get_max_nr_of_new_impl_trans_nodes/1 Name: impl_trans_term/3 Name: impl_trans_term_all/2 Name: impl_trans_id/4 Name: compute_transitions_if_necessary_saved/1 Name: max_nr_of_new_nodes_limit_not_reached/0 Name: find_trace_to_initial_state/2 Name: find_initialised_states/1 Name: tcltk_save_state_space/1 Name: tcltk_load_state/1 Name: compute_full_state_space_hash/1 Name: execute_id_trace_from_current/3 Name: set_trace_by_transition_ids/1 Name: try_set_trace_by_transition_ids/1 Name: extend_trace_by_transition_ids/1 Name: extract_term_trace_from_transition_ids/2 Name: add_counterexample_node/1 Name: add_counterexample_op/1 Name: reset_counterexample/0 Name: set_counterexample_by_transition_ids/1 Name: counterexample_node/1 Name: counterexample_op/1

Imports

Exports

Name: counter_init/0

Module: counter/counter

Name: new_counter/1

Module: counter/counter

Name: get_counter/2

Module: counter/counter

Name: inc_counter/1

Module: counter/counter

Name: inc_counter/2

Module: counter/counter

Name: inc_counter_by/2

Module: counter/counter

Name: reset_counter/1

Module: counter/counter

Name: set_counter/2

Module: counter/counter

Name: state_corresponds_to_initialised_b_machine/1

Module: specfile

Name: state_corresponds_to_fully_setup_b_machine/1

Module: specfile

Name: state_corresponds_to_set_up_constants/1

Module: specfile

Name: between/3

Module: between

Name: formatsilent/2

Module: debug

Name: b_top_level_operation/1

Module: bmachine

Name: debug_println/1

Module: debug

Name: channel/2

Module: haskell_csp

Name: print_error/1

Module: tools_printing

Name: format_error_with_nl/2

Module: tools_printing

Name: print_error_span/1

Module: error_manager

Name: find_identifier_uses/3

Module: bsyntaxtree

Name: ord_member/2

Module: ordsets

Name: translate_error_term/3

Module: translate

Name: register_event_listener/3

Module: eventhandling

Name: translate_event_with_src_and_target_id/5

Module: translate

Name: debug_mode/1

Module: debug

Name: print_dynamic_fact/2

Module: tools_printing

Name: print_dynamic_pred/4

Module: tools_printing

Name: my_term_hash/2

Module: hashing

Name: safe_on_exception/3

Module: tools_meta

Name: compute_all_transitions_if_necessary/2

Module: tcltk_interface

Name: b_or_z_mode/0

Module: specfile

Name: csp_mode/0

Module: specfile

Name: csp_with_bz_mode/0

Module: specfile

Name: animation_mode/1

Module: specfile

Name: get_state_space_stats/3

Name: get_state_space_stats/4

Name: gen_new_state_id/1

Name: history/1

Name: forward_history/1

Name: get_action_trace/1

Name: get_action_trace_with_limit/2

Name: get_action_term_trace/1

Name: op_trace_ids/1

Name: add_to_op_trace_ids/1

Name: remove_from_op_trace_ids/1

Name: reset_op_trace_ids/0

Name: get_state_id_trace/1

Name: current_state_id/1

Name: current_expression/2

Name: set_current_state_id/1

Name: current_options/1

Name: set_current_options/1

Name: get_current_predecessor_state_id/1

Name: add_id_at_front/1

Name: add_id_at_end/1

Name: add_id_random/1

Name: add_id_with_weight/2

Name: add_id_to_process/3

Name: pop_id_from_front/1

Name: pop_id_from_end/1

Name: pop_id_oldest/1

Name: retract_open_node/1

Name: open_ids_empty/0

Name: top_front_id/1

Name: top_front_weight/1

Name: visited_expression/3

Name: visited_expression/2

Name: visited_expression_id/1

Name: find_hashed_packed_visited_expression/3

Name: retract_visited_expression/2

Name: not_all_transitions_added/1

Name: not_invariant_checked/1

Name: set_invariant_checked/1

Name: invariant_not_yet_checked/1

Name: invariant_still_to_be_checked/1

Name: not_interesting/1

Name: mark_as_not_interesting/1

Name: max_reached_for_node/1

Name: max_reached_or_timeout_for_node/1

Name: use_no_timeout/1

Name: time_out_for_node/1

Name: time_out_for_node/3

Name: hash_to_id/2

Name: id_to_marker/2

Name: hash_to_nauty_id/2

Name: invariant_violated/1

Name: time_out_for_invariant/1

Name: time_out_for_assertions/1

Name: set_invariant_violated/1

Name: state_error_exists/0

Name: state_error/3

Name: store_state_error/3

Name: set_context_state/1

Name: set_context_state/2

Name: update_context_state/1

Name: clear_context_state/0

Name: get_current_context_state/1

Name: store_error_for_context_state/2

Name: copy_current_errors_to_state/2

Name: store_abort_error_for_context_state_if_possible/4

Name: abort_error_exists_in_context_state/1

Name: transition/3

Name: transition/4

Name: any_transition/3

Name: store_transition/4

Name: deadlocked_state/1

Name: is_initial_state_id/1

Name: is_concrete_constants_state_id/1

Name: multiple_concrete_constants_exist/0

Name: get_constants_state_for_id/2

Name: get_constants_state_id_for_id/2

Name: try_get_unique_constants_state/1

Name: get_constants_id_for_state_id/2

Name: get_variables_state_for_id/2

Name: out_degree/2

Name: operation_not_yet_covered/1

Name: operation_name_not_yet_covered/1

Name: get_operation_name_coverage_infos/4

Name: mark_operation_as_covered/1

Name: initialise_operation_not_yet_covered/0

Name: transition_info/2

Name: store_transition_infos/2

Name: keep_transition_info/1

Name: compute_transitions_if_necessary/1

Name: state_space_initialise/0

Name: state_space_initialise_with_stats/0

Name: state_space_reset/0

Name: state_space_add/2

Name: state_space_packed_add/2

Name: delete_node/1

Name: current_state_corresponds_to_initialised_b_machine/0

Name: current_state_corresponds_to_fully_setup_b_machine/0

Name: current_state_corresponds_to_setup_constants_b_machine/0

Name: visited_state_corresponds_to_initialised_b_machine/1

Name: visited_state_corresponds_to_setup_constants_b_machine/1

Name: specialized_inv/2

Name: assert_max_reached_for_node/1

Name: assert_time_out_for_node/3

Name: assert_time_out_for_invariant/1

Name: assert_time_out_for_assertions/1

Name: set_max_nr_of_new_impl_trans_nodes/1

Name: get_max_nr_of_new_impl_trans_nodes/1

Name: impl_trans_term/3

Name: impl_trans_term_all/2

Name: impl_trans_id/4

Name: compute_transitions_if_necessary_saved/1

Name: max_nr_of_new_nodes_limit_not_reached/0

Name: find_trace_to_initial_state/2

Name: find_initialised_states/1

Name: tcltk_save_state_space/1

Name: tcltk_load_state/1

Name: compute_full_state_space_hash/1

Name: execute_id_trace_from_current/3

Name: set_trace_by_transition_ids/1

Name: try_set_trace_by_transition_ids/1

Name: extend_trace_by_transition_ids/1

Name: extract_term_trace_from_transition_ids/2

Name: add_counterexample_node/1

Name: add_counterexample_op/1

Name: reset_counterexample/0

Name: set_counterexample_by_transition_ids/1

Name: counterexample_node/1

Name: counterexample_op/1

Predicates

Predicates:

abort_error_exists_in_context_state/1

abort_error_for_same_location_exists/5

add_counterexample_node/1

add_counterexample_op/1

add_to_op_trace_ids/1

any_transition/3

assert_echange/0

assert_max_reached_for_node/1

assert_time_out_for_assertions/1

assert_time_out_for_invariant/1

assert_time_out_for_node/3

bench_state_space/0

check_equi/2

check_state_space_version/0

clear_context_state/0

compress_span/2

compute_equivalence_classes/0

compute_full_state_space_hash/1

compute_op_string/6

compute_transitions_if_necessary/1

compute_transitions_if_necessary_saved/1

context_state/2

copy_current_errors_to_state/2

current_expression/2

current_options/1

current_packed_expression/2

current_state_corresponds_to_fully_setup_b_machine/0

current_state_corresponds_to_initialised_b_machine/0

current_state_corresponds_to_setup_constants_b_machine/0

current_state_id/1

deadlocked_state/1

decrease_max_nr_of_new_nodes/1

delete_node/1

execute_id_trace_from_current/3

extend_trace_by_transition_ids/1

extract_history_from_transition_ids/7

extract_term_trace_from_transition_ids/2

extract_trace_from_transition_ids/5

filter_state/3

find_aux/3

find_hashed_packed_visited_expression/3

find_init1/3

find_init2/4

find_initialised_states/1

find_trace_to_initial_state/2

gen_new_state_id/1

get_action_term_trace/1

get_action_trace/1

get_action_trace_with_limit/2

get_constants_id_for_id_aux/3

get_constants_id_for_state_id/2

get_constants_state_aux/2

get_constants_state_for_id/2

get_constants_state_id_for_id/2

get_current_context_state/1

get_current_predecessor_state_id/1

get_max_nr_of_new_impl_trans_nodes/1

get_operation_name_coverage_infos/4

get_state_id_trace/1

get_state_space_stats/3

get_state_space_stats/4

get_variables_state_for_id/2

get_vars_aux/2

has_functor_and_maybe_tau/2

history/1

impl_trans_id/4

impl_trans_term/3

impl_trans_term_all/2

inc_processed/0

init_equi/0

init_states_mode_cst_init/1

init_states_mode_one_step/1

initialise_operation_not_yet_covered/0

invariant_not_yet_checked/1

invariant_still_to_be_checked/1

invariant_violated/1

is_concrete_constants_state_id/1

is_initial_state_id/1

keep_transition_info/1

mark_as_not_interesting/1

mark_operation_as_covered/1

max_nr_of_new_nodes_limit_not_reached/0

max_reached_or_timeout_for_node/1

multiple_concrete_constants_exist/0

next_states_from_root/1

operation_name_not_yet_covered/1

portray_state_space/0

print_equi/0

print_error_term/2

print_state_space/1

project_on_action_term/2

prune_forward_history/3

recompute_all_hash/0

remove_from_op_trace_ids/1

reset_counterexample/0

reset_next_state_error_id_counter/0

reset_not_interesting/0

reset_op_trace_ids/0

reset_processed_nodes_counter/0

reset_state_counter/0

reset_state_counter/1

reset_trace/0

reset_transition_store/0

retract_hash/1

retract_open_node/1

retract_open_node_and_update_processed_nodes/1

retract_visited_expression/2

retractall_invariant_violated/1

retractall_visited_expression/1

reverse_and_project_on_action_term/3

same_span_location/2

save_nested_context_state/1

saved_gennum_count/1

set_context_number_of_errors/1

set_context_state/1

set_context_state/2

set_counterexample_by_transition_ids/1

set_current_options/1

set_current_state_id/1

set_invariant_checked/1

set_invariant_violated/1

set_max_nr_of_new_impl_trans_nodes/1

set_trace_by_transition_ids/1

split_equivalence_classes/0

state_error_exists/0

state_space_add/2

state_space_clean_all/0

state_space_initialise/0

state_space_initialise_with_stats/0

state_space_packed_add/2

state_space_reset/0

state_space_startup/0

state_space_version/1

store_abort_error_for_context_state_if_possible/4

store_error_for_context_state/2

store_state_error/3

store_transition/4

store_transition_info/2

store_transition_infos/2

tcltk_load_state/1

tcltk_save_state_space/1

time_out_for_node/1

trace/1

transfer_open_node_info/0

transfer_state_packing_info/0

transition/3

try_get_unique_constants_state/1

try_set_trace_by_transition_ids/1

update_context_state/1

update_forward_history/1

user_consult_without_redefine_warning/1

visited_expression/2

visited_expression/3

visited_expression_id/1

visited_state_corresponds_to_initialised_b_machine/1

visited_state_corresponds_to_setup_constants_b_machine/1

abort_error_exists_in_context_state/1

abort_error_for_same_location_exists/5

add_counterexample_node/1

add_counterexample_op/1

add_to_op_trace_ids/1

any_transition/3

assert_echange/0

assert_max_reached_for_node/1

assert_time_out_for_assertions/1

assert_time_out_for_invariant/1

assert_time_out_for_node/3

bench_state_space/0

check_equi/2

check_state_space_version/0

clear_context_state/0

compress_span/2

compute_equivalence_classes/0

compute_full_state_space_hash/1

compute_op_string/6

compute_transitions_if_necessary/1

compute_transitions_if_necessary_saved/1

context_state/2

copy_current_errors_to_state/2

current_expression/2

current_options/1

Dynamic: true

current_packed_expression/2

current_state_corresponds_to_fully_setup_b_machine/0

current_state_corresponds_to_initialised_b_machine/0

current_state_corresponds_to_setup_constants_b_machine/0

current_state_id/1

Dynamic: true

deadlocked_state/1

decrease_max_nr_of_new_nodes/1

delete_node/1

execute_id_trace_from_current/3

extend_trace_by_transition_ids/1

extract_history_from_transition_ids/7

extract_term_trace_from_transition_ids/2

extract_trace_from_transition_ids/5

filter_state/3

find_aux/3

find_hashed_packed_visited_expression/3

find_init1/3

find_init2/4

find_initialised_states/1

find_trace_to_initial_state/2

gen_new_state_id/1

get_action_term_trace/1

get_action_trace/1

get_action_trace_with_limit/2

get_constants_id_for_id_aux/3

get_constants_id_for_state_id/2

get_constants_state_aux/2

get_constants_state_for_id/2

get_constants_state_id_for_id/2

get_current_context_state/1

get_current_predecessor_state_id/1

get_max_nr_of_new_impl_trans_nodes/1

get_operation_name_coverage_infos/4

get_state_id_trace/1

get_state_space_stats/3

Description:
comment in to use only Prolog datastructures
comment in to use C++ multimap queue; can make use of HEURISTIC_FUNCTION

get_state_space_stats/4

get_variables_state_for_id/2

get_vars_aux/2

has_functor_and_maybe_tau/2

history/1

Dynamic: true

impl_trans_id/4

impl_trans_term/3

impl_trans_term_all/2

inc_processed/0

init_equi/0

init_states_mode_cst_init/1

init_states_mode_one_step/1

initialise_operation_not_yet_covered/0

invariant_not_yet_checked/1

invariant_still_to_be_checked/1

invariant_violated/1

is_concrete_constants_state_id/1

is_initial_state_id/1

keep_transition_info/1

mark_as_not_interesting/1

mark_operation_as_covered/1

max_nr_of_new_nodes_limit_not_reached/0

max_reached_or_timeout_for_node/1

multiple_concrete_constants_exist/0

next_states_from_root/1

operation_name_not_yet_covered/1

portray_state_space/0

print_equi/0

print_error_term/2

print_state_space/1

project_on_action_term/2

prune_forward_history/3

recompute_all_hash/0

remove_from_op_trace_ids/1

reset_counterexample/0

reset_next_state_error_id_counter/0

reset_not_interesting/0

reset_op_trace_ids/0

reset_processed_nodes_counter/0

reset_state_counter/0

reset_state_counter/1

reset_trace/0

reset_transition_store/0

retract_hash/1

retract_open_node/1

retract_open_node_and_update_processed_nodes/1

retract_visited_expression/2

retractall_invariant_violated/1

retractall_visited_expression/1

reverse_and_project_on_action_term/3

same_span_location/2

save_nested_context_state/1

saved_gennum_count/1

set_context_number_of_errors/1

set_context_state/1

set_context_state/2

set_counterexample_by_transition_ids/1

set_current_options/1

set_current_state_id/1

set_invariant_checked/1

set_invariant_violated/1

set_max_nr_of_new_impl_trans_nodes/1

set_trace_by_transition_ids/1

split_equivalence_classes/0

state_error_exists/0

state_space_add/2

state_space_clean_all/0

state_space_initialise/0

state_space_initialise_with_stats/0

state_space_packed_add/2

state_space_reset/0

state_space_startup/0

state_space_version/1

store_abort_error_for_context_state_if_possible/4

store_abort_error_for_context_state_if_possible(ErrType,Msg,Term,Span) :-
    %print(store(Msg,Term,Span)),nl,
    ( get_current_context_state(State) ->
    error_manager:get_error_context(Context),
    (abort_error_for_same_location_exists(State,Id1,ErrType,Msg,Span),
    abort_error_for_same_location_exists(State,Id2,ErrType,Msg,Span),
    Id2>Id1
    -> /* two errors of same type, for same state and same source location exists */
    /* TO DO: maybe merge state errors */
    simplify_span(Span,Span1),
    compress_span(Span1,Span2),
    store_state_error(State,abort_error(ErrType,'Further identical errors occurred (not stored !)',Term,span_context(Span2,Context)),_)
    ;
    format_error_with_nl('! An error occurred in state ~w: ~w !',[State,ErrType]),
    % usual errors: precondition_error, while_invariant_violation, while_variant_error,
    % assert_error, well_definedness_error, card_overflow_error
    print_error(Msg),
    print_error_term(Term,Span),
    % print_error(context_state_id(State)), % printed by print_error_context
    print_error_context,
    (debug_mode(on),visited_expression(State,S) -> translate:translate_bstate(S,O),print_error(O) ; true),
    compress_span(Span,Span2),
    print_error_span(Span2),
    store_state_error(State,abort_error(ErrType,Msg,Term,span_context(Span2,Context)),_)
    ),
    (add_new_event_in_error_scope(abort_error(ErrType)) -> true ; true), % should we use well_definedness_error?
    assert_real_error_occurred(abort_error) % Note that in this case the error manager list of errors maybe empty even though real_error_occured is true. (see ProB2 kernel test de.prob.cli.integration.rules.RulesMachineTest > testReuseStateSpace)
    ; % no current context_state exists:
    compress_span(Span,Span2),
    add_error(ErrType,Msg,Term,Span2)
).

store_error_for_context_state/2

store_state_error/3

store_transition/4

store_transition_info/2

store_transition_infos/2

tcltk_load_state/1

tcltk_save_state_space/1

time_out_for_node/1

trace/1

transfer_open_node_info/0

transfer_state_packing_info/0

transition/3

try_get_unique_constants_state/1

try_set_trace_by_transition_ids/1

update_context_state/1

update_forward_history/1

user_consult_without_redefine_warning/1

visited_expression/2

visited_expression/3

visited_expression_id/1

visited_state_corresponds_to_initialised_b_machine/1

visited_state_corresponds_to_setup_constants_b_machine/1

Determinacy Checker

Determinacy Checker:

! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(plspec_patch_libraries,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_terminal_colors,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_enter_debugger_upon_error,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_use_timer,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_avl_custom,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_core_only,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_src_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_core_only,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_myheap,false)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(disable_chr,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_70459,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pathes_lib.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_39617,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/error_manager.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_32663,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(debug) does not exist
! goal: absolute_file_name(probsrc(debug),_30999,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/state_space.pl')])

Name: state_error/3	dynamic predicate
Name: =/2
Name: get_current_context_state/1	Module: state_space

Name: same_span_location/2	Module: state_space
Name: state_error/3	dynamic predicate

Name: translate_ctrace2/5	Module: ltl
Name: translate_trace/4	Module: ltl

Name: assertz/1
Name: true
Name: counterexample_op/1	dynamic predicate
Name: ->/3

Name: translate_trace/4	Module: ltl
Name: translate_ctrace2/5	Module: ltl

Name: flush_output
Name: print/1
Name: assertz/1
Name: true
Name: echange	dynamic predicate
Name: ->/3

Name: compute_ample_set2/3	Module: ample_sets
Name: compute_transitions_pge2/2	Module: pge_algo

Name: format/2
Name: is/2
Name: statistics/2
Name: true
Name: fail
Name: my_term_hash/2	Module: hashing
Name: visited_expression/2	Module: state_space
Name: transition/4	dynamic predicate
Name: packed_visited_expression/2	dynamic predicate

Name: equivalent/2	dynamic predicate
Name: @</2
Name: ->/3
Name: true
Name: =/2

Name: true
Name: add_message/3	Module: foo_error
Name: >/2
Name: ->/3
Name: =/2
Name: state_space_version_in_file/1	dynamic predicate
Name: state_space_version/1	Module: state_space

Name: true
Name: bb_delete/2
Name: ->/3
Name: bb_put/2
Name: !
Name: saved_nested_context_state/2	dynamic predicate
Name: retract/1

Name: compute_state_space_transitions_if_necessary2/2	Module: safety_mc
Name: state_space_initialise_with_stats/0	Module: state_space
Name: state_space_initialise/0	Module: state_space
Name: impl_trans_term_all1/2	Module: ltl
Name: state_space_clean_all/0	Module: state_space
Name: explore_one_state/8	Module: state_space_explorer

Name: =/2
Name: !
Name: filter_state/3	Module: state_space
Name: sort/2
Name: find_identifier_uses/3	Module: bsyntaxtree
Name: RECURSIVE_CALL/2	Module: state_space

Name: print_equi/0	Module: state_space
Name: nl
Name: split_equivalence_classes/0	Module: state_space
Name: init_equi/0	Module: state_space

Name: compute_all_transitions_if_necessary/2	Module: tcltk_interface
Name: decrease_max_nr_of_new_nodes/1	Module: state_space
Name: !
Name: not_all_transitions_added/1	Module: foo_error

Name: compute_h2/3	Module: tcltk_interface
Name: get_set_up_constants_solution/1	Module: tcltk_interface
Name: find_local_path_to_global_event/6	Module: sap

Name: logxml_write_ids/2	Module: prob_cli
Name: check_abstract_constants/0	Module: prob_cli
Name: get_current_state/3	Module: predicate_debugger
Name: write_values_to_file/1	Module: b_show_history
Name: cli_execute2/3	Module: prob_cli
Name: tcltk_get_image_list/6	Module: graphical_state_viewer_images
Name: perform_single_operation/2	Module: b_trace_checking
Name: zmq_start_master/2	Module: prob_cli
Name: exec_eval_command/2	Module: prob_cli
Name: perform_one_operation_in_sequence/2	Module: b_trace_checking
Name: current_b_expression/1	Module: specfile
Name: get_state_for_graph/1	Module: state_custom_dot_graph
Name: print_cstate_graph/1	Module: state_as_dot_graph

Name: perform_single_operation/2	Module: b_trace_checking
Name: find_successor_state/4	Module: b_trace_checking
Name: perform_one_operation_in_sequence/2	Module: b_trace_checking

Name: state_corresponds_to_fully_setup_b_machine/1	Module: specfile
Name: unpack_state_top_level/2	Module: foo_error
Name: current_packed_expression/2	Module: state_space

Name: command_unavailable/2	Module: meta_interface
Name: tcltk_analyse_assertions/3	Module: predicate_evaluator
Name: tcltk_analyse_deadlock/2	Module: predicate_evaluator
Name: tcltk_analyse_invariant/2	Module: predicate_evaluator

Name: cli_check_properties/1	Module: prob_cli
Name: zmq_start_master/2	Module: prob_cli
Name: current_b_state_with_all_constants_valued/0	Module: predicate_evaluator
Name: command_unavailable/2	Module: meta_interface
Name: det_check_constants/0	Module: prob_cli
Name: visb_current_state_can_be_visualised/0	Module: visb_visualiser

Name: solve_using_smt_solver_aux/5	Module: eval_strings
Name: solver_clash_feedback/3	Module: eval_strings
Name: perform_one_operation_in_sequence/2	Module: b_trace_checking
Name: tcltk_can_react_to_item_right_click/2	Module: graphical_state_viewer_images
Name: select_ctl_mode/4	Module: ctl
Name: get_current_state_full_store/2	Module: eval_strings
Name: execute_id_trace_from_current/3	Module: state_space
Name: perform_action_tclk/4	Module: b_trace_checking
Name: cli_execute_add_virtual_transition/4	Module: prob_cli
Name: perform_single_operation/2	Module: b_trace_checking
Name: perform_random_initialisation/1	Module: prob_cli
Name: tcltk_get_visb_items/1	Module: visb_visualiser
Name: can_react_to_item_drag/6	Module: graphical_state_viewer_images
Name: set_current_state_id/1	Module: state_space
Name: tcltk_get_visb_events/1	Module: visb_visualiser
Name: extend_trace_by_transition_ids/1	Module: state_space
Name: perform_custom_operation_retry/2	Module: b_trace_checking
Name: tcltk_check_state_sequence_from_file/1	Module: b_trace_checking
Name: get_current_state_id/1	Module: external_functions
Name: exec_eval_command/2	Module: prob_cli
Name: model_check_aux/5	Module: prob_cli
Name: perform_random_step/4	Module: prob_cli
Name: get_current_history/2	Module: external_functions
Name: get_current_state_for_b_formula/2	Module: specfile
Name: get_state_id_trace/1	Module: state_space
Name: preprocess_ap/2	Module: ltl_tools
Name: set_current_state/1	Module: prob2_interface
Name: perform_sequence_of_operations2/2	Module: b_trace_checking
Name: current_packed_expression/2	Module: state_space
Name: replay_state_trace_from_file/3	Module: prob2_interface
Name: tcltk_react_to_item_right_click/2	Module: graphical_state_viewer_images
Name: mutate_invariant/2	Module: mutate_expressions
Name: get_current_b_expression/1	Module: predicate_evaluator
Name: visb_current_state_can_be_visualised/0	Module: visb_visualiser
Name: print_dfa_from_nfa_states_id/0	Module: reduce_graph_state_space
Name: execute_rest_action/2	Module: graphical_state_viewer_images
Name: do_det_checking/0	Module: prob_cli
Name: perform_random_initialisation_if_necessary/1	Module: prob_cli
Name: select_ltl_mode/4	Module: ltl
Name: current_expression/2	Module: state_space
Name: det_check_constants/0	Module: prob_cli
Name: build_modelcheck_return2/2	Module: prob2_interface
Name: print_current_state/0	Module: prob_cli
Name: build_modelcheck_return/2	Module: prob2_interface
Name: tcltk_perform_visb_click_event/1	Module: visb_visualiser
Name: generate_visb_html_for_current_state/2	Module: visb_visualiser
Name: tcltk_analyse_constants/1	Module: coverage_statistics

Name: fail
Name: assertz/1
Name: add_warning/3	Module: foo_error
Name: is/2
Name: =/2
Name: ->/3
Name: >/2
Name: !
Name: max_nr_of_new_nodes/1	dynamic predicate
Name: retract/1

Name: retractall/1
Name: retract_hash/1	Module: state_space
Name: true
Name: inc_counter_by/2	Module: counter/counter
Name: not_interesting/1	dynamic predicate
Name: retract/1
Name: ->/3
Name: retract_open_node_and_update_processed_nodes/1	Module: state_space
Name: retractall_invariant_violated/1	Module: state_space
Name: retractall_visited_expression/1	Module: state_space
Name: nl
Name: print/1

Name: assertz/1
Name: retractall/1
Name: append/3
Name: reverse/2	Module: foo_error
Name: op_trace_ids/1	dynamic predicate
Name: retract/1
Name: update_forward_history/1	Module: state_space
Name: history/1	Module: state_space
Name: nl
Name: print/1
Name: true
Name: ==/2
Name: ->/3
Name: =/2
Name: current_state_id/1	Module: state_space

prob_prolog/src/state_space.pl

Modules

Predicates of state_space

Module Information

1253 Lines

160 Predicates

Imported Modules: lists self_check error_manager gensym preferences tools module_information state_space_open_nodes_c state_packing hashing

129 Exports

34 specified Imports

Predicates:

Name: convert_result/3	Module: ltl
Name: tcltk_play_ltl_counterexample/2	Module: ltl
Name: executetrace/1	Module: ltl

Name: assertz/1
Name: retractall/1
Name: extract_history_from_transition_ids/7	Module: state_space
Name: op_trace_ids/1	dynamic predicate
Name: history/1	Module: state_space
Name: current_state_id/1	Module: state_space

Name: fail
Name: add_error/3	Module: foo_error
Name: RECURSIVE_CALL/7	Module: state_space
Name: !
Name: transition/4	dynamic predicate

Name: reverse_and_project_on_action_term/3	Module: state_space
Name: extract_trace_from_transition_ids/5	Module: state_space

Name: RECURSIVE_CALL/3	Module: state_space
Name: =/2
Name: ord_member/2	Module: ordsets
Name: ->/3

Name: find_init1/3	Module: state_space
Name: init_states_mode_cst_init/1	Module: state_space
Name: init_states_mode_one_step/1	Module: state_space

Name: find_init2/4	Module: state_space
Name: impl_trans_term/3	Module: state_space
Name: =/2
Name: !
Name: ==/2

Name: find_aux/3	Module: state_space
Name: find_init2/4	Module: state_space

Name: find_init1/3	Module: state_space
Name: has_functor_and_maybe_tau/2	Module: state_space

Name: fail
Name: next_states_from_root/1	Module: state_space
Name: init_states_mode_one_step/1	Module: state_space
Name: ->/3
Name: findall/3
Name: init_states_mode_cst_init/1	Module: state_space
Name: animation_mode/1	Module: specfile