Dynamic Predicates: prev_randomise_enumeration_order/1 current_candidate_options/1 cached_state_as_strings/2 last_detailed_error/3 saved_forward_history/2 cbc_inv_error_found/2 nr_cbc_sols/1 resetable_node/1 find_flag/2 non_det_constant/1 eval_elapsed_time/1 nr_csp_process_state/1

3423 Lines

381 Predicates

Imported Modules: random lists ordsets avl module_information typechecker self_check preferences debug error_manager kernel_waitflags tools specfile state_space_exploration_modes translate b_state_model_check bmachine b_interpreter b_trace_checking bsyntaxtree kernel_objects state_space model_checker succeed_max b_read_write_info b_show_history xtl_interface alloy2b/alloy2b model_checker bsyntaxtree state_space_dijkstra bmachine specfile tools lists store self_check b_global_sets translate predicate_evaluator eval_strings

199 Exports

94 specified Imports

Imports	Exports
Name: set_error_handler/1 Module: plspec/plspec/plspec_core Name: pretty_print_error/1 Module: plspec/plspec/prettyprinter Name: parse_single_csp_declaration/3 Module: haskell_csp Name: save_constants/1 Module: value_persistance Name: add_new_transitions_to_cache/1 Module: value_persistance Name: start_ltsmin/4 Module: ltsmin/ltsmin Name: format_with_colour_nl/4 Module: tools_printing Name: csv_to_trace/3 Module: ltsmin/ltsmin_trace Name: visited_expression/2 Module: state_space Name: set_depth_breadth_first_mode/1 Module: state_space_exploration_modes Name: dbf_modes/3 Module: state_space_exploration_modes Name: announce_event/1 Module: eventhandling Name: start_animation/0 Module: prob2_interface Name: update_preferences_from_spec/0 Module: prob2_interface Name: time_out_with_factor_call/4 Module: tools_timeout Name: time_out_call/2 Module: tools_timeout Name: translate_event_with_src_and_target_id/4 Module: translate Name: edit_file/2 Module: tools_commands Name: b_absolute_file_name_relative_to_opened_file/2 Module: specfile Name: tcltk_save_history_as_trace_file/2 Module: b_trace_checking Name: get_bexpression_column_template/4 Module: translate Name: extend_state_with_probids_and_lets/2 Module: eval_let_store Name: compute_heuristic_function_for_state_id/2 Module: state_space_exploration_modes Name: out_degree/2 Module: state_space Name: compute_transitions_if_necessary/1 Module: state_space Name: get_operation_description_for_transition/3 Module: specfile Name: b_load_machine_from_file/1 Module: bmachine Name: b_load_machine_probfile/1 Module: bmachine Name: get_filename_extension/2 Module: tools Name: open_xtl_file/1 Module: xtl_interface Name: type_check_csp_and_b/0 Module: specfile Name: file_exists/1 Module: file_systems Name: delete_file/1 Module: file_systems Name: call_fuzz_parser/2 Module: parsercall Name: load_eventb_file/1 Module: eclipse_interface Name: call_alloy2pl_parser/2 Module: parsercall Name: catch_clpfd_overflow_call2/2 Module: clpfd_interface Name: reset_max_reached/0 Module: succeed_max Name: max_reached/0 Module: succeed_max Name: max_reached/1 Module: succeed_max Name: get_virtual_time_out_from_exception/2 Module: error_manager Name: time_out/3 Module: timeout Name: profile_failure_driven_loop/2 Module: runtime_profiler Name: get_possible_top_level_event_matches_msg/2 Module: tools_matching Name: catch_clpfd_overflow_call1/1 Module: clpfd_interface Name: call_in_fresh_error_scope_for_one_solution/1 Module: error_manager Name: get_texpr_ids/2 Module: bsyntaxtree Name: extract_all_line_col/5 Module: error_manager Name: extract_span_from_event/4 Module: haskell_csp Name: extract_span_info/2 Module: haskell_csp Name: execute_model/5 Module: prob2_interface Name: count_occurences/2 Module: tools_lists Name: get_current_state_for_b_formula/2 Module: specfile Name: extend_typing_scope_for_stored_lets/2 Module: eval_let_store Name: b_parse_machine_expression_from_codes_with_prob_ids/2 Module: bmachine Name: type_with_errors/4 Module: bmachine Name: replace_ids_by_exprs/4 Module: bsyntaxtree Name: b_get_machine_operation_for_animation/7 Module: bmachine Name: unify_types_strict/2 Module: btypechecker Name: b_is_variable/2 Module: bmachine Name: b_is_constant/2 Module: bmachine Name: inline_prob_deferred_set_elements_into_bexpr/2 Module: b_global_sets Name: extend_state_with_probids_and_lets/2 Module: eval_let_store Name: init_wait_flags_with_call_stack/2 Module: kernel_waitflags Name: ground_wait_flags/1 Module: kernel_waitflags Name: b_is_unused_constant/1 Module: bmachine Name: format_to_codes/3 Module: codesio Name: safe_mul/3 Module: kernel_card_arithmetic Name: pretty_type/2 Module: translate Name: get_quantified_operation_enabling_condition/4 Module: b_operation_guards Name: b_get_properties_from_machine/1 Module: bmachine Name: b_get_machine_constants/1 Module: bmachine Name: b_machine_has_constants_or_properties/0 Module: bmachine Name: create_or_merge_exists/3 Module: bsyntaxtree Name: conjunct_predicates/2 Module: bsyntaxtree Name: b_parse_machine_formula/3 Module: bmachine Name: type_with_errors/4 Module: bmachine Name: get_primed_machine_variables/1 Module: bmachine Name: get_current_predecessor_state_id/1 Module: state_space Name: extract_variables_from_state_as_primed/2 Module: specfile Name: create_typed_id/3 Module: bsyntaxtree Name: maplist/4 Module: lists Name: maplist5/5 Module: tools Name: interruptable_call/1 Module: user_interrupts Name: registered_freetype/2 Module: kernel_freetypes Name: is_set_type/2 Module: bsyntaxtree Name: to_b_string/2 Module: kernel_strings Name: fuzzy_match_codes_lower_case/2 Module: tools_matching Name: animatable_process_without_arguments/1 Module: haskell_csp Name: animatable_process_cli/1 Module: haskell_csp Name: get_csp_assertions/1 Module: haskell_csp Name: translate_csp_assertion/2 Module: haskell_csp Name: translate_bexpression_with_limit/3 Module: translate Name: get_tk_table_position_info/2 Module: error_manager	Name: tcltk_goto_state/2 Name: tcltk_add_new_transition_transid/6 Name: tcltk_add_new_transition/5 Name: tcltk_get_options/1 Name: tcltk_get_options_dest_info/1 Name: tcltk_get_state/1 Name: tcltk_get_state/2 Name: tcltk_get_options_or_candidates/1 Name: tcltk_get_options_candidate_nr_name/2 Name: tcltk_get_options_nr_description/2 Name: tcltk_get_state_errors/1 Name: tcltk_get_detailed_state_error/6 Name: tcltk_open_state_error_in_editor/1 Name: tcltk_get_line_col/5 Name: tcltk_current_state_invariant_violated/0 Name: tcltk_get_status/3 Name: tcltk_get_ops_with_virtual_timeout/1 Name: tcltk_get_ops_with_real_timeout/1 Name: tcltk_get_ops_user_interrupt_occurred/0 Name: tcltk_compute_options/2 Name: can_generate_dot_from_last_state_error/0 Name: tcltk_initialise/0 Name: tcltk_reset/0 Name: tcltk_perform_nr/1 Name: tcltk_random_perform/0 Name: tcltk_random_perform/1 Name: tcltk_perform_nr_option/3 Name: tcltk_perform_action_term/2 Name: tcltk_is_sync_event/1 Name: tcltk_exists_an_open_node/0 Name: tcltk_goto_an_open_node/0 Name: tcltk_goto_max_reached_node/0 Name: tcltk_goto_timeout_node/0 Name: tcltk_state_exists_with_invariant_violated/0 Name: tcltk_goto_an_invariant_violation/0 Name: tcltk_goto_node_with_id/1 Name: tcltk_try_goto_node_with_id/1 Name: tcltk_current_node_has_no_real_transition/0 Name: tcltk_current_node_has_real_transition/0 Name: tcltk_current_node_has_partial_transition/0 Name: tcltk_goto_a_non_deterministic_node/1 Name: tcltk_goto_a_non_deterministic_output_node/1 Name: tcltk_goto_a_branching_node/0 Name: tcltk_goto_a_non_resetable_node/0 Name: tcltk_state_space_only_has_root_node/0 Name: tcltk_no_constants_or_no_inititalisation_found/0 Name: tcltk_goto_event_list_property_violation/3 Name: tcltk_goto_state_enabling_operation/2 Name: tcltk_find_max_reached_node/0 Name: tcltk_find_max_reached_node/1 Name: tcltk_search_among_existing_nodes/6 Name: find_invariant_violation_among_not_checked_nodes/1 Name: tcltk_model_check/12 Name: do_model_check/13 Name: tcltk_set_dbf_mode/1 Name: tcltk_dbf_modes/1 Name: tcltk_mark_current_node_to_be_recomputed_wo_timeout/0 Name: tcltk_mark_current_node_to_be_recomputed_with_random_enum/0 Name: tcltk_finish_current_node_to_be_recomputed_with_random_enum/0 Name: tcltk_hash_model_checking_imprecise/0 Name: tcltk_clear_state_space_and_refocus_to_current_state/0 Name: tcltk_constraint_based_check/1 Name: tcltk_constraint_based_check_op/2 Name: tcltk_constraint_based_check_op/3 Name: tcltk_constraint_based_check/2 Name: tcltk_constraint_based_check_with_timeout/2 Name: tcltk_cbc_find_trace/2 Name: tcltk_cbc_find_trace/4 Name: tcltk_cbc_refinement_check/2 Name: tcltk_constraint_find_valid_state/0 Name: tcltk_constraint_find_maximal_valid_state/0 Name: tcltk_constraint_find_dynamic_assertion_violation/0 Name: tcltk_constraint_find_valid_state_with_pred/3 Name: tcltk_constraint_find_deadlock_state/1 Name: tcltk_constraint_find_deadlock_state_with_goal/2 Name: tcltk_constraint_find_deadlock_state_with_goal/3 Name: tcltk_constraint_find_static_assertion_violation/1 Name: tcltk_check_if_feasible_operation/4 Name: cbc_constraint_find_static_assertion_violation/2 Name: tcltk_can_backtrack/0 Name: tcltk_can_backtrack/1 Name: tcltk_can_forward/0 Name: tcltk_can_forward/1 Name: tcltk_prepare_for_reload/0 Name: tcltk_backtrack/0 Name: tcltk_backtrack/1 Name: tcltk_fast_forward/0 Name: tcltk_forward/0 Name: tcltk_execute_trace_to_current_node/0 Name: tcltk_find_shortest_trace_to_current_node/1 Name: tcltk_execute_longest_trace_from/1 Name: tcltk_get_history/1 Name: tcltk_perform_action_string/3 Name: tcltk_perform_action/2 Name: tcltk_perform_action/4 Name: tcltk_open_xtl_file/1 Name: tcltk_open_z_file/1 Name: tcltk_open_z_tex_file/1 Name: tcltk_open_alloy_file/1 Name: tcltk_open_alloy_prolog_ast_file/1 Name: tcltk_open_cspm_file/1 Name: tcltk_add_csp_file/1 Name: tcltk_load_packaged_eventb_file/1 Name: tcltk_verify_alloy_cmd/4 Name: tcltk_get_alloy_cmd_names/1 Name: tcltk_load_alloy_cmd_in_current_translation/1 Name: tcltk_machine_has_assertions/0 Name: tcltk_unique_top_level_operation/1 Name: tcltk_top_level_operations/1 Name: compute_all_transitions_if_necessary/0 Name: compute_all_transitions_if_necessary/2 Name: compute_state_information_if_necessary/0 Name: compute_invariant_if_necessary/3 Name: check_invariantKO/2 Name: check_invariantKO/3 Name: catch_clpfd_overflow_call_for_state/4 Name: compute_ample_set/3 Name: compute_all_transitions/2 Name: add_transition/4 Name: add_trans_id/5 Name: tcltk_has_eventtrace/1 Name: tcltk_show_eventtrace/2 Name: tcltk_execute_model/3 Name: tcltk_execute_trace_to_node/1 Name: find_shortest_trace_to_node/4 Name: tcltk_explore_csp_process/2 Name: tcltk_visualize_csp_process/2 Name: get_csp_process_id/2 Name: get_csp_process_stats/1 Name: tcltk_add_user_executed_operation/2 Name: tcltk_add_user_executed_operation/3 Name: tcltk_add_user_executed_operation_typed/4 Name: tcltk_add_user_executed_operation_typed/6 Name: tcltk_add_user_executed_statement/3 Name: tcltk_add_user_modify_variable_transition/2 Name: tcltk_add_user_modify_variable_transition/4 Name: tcltk_analyse_option/2 Name: tcltk_analyse/6 Name: tcltk_show_typing_of_variables_and_constants/1 Name: tcltk_show_current_state/1 Name: tcltk_eval/4 Name: interruptable_tcltk_eval/4 Name: tcltk_eval_as_table/2 Name: tcltk_find_value_as_table/3 Name: find_value_in_cur_state/4 Name: tcltk_time_call/1 Name: eval_elapsed_time/1 Name: tcltk_check_csp_assertions/2 Name: tcltk_check_csp_assertion/4 Name: tcltk_check_csp_assertion/5 Name: checkAssertion/5 Name: tcltk_get_vacuous_guards/1 Name: tcltk_get_vacuous_invariants/1 Name: tcltk_get_vacuous_invariants_table/1 Name: tcltk_operations_covered_info/3 Name: operation_name_covered/1 Name: tcltk_show_expression_as_dot/2 Name: generate_dot_from_formula/2 Name: generate_dot_from_invariant/1 Name: generate_dot_from_properties/1 Name: generate_dot_from_assertions/1 Name: generate_dot_from_deadlock_po/1 Name: generate_dot_from_goal/1 Name: generate_dot_from_last_span_predicate/1 Name: generate_dot_from_operation/2 Name: generate_dot_from_operation_with_params/4 Name: write_dot_file_for_pred_expr/2 Name: write_dot_file_for_value_as_tree/2 Name: evaluate_expression_over_history_to_csv_file/2 Name: tcltk_evaluate_expression_over_history/2 Name: translate_error_for_tclk/2 Name: tcltk_set_initial_machine/0 Name: tcltk_clear_machine/0 Name: tcltk_open_b_file/1 Name: tcltk_open_b_file_for_minor_mode/2 Name: tcltk_run_ltsmin/5 Name: tcltk_save_history_as_trace_file/1 Name: tcltk_execute_until/1 Name: tcltk_bv_get_tops/1 Name: tcltk_bv_get_structure/3 Name: tcltk_bv_is_leaf/2 Name: tcltk_bv_get_values/3 Name: tcltk_bv_get_value/3 Name: tcltk_bv_show_formula_as_dot_tree/2 Name: tcltk_bv_show_formula_as_dot_graph/2 Name: tcltk_bv_show_value_as_dot_tree/2 Name: tcltk_bv_get_pp_formula_string/2 Name: tcltk_show_identifier_value_as_dot_tree/2 Name: tcltk_bv_get_unlimited_value/3 Name: tcltk_bv_get_unlimited_value_atom/2 Name: tcltk_get_constants_predicate/2 Name: get_cbc_data_base_id_checks/1 Name: get_cbc_data_base_text_checks/1 Name: tcltk_write_uml_sequence_chart/1 Name: get_ltl_formulas_from_file/2 Name: tcltk_mcts_auto_play/0 Name: tcltk_mcts_auto_play/1 Name: mcts_auto_play_available/0 Name: tcltk_simplify_predicate/2

Imports

Exports

Name: set_error_handler/1

Module: plspec/plspec/plspec_core

Name: pretty_print_error/1

Module: plspec/plspec/prettyprinter

Name: parse_single_csp_declaration/3

Module: haskell_csp

Name: save_constants/1

Module: value_persistance

Name: add_new_transitions_to_cache/1

Module: value_persistance

Name: start_ltsmin/4

Module: ltsmin/ltsmin

Name: format_with_colour_nl/4

Module: tools_printing

Name: csv_to_trace/3

Module: ltsmin/ltsmin_trace

Name: visited_expression/2

Module: state_space

Name: set_depth_breadth_first_mode/1

Module: state_space_exploration_modes

Name: dbf_modes/3

Module: state_space_exploration_modes

Name: announce_event/1

Module: eventhandling

Name: start_animation/0

Module: prob2_interface

Name: update_preferences_from_spec/0

Module: prob2_interface

Name: time_out_with_factor_call/4

Module: tools_timeout

Name: time_out_call/2

Module: tools_timeout

Name: translate_event_with_src_and_target_id/4

Module: translate

Name: edit_file/2

Module: tools_commands

Name: b_absolute_file_name_relative_to_opened_file/2

Module: specfile

Name: tcltk_save_history_as_trace_file/2

Module: b_trace_checking

Name: get_bexpression_column_template/4

Module: translate

Name: extend_state_with_probids_and_lets/2

Module: eval_let_store

Name: compute_heuristic_function_for_state_id/2

Module: state_space_exploration_modes

Name: out_degree/2

Module: state_space

Name: compute_transitions_if_necessary/1

Module: state_space

Name: get_operation_description_for_transition/3

Module: specfile

Name: b_load_machine_from_file/1

Module: bmachine

Name: b_load_machine_probfile/1

Module: bmachine

Name: get_filename_extension/2

Module: tools

Name: open_xtl_file/1

Module: xtl_interface

Name: type_check_csp_and_b/0

Module: specfile

Name: file_exists/1

Module: file_systems

Name: delete_file/1

Module: file_systems

Name: call_fuzz_parser/2

Module: parsercall

Name: load_eventb_file/1

Module: eclipse_interface

Name: call_alloy2pl_parser/2

Module: parsercall

Name: catch_clpfd_overflow_call2/2

Module: clpfd_interface

Name: reset_max_reached/0

Module: succeed_max

Name: max_reached/0

Module: succeed_max

Name: max_reached/1

Module: succeed_max

Name: get_virtual_time_out_from_exception/2

Module: error_manager

Name: time_out/3

Module: timeout

Name: profile_failure_driven_loop/2

Module: runtime_profiler

Name: get_possible_top_level_event_matches_msg/2

Module: tools_matching

Name: catch_clpfd_overflow_call1/1

Module: clpfd_interface

Name: call_in_fresh_error_scope_for_one_solution/1

Module: error_manager

Name: get_texpr_ids/2

Module: bsyntaxtree

Name: extract_all_line_col/5

Module: error_manager

Name: extract_span_from_event/4

Module: haskell_csp

Name: extract_span_info/2

Module: haskell_csp

Name: execute_model/5

Module: prob2_interface

Name: count_occurences/2

Module: tools_lists

Name: get_current_state_for_b_formula/2

Module: specfile

Name: extend_typing_scope_for_stored_lets/2

Module: eval_let_store

Name: b_parse_machine_expression_from_codes_with_prob_ids/2

Module: bmachine

Name: type_with_errors/4

Module: bmachine

Name: replace_ids_by_exprs/4

Module: bsyntaxtree

Name: b_get_machine_operation_for_animation/7

Module: bmachine

Name: unify_types_strict/2

Module: btypechecker

Name: b_is_variable/2

Module: bmachine

Name: b_is_constant/2

Module: bmachine

Name: inline_prob_deferred_set_elements_into_bexpr/2

Module: b_global_sets

Name: extend_state_with_probids_and_lets/2

Module: eval_let_store

Name: init_wait_flags_with_call_stack/2

Module: kernel_waitflags

Name: ground_wait_flags/1

Module: kernel_waitflags

Name: b_is_unused_constant/1

Module: bmachine

Name: format_to_codes/3

Module: codesio

Name: safe_mul/3

Module: kernel_card_arithmetic

Name: pretty_type/2

Module: translate

Name: get_quantified_operation_enabling_condition/4

Module: b_operation_guards

Name: b_get_properties_from_machine/1

Module: bmachine

Name: b_get_machine_constants/1

Module: bmachine

Name: b_machine_has_constants_or_properties/0

Module: bmachine

Name: create_or_merge_exists/3

Module: bsyntaxtree

Name: conjunct_predicates/2

Module: bsyntaxtree

Name: b_parse_machine_formula/3

Module: bmachine

Name: type_with_errors/4

Module: bmachine

Name: get_primed_machine_variables/1

Module: bmachine

Name: get_current_predecessor_state_id/1

Module: state_space

Name: extract_variables_from_state_as_primed/2

Module: specfile

Name: create_typed_id/3

Module: bsyntaxtree

Name: maplist/4

Module: lists

Name: maplist5/5

Module: tools

Name: interruptable_call/1

Module: user_interrupts

Name: registered_freetype/2

Module: kernel_freetypes

Name: is_set_type/2

Module: bsyntaxtree

Name: to_b_string/2

Module: kernel_strings

Name: fuzzy_match_codes_lower_case/2

Module: tools_matching

Name: animatable_process_without_arguments/1

Module: haskell_csp

Name: animatable_process_cli/1

Module: haskell_csp

Name: get_csp_assertions/1

Module: haskell_csp

Name: translate_csp_assertion/2

Module: haskell_csp

Name: translate_bexpression_with_limit/3

Module: translate

Name: get_tk_table_position_info/2

Module: error_manager

Name: tcltk_goto_state/2

Name: tcltk_add_new_transition_transid/6

Name: tcltk_add_new_transition/5

Name: tcltk_get_options/1

Name: tcltk_get_options_dest_info/1

Name: tcltk_get_state/1

Name: tcltk_get_state/2

Name: tcltk_get_options_or_candidates/1

Name: tcltk_get_options_candidate_nr_name/2

Name: tcltk_get_options_nr_description/2

Name: tcltk_get_state_errors/1

Name: tcltk_get_detailed_state_error/6

Name: tcltk_open_state_error_in_editor/1

Name: tcltk_get_line_col/5

Name: tcltk_current_state_invariant_violated/0

Name: tcltk_get_status/3

Name: tcltk_get_ops_with_virtual_timeout/1

Name: tcltk_get_ops_with_real_timeout/1

Name: tcltk_get_ops_user_interrupt_occurred/0

Name: tcltk_compute_options/2

Name: can_generate_dot_from_last_state_error/0

Name: tcltk_initialise/0

Name: tcltk_reset/0

Name: tcltk_perform_nr/1

Name: tcltk_random_perform/0

Name: tcltk_random_perform/1

Name: tcltk_perform_nr_option/3

Name: tcltk_perform_action_term/2

Name: tcltk_is_sync_event/1

Name: tcltk_exists_an_open_node/0

Name: tcltk_goto_an_open_node/0

Name: tcltk_goto_max_reached_node/0

Name: tcltk_goto_timeout_node/0

Name: tcltk_state_exists_with_invariant_violated/0

Name: tcltk_goto_an_invariant_violation/0

Name: tcltk_goto_node_with_id/1

Name: tcltk_try_goto_node_with_id/1

Name: tcltk_current_node_has_no_real_transition/0

Name: tcltk_current_node_has_real_transition/0

Name: tcltk_current_node_has_partial_transition/0

Name: tcltk_goto_a_non_deterministic_node/1

Name: tcltk_goto_a_non_deterministic_output_node/1

Name: tcltk_goto_a_branching_node/0

Name: tcltk_goto_a_non_resetable_node/0

Name: tcltk_state_space_only_has_root_node/0

Name: tcltk_no_constants_or_no_inititalisation_found/0

Name: tcltk_goto_event_list_property_violation/3

Name: tcltk_goto_state_enabling_operation/2

Name: tcltk_find_max_reached_node/0

Name: tcltk_find_max_reached_node/1

Name: tcltk_search_among_existing_nodes/6

Name: find_invariant_violation_among_not_checked_nodes/1

Name: tcltk_model_check/12

Name: do_model_check/13

Name: tcltk_set_dbf_mode/1

Name: tcltk_dbf_modes/1

Name: tcltk_mark_current_node_to_be_recomputed_wo_timeout/0

Name: tcltk_mark_current_node_to_be_recomputed_with_random_enum/0

Name: tcltk_finish_current_node_to_be_recomputed_with_random_enum/0

Name: tcltk_hash_model_checking_imprecise/0

Name: tcltk_clear_state_space_and_refocus_to_current_state/0

Name: tcltk_constraint_based_check/1

Name: tcltk_constraint_based_check_op/2

Name: tcltk_constraint_based_check_op/3

Name: tcltk_constraint_based_check/2

Name: tcltk_constraint_based_check_with_timeout/2

Name: tcltk_cbc_find_trace/2

Name: tcltk_cbc_find_trace/4

Name: tcltk_cbc_refinement_check/2

Name: tcltk_constraint_find_valid_state/0

Name: tcltk_constraint_find_maximal_valid_state/0

Name: tcltk_constraint_find_dynamic_assertion_violation/0

Name: tcltk_constraint_find_valid_state_with_pred/3

Name: tcltk_constraint_find_deadlock_state/1

Name: tcltk_constraint_find_deadlock_state_with_goal/2

Name: tcltk_constraint_find_deadlock_state_with_goal/3

Name: tcltk_constraint_find_static_assertion_violation/1

Name: tcltk_check_if_feasible_operation/4

Name: cbc_constraint_find_static_assertion_violation/2

Name: tcltk_can_backtrack/0

Name: tcltk_can_backtrack/1

Name: tcltk_can_forward/0

Name: tcltk_can_forward/1

Name: tcltk_prepare_for_reload/0

Name: tcltk_backtrack/0

Name: tcltk_backtrack/1

Name: tcltk_fast_forward/0

Name: tcltk_forward/0

Name: tcltk_execute_trace_to_current_node/0

Name: tcltk_find_shortest_trace_to_current_node/1

Name: tcltk_execute_longest_trace_from/1

Name: tcltk_get_history/1

Name: tcltk_perform_action_string/3

Name: tcltk_perform_action/2

Name: tcltk_perform_action/4

Name: tcltk_open_xtl_file/1

Name: tcltk_open_z_file/1

Name: tcltk_open_z_tex_file/1

Name: tcltk_open_alloy_file/1

Name: tcltk_open_alloy_prolog_ast_file/1

Name: tcltk_open_cspm_file/1

Name: tcltk_add_csp_file/1

Name: tcltk_load_packaged_eventb_file/1

Name: tcltk_verify_alloy_cmd/4

Name: tcltk_get_alloy_cmd_names/1

Name: tcltk_load_alloy_cmd_in_current_translation/1

Name: tcltk_machine_has_assertions/0

Name: tcltk_unique_top_level_operation/1

Name: tcltk_top_level_operations/1

Name: compute_all_transitions_if_necessary/0

Name: compute_all_transitions_if_necessary/2

Name: compute_state_information_if_necessary/0

Name: compute_invariant_if_necessary/3

Name: check_invariantKO/2

Name: check_invariantKO/3

Name: catch_clpfd_overflow_call_for_state/4

Name: compute_ample_set/3

Name: compute_all_transitions/2

Name: add_transition/4

Name: add_trans_id/5

Name: tcltk_has_eventtrace/1

Name: tcltk_show_eventtrace/2

Name: tcltk_execute_model/3

Name: tcltk_execute_trace_to_node/1

Name: find_shortest_trace_to_node/4

Name: tcltk_explore_csp_process/2

Name: tcltk_visualize_csp_process/2

Name: get_csp_process_id/2

Name: get_csp_process_stats/1

Name: tcltk_add_user_executed_operation/2

Name: tcltk_add_user_executed_operation/3

Name: tcltk_add_user_executed_operation_typed/4

Name: tcltk_add_user_executed_operation_typed/6

Name: tcltk_add_user_executed_statement/3

Name: tcltk_add_user_modify_variable_transition/2

Name: tcltk_add_user_modify_variable_transition/4

Name: tcltk_analyse_option/2

Name: tcltk_analyse/6

Name: tcltk_show_typing_of_variables_and_constants/1

Name: tcltk_show_current_state/1

Name: tcltk_eval/4

Name: interruptable_tcltk_eval/4

Name: tcltk_eval_as_table/2

Name: tcltk_find_value_as_table/3

Name: find_value_in_cur_state/4

Name: tcltk_time_call/1

Name: eval_elapsed_time/1

Name: tcltk_check_csp_assertions/2

Name: tcltk_check_csp_assertion/4

Name: tcltk_check_csp_assertion/5

Name: checkAssertion/5

Name: tcltk_get_vacuous_guards/1

Name: tcltk_get_vacuous_invariants/1

Name: tcltk_get_vacuous_invariants_table/1

Name: tcltk_operations_covered_info/3

Name: operation_name_covered/1

Name: tcltk_show_expression_as_dot/2

Name: generate_dot_from_formula/2

Name: generate_dot_from_invariant/1

Name: generate_dot_from_properties/1

Name: generate_dot_from_assertions/1

Name: generate_dot_from_deadlock_po/1

Name: generate_dot_from_goal/1

Name: generate_dot_from_last_span_predicate/1

Name: generate_dot_from_operation/2

Name: generate_dot_from_operation_with_params/4

Name: write_dot_file_for_pred_expr/2

Name: write_dot_file_for_value_as_tree/2

Name: evaluate_expression_over_history_to_csv_file/2

Name: tcltk_evaluate_expression_over_history/2

Name: translate_error_for_tclk/2

Name: tcltk_set_initial_machine/0

Name: tcltk_clear_machine/0

Name: tcltk_open_b_file/1

Name: tcltk_open_b_file_for_minor_mode/2

Name: tcltk_run_ltsmin/5

Name: tcltk_save_history_as_trace_file/1

Name: tcltk_execute_until/1

Name: tcltk_bv_get_tops/1

Name: tcltk_bv_get_structure/3

Name: tcltk_bv_is_leaf/2

Name: tcltk_bv_get_values/3

Name: tcltk_bv_get_value/3

Name: tcltk_bv_show_formula_as_dot_tree/2

Name: tcltk_bv_show_formula_as_dot_graph/2

Name: tcltk_bv_show_value_as_dot_tree/2

Name: tcltk_bv_get_pp_formula_string/2

Name: tcltk_show_identifier_value_as_dot_tree/2

Name: tcltk_bv_get_unlimited_value/3

Name: tcltk_bv_get_unlimited_value_atom/2

Name: tcltk_get_constants_predicate/2

Name: get_cbc_data_base_id_checks/1

Name: get_cbc_data_base_text_checks/1

Name: tcltk_write_uml_sequence_chart/1

Name: get_ltl_formulas_from_file/2

Name: tcltk_mcts_auto_play/0

Name: tcltk_mcts_auto_play/1

Name: mcts_auto_play_available/0

Name: tcltk_simplify_predicate/2

Predicates

Predicates:

adapt_tcl_operation_name/2

add_additional_destination_infos/3

add_csp_general_process_id/2

add_csp_process_id/2

add_csp_process_id1/3

add_csp_process_id_normalized/4

add_id_to_history/1

add_new_transition_transid_with_infos/7

add_or_between_constant_predicates/2

add_partial_transitions/2

add_trans_id/5

add_trans_id_with_infos/8

add_transition/4

add_transitions__with_timeout_fail_loop/3

add_transitions__with_timeout_fail_loop2/4

add_transitions_fail_loop/2

add_transitions_fail_loop2/3

assert_temp_predicate_with_prob_def_set_elements/1

b_compute_expression_with_prob_ids/3

b_full_execute_top_level_statement_with_probids/4

b_load_aux/1

b_trans_one_solution_with_pred/6

b_trans_one_solution_with_pred2/6

bindings_to_state/2

call_cbc_command/1

call_pred_on_expanded_state/4

can_generate_dot_from_last_state_error/0

catch_clpfd_overflow_call_for_state/4

cbc_constraint_find_static_assertion_violation/2

checkAssertion/5

check_cst/4

check_event_list_property/3

check_valid_operation/1

check_we_are_in_b_mode/1

compute_all_inits/0

compute_all_transitions/2

compute_all_transitions2/2

compute_all_transitions_if_necessary/0

compute_all_transitions_if_necessary/1

compute_all_transitions_if_necessary/2

compute_invariant_if_necessary/2

compute_invariant_if_necessary/3

compute_invariant_if_necessary_and_requested/2

compute_state_information_if_necessary/0

compute_state_information_if_necessary/1

construct_list/2

convert_explain_tag/2

convert_trace_to_list_of_strings/2

convert_typed_varlist/3

convert_value_to_tcl/2

count_nodes/0

csp_ref_style/2

decompose/4

decompose_expression_for_dot/3

decompose_fields_for_dot/3

dif_ID/2

do_model_check/13

eval_string_in_cur_state/3

evaluate_bexpr_over_state/7

evaluate_expression_over_history_to_csv_file/2

extract_actions/5

extract_span_from_action/2

extract_trans_id/2

filter_constants_bindings/2

filter_constants_bindings1/3

find_id_in_forward_history/2

find_id_in_history/2

find_invariant_violation_among_not_checked_nodes/1

find_match_string/3

find_non_det_constants/0

find_non_det_constants1/2

find_resetable_nodes/0

find_resetable_nodes_loop/0

find_resetable_nodes_loop/2

find_shortest_trace_to_node/4

find_successor_state/2

find_trace_to_current_node/1

find_value/6

find_value_in_cur_state/4

force_check_invariantKO/2

fuzzy_find_value/6

gen_forward_history/4

gen_unknown_forward/2

generate_dot_from_assertions/1

generate_dot_from_deadlock_po/1

generate_dot_from_formula/2

generate_dot_from_goal/1

generate_dot_from_invariant/1

generate_dot_from_last_span_predicate/1

generate_dot_from_operation/2

generate_dot_from_operation_with_params/4

generate_dot_from_properties/1

generate_tree_in_cur_state/3

generate_typing_list/4

get_a_part_of_the_found_solutions/3

get_animation_operation_parameters/2

get_cand_dest/2

get_cand_name/2

get_cbc_data_base_id_checks/1

get_cbc_data_base_text_checks/1

get_check_name/3

get_constants_as_disjoint_predicate/2

get_cov/2

get_csp_process_id/2

get_csp_process_stats/1

get_current_option_eventtrace/2

get_current_state_errors/2

get_expr_and_source/2

get_id_of_node_and_add_if_required_with_skip_check/6

get_id_type/3

get_identifier/2

get_inner_span/2

get_ltl_formulas_from_file/2

get_properties/2

get_set_up_constants_solution/1

get_source_text_positions/5

get_start_transition_term/2

go_forward/5

inc_nr_cbc_sols/0

insert_custom_predicate_into_guard/3

interruptable_tcltk_eval/4

is_already_explored/1

is_constant_binding/2

is_det_controller_state/2

is_heuristic/1

is_initialisation_op/1

is_self_loop/2

is_valid_controller_state/2

no_quotes_necessary/1

non_det_modified/2

not_yet_covered_info/3

notify_change_of_animation_mode/0

nr_cbc_sols/1

operation_name_covered/1

operation_name_covered/2

ops_with_timeout/3

option_dest_info/4

parse_machine_expression/2

parse_machine_formula/2

parse_parameter_values/3

parse_tclk_parameter_values_and_pred/4

peel2/2

possible_trans_name_for_successors/2

potentially_enabled_operation/3

print_trans/1

prob_plspec_error_handler/1

process_ltsmin_result/3

prune_list/2

query_op_transition/1

re_execute_transition/3

re_execute_transition_if_necessary/3

relative_deadlock_freedom/2

replay_ltsmin_trace/2

reset_nr_cbc_sols/0

reset_tcltk_interface/0

resetable_node/1

retrieve_tag_adapted_text_for_id/4

retrieve_tag_text/3

retrieve_tag_text_for_id/4

run_assertion_check/3

search_among_existing_nodes/6

seperate_state_into_const_and_vars/3

set_cbc_state/3

simple_value_to_match/1

tcltk_add_cbc_state/2

tcltk_add_csp_file/1

tcltk_add_new_transition/5

tcltk_add_new_transition_transid/6

tcltk_add_user_executed_operation/2

tcltk_add_user_executed_operation/3

tcltk_add_user_executed_operation_typed/4

tcltk_add_user_executed_operation_typed/6

tcltk_add_user_executed_statement/3

tcltk_add_user_modify_variable_transition/2

tcltk_add_user_modify_variable_transition/4

tcltk_analyse/6

tcltk_analyse2/3

tcltk_analyse_option/2

tcltk_backtrack/0

tcltk_backtrack/1

tcltk_bv_get_pp_formula_string/2

tcltk_bv_get_structure/3

tcltk_bv_get_tops/1

tcltk_bv_get_unlimited_value/3

tcltk_bv_get_unlimited_value_atom/2

tcltk_bv_get_value/3

tcltk_bv_get_values/3

tcltk_bv_is_leaf/2

tcltk_bv_show_formula_as_dot_graph/2

tcltk_bv_show_formula_as_dot_tree/2

tcltk_bv_show_value_as_dot_tree/2

tcltk_can_backtrack/0

tcltk_can_backtrack/1

tcltk_can_forward/0

tcltk_can_forward/1

tcltk_cbc_find_trace/2

tcltk_cbc_find_trace/4

tcltk_cbc_find_trace_aux/5

tcltk_cbc_refinement_check/2

tcltk_check_csp_assertion/4

tcltk_check_csp_assertion/5

tcltk_check_csp_assertions/2

tcltk_check_if_feasible_operation/4

tcltk_clear_machine/0

tcltk_clear_state_space_and_refocus_to_current_state/0

tcltk_compute_options/2

tcltk_constraint_based_check/2

tcltk_constraint_based_check/1

tcltk_constraint_based_check_op/2

tcltk_constraint_based_check_op/3

tcltk_constraint_based_check_op2/3

tcltk_constraint_based_check_with_timeout/2

tcltk_constraint_find_deadlock_state/1

tcltk_constraint_find_deadlock_state_with_goal/2

tcltk_constraint_find_deadlock_state_with_goal/3

tcltk_constraint_find_dynamic_assertion_violation/0

tcltk_constraint_find_maximal_valid_state/0

tcltk_constraint_find_static_assertion_violation/1

tcltk_constraint_find_valid_state/0

tcltk_constraint_find_valid_state_with_pred/3

tcltk_csp_in_situ_refinement/4

tcltk_csp_in_situ_refinement/5

tcltk_current_node_has_no_real_transition/0

tcltk_current_node_has_partial_transition/0

tcltk_current_node_has_real_transition/0

tcltk_current_state_invariant_violated/0

tcltk_dbf_modes/1

tcltk_eval/4

tcltk_eval_as_table/2

tcltk_eval_string_in_cur_state/2

tcltk_evaluate_expression_over_history/2

tcltk_execute_longest_trace_from/1

tcltk_execute_model/3

tcltk_execute_trace_from_to_found_predicate/3

tcltk_execute_trace_to_current_node/0

tcltk_execute_trace_to_node/1

tcltk_execute_until/1

tcltk_exists_an_open_node/0

tcltk_explore_csp_process/2

tcltk_fast_forward/0

tcltk_find_max_reached_node/0

tcltk_find_max_reached_node/1

tcltk_find_shortest_trace_to_current_node/1

tcltk_find_value_as_table/3

tcltk_finish_current_node_to_be_recomputed_with_random_enum/0

tcltk_forward/0

tcltk_forward/1

tcltk_get_alloy_cmd_names/1

tcltk_get_candidate_operations/1

tcltk_get_candidates_dest_info/1

tcltk_get_computed_options/2

tcltk_get_constants_predicate/2

tcltk_get_detailed_state_error/6

tcltk_get_history/1

tcltk_get_line_col/5

tcltk_get_ops_user_interrupt_occurred/0

tcltk_get_ops_with_real_timeout/1

tcltk_get_ops_with_virtual_timeout/1

tcltk_get_options/1

tcltk_get_options/2

tcltk_get_options_candidate_nr_name/2

tcltk_get_options_dest_info/1

tcltk_get_options_dest_info/2

tcltk_get_options_nr_description/2

tcltk_get_options_or_candidates/1

tcltk_get_state/1

tcltk_get_state/2

tcltk_get_state_errors/1

tcltk_get_status/3

tcltk_get_vacuous_guards/1

tcltk_get_vacuous_invariants/1

tcltk_get_vacuous_invariants_table/1

tcltk_goto_a_branching_node/0

tcltk_goto_a_non_deterministic_node/1

tcltk_goto_a_non_deterministic_output_node/1

tcltk_goto_a_non_resetable_node/0

tcltk_goto_an_invariant_violation/0

tcltk_goto_an_open_node/0

tcltk_goto_event_list_property_violation/3

tcltk_goto_max_reached_node/0

tcltk_goto_node_with_id/1

tcltk_goto_state/2

tcltk_goto_state_enabling_operation/2

tcltk_goto_timeout_node/0

tcltk_has_eventtrace/1

tcltk_hash_model_checking_imprecise/0

tcltk_initialise/0

tcltk_is_sync_event/1

tcltk_load_alloy_cmd_in_current_translation/1

tcltk_load_packaged_eventb_file/1

tcltk_machine_has_assertions/0

tcltk_mark_current_node_to_be_recomputed_with_random_enum/0

tcltk_mark_current_node_to_be_recomputed_wo_timeout/0

tcltk_mark_node_for_recomputed/1

tcltk_mcts_auto_play/0

tcltk_mcts_auto_play/1

tcltk_model_check/12

tcltk_no_constants_or_no_inititalisation_found/0

tcltk_open_alloy_file/1

tcltk_open_alloy_prolog_ast_file/1

tcltk_open_b_file/1

tcltk_open_b_file_for_minor_mode/2

tcltk_open_cspm_file/1

tcltk_open_state_error_in_editor/1

tcltk_open_xtl_file/1

tcltk_open_z_file/1

tcltk_open_z_file2/1

tcltk_open_z_tex_file/1

tcltk_operations_covered_info/3

tcltk_perform_action/2

tcltk_perform_action/3

tcltk_perform_action/4

tcltk_perform_action_string/3

tcltk_perform_action_term/2

tcltk_perform_nr/1

tcltk_perform_nr_option/3

tcltk_play_counterexample/3

tcltk_play_ltl_ctl_counterexample_trace/4

tcltk_prepare_for_reload/0

tcltk_random_perform/0

tcltk_random_perform/1

tcltk_random_perform2/2

tcltk_reset/0

tcltk_run_ltsmin/5

tcltk_save_history_as_trace_file/1

tcltk_search_among_existing_nodes/6

tcltk_set_dbf_mode/1

tcltk_set_failed_to_open_file/1

tcltk_set_initial_machine/0

tcltk_show_current_state/1

tcltk_show_eventtrace/2

tcltk_show_expression_as_dot/2

tcltk_show_identifier_value_as_dot_tree/2

tcltk_show_typed_expression_as_dot_graph/2

tcltk_show_typing_of_variables_and_constants/1

tcltk_simplify_predicate/2

tcltk_state_exists_with_invariant_violated/0

tcltk_state_space_only_has_root_node/0

tcltk_time_call/1

tcltk_top_level_operations/1

tcltk_try_goto_node_with_id/1

tcltk_try_reload/0

tcltk_unique_top_level_operation/1

tcltk_verify_alloy_cmd/4

tcltk_visualize_csp_process/2

tcltk_write_uml_sequence_chart/1

transform_value_to_expr/2

transitions_computed_for_node/1

translate_bstate_to_pred/2

translate_csp_ref_style/2

translate_ctl_result/3

translate_error_for_tclk/2

translate_ltl_formula/2

translate_ltl_formulas/2

translate_ltl_result/2

translate_state_err_for_tcltk/2

treat_csp_ass/6

update_ass/2

update_history_from_trace/1

update_variable/4

valid_id/1

valid_operation_or_init/2

write_dot_file_for_pred_expr/2

write_dot_file_for_pred_expr/3

write_dot_file_for_pred_expr_and_state/4

write_dot_file_for_value_as_tree/2

adapt_tcl_operation_name/2

add_additional_destination_infos/3

add_csp_general_process_id/2

add_csp_process_id/2

add_csp_process_id1/3

Meta: add_csp_process_id1(-,-,1)

add_csp_process_id_normalized/4

add_id_to_history/1

add_new_transition_transid_with_infos/7

Description:
print_message(tcltk_add_new_transition(FromID,Action,ToID,Exists)), %%

add_or_between_constant_predicates/2

add_partial_transitions/2

add_trans_id/5

add_trans_id_with_infos/8

add_transition/4

Description:
print_bt_message(specfile_trans(CurState,ActionName,Act,NewExpression,TransInfo,Residue)), %%

add_transitions__with_timeout_fail_loop/3

add_transitions__with_timeout_fail_loop2/4

Description:
statistics(runtime,[T1,_]), print(try(ActionName,T1)),nl,%%
statistics(runtime,[T2,_]), TDiff is T2-T1, print(added_transition(CurID,ActionName,TDiff,TimeOutRes)),nl, %%
add_transition(CurID,CurState,ActionName,_NewId) ,

add_transitions__with_timeout_fail_loop2(Level,CurID,CurState,CurTO) :- % statistics(runtime,_),
    % TO DO: prepare computing the state: expanding const and vars, unpacking, ...
    possible_trans_name_for_successors(CurState,ActionName),
    profile_failure_driven_loop(ActionName,CurID),
    % Note: we enumerate possible transition names so that we can catch the time-out per name !
    % statistics(runtime,[T1,DeltaT]), print(delta_time(ActionName,DeltaT)),nl,
    % first enumerate possible Operations/... to obtain timeout per operation/...
    % TO DO: divide CurTO by number of transitions ???
    % We could also decide to have one time-out per state, only if that one is triggered move to
    % finer-grained timeouts
    % For probcli ../prob_examples/public_examples/B/Benchmarks/Cruise_finite1.mch --model-check, there are 35360 calls to timeout/3 (one per state the model checker reached and per transition group), with -disable-timeout none
    % In SICS 4.3.5 the runtime increased from 1.480 to 2.270 seconds = 0.022 ms per timeout call
    % In SICS 4.4.1 the runtime increased from 1.494 to 3.033 seconds. = 0.044 ms per timeout call.
    %% statistics(runtime,[T1,_]), print(try(ActionName,T1)),nl,
    set_error_context(operation(ActionName,CurID)),
    time_out_with_enum_warning_for_findall_in_current_error_scope(Level,
    add_transition(CurID,CurState,ActionName,_NewId),CurTO,TimeOutRes),
    %% statistics(runtime,[T2,_]), TDiff is T2-T1, print(added_transition(CurID,ActionName,TDiff,TimeOutRes)),nl,
    %% add_transition(CurID,CurState,ActionName,_NewId) ,
    ((TimeOutRes==time_out ; nonvar(TimeOutRes),TimeOutRes=virtual_time_out(_), \+ max_reached(ActionName))
    % virtual time outs not relevant if we have already stopped earlier anyway; TO DO: does not seem to work for INITIALISATION
    -> (TimeOutRes=virtual_time_out(_) -> true
    ; print_message('TIME OUT: '),print_message(CurID),
    print_message(CurTO),print_message(ActionName)
    ),
    (var(ActionName)
    -> assert_time_out_for_node(CurID,'unspecified_operation',TimeOutRes)
    ; assert_time_out_for_node(CurID,ActionName,TimeOutRes)) % TO DO: assert info per ActionSkeleton ?
    ; true
    ),fail.

add_transitions__with_timeout_fail_loop2(_,_,_,_) :- clear_error_context.

add_transitions_fail_loop/2

add_transitions_fail_loop2/3

assert_temp_predicate_with_prob_def_set_elements/1

b_compute_expression_with_prob_ids/3

b_full_execute_top_level_statement_with_probids/4

Description:
allows one to execute any statement (not just operations).

b_load_aux/1

b_trans_one_solution_with_pred/6

b_trans_one_solution_with_pred2/6

bindings_to_state/2

call_cbc_command/1

call_pred_on_expanded_state/4

Meta: call_pred_on_expanded_state(3,-,-,-)

can_generate_dot_from_last_state_error/0

catch_clpfd_overflow_call_for_state/4

Meta: catch_clpfd_overflow_call_for_state(-,-,0,0)

cbc_constraint_find_static_assertion_violation/2

checkAssertion/5

check_cst/4

check_event_list_property/3

check_valid_operation/1

check_we_are_in_b_mode/1

compute_all_inits/0

compute_all_transitions/2

compute_all_transitions2/2

compute_all_transitions_if_necessary/0

compute_all_transitions_if_necessary/1

compute_all_transitions_if_necessary/2

compute_invariant_if_necessary/2

compute_invariant_if_necessary/3

compute_invariant_if_necessary_and_requested/2

compute_state_information_if_necessary/0

compute_state_information_if_necessary/1

construct_list/2

convert_explain_tag/2

convert_trace_to_list_of_strings/2

convert_typed_varlist/3

convert_value_to_tcl/2

count_nodes/0

csp_ref_style/2

decompose/4

decompose_expression_for_dot/3

decompose_fields_for_dot/3

dif_ID/2

do_model_check/13

eval_string_in_cur_state/3

evaluate_bexpr_over_state/7

evaluate_expression_over_history_to_csv_file/2

extract_actions/5

extract_span_from_action/2

extract_trans_id/2

filter_constants_bindings/2

filter_constants_bindings1/3

find_id_in_forward_history/2

find_id_in_history/2

find_invariant_violation_among_not_checked_nodes/1

find_match_string/3

find_non_det_constants/0

find_non_det_constants1/2

find_resetable_nodes/0

find_resetable_nodes_loop/0

find_resetable_nodes_loop/2

find_shortest_trace_to_node/4

find_successor_state/2

find_trace_to_current_node/1

find_value/6

find_value_in_cur_state/4

force_check_invariantKO/2

fuzzy_find_value/6

gen_forward_history/4

gen_unknown_forward/2

generate_dot_from_assertions/1

generate_dot_from_deadlock_po/1

generate_dot_from_formula/2

generate_dot_from_goal/1

generate_dot_from_invariant/1

generate_dot_from_last_span_predicate/1

generate_dot_from_operation/2

generate_dot_from_operation_with_params/4

generate_dot_from_properties/1

generate_tree_in_cur_state/3

generate_typing_list/4

get_a_part_of_the_found_solutions/3

get_animation_operation_parameters/2

get_cand_dest/2

get_cand_name/2

get_cbc_data_base_id_checks/1

get_cbc_data_base_text_checks/1

get_check_name/3

get_constants_as_disjoint_predicate/2

get_cov/2

get_csp_process_id/2

get_csp_process_stats/1

get_current_option_eventtrace/2

get_current_state_errors/2

get_expr_and_source/2

get_id_of_node_and_add_if_required_with_skip_check/6

get_id_type/3

get_identifier/2

get_inner_span/2

get_ltl_formulas_from_file/2

Description:
Parse and get LTL formulas from LTL File %%%%

get_properties/2

get_set_up_constants_solution/1

get_source_text_positions/5

get_start_transition_term/2

go_forward/5

inc_nr_cbc_sols/0

insert_custom_predicate_into_guard/3

interruptable_tcltk_eval/4

is_already_explored/1

is_constant_binding/2

is_det_controller_state/2

is_heuristic/1

is_initialisation_op/1

is_self_loop/2

is_valid_controller_state/2

keep_min2/3

keep_min_heuristic/2

map_over_history/2

Meta: map_over_history(3,-)

no_quotes_necessary/1

non_det_modified/2

not_yet_covered_info/3

notify_change_of_animation_mode/0

nr_cbc_sols/1

Dynamic: true

operation_name_covered/1

operation_name_covered/2

ops_with_timeout/3

option_dest_info/4

parse_machine_expression/2

parse_machine_formula/2

parse_parameter_values/3

parse_tclk_parameter_values_and_pred/4

peel2/2

possible_trans_name_for_successors/2

potentially_enabled_operation/3

print_trans/1

prob_plspec_error_handler/1

process_ltsmin_result/3

prune_list/2

query_op_transition/1

re_execute_transition/3

Description:
print(trans(ActionTerm)),nl,

re_execute_transition_if_necessary/3

relative_deadlock_freedom/2

replay_ltsmin_trace/2

reset_nr_cbc_sols/0

reset_tcltk_interface/0

resetable_node/1

Dynamic: true

retrieve_tag_adapted_text_for_id/4

retrieve_tag_text/3

retrieve_tag_text_for_id/4

run_assertion_check/3

Description:
print(add_csp_general_process_id(Spec,CSpec,SpecNodeID)),nl,

run_assertion_check(assertModelCheckExt(Negated,Spec,Type,ModelStyle),Negated,ResTrace) :-
    haskell_csp_analyzer: compile_body(Spec,'assertModelCheck',[],[],CSpec),
    debug_println(9,assertModelCheckExt(Negated,CSpec,Type,ModelStyle)),
    add_csp_general_process_id(CSpec,SpecNodeID),
    translate_csp_ref_style(ModelStyle,RefStyle),
    in_situ_model_check(SpecNodeID,ResTrace,Type,RefStyle,10000000),
    formatsilent('Result trace for assertModelCheck: ~w~n',[ResTrace]).

run_assertion_check(assertModelCheck(Negated,Spec,Style),Negated,ResTrace) :-
    run_assertion_check(assertModelCheckExt(Negated,Spec,Style,'FailureDivergence'),Negated,ResTrace).

run_assertion_check(assertRef(Negated,Spec,Style,Impl,Span),Negated,ResTrace) :-
    haskell_csp_analyzer: compile_body(Spec,'assertRef',[],[],CSpec),
    haskell_csp_analyzer: compile_body(Impl,'assertRef',[],[],CImpl),
    debug_println(9,assertRef(Negated,CSpec,Style,CImpl,Span)),
    add_csp_general_process_id(CSpec,SpecNodeID),
    add_csp_general_process_id(CImpl,ImplNodeID),
    translate_csp_ref_style(Style,RefStyle),
    refinement_checker:in_situ_ref_search(ImplNodeID,SpecNodeID,ResTrace,RefStyle,10000000).

run_assertion_check(assertLtl(Negated,Spec,FormulaAsAtom,_Span),Negated,ResTrace) :-
    add_csp_process_id_normalized(Spec,'assertLtl',CSpec,CSpecNodeID),
    %% print(add_csp_general_process_id(Spec,CSpec,SpecNodeID)),nl,
    tcltk_reset,
    ltl_model_check_with_ce1(CSpec,FormulaAsAtom,-1,specific_node(CSpecNodeID),Result),
    translate_ltl_result(Result,ResTrace),
    debug_println(9,ltl_result(Negated,CSpec,CSpecNodeID,FormulaAsAtom,Result)).

run_assertion_check(assertCtl(Negated,Spec,FormulaAsAtom,_Span),Negated,ResTrace) :-
    add_csp_process_id_normalized(Spec,'assertCtl',CSpec,CSpecNodeID),
    tcltk_reset,
    ctl_model_check_with_ce(CSpec,FormulaAsAtom,-1,specific_node(CSpecNodeID),Result,Trace),
    debug_println(9,ctl_result(Negated,CSpec,CSpecNodeID,FormulaAsAtom,Result)),
    translate_ctl_result(Result,Trace,ResTrace).

search_among_existing_nodes/6

search_among_existing_nodes(invariant_violation,_FindDeadlocks,FindInvViolations,
    _FindGoal,_FindAssViolations,_FindStateErrors) :-
    (get_state_space_stats(_,_,PrN), PrN>100
    -> print_message('Search Among Processed Nodes'), print_message(number_of_nodes(PrN)) ; true),
    FindInvViolations=1,
    (invariant_violated(ResID) -> true
    ; find_invariant_violation_among_not_checked_nodes(ResID)),
    tcltk_execute_trace_to_node(ResID).

search_among_existing_nodes(DEADLOCK,FindDeadlocks,_,_,_,_) :-
    FindDeadlocks=1,
    visited_expression_id(ResID),
    transitions_computed_for_node(ResID),
    is_deadlocked(ResID),
    (time_out_for_node(ResID)
    -> DEADLOCK = possible_deadlock_timeout
    ; get_preference(store_only_one_incoming_transition,true) -> DEADLOCK = possible_deadlock
    ; DEADLOCK = deadlock),
    print_message(deadlock_among_existing_nodes(ResID)),
    tcltk_execute_trace_to_node(ResID).

search_among_existing_nodes(goal_found,_,_,FindGoal,_,_) :-
    FindGoal=1,
    %visited_expression(ResID,_CurState),
    %\+(not_all_transitions_added(ResID)), % if commented out: will also look at open nodes
    node_satisfies_goal(ResID),
    tcltk_execute_trace_to_node(ResID).

search_among_existing_nodes(assertion_violation,_,_,_,FindAssViolations,_) :-
    FindAssViolations=1,
    b_machine_has_assertions,
    visited_expression(ResID,CurState),
    transitions_computed_for_node(ResID),
    state_violates_assertions(ResID,CurState),
    tcltk_execute_trace_to_node(ResID).

search_among_existing_nodes(ERR,_,_,_,_,FindStateErrors) :- FindStateErrors=1,
    state_space:state_error(ResID,_,Error), Error \== invariant_violated,
    (Error = abort_error(ERR,_,_,_) -> true ; ERR = state_error(Error)),
    tcltk_execute_trace_to_node(ResID).

search_among_existing_nodes(all,_,_,_,_,_).

seperate_state_into_const_and_vars/3

set_cbc_state/3

simple_value_to_match/1

tcltk_add_cbc_state/2

tcltk_add_csp_file/1

tcltk_add_new_transition/5

tcltk_add_new_transition_transid/6

tcltk_add_user_executed_operation/2

tcltk_add_user_executed_operation/3

tcltk_add_user_executed_operation_typed/4

tcltk_add_user_executed_operation_typed/6

tcltk_add_user_executed_statement/3

tcltk_add_user_modify_variable_transition/2

tcltk_add_user_modify_variable_transition/4

tcltk_analyse/6

tcltk_analyse2/3

tcltk_analyse_option/2

tcltk_backtrack/0

tcltk_backtrack/1

tcltk_bv_get_pp_formula_string/2

tcltk_bv_get_structure/3

tcltk_bv_get_tops/1

tcltk_bv_get_unlimited_value/3

tcltk_bv_get_unlimited_value_atom/2

tcltk_bv_get_value/3

tcltk_bv_get_values/3

tcltk_bv_is_leaf/2

tcltk_bv_show_formula_as_dot_graph/2

tcltk_bv_show_formula_as_dot_tree/2

tcltk_bv_show_value_as_dot_tree/2

tcltk_can_backtrack/0

tcltk_can_backtrack/1

tcltk_can_forward/0

tcltk_can_forward/1

tcltk_cbc_find_trace/2

tcltk_cbc_find_trace/4

tcltk_cbc_find_trace_aux/5

tcltk_cbc_refinement_check/2

tcltk_check_csp_assertion/4

tcltk_check_csp_assertion/5

tcltk_check_csp_assertions/2

tcltk_check_if_feasible_operation/4

tcltk_clear_machine/0

tcltk_clear_state_space_and_refocus_to_current_state/0

tcltk_compute_options/2

tcltk_constraint_based_check/2

Description:
print(list(List)),nl, %%

tcltk_constraint_based_check/1

tcltk_constraint_based_check_op/2

tcltk_constraint_based_check_op/3

tcltk_constraint_based_check_op2/3

tcltk_constraint_based_check_with_timeout/2

tcltk_constraint_find_deadlock_state/1

tcltk_constraint_find_deadlock_state_with_goal/2

tcltk_constraint_find_deadlock_state_with_goal/3

tcltk_constraint_find_dynamic_assertion_violation/0

tcltk_constraint_find_maximal_valid_state/0

tcltk_constraint_find_static_assertion_violation/1

tcltk_constraint_find_valid_state/0

tcltk_constraint_find_valid_state_with_pred/3

tcltk_csp_in_situ_refinement/4

tcltk_csp_in_situ_refinement/5

tcltk_current_node_has_no_real_transition/0

tcltk_current_node_has_partial_transition/0

tcltk_current_node_has_real_transition/0

tcltk_current_state_invariant_violated/0

tcltk_dbf_modes/1

tcltk_eval/4

tcltk_eval_as_table/2

tcltk_eval_string_in_cur_state/2

tcltk_evaluate_expression_over_history/2

tcltk_execute_longest_trace_from/1

tcltk_execute_model/3

tcltk_execute_trace_from_to_found_predicate/3

tcltk_execute_trace_to_current_node/0

tcltk_execute_trace_to_node/1

tcltk_execute_until/1

tcltk_exists_an_open_node/0

tcltk_explore_csp_process/2

tcltk_fast_forward/0

tcltk_find_max_reached_node/0

tcltk_find_max_reached_node/1

tcltk_find_shortest_trace_to_current_node/1

tcltk_find_value_as_table/3

tcltk_finish_current_node_to_be_recomputed_with_random_enum/0

tcltk_forward/0

tcltk_forward/1

tcltk_get_alloy_cmd_names/1

Description:
tcltk_get_alloy_cmd_names(-CmdNames).

tcltk_get_candidate_operations/1

tcltk_get_candidates_dest_info/1

tcltk_get_computed_options/2

tcltk_get_constants_predicate/2

Description:
Used to get the constant values for the currently loaded B machine in form of a B predicate.
In case that the constants in the model has not been set up then all possible constants'
evaluations will be provided in form of a predicate in Disjunctive Normal Form.
Predicate used for setting up constants when model checking with TLC. (TLA)

tcltk_get_detailed_state_error/6

tcltk_get_history/1

Description:
fd_copy_term(X,Y,true) :- copy_term(X,Y).

tcltk_get_line_col/5

tcltk_get_ops_user_interrupt_occurred/0

tcltk_get_ops_with_real_timeout/1

tcltk_get_ops_with_virtual_timeout/1

tcltk_get_options/1

tcltk_get_options/2

tcltk_get_options_candidate_nr_name/2

tcltk_get_options_dest_info/1

tcltk_get_options_dest_info/2

tcltk_get_options_nr_description/2

tcltk_get_options_or_candidates/1

tcltk_get_state/1

tcltk_get_state/2

tcltk_get_state_errors/1

tcltk_get_status/3

tcltk_get_vacuous_guards/1

tcltk_get_vacuous_invariants/1

tcltk_get_vacuous_invariants_table/1

tcltk_goto_a_branching_node/0

tcltk_goto_a_non_deterministic_node/1

tcltk_goto_a_non_deterministic_output_node/1

tcltk_goto_a_non_resetable_node/0

tcltk_goto_an_invariant_violation/0

tcltk_goto_an_open_node/0

tcltk_goto_event_list_property_violation/3

tcltk_goto_max_reached_node/0

tcltk_goto_node_with_id/1

tcltk_goto_state/2

tcltk_goto_state_enabling_operation/2

tcltk_goto_timeout_node/0

tcltk_has_eventtrace/1

tcltk_hash_model_checking_imprecise/0

tcltk_initialise/0

tcltk_is_sync_event/1

tcltk_load_alloy_cmd_in_current_translation/1

Description:
tcltk_load_alloy_cmd_in_current_translation(+CmdName).

tcltk_load_packaged_eventb_file/1

tcltk_machine_has_assertions/0

tcltk_mark_current_node_to_be_recomputed_with_random_enum/0

tcltk_mark_current_node_to_be_recomputed_wo_timeout/0

tcltk_mark_node_for_recomputed/1

tcltk_mcts_auto_play/0

tcltk_mcts_auto_play/1

tcltk_model_check/12

tcltk_no_constants_or_no_inititalisation_found/0

tcltk_open_alloy_file/1

tcltk_open_alloy_prolog_ast_file/1

tcltk_open_b_file/1

tcltk_open_b_file_for_minor_mode/2

tcltk_open_cspm_file/1

tcltk_open_state_error_in_editor/1

tcltk_open_xtl_file/1

tcltk_open_z_file/1

tcltk_open_z_file2/1

tcltk_open_z_tex_file/1

tcltk_operations_covered_info/3

tcltk_perform_action/2

tcltk_perform_action/3

tcltk_perform_action/4

tcltk_perform_action_string/3

tcltk_perform_action_term/2

tcltk_perform_nr/1

tcltk_perform_nr_option/3

tcltk_play_counterexample/3

tcltk_play_ltl_ctl_counterexample_trace/4

tcltk_prepare_for_reload/0

tcltk_random_perform/0

tcltk_random_perform/1

tcltk_random_perform2/2

tcltk_reset/0

tcltk_run_ltsmin/5

tcltk_save_history_as_trace_file/1

tcltk_search_among_existing_nodes/6

tcltk_set_dbf_mode/1

tcltk_set_failed_to_open_file/1

tcltk_set_initial_machine/0

tcltk_show_current_state/1

tcltk_show_eventtrace/2

tcltk_show_expression_as_dot/2

tcltk_show_identifier_value_as_dot_tree/2

tcltk_show_typed_expression_as_dot_graph/2

tcltk_show_typing_of_variables_and_constants/1

tcltk_simplify_predicate/2

tcltk_state_exists_with_invariant_violated/0

tcltk_state_space_only_has_root_node/0

tcltk_time_call/1

Meta: tcltk_time_call(0)

tcltk_top_level_operations/1

tcltk_try_goto_node_with_id/1

tcltk_try_reload/0

tcltk_unique_top_level_operation/1

tcltk_verify_alloy_cmd/4

Description:
tcltk_verify_alloy_cmd(+CmdName, +SolverName, -CmdIsValid, -IsCheckCmd).

tcltk_visualize_csp_process/2

tcltk_write_uml_sequence_chart/1

transform_value_to_expr/2

transitions_computed_for_node/1

translate_bstate_to_pred/2

translate_csp_ref_style/2

translate_ctl_result/3

translate_error_for_tclk/2

translate_ltl_formula/2

translate_ltl_formulas/2

translate_ltl_result/2

translate_state_err_for_tcltk/2

treat_csp_ass/6

update_ass/2

update_history_from_trace/1

update_variable/4

valid_id/1

valid_operation_or_init/2

write_dot_file_for_pred_expr/2

write_dot_file_for_pred_expr/3

write_dot_file_for_pred_expr_and_state/4

write_dot_file_for_value_as_tree/2

Determinacy Checker

Determinacy Checker:

! 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_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(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_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),_84889,[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'),_54615,[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),_47661,[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),_45997,[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(preferences) does not exist
! goal: absolute_file_name(probsrc(preferences),_37169,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(debug) does not exist
! goal: absolute_file_name(probsrc(debug),_37569,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file covsrc(coverage_tools_annotations) does not exist
! goal: absolute_file_name(covsrc(coverage_tools_annotations),_38779,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_waitflags.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_38637,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(specfile) does not exist
! goal: absolute_file_name(probsrc(specfile),_39037,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(state_space_exploration_modes) does not exist
! goal: absolute_file_name(probsrc(state_space_exploration_modes),_39437,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(translate) does not exist
! goal: absolute_file_name(probsrc(translate),_39837,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_state_model_check) does not exist
! goal: absolute_file_name(probsrc(b_state_model_check),_40237,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bmachine) does not exist
! goal: absolute_file_name(probsrc(bmachine),_40637,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_interpreter) does not exist
! goal: absolute_file_name(probsrc(b_interpreter),_41037,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_trace_checking) does not exist
! goal: absolute_file_name(probsrc(b_trace_checking),_41437,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_41837,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! 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(no_wd_checking,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(clpfd_interface) does not exist
! goal: absolute_file_name(probsrc(clpfd_interface),_199895,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/typing_tools.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_195053,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_freetypes.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file chrsrc(chr_integer_inequality) does not exist
! goal: absolute_file_name(chrsrc(chr_integer_inequality),_194485,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/clpfd_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_207289,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_records.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file prob_rewrite_rules(b_ast_cleanup_rewrite_rules) does not exist
! goal: absolute_file_name(prob_rewrite_rules(b_ast_cleanup_rewrite_rules),_207001,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_ast_cleanup.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_250367,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pragmas.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(module_information) does not exist
! goal: absolute_file_name(probsrc(module_information),_251747,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine_static_checks.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_state_model_check) does not exist
! goal: absolute_file_name(probsrc(b_state_model_check),_252369,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_read_write_info.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'),_264623,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/state_space.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(external_functions_reals) does not exist
! goal: absolute_file_name(extrasrc(external_functions_reals),_263859,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(external_functions_svg) does not exist
! goal: absolute_file_name(extrasrc(external_functions_svg),_263859,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.pl')])
! Existence error in user:check_arithmetic_function/1
! procedure user:check_arithmetic_function/1 does not exist
! goal: user:check_arithmetic_function(log(2,4))
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(preferences) does not exist
! goal: absolute_file_name(probsrc(preferences),_264481,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_z.pl')])
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(atts))
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_265475,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_strings.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_freetypes) does not exist
! goal: absolute_file_name(probsrc(kernel_freetypes),_259213,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.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),_250367,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine_static_checks.pl')])
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(logarr))
! Existence error in argument 1 of absolute_file_name/3
! file probcspsrc(haskell_csp) does not exist
! goal: absolute_file_name(probcspsrc(haskell_csp),_252941,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xtl_interface.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_247233,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine_eventb.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_246945,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_machine_hierarchy.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_216547,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_210143,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/parsercall.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bmachine_eventb) does not exist
! goal: absolute_file_name(probsrc(bmachine_eventb),_200175,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/btypechecker.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(closures) does not exist
! goal: absolute_file_name(probsrc(closures),_200175,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/memoization.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_use_timer,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(custom_explicit_sets) does not exist
! goal: absolute_file_name(probsrc(custom_explicit_sets),_194197,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_compiler.pl')])
! 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_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_watch_flag,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_reals) does not exist
! goal: absolute_file_name(probsrc(kernel_reals),_200463,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_interpreter_check.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(clpfd_interface) does not exist
! goal: absolute_file_name(probsrc(clpfd_interface),_194769,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_equality.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_wd_checking,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,xxxtrue)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_169053,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/custom_explicit_sets.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_lists) does not exist
! goal: absolute_file_name(probsrc(tools_lists),_164921,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_tools.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_watch_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_waitflags) does not exist
! goal: absolute_file_name(probsrc(kernel_waitflags),_165067,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/runtime_profiler.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_waitflags) does not exist
! goal: absolute_file_name(probsrc(kernel_waitflags),_162923,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/delay.pl')])
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(atts))
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(avl_tools) does not exist
! goal: absolute_file_name(probsrc(avl_tools),_146157,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bsets_clp.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'),_146157,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_reals.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_139757,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_interpreter.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'),_139903,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/succeed_max.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_139903,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/value_persistance.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(btypechecker) does not exist
! goal: absolute_file_name(probsrc(btypechecker),_127677,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/specfile.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(gensym) does not exist
! goal: absolute_file_name(probsrc(gensym),_107641,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/translate.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(custom_explicit_sets) does not exist
! goal: absolute_file_name(probsrc(custom_explicit_sets),_78659,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bsyntaxtree.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('random_permutations/random_permutations') does not exist
! goal: absolute_file_name(extension('random_permutations/random_permutations'),_80807,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/fd_utils_clpfd.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),_78805,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/partition_detection.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'),_42713,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_objects.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(state_space) does not exist
! goal: absolute_file_name(probsrc(state_space),_42571,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('plspec/plspec/plspec_core') does not exist
! goal: absolute_file_name(extension('plspec/plspec/plspec_core'),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/tcltk_interface.pl')])

Name: true
Name: assertz/1
Name: avl_store/4	Module: foo_error
Name: =/2
Name: ->/3
Name: empty_avl/1	Module: foo_error
Name: specialized_inv/2	Module: foo_error
Name: retract/1
Name: invariant_violated/1	Module: foo_error
Name: not/1
Name: invariant_still_to_be_checked/1	Module: foo_error
Name: b_operation_preserves_invariant/2	Module: foo_error

Name: add_trans_id/5	Module: tcltk_interface
Name: true
Name: transition/4	Module: foo_error
Name: ->/3
Name: get_start_transition_term/2	Module: tcltk_interface
Name: clear_span/2	Module: haskell_csp_analyzer
Name: add_csp_process_id/2	Module: tcltk_interface
Name: animatable_process_without_arguments/1	Module: haskell_csp
Name: ->/2
Name: !

Name: tcltk_explore_csp_process/2	Module: tcltk_interface
Name: add_csp_process_id_normalized/4	Module: tcltk_interface
Name: run_assertion_check/3	Module: tcltk_interface

Name: add_csp_general_process_id/2	Module: tcltk_interface
Name: tcltk_csp_in_situ_refinement/5	Module: tcltk_interface

Name: add_error_fail/3	Module: foo_error
Name: add_trans_id/5	Module: tcltk_interface
Name: get_start_expr/2	Module: xtl_interface
Name: =/2
Name: transition/4	Module: foo_error
Name: ->/3
Name: get_start_transition_term/2	Module: tcltk_interface
Name: call/2

Name: add_csp_general_process_id/2	Module: tcltk_interface
Name: compile_body/5	Module: haskell_csp_analyzer
Name: clear_span/2	Module: haskell_csp_analyzer

Name: retractall/1
Name: assertz/1
Name: add_message/3	Module: foo_error
Name: \=/2
Name: =/2
Name: ->/3
Name: add_warning/3	Module: foo_error
Name: true
Name: history/1	Module: foo_error
Name: retract/1

Name: update_history_from_trace/1	Module: tcltk_interface
Name: tcltk_goto_state/2	Module: tcltk_interface

Name: true
Name: add_additional_destination_infos/3	Module: tcltk_interface
Name: not_all_transitions_added/1	Module: foo_error
Name: b_or_z_mode	Module: foo_error
Name: \=/2
Name: ->/3
Name: mark_operation_as_covered/1	Module: foo_error
Name: add_internal_error/2	Module: foo_error
Name: store_transition_infos/2	Module: foo_error
Name: store_transition/4	Module: foo_error
Name: any_transition/3	Module: foo_error
Name: preference/2	Module: preferences
Name: transition/4	Module: foo_error
Name: operation_not_yet_covered/1	Module: foo_error
Name: not/1
Name: =/2
Name: get_id_of_node_and_add_if_required_with_skip_check/6	Module: tcltk_interface
Name: get_operation_internal_name/2	Module: foo_error

Name: tcltk_add_new_transition_transid/6	Module: tcltk_interface
Name: add_trans_id_with_infos/8	Module: tcltk_interface

Name: fail
Name: add_trans_id_with_infos/8	Module: tcltk_interface
Name: partial_trans/4	Module: foo_error
Name: any_transition/3	Module: foo_error
Name: not/1

Name: add_csp_process_id1/3	Module: tcltk_interface
Name: add_csp_general_process_id/2	Module: tcltk_interface
Name: exec_aux/9	Module: visb_visualiser
Name: prob2_exec_custom_aux/4	Module: prob2_interface
Name: prob2_execute_custom_operation_with_predicate_aux/5	Module: prob2_interface
Name: execute_custom_operation/4	Module: eclipse_interface
Name: b_trans_one_solution_with_pred2/6	Module: tcltk_interface
Name: tcltk_clear_state_space_and_refocus_to_current_state/0	Module: tcltk_interface

Name: add_new_transition_transid_with_infos/7	Module: tcltk_interface
Name: nl
Name: print_goal/1	Module: tools_printing
Name: add_error/3	Module: foo_error
Name: true
Name: =/2
Name: ->/3

Name: add_trans_id_with_infos/8	Module: tcltk_interface
Name: specfile_trans/6	Module: foo_error
Name: extract_infos_from_prepared_state/2	Module: foo_error

Name: add_transitions_fail_loop2/3	Module: tcltk_interface
Name: add_transition_timeout/5	Module: pge_algo

Name: call_cleanup/2
Name: enter_new_error_scope/2	Module: foo_error

Name: clear_error_context	Module: foo_error
Name: fail
Name: true
Name: assert_time_out_for_node/3	Module: foo_error
Name: var/1
Name: ->/3
Name: print_message/1	Module: foo_error
Name: =/2
Name: max_reached/1	Module: succeed_max
Name: not/1
Name: nonvar/1
Name: ==/2
Name: time_out_with_enum_warning_for_findall_in_current_error_scope/4	Module: foo_error
Name: set_error_context/1	Module: foo_error
Name: profile_failure_driven_loop/2	Module: runtime_profiler
Name: possible_trans_name_for_successors/2	Module: tcltk_interface

Name: assert_temp_typed_predicate/1	Module: bmachine
Name: inline_prob_deferred_set_elements_into_bexpr/2	Module: b_global_sets

Name: b_compute_expression_nowf/6	Module: b_interpreter
Name: extend_state_with_probids_and_lets/2	Module: eval_let_store

Name: compute_for_dot/3	Module: tcltk_interface
Name: evaluate_bexpr_over_state/7	Module: tcltk_interface
Name: eval_string_in_cur_state/3	Module: tcltk_interface
Name: print_seq_chart_transition/2	Module: uml_generator

Name: store_updates_and_normalise/3	Module: store
Name: ground_wait_flags/1	Module: kernel_waitflags
Name: b_execute_top_level_statement/7	Module: foo_error
Name: init_wait_flags_with_call_stack/2	Module: kernel_waitflags
Name: extend_state_with_probids_and_lets/2	Module: eval_let_store

Name: cbc_constraint_find_static_assertion_violation/2	Module: tcltk_interface
Name: tcltk_constraint_based_check_op2/3	Module: tcltk_interface
Name: tcltk_constraint_find_deadlock_state/1	Module: tcltk_interface
Name: tcltk_constraint_find_maximal_valid_state/0	Module: tcltk_interface
Name: tcltk_constraint_find_dynamic_assertion_violation/0	Module: tcltk_interface
Name: tcltk_constraint_find_valid_state_with_pred/3	Module: tcltk_interface
Name: tcltk_constraint_find_deadlock_state_with_goal/2	Module: tcltk_interface
Name: tcltk_constraint_find_valid_state/0	Module: tcltk_interface

Name: =/2
Name: call/4
Name: state_corresponds_to_initialised_b_machine/2	Module: foo_error
Name: ->/3
Name: visited_expression/2	Module: state_space
Name: format/2
Name: get_operation_name/2	Module: specfile
Name: nl
Name: print/1
Name: !

Name: state_error/3	Module: foo_error
Name: current_state_id/1	Module: foo_error
Name: get_inner_span/2	Module: tcltk_interface
Name: !
Name: last_detailed_error/3	dynamic predicate

Name: =/2
Name: tcltk_add_cbc_state/2	Module: tcltk_interface
Name: ->/3
Name: call_cbc_command/1	Module: tcltk_interface

prob_prolog/src/tcltk_interface.pl

Modules

Predicates of tcltk_interface

Module Information

Dynamic Predicates: prev_randomise_enumeration_order/1 current_candidate_options/1 cached_state_as_strings/2 last_detailed_error/3 saved_forward_history/2 cbc_inv_error_found/2 nr_cbc_sols/1 resetable_node/1 find_flag/2 non_det_constant/1 eval_elapsed_time/1 nr_csp_process_state/1

3423 Lines

381 Predicates

199 Exports

94 specified Imports

Predicates:

Name: check_csp_assertion/3	Module: prob2_interface
Name: treat_csp_ass/6	Module: tcltk_interface
Name: tcltk_check_csp_assertion/5	Module: tcltk_interface

Name: peel2/2	Module: tcltk_interface
Name: assertz/1
Name: RECURSIVE_CALL/4	Module: tcltk_interface
Name: =/2
Name: ->/3

Name: is_det_controller_state/2	Module: tcltk_interface
Name: is_valid_controller_state/2	Module: tcltk_interface
Name: relative_deadlock_freedom/2	Module: tcltk_interface

Name: check_invariantKO/3	Module: tcltk_interface
Name: animation_mode/1	Module: foo_error

Name: force_check_invariantKO/2	Module: tcltk_interface
Name: assertz/1
Name: preference/2	Module: preferences
Name: ->/3
Name: state_corresponds_to_initialised_b_machine/1	Module: foo_error
Name: set_invariant_checked/1	Module: foo_error
Name: !
Name: invariant_violated/1	Module: foo_error

Name: compute_all_transitions_if_necessary/2	Module: tcltk_interface
Name: compute_transitions/4	Module: model_checker

Name: exec_aux/9	Module: visb_visualiser
Name: generate_trace/4	Module: trace_generator
Name: ENABLED_TRANSITION/3	Module: external_functions
Name: compute_state_information_if_necessary/1	Module: tcltk_interface
Name: state_space_children/2	Module: tcltk_tree_inspector
Name: non_det_transition/4	Module: external_functions
Name: compute_all_transitions_if_necessary/1	Module: tcltk_interface
Name: ENABLED/3	Module: external_functions
Name: compute_all_transitions_if_necessary/0	Module: tcltk_interface
Name: non_det_output_transition2/2	Module: external_functions
Name: compute_transitions_if_necessary/1	Module: state_space
Name: perform_single_replay_step_statespace/6	Module: b_intelligent_trace_replay

Name: true
Name: clear_context_state	Module: foo_error
Name: compute_all_transitions/2	Module: tcltk_interface
Name: compute_invariant_if_necessary_and_requested/2	Module: tcltk_interface
Name: ==/2
Name: ->/3
Name: prepare_state_for_specfile_trans/3	Module: foo_error
Name: visited_expression/2	Module: state_space
Name: set_context_state/1	Module: foo_error
Name: retract_open_node/1	Module: foo_error

Name: RECURSIVE_CALL/3	Module: tcltk_interface
Name: b_compute_expression_with_prob_ids/3	Module: tcltk_interface
Name: format/2
Name: translate_bexpression_with_limit/3	Module: translate
Name: !
Name: get_texpr_expr/2	Module: foo_error

Name: compute_invariant_if_necessary/2	Module: tcltk_interface
Name: open_search_do_one_node/16	Module: model_checker