Dynamic Predicates: junit_mode/1 file_loaded/2 execute_timeout_occurred/0 max_walltime/3 assertion_counter/1 dot_file_prefix/1 dot_file_number/1 probcli_time_stamp/1 loaded_main_file/2 eval_result/2 last_repl_error/2 current_repl_input_stream/2 trace_eval/0 expected_error_occurred/1 error_did_not_occur/1 current_probcli_command/1 accumulated_infos/3 option/1

4288 Lines

382 Predicates

Imported Modules: module_information debugging_calls tcltk_interface eclipse_interface prob_socketserver debug preferences basic_unit_tests error_manager zmq/master/master zmq/worker/worker ltsmin/ltsmin system codesio logger specfile kodkod_test hit_profiler counter/counter predicate_evaluator refinement_checker version eval_strings table_tools lists

0 Exports

174 specified Imports

Imports	Exports
Name: startup_prob/0 Module: prob_startup Name: string_concatenate/3 Module: tools Name: arg_is_number/2 Module: tools Name: print_error/1 Module: tools_printing Name: start_animation/0 Module: prob2_interface Name: is_initialised_state/1 Module: prob2_interface Name: set_eclipse_preference/2 Module: prob2_interface Name: update_preferences_from_spec/1 Module: prob2_interface Name: load_cspm_spec_from_cspm_file/1 Module: prob2_interface Name: compute_the_coverage/5 Module: coverage_statistics Name: set_storage_directory/1 Module: value_persistance Name: unset_storage_directory/0 Module: value_persistance Name: check_default_trace_for_specfile/1 Module: b_trace_checking Name: tcltk_check_state_sequence_from_file/1 Module: b_trace_checking Name: tcltk_save_history_as_trace_file/2 Module: b_trace_checking Name: file_exists/1 Module: file_systems Name: run_typecheck_testcase/2 Module: test_typechecker Name: disable_interaction_on_errors/0 Module: self_check Name: perform_self_check/2 Module: self_check Name: turn_off_run_time_type_checks/0 Module: self_check Name: turn_on_run_time_type_checks/0 Module: self_check Name: b_write_machine_representation_to_file/2 Module: bmachine Name: full_b_machine/1 Module: bmachine Name: b_write_eventb_machine_to_classicalb_to_file/1 Module: bmachine Name: set_cspm_main_process/1 Module: xtl_interface Name: is_dot_command/1 Module: meta_interface Name: call_dot_command/3 Module: meta_interface Name: is_dot_command_for_expr/1 Module: meta_interface Name: call_dot_command_for_expr/4 Module: meta_interface Name: command_description/3 Module: meta_interface Name: test_predicate_analysis/0 Module: predicate_analysis Name: write_history_to_file/2 Module: b_show_history Name: write_values_to_file/1 Module: b_show_history Name: write_all_values_to_dir/1 Module: b_show_history Name: write_history_to_user_output/1 Module: b_show_history Name: write_all_deadlocking_paths_to_xml/1 Module: sap Name: test_generation_by_xml_description/1 Module: sap Name: run_disprover_on_all_pos/1 Module: disprover_test_runner Name: load_po_file/1 Module: disprover_test_runner Name: print_disprover_stats/0 Module: disprover_test_runner Name: set_disprover_timeout/1 Module: disprover_test_runner Name: set_disprover_options/1 Module: disprover_test_runner Name: reset_disprover_timeout/0 Module: disprover_test_runner Name: process_latex_file/2 Module: latex_processor Name: safe_time_out/3 Module: tools_meta Name: set_junit_dir/1 Module: junit_tests Name: print_junit/2 Module: junit_tests Name: create_junit_result/6 Module: junit_tests Name: get_options/4 Module: tools Name: get_options/5 Module: tools Name: store_virtual_event/1 Module: eventhandling Name: b_set_initial_machine/0 Module: bmachine Name: safe_absolute_file_name/2 Module: tools Name: safe_absolute_file_name/3 Module: tools Name: show_cache_file_contents/0 Module: value_persistance Name: show_cache_file_constants/0 Module: value_persistance Name: print_op_cache/0 Module: b_operation_cache Name: reset_memo_with_statistics/0 Module: memoization Name: not_all_transitions_added/1 Module: state_space Name: not_invariant_checked/1 Module: state_space Name: current_expression/2 Module: state_space Name: count_occurences/2 Module: tools_lists Name: start_ms_timer/1 Module: tools Name: stop_ms_timer/1 Module: tools Name: stop_ms_timer/2 Module: tools Name: stop_ms_timer_with_msg/2 Module: tools Name: b_top_level_operation/1 Module: bmachine Name: ajoin/2 Module: tools_strings Name: ajoin_with_sep/3 Module: tools_strings Name: reset_side_effect_occurred/0 Module: external_functions Name: side_effect_occurred/1 Module: external_functions Name: profile_single_call/3 Module: runtime_profiler Name: b_machine_has_constants/0 Module: bmachine Name: b_is_constant/1 Module: bmachine Name: b_get_invariant_from_machine/1 Module: bmachine Name: b_specialized_invariant_for_op/2 Module: bmachine Name: b_machine_has_constants/0 Module: bmachine Name: get_assertions_from_machine/2 Module: bmachine Name: b_get_machine_goal/1 Module: bmachine Name: b_get_assertions/3 Module: bmachine Name: tcltk_debug_properties/3 Module: predicate_debugger Name: current_state_corresponds_to_setup_constants_b_machine/0 Module: state_space Name: system_call/4 Module: system_call Name: csv_to_trace/3 Module: ltsmin/ltsmin_trace Name: b_machine_name/1 Module: bmachine Name: get_modulename_filename/2 Module: tools Name: get_csp_assertions_as_string/2 Module: haskell_csp Name: parse_and_load_cspm_file_into_specific_pl_file/2 Module: haskell_csp Name: evaluate_csp_expression/2 Module: haskell_csp Name: evaluate_csp_expression/3 Module: haskell_csp Name: write_lines_to_file/2 Module: tools_files Name: pretty_print_coverage_information_to_file/1 Module: coverage_statistics Name: platform_is_64_bit/0 Module: tools Name: b_machine_statistics/2 Module: bmachine Name: b_get_main_filename/1 Module: bmachine Name: get_tail_filename/2 Module: tools Name: term_hash/2 Module: terms Name: state_error/3 Module: state_space Name: invariant_violated/1 Module: state_space Name: time_out_for_invariant/1 Module: state_space Name: time_out_for_assertions/1 Module: state_space Name: time_out_for_node/3 Module: state_space Name: get_filename_extension/2 Module: tools Name: check_java_version/2 Module: parsercall Name: get_parser_version/1 Module: parsercall Name: ensure_console_parser_launched/0 Module: parsercall Name: get_parser_version/1 Module: parsercall Name: get_java_command_path/1 Module: parsercall Name: get_java_fullversion/1 Module: parsercall Name: compile_time_flags/1 Module: compile_time_flags Name: relevant_prolog_flags/1 Module: compile_time_flags Name: set_depth_breadth_first_mode/1 Module: state_space_exploration_modes Name: convert_cli_arg/2 Module: tools_strings Name: model_checking_is_incomplete/6 Module: model_checker Name: current_state_id/1 Module: state_space Name: tcltk_constraint_based_check/2 Module: tcltk_interface Name: tcltk_constraint_based_check_with_timeout/2 Module: tcltk_interface Name: tcltk_constraint_find_deadlock_state_with_goal/3 Module: tcltk_interface Name: tcltk_cbc_find_trace/4 Module: tcltk_interface Name: tcltk_cbc_refinement_check/2 Module: tcltk_interface Name: b_is_operation_name/1 Module: bmachine Name: cbc_find_redundant_invariants/2 Module: b_state_model_check Name: predicate_uses_unfixed_deferred_set/2 Module: solver_interface Name: unfixed_typed_id_in_list/3 Module: solver_interface Name: get_texpr_id/2 Module: bsyntaxtree Name: pretty_type/2 Module: translate Name: safe_open_file/4 Module: tools_io Name: infeasible_operation_cache/1 Module: enabling_analysis Name: explore_and_generate_testcases/7 Module: sap Name: cbc_gen_test_cases_from_string/5 Module: sap Name: tcl_get_stored_test_cases/1 Module: sap Name: print_bexpr/1 Module: translate Name: print_error/1 Module: tools_printing Name: format_error/2 Module: tools_printing Name: ensure_console_parser_launched/0 Module: parsercall Name: interruptable_call/1 Module: user_interrupts Name: reset_terminal_colour/1 Module: tools_printing Name: print_red/1 Module: tools_printing Name: print_green/1 Module: tools_printing Name: safe_open_file/4 Module: tools_io Name: format_with_colour/4 Module: tools_printing Name: toggle_perfmessages/0 Module: performance_messages Name: show_dot_file/1 Module: tools_commands Name: show_ps_file/1 Module: tools_commands Name: gen_dot_output/4 Module: tools_commands Name: transition/4 Module: state_space Name: edit_file/2 Module: tools_commands Name: extract_file_line_col/6 Module: error_manager Name: source_code_for_identifier/6 Module: bmachine Name: get_machine_identifiers/2 Module: prob2_interface Name: b_global_set/1 Module: b_global_sets Name: is_b_global_constant/3 Module: b_global_sets Name: get_machine_identifier_names/7 Module: b_machine_hierarchy Name: b_get_properties_from_machine/1 Module: bmachine Name: predicate_components/2 Module: bsyntaxtree Name: lookup_value_for_existing_id/3 Module: store Name: abstract_constant/2 Module: b_machine_hierarchy Name: set_unicode_mode/0 Module: translate Name: unset_unicode_mode/0 Module: translate Name: truncate_atom/3 Module: tools_strings Name: random/3 Module: random Name: visited_expression/2 Module: state_space Name: b_machine_has_constants_or_properties/0 Module: bmachine Name: tcltk_cbc_enabling_analysis/1 Module: enabling_analysis Name: print_enable_table/1 Module: enabling_analysis Name: is_timeout_enabling_result/1 Module: enabling_analysis Name: feasible_operation_with_timeout/3 Module: enabling_analysis Name: tcltk_read_write_matrix/1 Module: b_read_write_info Name: max_tagged_integer/1 Module: tools Name: print_runtime_profile/0 Module: runtime_profiler Name: print_source_profile/0 Module: source_profiler Name: print_memo_profile/0 Module: memoization Name: setrand/1 Module: random Name: announce_event/1 Module: eventhandling

Imports

Exports

Name: startup_prob/0

Module: prob_startup

Name: string_concatenate/3

Module: tools

Name: arg_is_number/2

Module: tools

Name: print_error/1

Module: tools_printing

Name: start_animation/0

Module: prob2_interface

Name: is_initialised_state/1

Module: prob2_interface

Name: set_eclipse_preference/2

Module: prob2_interface

Name: update_preferences_from_spec/1

Module: prob2_interface

Name: load_cspm_spec_from_cspm_file/1

Module: prob2_interface

Name: compute_the_coverage/5

Module: coverage_statistics

Name: set_storage_directory/1

Module: value_persistance

Name: unset_storage_directory/0

Module: value_persistance

Name: check_default_trace_for_specfile/1

Module: b_trace_checking

Name: tcltk_check_state_sequence_from_file/1

Module: b_trace_checking

Name: tcltk_save_history_as_trace_file/2

Module: b_trace_checking

Name: file_exists/1

Module: file_systems

Name: run_typecheck_testcase/2

Module: test_typechecker

Name: disable_interaction_on_errors/0

Module: self_check

Name: perform_self_check/2

Module: self_check

Name: turn_off_run_time_type_checks/0

Module: self_check

Name: turn_on_run_time_type_checks/0

Module: self_check

Name: b_write_machine_representation_to_file/2

Module: bmachine

Name: full_b_machine/1

Module: bmachine

Name: b_write_eventb_machine_to_classicalb_to_file/1

Module: bmachine

Name: set_cspm_main_process/1

Module: xtl_interface

Name: is_dot_command/1

Module: meta_interface

Name: call_dot_command/3

Module: meta_interface

Name: is_dot_command_for_expr/1

Module: meta_interface

Name: call_dot_command_for_expr/4

Module: meta_interface

Name: command_description/3

Module: meta_interface

Name: test_predicate_analysis/0

Module: predicate_analysis

Name: write_history_to_file/2

Module: b_show_history

Name: write_values_to_file/1

Module: b_show_history

Name: write_all_values_to_dir/1

Module: b_show_history

Name: write_history_to_user_output/1

Module: b_show_history

Name: write_all_deadlocking_paths_to_xml/1

Module: sap

Name: test_generation_by_xml_description/1

Module: sap

Name: run_disprover_on_all_pos/1

Module: disprover_test_runner

Name: load_po_file/1

Module: disprover_test_runner

Name: print_disprover_stats/0

Module: disprover_test_runner

Name: set_disprover_timeout/1

Module: disprover_test_runner

Name: set_disprover_options/1

Module: disprover_test_runner

Name: reset_disprover_timeout/0

Module: disprover_test_runner

Name: process_latex_file/2

Module: latex_processor

Name: safe_time_out/3

Module: tools_meta

Name: set_junit_dir/1

Module: junit_tests

Name: print_junit/2

Module: junit_tests

Name: create_junit_result/6

Module: junit_tests

Name: get_options/4

Module: tools

Name: get_options/5

Module: tools

Name: store_virtual_event/1

Module: eventhandling

Name: b_set_initial_machine/0

Module: bmachine

Name: safe_absolute_file_name/2

Module: tools

Name: safe_absolute_file_name/3

Module: tools

Name: show_cache_file_contents/0

Module: value_persistance

Name: show_cache_file_constants/0

Module: value_persistance

Name: print_op_cache/0

Module: b_operation_cache

Name: reset_memo_with_statistics/0

Module: memoization

Name: not_all_transitions_added/1

Module: state_space

Name: not_invariant_checked/1

Module: state_space

Name: current_expression/2

Module: state_space

Name: count_occurences/2

Module: tools_lists

Name: start_ms_timer/1

Module: tools

Name: stop_ms_timer/1

Module: tools

Name: stop_ms_timer/2

Module: tools

Name: stop_ms_timer_with_msg/2

Module: tools

Name: b_top_level_operation/1

Module: bmachine

Name: ajoin/2

Module: tools_strings

Name: ajoin_with_sep/3

Module: tools_strings

Name: reset_side_effect_occurred/0

Module: external_functions

Name: side_effect_occurred/1

Module: external_functions

Name: profile_single_call/3

Module: runtime_profiler

Name: b_machine_has_constants/0

Module: bmachine

Name: b_is_constant/1

Module: bmachine

Name: b_get_invariant_from_machine/1

Module: bmachine

Name: b_specialized_invariant_for_op/2

Module: bmachine

Name: b_machine_has_constants/0

Module: bmachine

Name: get_assertions_from_machine/2

Module: bmachine

Name: b_get_machine_goal/1

Module: bmachine

Name: b_get_assertions/3

Module: bmachine

Name: tcltk_debug_properties/3

Module: predicate_debugger

Name: current_state_corresponds_to_setup_constants_b_machine/0

Module: state_space

Name: system_call/4

Module: system_call

Name: csv_to_trace/3

Module: ltsmin/ltsmin_trace

Name: b_machine_name/1

Module: bmachine

Name: get_modulename_filename/2

Module: tools

Name: get_csp_assertions_as_string/2

Module: haskell_csp

Name: parse_and_load_cspm_file_into_specific_pl_file/2

Module: haskell_csp

Name: evaluate_csp_expression/2

Module: haskell_csp

Name: evaluate_csp_expression/3

Module: haskell_csp

Name: write_lines_to_file/2

Module: tools_files

Name: pretty_print_coverage_information_to_file/1

Module: coverage_statistics

Name: platform_is_64_bit/0

Module: tools

Name: b_machine_statistics/2

Module: bmachine

Name: b_get_main_filename/1

Module: bmachine

Name: get_tail_filename/2

Module: tools

Name: term_hash/2

Module: terms

Name: state_error/3

Module: state_space

Name: invariant_violated/1

Module: state_space

Name: time_out_for_invariant/1

Module: state_space

Name: time_out_for_assertions/1

Module: state_space

Name: time_out_for_node/3

Module: state_space

Name: get_filename_extension/2

Module: tools

Name: check_java_version/2

Module: parsercall

Name: get_parser_version/1

Module: parsercall

Name: ensure_console_parser_launched/0

Module: parsercall

Name: get_parser_version/1

Module: parsercall

Name: get_java_command_path/1

Module: parsercall

Name: get_java_fullversion/1

Module: parsercall

Name: compile_time_flags/1

Module: compile_time_flags

Name: relevant_prolog_flags/1

Module: compile_time_flags

Name: set_depth_breadth_first_mode/1

Module: state_space_exploration_modes

Name: convert_cli_arg/2

Module: tools_strings

Name: model_checking_is_incomplete/6

Module: model_checker

Name: current_state_id/1

Module: state_space

Name: tcltk_constraint_based_check/2

Module: tcltk_interface

Name: tcltk_constraint_based_check_with_timeout/2

Module: tcltk_interface

Name: tcltk_constraint_find_deadlock_state_with_goal/3

Module: tcltk_interface

Name: tcltk_cbc_find_trace/4

Module: tcltk_interface

Name: tcltk_cbc_refinement_check/2

Module: tcltk_interface

Name: b_is_operation_name/1

Module: bmachine

Name: cbc_find_redundant_invariants/2

Module: b_state_model_check

Name: predicate_uses_unfixed_deferred_set/2

Module: solver_interface

Name: unfixed_typed_id_in_list/3

Module: solver_interface

Name: get_texpr_id/2

Module: bsyntaxtree

Name: pretty_type/2

Module: translate

Name: safe_open_file/4

Module: tools_io

Name: infeasible_operation_cache/1

Module: enabling_analysis

Name: explore_and_generate_testcases/7

Module: sap

Name: cbc_gen_test_cases_from_string/5

Module: sap

Name: tcl_get_stored_test_cases/1

Module: sap

Name: print_bexpr/1

Module: translate

Name: print_error/1

Module: tools_printing

Name: format_error/2

Module: tools_printing

Name: ensure_console_parser_launched/0

Module: parsercall

Name: interruptable_call/1

Module: user_interrupts

Name: reset_terminal_colour/1

Module: tools_printing

Name: print_red/1

Module: tools_printing

Name: print_green/1

Module: tools_printing

Name: safe_open_file/4

Module: tools_io

Name: format_with_colour/4

Module: tools_printing

Name: toggle_perfmessages/0

Module: performance_messages

Name: show_dot_file/1

Module: tools_commands

Name: show_ps_file/1

Module: tools_commands

Name: gen_dot_output/4

Module: tools_commands

Name: transition/4

Module: state_space

Name: edit_file/2

Module: tools_commands

Name: extract_file_line_col/6

Module: error_manager

Name: source_code_for_identifier/6

Module: bmachine

Name: get_machine_identifiers/2

Module: prob2_interface

Name: b_global_set/1

Module: b_global_sets

Name: is_b_global_constant/3

Module: b_global_sets

Name: get_machine_identifier_names/7

Module: b_machine_hierarchy

Name: b_get_properties_from_machine/1

Module: bmachine

Name: predicate_components/2

Module: bsyntaxtree

Name: lookup_value_for_existing_id/3

Module: store

Name: abstract_constant/2

Module: b_machine_hierarchy

Name: set_unicode_mode/0

Module: translate

Name: unset_unicode_mode/0

Module: translate

Name: truncate_atom/3

Module: tools_strings

Name: random/3

Module: random

Name: visited_expression/2

Module: state_space

Name: b_machine_has_constants_or_properties/0

Module: bmachine

Name: tcltk_cbc_enabling_analysis/1

Module: enabling_analysis

Name: print_enable_table/1

Module: enabling_analysis

Name: is_timeout_enabling_result/1

Module: enabling_analysis

Name: feasible_operation_with_timeout/3

Module: enabling_analysis

Name: tcltk_read_write_matrix/1

Module: b_read_write_info

Name: max_tagged_integer/1

Module: tools

Name: print_runtime_profile/0

Module: runtime_profiler

Name: print_source_profile/0

Module: source_profiler

Name: print_memo_profile/0

Module: memoization

Name: setrand/1

Module: random

Name: announce_event/1

Module: eventhandling

Predicates

Predicates:

accumulate_infos/2

add_eval_result/1

add_model_checking_warnings/4

add_vacuous_invariant/1

allow_filter_unused_constants/0

animate_machine/0

animate_machine2/0

animation_mode_does_not_support_animation/1

append_assertion/1

assert_all_options/1

assert_option/1

atom_contains_codes/2

available_commands/1

browse/0

browse_all_machines/1

browse_machine/1

call_probcli_option/1

cbc_assertions/2

cbc_check/1

cbc_deadlock_check/1

cbc_redundant_invariants/1

cbc_refinement/0

cbc_sequence/3

cbc_test_case_generation/3

check_abstract_constants/0

check_all_expected_errors_occurred/1

check_complete/0

check_complete_operation_coverage/0

check_deadlock_fail/1

check_loaded_not_empty/1

check_model_result/2

check_parser_version/0

check_partial_trans/2

check_ref_result/1

check_required_infos/3

cli_add_additional_property/1

cli_animateOperationNr/3

cli_assertions_ok/2

cli_checkAssertion/4

cli_check_assertions/2

cli_check_assertions/3

cli_check_csp_assertion/2

cli_check_goal/0

cli_check_properties/0

cli_check_properties/1

cli_check_scc_for_ltl_formula/2

cli_check_statespace_hash/2

cli_computeOperations/1

cli_csp_get_assertions/0

cli_csp_in_situ_refinement_check/4

cli_csp_translate_to_file/1

cli_ctl_model_check/3

cli_eval_csp_expression/1

cli_execute/3

cli_execute_add_virtual_transition/3

cli_get_coverage_information/1

cli_get_min_max_coverage/1

cli_ltl_model_check/3

cli_mc/1

cli_print_all_values/1

cli_print_history/1

cli_print_junit_results/1

cli_print_machine_statistics/0

cli_print_pred_info/1

cli_print_statistics/0

cli_print_values/1

cli_process_loaded_file/2

cli_process_loaded_file_afer_start_animation/1

cli_random_animate/2

cli_random_animate/3

cli_set_empty_machine/0

cli_set_goal/1

cli_set_options/2

cli_set_searchscope/1

cli_show_coverage/2

cli_show_coverage/4

cli_show_help/2

cli_show_variable_coverage/1

cli_start_animation/1

cli_start_initialisation/1

cli_start_logging/5

cli_start_mc_with_tlc/0

cli_start_model_check/2

cli_start_refinement_check/4

cli_start_selfcheck/0

cli_start_socketserver/1

cli_start_sym_mc_with_lts/1

cli_start_trace_check/1

cli_start_trace_state_check/1

cli_symbolic_model_check/1

close_repl_input_stream/1

command_option/1

compare_kodkod_performance1/3

computeOperations_for_root_required/0

constraint_based_check/1

construct_and_execute_tlc_command/1

convert_dash_to_underscore/2

count_assertions/3

coverage/1

create_state_error_description/2

definite_error_occurred/0

display_match/3

display_match/4

do_det_checking/0

do_enabling_analysis_csv/2

do_feasibility_analysis/2

do_not_execute_automatically/1

do_one_gui_event/0

dot_command/2

dot_command_for_expr/4

error_occurred_with_msg/2

error_occurred_with_msg/3

eval_probcli_repl_line/1

eval_string_or_file/5

evaluate_expressions/1

evaluate_from_commandline/0

generate_read_write_matrix/1

generate_time_stamp/2

get_comma_or_space_separated_options/2

get_dot_file/2

get_error_category_and_type/3

get_error_or_warning_span/4

get_probcli_elapsed_walltime/2

get_quoted_atom/4

get_state_errors/1

get_state_space_errors/0

get_xml_add_description/2

go_cli_with_junit_check/1

handle_symbolic_model_check_result/1

help/0

if_option_set/2

if_option_set/3

if_option_set_loaded/3

if_options_set/2

ifm_option_set/2

ifm_option_set/3

ifm_option_set_loaded/3

initialise_required/0

irrelevant_xml_if_zero/1

irrelevant_xml_info/1

is_constant_binding/1

is_eventb_b/1

is_ws/1

just_assert_option/1

load_b_file_with_options/1

loaded_root_filename/1

logxml_write_ids/2

ltl_check_assertions/0

mcm_test_case_generation/4

memory_intensive_option/1

normalise_option_atom/2

normalise_pref_name/2

not_command_option/1

open_file_at_position/1

option_only_works_for_single_file/1

option_requires_all_properties/1

option_verbose/0

options_allow_start_without_file/0

parse_eval_command/3

perform/1

perform_random_init_after_setup_constants/0

perform_random_initialisation/0

perform_random_initialisation/1

perform_random_initialisation_if_necessary/1

perform_random_step/1

perform_random_step/4

perform_random_steps/2

perform_random_steps_aux/3

perform_symbolic_model_checking/2

portray_message/2

pracc/1

pred_eval_hook/5

pretty_print_internal_rep/3

pretty_print_internal_rep_to_B/1

print_accumulated_infos/1

print_bindings/1

print_cbc_stats/2

print_compile_time_flags/0

print_current_state/0

print_eval_command_help/1

print_probcli_error_non_strict/2

print_prolog_flags/0

print_property_partitions/0

print_repeats/2

print_repl_prompt/0

print_repl_prompt/1

print_repl_prompt_s/1

print_set/1

print_sets/0

print_short_version/0

print_state_silent/1

print_total_probcli_timer/0

prob_trimcore_silent/0

prob_trimcore_verbose/0

probcli_add_light_warning/2

probcli_startup/0

process_cbc_assertion_result/2

process_ltsmin_result/1

profile_statistics/0

profiling_on/0

recognised_cli_option/4

repl_multi_read_line/1

repl_multi_read_line_aux/3

reset_cli/0

reset_dot_file_number/0

reset_expected_error_occurred/0

set_current_probcli_command/1

set_dot_file_prefix/1

set_dot_file_prefix_if_option_set/1

set_junit_mode/1

set_new_random_seed/0

set_optional_errors/0

set_pref/2

set_prefs/0

set_random_seed_to_deterministic_start_seed/0

set_repl_input_file/2

show_cache/0

show_initialisation_summary/1

show_last_expression_as_table/0

show_operation_coverage_summary/1

specfile_trans_with_check/5

split_by_seperator/2

split_by_seperator2/2

start_animation_without_computing/0

start_check_disabled/2

start_ltsmin_srv/2

start_probcli_timer/1

start_xml_feature/2

start_xml_feature/4

stop_probcli_debug_timer/2

stop_probcli_timer/2

stop_probcli_timer/3

stop_xml_feature/2

store_last_error_location_for_repl/0

strip_leading_ws/2

strip_ws/2

strip_ws2/2

test_kodkod_and_exit/2

translate_exception/2

treat_existence_error/4

trimcore_if_useful/1

truncate_animate_action/2

unset_analyse_hook/0

unset_current_probcli_command/0

we_need_only_static_assertions/1

write_deferred_set_used/1

write_dot_graph_to_new_file/2

write_important_xml_element_to_log/2

write_result_to_file/1

xml_log_machine_statistics/0

zmq_delayed_option/1

zmq_get_important_options/1

zmq_get_initialisation_term/1

zmq_important_option/1

zmq_set_important_options/1

zmq_set_option/1

zmq_start_master/2

zmq_start_worker/2

zmq_worker_load_model/1

accumulate_infos/2

add_eval_result/1

add_model_checking_warnings/4

add_vacuous_invariant/1

allow_filter_unused_constants/0

animate_machine/0

animate_machine2/0

animation_mode_does_not_support_animation/1

append_assertion/1

assert_all_options/1

assert_option/1

atom_contains_codes/2

available_commands/1

browse/0

browse_all_machines/1

browse_machine/1

call_probcli_option/1

Meta: call_probcli_option(0)

cbc_assertions/2

cbc_check/1

cbc_deadlock_check/1

cbc_redundant_invariants/1

cbc_refinement/0

cbc_sequence/3

cbc_test_case_generation/3

cbc_test_case_generation(ADepth,TargetString,Output) :-
    arg_is_number(ADepth,MaxDepth),
    ( option(cbc_cover_all) -> Events=all
    ; (get_comma_or_space_separated_options(cbc_cover,Events), Events \= []) -> true
    ; Events=all ),
    (\+ option(cbc_cover_final) -> FEvents = Events
    ; Events=all -> FEvents=all,
    add_error(cbc_cover_final,'Option cbc_cover_final not compatible with trying to cover all events')
    ; FEvents = final(Events),
    println_silent('constraint based test case generation, target events considered final')),
    printsilent('constraint based test case generation, maximum search depth: '),printsilent(MaxDepth),nls,
    printsilent('constraint based test case generation, target state predicate: '),printsilent(TargetString),nls,
    printsilent('constraint based test case generation, output file: '),printsilent(Output),nls,
    (TargetString = '#not_invariant' ->
    printsilent('constraint based test case generation, performing bounded model checking'),nls
    ; option(silent) -> true
    ; print('constraint based test case generation, events to cover: '),print_list(Events),nl),
    cbc_gen_test_cases_from_string(FEvents,TargetString,MaxDepth,Output,Uncovered),
    !,
    %print('mcm test case generation, generated test cases: '),print(NumTests),nl,
    (TargetString = '#not_invariant'
    -> tcl_get_stored_test_cases(list(Tests)), %print(tests(Tests)),nl,
    (Tests=[] -> print_green('No counterexample found'),nl
    ; Tests = [_|_] -> add_error(invariant_violation,'Invariant violation found by bmc')
    ; add_internal_error('Unexpected bmc result: ',Tests))
    ; (Uncovered=[_|_],option(strict_raise_error))
    -> add_error(cbc_tests,'Uncovered events: ',Uncovered)
    ; print_uncovered('constraint based test case generation, ',Uncovered)
).

cbc_test_case_generation(_ADepth,_ATarget,_Output) :-
    print_error('### CBC Test Case Generation failed'),
    error_occurred(cbc_tests).

check_abstract_constants/0

check_all_expected_errors_occurred/1

check_complete/0

check_complete_operation_coverage/0

check_deadlock_fail/1

check_loaded_not_empty/1

check_model_result/2

check_parser_version/0

check_partial_trans/2

check_ref_result/1

check_required_infos/3

cli_add_additional_property/1

cli_animateOperationNr/3

cli_assertions_ok/2

cli_checkAssertion/4

cli_check_assertions/2

cli_check_assertions/3

cli_check_csp_assertion/2

cli_check_goal/0

cli_check_properties/0

cli_check_properties/1

cli_check_scc_for_ltl_formula/2

cli_check_statespace_hash/2

cli_computeOperations/1

cli_csp_get_assertions/0

cli_csp_in_situ_refinement_check/4

cli_csp_translate_to_file/1

cli_ctl_model_check/3

cli_eval_csp_expression/1

cli_execute/3

cli_execute_add_virtual_transition/3

cli_execute_aux/7

cli_execute_aux(Nr,Steps,CurState,_,_ErrorOnDeadlock,_LastActionName,Result) :- Nr>Steps,!,
    formatsilent('Stopping execution after ~w steps~n',[Steps]), Result = stopped,
    print_state_silent(CurState),
    cli_execute_add_virtual_transition(Steps,CurState,Result).

cli_execute_aux(Nr,Steps,CurState0,MEMO,ErrorOnDeadlock,LastActionName,Result) :-
    (Nr mod 5000 =:= 0, \+option(animate_stats), \+option(silent)
    -> (var(LastActionName) -> format('Step ~w~n',[Nr])
    ; format('Step ~w (after ~w)~n',[Nr,LastActionName])),
    (option(verbose) -> print_state_silent(CurState0) ; true),
    %copy_term(CurState0,CurState), tools_printing:print_term_summary((CurState0)),nl,
    !,
    garbage_collect,
    !,
    print('Memory used: '),tools:print_memory_used_wo_gc,flush_output,nl %nl_time
    ; true),
    prepare_state_for_specfile_trans(CurState0,MEMO,CurState), % ensure we memoize expanded constants in MEMO
    % avoid re-expanding constants in every state !
    % relevant e.g. for probcli -execute 20001 DataValidationTestSmallStep.mch -init
    (cli_invariant_ko(CurState,LastActionName,InvStatus,CliErr) -> % also recognises no_inv command
    N1 is Nr-1,
    ajoin(['INVARIANT ',InvStatus,' after ',N1,' steps (after ',LastActionName,').'],ErrMsg),
    format('~w~n',[ErrMsg]),!,
    print_state_silent(CurState),
    error_occurred_with_msg(CliErr,ErrMsg),
    Result=CliErr,
    cli_execute_add_virtual_transition(N1,CurState,Result)
    ; \+ cli_assertions_ok(CurState,LastActionName) -> % also recognises no_inv command
    N1 is Nr-1,
    format('ASSERTION VIOLATED after ~w steps (after ~w).~n',[N1,LastActionName]),!,
    print_state_silent(CurState),
    error_occurred(assertion_violation), Result=assertion_violation,
    cli_execute_add_virtual_transition(N1,CurState,Result)
    ; cli_goal_found(CurState) -> % also recognizes no_goal command
    N1 is Nr-1,
    format('GOAL FOUND after ~w steps (after ~w).~n',[N1,LastActionName]),!,
    print_state_silent(CurState), Result=goal_found,
    cli_execute_add_virtual_transition(N1,CurState,Result)
    ; reset_side_effect_occurred,
    cli_trans(CurState,ActionName,NewState,Nr),
    !,
    N1 is Nr+1,
    (NewState=CurState0, % could be expensive for large states; states are expanded ! % TO DO: look only at written variables ?!
    \+ side_effect_occurred(file)
    -> formatsilent('Infinite loop reached after ~w steps (looping on ~w).~n',[N1,ActionName]),
    Result=loop,
    cli_execute_add_virtual_transition(N1,CurState,Result)
    ; cli_execute_aux(N1,Steps,NewState,MEMO,ErrorOnDeadlock,ActionName,Result))
).

cli_execute_aux(Nr,_Steps,CurState,_,_ErrorOnDeadlock,LastActionName,Result) :- execute_timeout_occurred,!,
    N1 is Nr-1,
    formatsilent('Timeout occurred after ~w steps (after ~w).~n',[N1,LastActionName]),
    Result=time_out,
    print_state_silent(CurState),
    cli_execute_add_virtual_transition(N1,CurState,Result).

cli_execute_aux(Nr,_Steps,CurState,_,ErrorOnDeadlock,LastActionName,Result) :- N1 is Nr-1,
    formatsilent('Deadlock reached after ~w steps (after ~w).~n',[N1,LastActionName]),
    Result=deadlock,
    (ErrorOnDeadlock=true,\+ option(no_deadlocks) -> error_occurred(deadlock) ; true),
    print_state_silent(CurState),
    cli_execute_add_virtual_transition(N1,CurState,Result).

cli_execute_from/5

cli_execute_trans/4

cli_find_ltl_ap/1

cli_get_coverage_information/1

cli_get_min_max_coverage/1

cli_goal_found/1

cli_init_options/2

cli_init_options2/2

Description:
assert(option(log('/tmp/ProBLog.log'))), print('LOGGING'),nl, %% coment in to build a version of probcli that automatically logs

cli_load_files3(MainFile0,Rest,NOW,NrOfFile) :-
    safe_absolute_file_name(MainFile0,MainFile,[access(none)]), % converts Windows slash into Unix slash,...
    if_option_set(file_info,print_file_info(MainFile)),
    ((Rest=[_|_] ; NrOfFile>1)
    -> length(Rest,RLen), Tot is NrOfFile+RLen,
    format('~n~n% Processing file ~w/~w: ~w~n',[NrOfFile,Tot,MainFile]) % was formatsilent
    ; true),
    start_xml_feature(process_file,filename,MainFile,FINFO),
    ( file_exists(MainFile) ->
    debug_println(6,file_exists(MainFile)),
    ( load_main_file(MainFile,NOW,Already_FullyProcessed) ->
    (Already_FullyProcessed==true -> true
    ; assert(file_loaded(true,MainFile)),
    trimcore_if_useful(Rest),
    writeln_log_time(start_processing(NOW)),
    start_probcli_timer(Timer),
    (cli_process_loaded_file(NOW,MainFile)
    -> stop_probcli_debug_timer(Timer,'% Finished processing file after')
    ; print_error('### Processing or loading file failed: '), print_error(MainFile)
    ),
    writeln_log_time(finished_processing(NOW))
    )
    ; otherwise ->
    assert(file_loaded(error,MainFile)),
    print_error('### Loading Machine Failed'),
    writeln_log_time(loading_failed(NOW,MainFile)),
    error_occurred(load_main_file)
    ),
    nls
    ; otherwise ->
    nl, assert(file_loaded(error,MainFile)),
    (number(MainFile0)
    -> add_error(load_main_file,'Command-line argument is a number which is not associated with a command and does not exist as file: ',MainFile0)
    ; atom_codes(MainFile0,[45|_]) % starts with a dash - : probably an illegal command-line option
    -> add_error(load_main_file,'Specified Option or File does not exist: ',MainFile0)
    ; add_error(load_main_file,'Specified File does not exist: ',MainFile)
    )
    ),
    check_all_expected_errors_occurred(NOW),
       stop_xml_feature(process_file,FINFO),

    reset_expected_error_occurred, % reset for next file
    reset_errors,
    NOW1 is NOW+1, update_time_stamp(NOW1),
    cli_load_files2(Rest,NOW1,NrOfFile).

cli_ltl_model_check/3

cli_mc/1

cli_print_all_values/1

cli_print_history/1

cli_print_junit_results/1

cli_print_machine_statistics/0

cli_print_pred_info/1

cli_print_statistics/0

cli_print_values/1

cli_process_loaded_file/2

cli_process_loaded_file_afer_start_animation/1

cli_process_loaded_file_afer_start_animation(NOW) :-
    ifm_option_set(cli_print_machine_statistics,
    cli_print_machine_statistics),
    ifm_option_set(pretty_print_internal_rep(PPFILE1,TYPES,ASCII),
    pretty_print_internal_rep(PPFILE1,TYPES,ASCII)),
    ifm_option_set(pretty_print_internal_rep_to_B(PPFILE3),
    b_write_eventb_machine_to_classicalb_to_file(PPFILE3)),

    if_option_set_loaded(state_trace(TraceFile),state_trace,
    cli_start_trace_state_check(TraceFile)),

    if_option_set(evaldot(EvalDotF),
    set_eval_dot_file(EvalDotF)),

    (initialise_required
    -> check_loaded(initialise),
    cli_start_initialisation(NOW),
    writeln_log_time(initialised(NOW))
    ; true),

    if_option_set(zmq_assertion(Identifier),
    zmq_start_master(assertion,Identifier)),

    if_option_set(cli_start_mc_with_tlc,cli_start_mc_with_tlc),
    if_option_set(cli_start_sym_mc_with_lts(LType),cli_start_sym_mc_with_lts(LType)),

    if_option_set(cli_symbolic_model_check(Algorithm),cli_symbolic_model_check(Algorithm)),

    if_option_set_loaded(cli_check_properties,check_properties,
    cli_check_properties(NOW)),
    ifm_option_set_loaded(cli_check_assertions(ALL,ReqInfos),check_assertions,
    cli_check_assertions(ALL,ReqInfos,NOW)),
    if_option_set(set_goal(GOAL),
    cli_set_goal(GOAL)),
    if_option_set(set_searchscope(SCOPE),
    cli_set_searchscope(SCOPE)),
    ifm_option_set_loaded(cli_mc(Nr),model_check,
    cli_start_model_check(Nr,NOW)),
    ifm_option_set_loaded(cli_random_animate(Steps,ErrOnDeadlock),animate,
    cli_random_animate(NOW,Steps,ErrOnDeadlock)),
    ifm_option_set_loaded(execute(ESteps,ErrOnDeadlock,From),execute,
    cli_execute(ESteps,ErrOnDeadlock,From)),
    if_option_set_loaded(pa_check,predicate_analysis,
    test_predicate_analysis),

    cbc_check(NOW),

    ifm_option_set_loaded(logxml_write_ids(Prefix,IDScope),logxml_write_ids,
    logxml_write_ids(Prefix,IDScope)),

    if_options_set(generate_read_write_matrix_csv(RWCsvFile),
    generate_read_write_matrix(RWCsvFile)),
    if_options_set(feasibility_analysis_csv(TimeOut,EnablingCsvFile),
    do_feasibility_analysis(TimeOut,EnablingCsvFile)),
    ifm_option_set_loaded(mcm_tests(ADepth1,AMaxS,ATarget1,Output1),mcm_test_cases,
    mcm_test_case_generation(ADepth1,AMaxS,ATarget1,Output1)),
    ifm_option_set_loaded(all_deadlocking_paths(File),all_deadlocking_paths,
    write_all_deadlocking_paths_to_xml(File)),
    ifm_option_set_loaded(cbc_tests(ADepth2,ATarget2,Output2),cb_test_cases,
    cbc_test_case_generation(ADepth2,ATarget2,Output2)),
    ifm_option_set_loaded(test_description(TestDescFile),cb_test_cases,
    test_generation_by_xml_description(TestDescFile)),
    if_options_set(csp_in_situ_refinement_check(RP,RType,RQ),
    cli_csp_in_situ_refinement_check(RP,RType,RQ,NOW)),
    if_options_set(csp_checkAssertion(Proc,Model,AssertionType),
    cli_checkAssertion(Proc,Model,AssertionType,NOW)),
    if_options_set(check_csp_assertion(Assertion),
    cli_check_csp_assertion(Assertion,NOW)),
    if_options_set(refinement_check(RefFile,PerformSingleFailures,RefNrNodes),
    cli_start_refinement_check(RefFile,PerformSingleFailures,RefNrNodes,NOW)),
    if_options_set(ctl_formula_model_check(Formula,Expected),cli_ctl_model_check(Formula,Expected,_)),
    % TO DO print ctl/ltl statistics
    if_options_set(csp_get_assertions,cli_csp_get_assertions),
    if_options_set(eval_csp_expression(CspExpr),cli_eval_csp_expression(CspExpr)),
    if_options_set(csp_translate_to_file(PlFile),cli_csp_translate_to_file(PlFile)),
    if_options_set(get_min_max_coverage(MinMxFileName),cli_get_min_max_coverage(MinMxFileName)),
    if_options_set(get_coverage_information(CovFileName),cli_get_coverage_information(CovFileName)),
    if_options_set(vacuity_check,cli_vacuity_check),
    if_option_set_loaded(check_goal,check_goal,cli_check_goal),
    if_option_set_loaded(animate,animate,
    (animate_machine -> true ; true)),
    if_option_set(ltsmin, start_ltsmin_srv('/tmp/ltsmin.probz', NOW)),
    if_option_set(ltsmin2(EndpointPath), start_ltsmin_srv(EndpointPath, NOW)),
    if_option_set(ltsmin_ltl_output(Path), ltsmin_ltl_output(Path, NOW)),
    evaluate_from_commandline,
    if_option_set_loaded(ltl_assertions,check_ltl_assertions,
    (timeout_call(ltl_check_assertions,NOW) -> true; true)),
    ifm_option_set_loaded(ltl_formula_model_check(Formula,Expected),check_ltl_assertions,
    (option(cli_start_sym_mc_with_lts(_))-> true % we request LTSMin, do not start prob model check
    ; timeout_call(cli_ltl_model_check(Formula,Expected,_),NOW) -> true; true)),
    ifm_option_set_loaded(ltl_file(LtlFilename),check_ltl_file,
    (ltl_check_file(LtlFilename) -> true; true)),
    ifm_option_set_loaded(history(HistoryFilename),history,
    cli_print_history(HistoryFilename)),
    ifm_option_set_loaded(print_values(ValuesFilename),values,
    cli_print_values(ValuesFilename)),
    ifm_option_set_loaded(print_all_values(ValuesDirname),values,
    cli_print_all_values(ValuesDirname)),
    if_options_set(save_state_for_refinement(SaveRefF),
    refinement_checker:tcltk_save_specification_state_for_refinement(SaveRefF)),
    if_options_set(dot_command(DCommand,DotFile),
    dot_command(DCommand,DotFile)),
    if_options_set(dot_command_for_expr(DECommand,Expr,DotFile,Opts),
    dot_command_for_expr(DECommand,Expr,DotFile,Opts)),
    if_options_set(evaluate_expression_over_history_to_csv_file(HistExpr,HistDotFile),
    tcltk_interface:evaluate_expression_over_history_to_csv_file(HistExpr,HistDotFile)),
    if_options_set(enabling_analysis_csv(EnablingCsvFile),
    do_enabling_analysis_csv(EnablingCsvFile,NOW)),
    if_options_set(process_latex_file(LatexF1,LatexF2),
    process_latex_file(LatexF1,LatexF2)),
    ifm_option_set(coverage(Nodes,Operations,ShowEnabledInfo),
    cli_show_coverage(Nodes,Operations,ShowEnabledInfo,NOW)),
    ifm_option_set(check_statespace_hash(ExpectedHash,Kind),
    cli_check_statespace_hash(ExpectedHash,Kind)),
    ifm_option_set(variable_coverage,
    cli_show_variable_coverage(NOW)),
    ifm_option_set(coverage(ShowEnabledInfo),
    cli_show_coverage(ShowEnabledInfo,NOW)),
    if_option_set(save_state(StateFile),
    save_state(StateFile)),
    if_option_set(prob_profile,
    prob_profile),
    if_option_set(statistics,
    cli_print_statistics),
    if_option_set(profile_statistics,
    profile_statistics),
    if_option_set(show_cache,
    show_cache),
    if_option_set(check_complete, check_complete),
    if_option_set(check_complete_operation_coverage, check_complete_operation_coverage),
    if_option_set(check_scc_for_ltl_formula(LtlFormula,SCC),cli_check_scc_for_ltl_formula(LtlFormula,SCC)).

cli_random_animate/2

cli_random_animate/3

cli_set_empty_machine/0

cli_set_goal/1

cli_set_options/2

Description:
adds -ll to have an automatically logging probcli to /tmp/prob_cli_debug.log

cli_set_searchscope/1

cli_show_coverage/2

cli_show_coverage/4

cli_show_help/2

cli_show_variable_coverage/1

cli_start_animation/1

cli_start_initialisation/1

cli_start_logging/5

cli_start_mc_with_tlc/0

cli_start_model_check/2

cli_start_refinement_check/4

cli_start_selfcheck/0

cli_start_socketserver/1

cli_start_sym_mc_with_lts/1

cli_start_trace_check/1

cli_start_trace_state_check/1

cli_symbolic_model_check/1

close_repl_input_stream/1

command_option/1

compare_kodkod_performance1/3

computeOperations_for_root_required/0

constraint_based_check/1

constraint_based_check(all) :-
    check_loaded_not_empty(constraint_based_check),
    print_repl_prompt_s('% Starting Constraint-Based Check for all Operations: '),nl,
    start_xml_feature(cbc_operation_check,all_operations,true,FINFO),
    (tcltk_constraint_based_check(list(Result),ErrorsWereFound)
    -> print('% Constraint-Based Check Result: '),nl,
    print(Result),nl,
    write_result_to_file(Result),
    (ErrorsWereFound=true
    -> print_red('*** CONSTRAINT-BASED CHECK FOUND ERRORS ***'),nl, error_occurred(cbc)
    ; (ErrorsWereFound=false -> print_green('NO ERRORS FOUND'),nl)
    ; print_red('*** TIMEOUT OCCURRED ***'),nl,error_occurred(cbc)
    )
    ; write_result_to_file(cbc_check_failed), Result=internal_error, ErrorsWereFound=false,
    add_internal_error('ConstraintBasedCheck unexpectedly failed. ',cbc_check(all)),definite_error_occurred
    ),nl,
    write_xml_element_to_log(cbc_check_result,[result/Result,errors_were_found/ErrorsWereFound]),
    stop_xml_feature(cbc_operation_check,FINFO).

constraint_based_check(OpName) :- OpName\=all, % -cbc OpName
    check_loaded_not_empty(constraint_based_check),
    print_repl_prompt_s('% Starting Constraint-Based Check for Operation: '), print(OpName),nl,
    start_xml_feature(cbc_operation_check,operation,OpName,FINFO),
        (tcltk_constraint_based_check_with_timeout(OpName,Result)
    -> print('% Constraint-Based Check Result: '),nl, print(Result),nl,
    write_result_to_file(Result),
    (Result=time_out
    -> print_red('*** TIMEOUT OCCURRED ***'),nl, error_occurred(cbc)
    ; (Result=ok -> print_green('NO ERRORS FOUND'),nl)
    ; print_red('*** CONSTRAINT-BASED CHECK FOUND ERRORS ***'),nl,error_occurred(cbc) )
    ; write_result_to_file(constraint_based_check_failed), Result=internal_error,
    add_error(probcli,'ConstraintBasedCheck unexpectedly failed'),
    (b_is_operation_name(OpName) -> true
    ; add_error(probcli,'Unknown Operation Name: ',OpName)),
    definite_error_occurred
        ),nl,
    write_xml_element_to_log(cbc_check_result,[result/Result]),
    stop_xml_feature(cbc_operation_check,FINFO).

construct_and_execute_tlc_command/1

convert_dash_to_underscore/2

count_assertions/3

coverage/1

create_state_error_description/2

definite_error_occurred/0

display_match/3

display_match/4

do_det_checking/0

do_enabling_analysis_csv/2

do_feasibility_analysis/2

do_not_execute_automatically/1

do_one_gui_event/0

Description:
sp_4_1_3_nested_exception_patch.pl BEGIN
Compile this to patch a bug in 4.1.3 affecting nested exception handlers.
This source code is a no-op on other versions of sicstus than 4.1.3.
sp_4_1_3_nested_exception_patch.pl END

dot_command/2

dot_command_for_expr/4

Dynamic: true

Dynamic: true

error_occurred(Type,ErrOrWarning,ExtractedSpan,Msg) :- option(expect_error_pos(Type,Line,Col)),!,
    write_xml_element_to_log(expected_error_occurred,[category/Type, type/ErrOrWarning, message/Msg]),
    assert(expected_error_occurred(Type)),
    (get_error_or_warning_span(ExtractedSpan,Type,EL,EC)
    -> ((EL,EC)=(Line,Col) -> debug_println(9,expect_error_pos_ok(Type,EL,EC))
    ; format('Unexpected line ~w and column ~w for error ~w! Expected line ~w and column ~w.~n',[EL,EC,Type,Line,Col]),
    definite_error_occurred
    )
    ; format('*** Could not obtain position information for error ~w! Expected line ~w and column ~w.~n',[Type,Line,Col]),
    %display_error_statistics,
    definite_error_occurred).

error_occurred(Type,ErrOrWarning,ExtractedSpan,Msg) :-
    option(expect_error(Type)),!,
    inc_counter(cli_expected_errors),
    get_xml_span(ExtractedSpan,XML),
    write_xml_element_to_log(expected_error_occurred,[category/Type, type/ErrOrWarning, message/Msg|XML]),
    assert(expected_error_occurred(Type)).

error_occurred(Type,ErrOrWarning,ExtractedSpan,Msg) :-
    (probcli_time_stamp(NOW) -> true ; NOW=unknown),
    writeln_log(error_occurred(NOW,Type)),
    get_xml_span(ExtractedSpan,XML),
    (option(optional_error(Type)) ->
    write_xml_element_to_log(optional_error_occurred,[category/Type, type/ErrOrWarning, message/Msg|XML]),
    format(user_output,'% Optional error occured: ~w~n',[Type])
    ;
    write_xml_element_to_log(error_occurred,[category/Type, type/ErrOrWarning, message/Msg|XML]),
    (ErrOrWarning = warning -> inc_counter(cli_warnings) ; inc_counter(cli_errors)),
    (option(strict_raise_error) ->
                print_error('*** Unexpected error occurred ***'),
                print_error(Type),
    findall(Err,option(expect_error(Err)),Ls), (Ls=[] -> true ; print_error(expected(Ls))),
                definite_error_occurred
            ; ErrOrWarning=error,serious_error(Type)
            -> print_error('*** Serious error occurred ***'),
                print_error(Type),
                definite_error_occurred
            ; print_probcli_error_non_strict(Type,ErrOrWarning)
)
).

error_occurred_with_msg/2

error_occurred_with_msg/3

eval_command_help(exit,[],'Exit ProB').

eval_command_help(find,['P'],'Find state in state-space which makes LTL atomic proposition P true; LTL Propositions: {B-Pred}, e(Op), [Op], true, false, sink').

eval_command_help(ltl,['F'],'Check LTL formula F; LTL Operators: G,F,X,U,W,R,not,&,or,=>; LTL Propositions: {B-Pred}, e(Op), [Op], true, false, sink; Past-LTL Operators: Y,H,O,S,T (dual to X,G,F,U,R)').

eval_command_help(ctl,['F'],'Check CTL formula F; CTL Syntax: ExUy,EXx,AXx,EFx,AGx,EX[Op]x,e(Op),{B-Pred}').

eval_command_help(browse,opt('PAT'),'Browse available constants, variables, sets and lets introduced in REPL').

eval_command_help(apropos,['PAT'],'Find constant or variable whose names contains PAT').

eval_command_help(hbrowse,['PAT'],'Browse machine hierarchy for all identifiers whose names contains PAT').

eval_command_help(show_components,[],'Show components of PROPERTIES').

eval_command_help(abstract_constants,[],'Show ABSTRACT_CONSTANTS and check if can be fully evaluated').

eval_command_help(show_last_as_table,[],'Show last evaluated expression in tabular form').

eval_command_help(show_last_as_dot(_),['F'],'Show expression or predicate F as dot graph').

eval_command_help(unsat_core,[],'Compute Unsatisfiable Core of last evaluated predicate').

eval_command_help(help,opt('CMD'),'Provide help about REPL command CMD').

eval_command_help(replay_repl_file,['FILE'],'Replay FILE of REPL commands').

eval_command_help(show_source,['ID'],'Show origin and source code definition of identifier ID').

eval_command_help(show_origin,['ID'],'Show origin of identifier ID and try opening in EDITOR').

eval_command_help(state_space_stats,[],'Show statistics about state space').

eval_command_help(state_space_display,[],'Show complete state space transitions (could be very big !)').

eval_command_help(show_state_info,[],'Show current state').

eval_command_help(statistics,[],'Show statistics about last evaluation').

eval_command_help(trim,[],'Trim memory usage of probcli (try and give memory back to the OS)').

eval_command_help(type,['E'],'Show type of expression E').

eval_command_help(cvc4,['P'],'Solve predicate P using CVC4 solver').

eval_command_help(kodkod,['P'],'Solve predicate P using SAT solver via Kodkod').

eval_command_help(z3,['P'],'Solve predicate P using Z3 solver').

eval_command_help(edit_main_file,opt('ID'),'Edit main file (or origin of identifier ID) using EDITOR (path_to_text_editor preference)').

eval_command_help(comment,['STRING'],'provide STRING as a comment (mainly useful for :replay files)').

eval_help/0

eval_line/1

eval_line([]) :- !, print_repl_prompt('Type :q or :quit to quit.'),nl,eval.

eval_line(end_of_file) :- !, halt_exception(0).

eval_line(":r") :- !, eval_line("--reload").

eval_line(":reload") :- !, eval_line("--reload").

eval_line("--reload") :- !,
    (reload_mainfile -> true ; get_errors,print_repl_prompt('### Error(s) occured during reload (use :e to jump to first error)'),nl),
    eval.

eval_line(":prefs") :- !,print_eclipse_prefs, eval.

eval_line([45|Command]) :- % -command
    generate_atom_list([45|Command],[],ArgV),
    %print(argv(ArgV)),nl,
    % try and parse like commands passed to probcli
    get_options(ArgV,recognised_cli_option,Options,[],fail),
    print_repl_prompt('Executing probcli command: '),print_repl_prompt(Options),nl,!,
    (maplist(call_probcli_option,Options) -> true
    ; print_red('Failed to execute probcli arguments'),nl),
    eval.

eval_line("+") :- !, add_last_expression_to_unit_tests, eval.

eval_line("$+") :- !, preferences:temporary_set_preference(expand_avl_upto,-1,CHNG),
    print_last_value,preferences:reset_temporary_preference(expand_avl_upto,CHNG),
    eval.

eval_line("$$$") :- !, % $$0 - $$9 commands to print last expression with indentation
    indent_print_last_expression, eval.

eval_line("!trace") :- !, eval_line("^").

eval_line("^") :- !,
    (retract(trace_eval) -> print_repl_prompt('TRACING OFF'),nl
    ; assert(trace_eval), print_repl_prompt('TRACING ON'),nl), eval.

eval_line("!observe") :- !, toggle_observe_evaluation.

eval_line("!v") :- !, tcltk_turn_debugging_off.

eval_line("!p") :- !, toggle_perfmessages.

eval_line("!perf") :- !, toggle_perfmessages.

eval_line("!profile") :- !, eval_line("%").

eval_line("%") :- !, print_repl_prompt('PROFILING : '), %spy([avl:avl_size/2]),
    (current_prolog_flag(profiling,on)
    -> set_prolog_flag(profiling,off), print('OFF') ;
    set_prolog_flag(profiling,on), print('ON')),
    nl,print_repl_prompt('USE %% to print profile info'),nl,eval.

eval_line("%%") :- !, nl,print_repl_prompt('PROFILE INFORMATION:'), nl,
    on_exception(error(existence_error(_,_),_),print_profile, print_red('CAN ONLY BE USED WHEN RUNNING PROB FROM SOURCE')),
    nl, debug:timer_statistics,
    eval.

eval_line("%%%") :- !, nl,print('PROFILE INFORMATION (Starting TK Viewer):'), nl,
    on_exception(error(existence_error(_,_),_),
    (use_module(library(gauge)),gauge:view), print_red('CAN ONLY BE USED WHEN RUNNING PROB FROM SOURCE')),
    nl,eval.

eval_line("!debug") :- !,
    print_repl_prompt('ENTERING PROLOG DEBUG MODE:'),
    on_exception(error(existence_error(_,_),_),debug, print_red('CAN ONLY BE USED WHEN RUNNING PROB FROM SOURCE')),
    nl,
    eval.

eval_line("@") :- !, get_preference(find_abort_values,OldVal),
    print_repl_prompt('Try more aggressively to detect ill-defined expressions: '),
    (OldVal=true -> Val=false ; Val=true), print(Val),nl,
    temporary_set_preference(find_abort_values,Val) , eval.

eval_line("!") :- !, toggle_eval_det,eval.

eval_line("!norm") :- !, toggle_normalising,eval.

eval_line(Codes) :- parse_eval_command(Codes,CommandName,Argument),!,
    debug_println(9,executing_eval_command(CommandName,Argument)),
    (exec_eval_command(CommandName,Argument) -> eval
    ; format_with_colour(user_error,[red,bold],'Command ~w failed~n',[CommandName]), eval).

eval_line(ExpressionOrPredicate) :- (trace_eval -> trace ; true),
    (eval_codes(ExpressionOrPredicate,exists,_,_,_,_)
    -> eval ; print_red('Evaluation failed'),nl,eval).

eval_probcli_repl_line/1

eval_string_or_file/5

eval_string_or_file(string,String,_,Expected,Recheck) :-
    set_current_probcli_command(eval_string(String)),
    (option(silent),nonvar(Expected) -> true
    ; print('eval: '), print(String),nl),
    reset_error_spans, % avoid underlining previous errors in eval_string
    eval_string_with_time_out(String,StringResult,EnumWarning,_LS),
    % print(enumwarning(EnumWarning,Expected)),nl,
    add_eval_result(StringResult),
    (Expected\=StringResult
    -> format_error('### Evaluation error, expected result to be: ~w (but was ~w)~n',[Expected,StringResult]),
    error_occurred(eval_string)
    ; EnumWarning = false -> true % TO DO: recheck if requested
    ; gen_enum_warning(Expected) % now also generate enum warnings when Expected not set (eval instead of evalt/evalf)
    ),
    (Recheck=recheck(Mode) -> recheck_pp_of_last_expression(Mode,_,_) ; true),
    unset_current_probcli_command.

eval_string_or_file(file,File,Quantifier,Expected,_) :-
    % evaluate a single formula stored in a file
    set_current_probcli_command(eval_file(File)),
    turn_show_error_source_off, % reduce clutter in user feedback; eval_file used in ProB Logic Calculator for example
    formatsilent('~nEvaluating file: ~w~n',[File]),
    error_manager:reset_error_scopes, % TO DO: avoid that exceptions mess up error scopes in eval_string/file
    statistics(runtime,[Start,_]),nl,
    (Expected=='TRUE' -> TypeInfo=predicate(_) % avoids parsing as expression
    ; true),
    (eval_file(File,Quantifier,Result,EnumWarning,TypeInfo)
    -> add_eval_result(Result),
    (EnumWarning = false -> true ; gen_enum_warning(EnumWarning)),
    (Result\=Expected -> print_error('### Error, expected result to be: '),
    print_error(Expected),
    print_error('### File: '), print_error(File),
    error_occurred(eval_file)
    ; true)
    ; add_eval_result(eval_file_failed),
    print_error('### Eval from file failed: '), print_error(File),
    error_occurred(eval_file)
    ),
    (debug_mode(on) -> statistics(runtime,[Stop,_]), Time is Stop - Start,
    print(File),print(' time: '), print(Time), print(' ms'),nl
    ; true),
    turn_show_error_source_on,
    unset_current_probcli_command.

evaluate_expressions/1

evaluate_from_commandline/0

exec_eval_command/2

exec_eval_command(quit,_) :- !, halt_exception(0).

exec_eval_command(exit,_) :- !,halt.

exec_eval_command(browse,CodesToMatch) :- !,
    (CodesToMatch=[] -> browse % maybe merge with apropos functionality
    ; exec_eval_command(apropos,CodesToMatch)).

exec_eval_command(find,FORMULA) :-
    atom_codes(APF,FORMULA),cli_find_ltl_ap(APF).

exec_eval_command(apropos,CodesToMatch) :- /* :* Pattern (apropos command) */
    browse_machine(CodesToMatch).

exec_eval_command(hbrowse,CodesToMatch) :- /* :* Pattern (apropos command) */
    browse_all_machines(CodesToMatch).

exec_eval_command(show_components,_) :-
    print_property_partitions.

exec_eval_command(check_abstract_constants,_) :-
    check_abstract_constants.

exec_eval_command(help,Arg) :-
    (Arg=[] -> eval_help
    ; print_eval_command_help(Arg) -> true
    ; (Arg=[58|RA],print_eval_command_help(RA)) -> true % remove : at front
    ; format('Cannot provide help about ~s~n',[Arg]),
    available_commands(LC), format('Available commands: ~w~n',[LC])
).

exec_eval_command(ctl,FORMULA) :-
    atom_codes(F,FORMULA),
    (cli_ctl_model_check(F,_,Status)
    -> (Status=false -> write_history_to_user_output([show_init,show_states]) ; true)
    ; print('CTL Syntax: ExUy,EXx,AXx,EFx,AGx,EX[Op]x,e(Op),{B-Pred}'),nl).

exec_eval_command(ltl,FORMULA) :-
    atom_codes(F,FORMULA),
    (cli_ltl_model_check(F,_,Status)
    -> (Status=no -> write_history_to_user_output([show_init,show_states]) ; true)
    ; print('LTL Operators: G,F,X,U,W,R,not,&,or,=>'),nl,
    print('LTL Propositions: {B-Pred}, e(Op), [Op], true, false, sink'),nl,
    print('Past-LTL Operators: Y,H,O,S,T (dual to X,G,F,U,R)'),nl
).

exec_eval_command(statistics,_) :- !, print_last_info.

exec_eval_command(state_space_stats,_) :- !,
    state_space:get_state_space_stats(TotalNodeSum,TotalTransSum,ProcessedTotal),
    format('Statespace: ~w states (~w processed) and ~w transitions.~n',[TotalNodeSum,ProcessedTotal,TotalTransSum]).

exec_eval_command(state_space_display,_) :- !,
    ( visited_expression(ID,State),
    functor(State,F,N),
    format('State ID ~w (~w/~w)~n',[ID,F,N]),
    transition(ID,OperationTerm,_OpID,ToID),
    functor(OperationTerm,F2,N2),
    format(' -> ~w (~w/~w)~n',[ToID,F2,N2]),
    fail
    ;
    current_state_id(ID),
    format('Current State ID ~w~n',[ID])
).

exec_eval_command(show_state_info,_) :- !,
    current_expression(ID,CurState),
    expand_const_and_vars_to_full_store(CurState,EState),
    format('Current state id ~w : ~n',[ID]),translate:print_state(EState),nl.

exec_eval_command(unsat_core,_) :- !, % :core
    unsat_core_last_expression.

exec_eval_command(trimcore,_) :- !, % :trim
    prob_trimcore_verbose.

exec_eval_command(show_last_as_table,_) :- !, % :show
    show_last_expression_as_table.

exec_eval_command(show_last_as_dot(Show),Arg) :- !,
    (Arg = [] -> print('*** :dot requires an expression or predicate as argument.'),nl
    ; safe_absolute_file_name('~/probcli_repl.dot',AFile),
    set_eval_dot_file(AFile),
    format('Displaying evaluation result in: ~w~n',[AFile]),
    (eval_codes(Arg,exists,_,_,_,_) -> true ; true), unset_eval_dot_file,
    ( Show=no_dot_viewing -> true
    ; Show=dotty -> show_dot_file(AFile)
    ; safe_absolute_file_name('~/probcli_repl.pdf',PDFFile),
    gen_dot_output(AFile,Show,pdf,PDFFile),
    show_ps_file(PDFFile) % we assume psviewer can also open pdf
)).

exec_eval_command(replay_repl_file,FILEC) :- !,
    atom_codes(File,FILEC),
    set_repl_input_file(not_verbose,File).

exec_eval_command(show_source,IDC) :- !,
    atom_codes(ID,IDC),
    show_source(ID).

exec_eval_command(show_origin,IDC) :- !,
    atom_codes(ID,IDC),
    show_origin(ID).

exec_eval_command(edit_main_file,Arg) :- !,
    (Arg=[] -> edit_main_file ; exec_eval_command(show_origin,Arg)).

exec_eval_command(comment,_Arg) :- !. % do nothing; argument was a comment; mainly useful for :replay files

generate_read_write_matrix/1

generate_time_stamp/2

get_comma_or_space_separated_options/2

get_dot_file/2

get_error_category_and_type/3

get_error_or_warning_span/4

get_probcli_elapsed_walltime/2

get_quoted_atom/4

get_state_errors/1

get_state_space_errors/0

get_xml_add_description/2

Description:
cli_set_options(['-vv','-version'|ArgV],RemArgV), %% comment in to have an automatically verbose probcli

go_cli2(ArgV) :- %print(probcli_startup),nl_time,
    probcli_startup,
    external_functions:reset_argv,
    cli_set_options(ArgV,RemArgV),
    %% cli_set_options(['-vv','-version'|ArgV],RemArgV), %% comment in to have an automatically verbose probcli
    !,
    ( RemArgV=[File],no_command_issued,
    get_filename_extension(File,Ext),
    \+ do_not_execute_automatically(Ext)
    % then assume we want to do -execute_all:
    -> assert_option(execute(2147483647,false,current_state))
    ; true),
    if_option_set(test_mode,set_random_seed_to_deterministic_start_seed, set_new_random_seed),
    if_option_set(verbose,
    verbose, %tcltk_turn_debugging_on(19),
    tcltk_turn_debugging_off),
    if_option_set(very_verbose,
    very_verbose), %tcltk_turn_debugging_on(5)),
    if_option_set(profiling_on,profiling_on),
    debug_print(9,'Command Line Arguments: '),debug_println(9,ArgV),
    if_option_set(very_verbose,
    print_options),
    debug_print(6,'Command Line File Args: '),debug_println(6,RemArgV),
    if_option_set(cache_storage(StorageDir), set_storage_directory(StorageDir)),
    if_option_set(parsercp(ParserLoc),
    assert(parsercall:parser_location(ParserLoc))),
    generate_time_stamp(Datime,NOW),
    if_option_set(log(LogF,Mode),
    cli_start_logging(LogF,Mode,NOW,Datime,RemArgV)),
    if_option_set(runtimechecking,
    turn_on_run_time_type_checks,
    turn_off_run_time_type_checks),
    if_option_set(junit(JUX),
    set_junit_mode(JUX)),
    set_prefs,
    set_optional_errors,
    cli_show_help(ArgV,RemArgV),
    if_option_set(set_argv(ArgVStr),
    set_argv(ArgVStr)),
    if_option_set(selfcheck(_),
    cli_start_selfcheck),
    if_option_set(typechecker_test(Filename),
    (run_typecheck_testcase(Filename,typesok) -> halt_prob(NOW); halt1_prob(NOW))),
    if_option_set(print_version, print_version),
    if_option_set(print_short_version, print_short_version),
    if_option_set(check_java_version, check_java_version),
    if_option_set(very_verbose,
    preferences:print_preferences),
    if_option_set(zmq_worker(Identifier), zmq_start_worker(Identifier, NOW)),
    %if_option_set(zmq_worker2(MasterIP, Port, ProxyID, Logfile), zmq_start_worker(MasterIP,Port,ProxyID,Logfile,NOW)),
    debug_println(6,loading(RemArgV)),
    cli_load_files(RemArgV,NOW), % all CLI arguments which are not understood are supposed to be files to be treated
    debug_println(6,finished_loading(RemArgV)),
    %if_options_set(analyse_log(LF,RowID,ForGnu),
    % analyse_log(LF,RowID,ForGnu)),
    %if_options_set(check_log(LF),
    % check_log(LF)),
    if_option_set(socket(Port),
    cli_start_socketserver(Port)),
    % check_all_expected_errors_occurred(NOW), % is now checked for each file; socket_server should not generate errors ?
    debug_println(20,'% ProB Finished'),
    cli_print_junit_results(ArgV),
    get_counter(cli_errors,CErrs), get_counter(cli_warnings,CWarns), get_counter(cli_expected_errors,EErrs),
    writeln_log_time(prob_finished(NOW,CErrs,CWarns)),
    (EErrs>0 -> write_xml_element_to_log('probcli-errors',[errors/CErrs,warnings/CWarns,expected_errors/EErrs])
    ; write_xml_element_to_log('probcli-errors',[errors/CErrs,warnings/CWarns])
    ),
    ((CErrs>0 ; CWarns>0) -> format(user_error,'! Total Errors: ~w, Warnings:~w~n',[CErrs,CWarns]) ; true),
    stop_xml_group_in_log('probcli-run'). % Generating this tag means probcli ran to completion without segfault,...

go_cli_with_junit_check/1

handle_symbolic_model_check_result/1

help/0

if_option_set/2

Meta: if_option_set(-,0)

if_option_set/3

Meta: if_option_set(-,0,0)

if_option_set_loaded/3

Meta: if_option_set_loaded(-,-,0)

if_options_set/2

Meta: if_options_set(-,0)

ifm_option_set/2

Meta: ifm_option_set(-,0)

ifm_option_set/3

ifm_option_set_loaded/3

Meta: ifm_option_set_loaded(-,-,0)

initialise_required/0

irrelevant_xml_if_zero/1

irrelevant_xml_info/1

is_constant_binding/1

is_eventb_b/1

is_ws/1

just_assert_option/1

load_b_file_with_options/1

loaded_root_filename/1

logxml_write_ids/2

ltl_check_assertions/0

mcm_test_case_generation/4

memory_intensive_option/1

model_check/3

model_check(Nr,Time,ErrRes) :-
    statistics(runtime,[T1,_]),
    statistics(walltime,[W1,_]),
    (option(no_deadlocks) -> FindDeadlocks=0 ; FindDeadlocks=1),
    (option(no_invariant_violations) -> FindInvViolations=0 ; FindInvViolations=1),
    (option(no_goal) -> FindGoal=0 ; FindGoal=1),
    (option(no_assertion_violations)
    -> FindAssViolations=0
    ; FindAssViolations=1
    ),
    get_preference(por,POR),
    get_preference(pge,PGE),
    StopAtFullCoverage=0,
    %STOPMCAFTER = 86400000, /* 86400000 = 1 day timeout */
    STOPMCAFTER = 1152921504606846975, /* equals 13,343,998,895 days */
    InspectExistingNodes = 1,
    write_xml_element_to_log(model_checking_options,[find_deadlocks/FindDeadlocks,
    find_invariant_violations/FindInvViolations, find_goal/FindGoal,
    find_assertion_violations/FindAssViolations,
    partial_order_reduction/POR,
    partial_guard_evaluation/PGE,
    inspect_existing_nodes/InspectExistingNodes]),
    (tcltk_interface:do_model_check(Nr,NodesAnalysed,STOPMCAFTER,ErrRes,FindDeadlocks,FindInvViolations,FindGoal,FindAssViolations,StopAtFullCoverage,POR,PGE, InspectExistingNodes)
    -> (statistics(runtime,[T2,_]), statistics(walltime,[W2,_]),
    Time1 is T2-T1, WTime is W2-W1,
    (model_checker: expired_static_analysis_time(AnalysisTime) ->
    Time is Time1 - AnalysisTime
    ; Time = Time1),
    formatsilent('Model checking time: ~w ms (~w ms walltime)~n',[Time,WTime]),
    formatsilent('States analysed: ~w~n',[NodesAnalysed]),
    state_space: get_state_space_stats(_,NrTransitions,_),
    printsilent('Transitions fired: '),printsilent(NrTransitions),nls,
    write_xml_element_to_log(model_checking_statistics,
    [result/ErrRes,runtime/Time,walltime/WTime,states/NodesAnalysed,transitions/NrTransitions]),
    (ErrRes = no
    -> print('No counter example Found, not all nodes visited'),nl,
    add_warning(model_check_incomplete,'Not all nodes examined due to limit set by user: ',Nr)
    ; (ErrRes=all
    -> (tcltk_find_max_reached_node
    -> print('No counter example found. However, not all transitions were computed !')
    ; print_green('No counter example found. ALL nodes visited.')
    ),
    add_model_checking_warnings(FindInvViolations,FindDeadlocks,FindGoal,FindAssViolations)
    ; print_red('*** COUNTER EXAMPLE FOUND ***'),nl,
    debug_println(20,ErrRes),nl,
    tcltk_interface:translate_error_for_tclk(ErrRes,TclTkRes),
    print(TclTkRes),nl,
    (option(silent) -> true
    ; option(no_counter_examples) -> true
    ; tcltk_interface:tcltk_get_history(list(Hist)),
    length(Hist,Len),
    format('*** TRACE (length=~w):~n',[Len]),
    reverse(Hist,Trace),
    print_nr_list(Trace),
    (option_verbose,
    current_state_id(ID),invariant_violated(ID)
    -> print('*** '),
    b_interpreter:analyse_invariant_for_state(ID)
    ; true)
    ),
    error_occurred(TclTkRes)
    )
    ),nl
    )
    ; ( statistics(runtime,[T2,_]),
    Time1 is T2-T1,
    (model_checker: expired_static_analysis_time(AnalysisTime) ->
    Time is Time1 - AnalysisTime
    ; Time = Time1),
    printsilent('Model checking time: '), printsilent(Time), printsilent(' ms'),nls,
    print_error('*** Model checking FAILED '),nl,
    ErrRes=fail,
    definite_error_occurred)
).

model_check/4

my_tell/1

no_command_issued/0

normalise_option_atom/2

normalise_pref_name/2

not_command_option/1

open_file_at_position/1

option_only_works_for_single_file/1

option_requires_all_properties/1

option_verbose/0

options_allow_start_without_file/0

parse_eval_command/3

perform/1

perform_random_init_after_setup_constants/0

perform_random_initialisation/0

perform_random_initialisation/1

perform_random_initialisation_if_necessary/1

perform_random_step/1

perform_random_step/4

perform_random_steps/2

perform_random_steps_aux/3

perform_symbolic_model_checking/2

portray_message/2

pracc/1

pred_eval_hook/5

pretty_print_internal_rep/3

pretty_print_internal_rep_to_B/1

print_accumulated_infos/1

print_bindings/1

print_cbc_stats/2

print_compile_time_flags/0

print_current_state/0

print_eval_command_help/1

print_eval_results/0

print_file_info/1

print_help/0

Description:
print(' -parsercp CP class path of the B Parser, this has to be a valid Java class path'),nl,
print(' -cspm load CSP-M .csp file rather than B Machine .mch/.ref/.imp File'),nl,
print(' -csp load CSP-M .pl file rather than B Machine File'),nl,

print_help :-
    print_version,
    print('Usage: probcli FILE [OPTIONS]'),nl,
    print(' OPTIONS are: '),nl,
    print(' -mc Nr model check; checking at most Nr states'),nl,
    print(' -model_check model check without limit on states explored'),nl,
    ( \+ option_verbose ->
    print(' -noXXX XXX=dead,inv,goal,ass (for model check)'),nl % -nodead, -noinv, -nogoal, -noass
    ;
    print(' -nodead do not look for deadlocks (for model check, animate, execute)'),nl,
    print(' -noinv do not look for invariant violations (for model check, animate, execute)'),nl,
    print(' -nogoal do not look for GOAL predicate (for model check, execute)'),nl,
    print(' -noass do not look for ASSERTION violations (for model check, execute)'),nl
    ),
    print(' -bf proceed breadth-first (default is mixed bf/df)'),nl,
    print(' -df proceed depth-first'),nl,
    print(' -mc_mode M M=hash,heuristic,random,dlk,breadth-first,depth-first,mixed'),nl, % dlk stands for out_degree_hash
    print(' -timeout N total timeout in ms for model/refinement checking and'),nl,
    print(' and execute steps and disprover checks'),nl,
    print(' -disable_timeout disable timeouts for operations, invariants,....'),nl, % speeds up mc
    print(' -t trace check (associated .trace file must exist)'),nl,
    print(' -init initialise specification'),nl,
    print(' -cbc OPNAME constraint-based invariant checking for an operation'),nl,
    print(' (you can also use OPNAME=all)'),nl,
    print(' -cbc_deadlock constraint-based deadlock checking'),nl,
    ( \+ option_verbose -> true ;
    print(' -cbc_deadlock_pred PRED as above but with additional predicate'),nl
    ),
    print(' -cbc_assertions constraint-based static assertion checking'),nl,
    print(' -cbc_refinement constraint-based static refinement checking'),nl,
    print(' -cbc_sequence S constraint-based search for sequence of operations'),nl,
    print(' -strict raise error if model-checking finds counter example'),nl,
    print(' or trace checking fails or any error state found'),nl,
    print(' -expcterr ERR expect error to occur (ERR=cbc,mc,ltl,...)'),nl,
    print(' -animate Nr random animation (max. Nr steps)'),nl,
    print(' -animate_all random animation until a deadlock is reached'),nl,
    print(' -animate_stats provide feedback which operations are animated or executed'),nl,
    print(' -execute Nr execute specification (maximally Nr steps)'),nl,
    print(' in contrast to -animate: stops at first operation found, is deterministic,'),nl,
    print(' does not store intermediate states and does not use TIME_OUT preference'),nl,
    print(' -execute_all execute until a deadlock, direct loop, goal or error is reached'),nl,
    print(' -execute_monitor monitor performance of execute'),nl,
    print(' -his File write history to File'),nl,
    print(' -his_option O additional option when writing a history (show_init,show_states,json,trace_file)'),nl,
    print(' -sptxt File save constants and variable values of last discovered state to File'),nl,
    print(' -sstxt Dir save constants and variable values of all discovered states to files in Dir'),nl,
    print(' -cache Directory automatically save constants to files and avoid recomputation'),nl,
    print(' -det_check check if animation steps are deterministic'),nl,
    print(' -det_constants only check if SETUP_CONSTANTS step is deterministic'),nl,
    ( \+ option_verbose -> true ;
    print(' -i interactive animation. Only for interactive sessions,'),nl,
    print(' the output can arbitrarily change in future versions. '),nl,
    print(' Do not build automatic tools using the interactive mode'),nl
    ),
    print(' -repl start interactive read-eval-loop'),nl,
    print(' -eval "E" evaluate expression or predicate'),nl,
    print(' -eval_file FILE evaluate expression or predicate from file'),nl,
    print(' -c print coverage statistics'),nl,
    print(' -cc Nr Nr print and check coverage statistics'),nl,
    print(' -vacuity_check look for vacuous implications in invariant'),nl,
    print(' -cbc_redundant_invariants Nr find redundant invariants, expecting Nr'),nl, % Nr exepcted
    print(' -statistics print memory and other statistics at the end'),nl,
    print(' -p PREF Val set preference to value'),nl,
    print(' -prefs FILE set preferences from Prolog file'),nl,
    print(' -pref_group GROUP SETTING set group of preferences to predefined values'),nl,
    print(' -card GS Val set scope of B deferred set'),nl,
    print(' -goal "PRED" set GOAL predicate for model checker'),nl,
    print(' -check_goal check GOAL (after -mc, -t, or -animate)'),nl,
    print(' -scope "PRED" set scope predicate for model checker'),nl,
    print(' -s Port start socket server on given port'),nl,
    print(' -ss start socket server on port 9000'),nl,
    print(' -sf start socket server on some free port'),nl,
    print(' -l LogFile log activities in LogFile'),nl,
    print(' -ll log activities in /tmp/prob_cli_debug.log'),nl,
    ( \+ option_verbose -> true ;
    print(' -lg LogFile analyse logfile using gnuplot'),nl
    ),
    print(' -logxml LogFile log activities in XML LogFile'),nl,
    print(' -logxml_write_ids P write variables/constants starting with P to XML LogFile'),nl,
    print(' -pp FILE pretty-print internal representation to file (or user_output)'), nl,
    print(' -ppf FILE like -pp, but force printing of all type infos'),nl,
    print(' -ppB FILE pretty-print Event-B model to file in valid B syntax'),nl,
    print(' -v verbose'),nl,
    ( \+ option_verbose -> true ;
    print(' -vv very verbose'),nl
    ),
    print(' -mc_with_tlc model check using the model checker TLC'),nl,
    print(' -mc_with_lts_sym model check using the model checker LTSmin (symbolic)'),nl,
    print(' -mc_with_lts_seq model check using the model checker LTSmin (sequential)'),nl,

    ( \+ option_verbose -> true ;
    print(' -ltsmin_option OPT set option for LTSmin (e.g, por)'),nl,
    print(' -ltsmin_ltl_output FILE set output file for LTSMin'),nl,
    print(' -symbolic_model_check ALGO ALGO is bmc, kinduction, ctigar, ic3'),nl,
    print(' -enabling_analysis_csv FILE perform operation enabling analysis'),nl,
    print(' -feasibility_analysis perform operation feasibility analysis'),nl,
    print(' -read_write_matrix show read/write matrix for operations'),nl
    ),
    print(' -version print version information (-svers for short info)'),nl,
    print(' -check_java_version check that Java version compatible with ProB parser'),nl,
    print(' -assertions check ASSERTIONS'),nl,
    print(' -main_assertions check ASSERTIONS from main file only'),nl,
    print(' -properties check PROPERTIES'),nl,
    print(' -cache Dir use directory "Dir" to cache constants and variables'),nl,
    print(' -ltlfile F check LTL formulas in file F'),nl,
    print(' -ltlassertions check LTL assertions (in DEFINITIONS)'),nl,
    print(' -ltllimit L explore at most L states when model-checking LTL or CTL'),nl,
    print(' -ltlformula \"F\" check the LTL formula F'),nl,
    print(' -ctlformula \"F\" check the CTL formula F'),nl,
    print(' -save File save state space for later refinement check'),nl,
    print(' -refchk File refinement check against previous saved state space'),nl,
    print(' -mcm_tests Depth MaxStates EndPredicate File'),nl,
    print(' generate test cases with maximum length Depth, explore'),nl,
    print(' maximally MaxStates, the last state satisfies EndPredicate'),nl,
    print(' and the test cases are written to File'),nl,
    print(' -mcm_cover Operation'),nl,
    print(' when generating MCM test cases, Operation should be covered'),nl,
    print(' -cbc_tests Depth EndPredicate File'),nl,
    print(' generate test cases by constraint solving with maximum'),nl,
    print(' length Depth, the last state satisfies EndPredicate'),nl,
    print(' and the test cases are written to File'),nl,
    print(' -cbc_cover Operation'),nl,
    print(' when generating CBC test cases, Operation should be covered'),nl,
    % print(' -cbc_cover_all try and cover all operations'),nl, % is now default if no cbc_cover provided
    print(' -test_description File'),nl,
    print(' read information for test generation from File'),nl,
    print(' -dot CMD File write a graph to a dot file, with CMD being one of:'),nl,
    (is_dot_command(Cmd),command_description(Cmd,_,Desc),
    format(' ~w : ~w~n',[Cmd,Desc]),fail
    ; true),
    print(' -dotexpr CMD Expr File write a graph for Expr to a dot file, with CMD:'),nl,
    (is_dot_command_for_expr(Cmd),command_description(Cmd,_,Desc),
    format(' ~w : ~w~n',[Cmd,Desc]),fail
    ; true),
    print(' -dot_output Path generate dot files for false assertions/properties'),nl,
    print(' -dot_all also generate dot files for true assertions/properties'),nl,
    print(' -csvhist E File evaluate expression over history and generate CSV file.'),nl,
    print(' -load_state File load state from a saved state (generated by ProB Tcl/Tk or -save_state)'),nl,
    % For Eclipse Version only
    %% print(' -parsercp CP class path of the B Parser, this has to be a valid Java class path'),nl,
    %% print(' -cspm load CSP-M .csp file rather than B Machine .mch/.ref/.imp File'),nl,
    %% print(' -csp load CSP-M .pl file rather than B Machine File'),nl,

    /* Options -cspref, -cspdeadlock, -cspdeterministic, and -csplivelock are deprecated, should be excluded in favor of -csp_assertion */
    print(' -cspref Spec [m= Impl File'),nl,
    print(' checks a refinement statement,'),nl,
    print(' where Spec and Impl are processes from File, and \'m\' the type of the refinement:'),nl,
    print(' \'T\' for traces, \'F\' for failures, or \'FD\' for failures-divergences.'),nl,
    print(' -cspdeadlock P m File'),nl,
    print(' checks a process for deadlock,'),nl,
    print(' where \'P\' is a process from File, and \'m\' the type of the model:'),nl,
    print(' \'F\' for failures and \'FD\' for failures-divergences.'),nl,
    print(' -cspdeterministic P m File'),nl,
    print(' checks a process for determinism,'),nl,
    print(' where \'P\' is a process from File, and \'m\' the type of the model:'),nl,
    print(' \'F\' for failures and \'FD\' for failures-divergences.'),nl,
    print(' -csplivelock P File'),nl,
    print(' checks a process for divergence,'),nl,
    print(' where \'P\' is a process from File.'),nl,
    /* Options -cspref, -cspdeadlock, -cspdeterministic, and -csplivelock are deprecated, should be excluded in favor of -csp_assertion */

    print(' -csp_assertion \"A\" File'),nl,
    print(' checks the CSP assertion \'A\' on file \'File\''),nl,
        print(' -csp_eval "E" evaluate CSP-M expression.'),nl,
    print(' -csp-guide File CSP||B: Use the CSP File to control the B machine'),nl,
    print(' '),nl,
    ( \+ option_verbose -> true
    ;
        print(' -test_mode set random seed to the Prolog\'s current random state'),nl,
    print(' -rc runtime checking of types/pre-/post-conditions'),nl,
    print(' -state_trace File read a file of B predicates (one per line) and try find a matching trace.'),nl

    ),
    print(' FILE extensions are: '),nl,
    print(' .mch for B abstract machines'),nl,
    print(' .ref for B refinement machines'),nl,
    print(' .imp for B implementation machines'),nl,
    print(' .sys for Event-B abstract machines'),nl,
    print(' .rmch for B Rule DSL machines'),nl,
    print(' .csp, .cspm for CSP-M files, same format as FDR'),nl,
    print(' .eventb for Event-B packages exported from Rodin ProB Plugin'),nl,
    print(' .tex, .zed for Z models'),nl,
    print(' .tla for TLA+ models'),nl,
    print(' .als for Alloy models'),nl,
    print(' .P for Prolog XTL models'),nl,
    ( option_verbose ->
    print(' Preferences PREF are: '),nl,
    print_eclipse_prefs
    ; otherwise ->
    print(' Use --help -v to print available preferences PREF'),nl
    ),
    print(' Set NO_COLOR environment variable to disable terminal colors'),nl,
    print(' More info at: http://www.stups.hhu.de/ProB/'),nl,
    print(' and at: http://www.prob2.de/probcli/'),nl,
    % http://www.stups.hhu.de/ProB/index.php5/Using_the_Command-Line_Version_of_ProB
    nl.

print_probcli_error_non_strict/2

print_prolog_flags/0

print_property_partitions/0

print_repeats/2

print_repl_prompt/0

print_repl_prompt/1

print_repl_prompt_s/1

print_set/1

print_sets/0

print_short_version/0

print_state_silent/1

print_total_probcli_timer/0

prob_trimcore_silent/0

prob_trimcore_verbose/0

probcli_add_light_warning/2

probcli_startup/0

process_cbc_assertion_result/2

process_cbc_assertion_result(time_out,_) :- !,
    write_result_to_file(no_counterexample_found('"TIME_OUT"')),
        print_red('*** TIME_OUT occurred ***'),nl,
        error_occurred(cbc_assertions_time_out).

process_cbc_assertion_result(no_counterexample_exists(Constants,TotPredicate,OtherInfo),AllowEnumWarning) :- !,
           print_green('No counter-example to ASSERTION exists '),(OtherInfo=[] -> true ; print(OtherInfo)),nl,
           (unfixed_typed_id_in_list(TID,CType,Constants) % TO DO: look only at component
            -> write_deferred_set_used(AllowEnumWarning),
                get_texpr_id(TID,CID),pretty_type(CType,CTypeS),
            format('Warning: Some constants use deferred sets (e.g., ~w:~w) which have only been checked for a single cardinality!~n',[CID,CTypeS])
            ; predicate_uses_unfixed_deferred_set(TotPredicate,CType)
            -> write_deferred_set_used(AllowEnumWarning),pretty_type(CType,CTypeS),
            format('Warning: Some quantified variables use deferred sets (e.g., ~w) which have only been checked for a single cardinality!~n',[CTypeS]) % happens for tests 1173, 1174
            ; write_result_to_file(no_counterexample_exists)
        %,print('Computing unsat core: '),nl,unsat_cores:unsat_core(TotPredicate,Core),print('CORE: '),translate:print_bexpr(Core),nl
       ). % WE HAVE A PROOF

process_cbc_assertion_result(no_counterexample_found,AllowEnumWarning) :- !,
           write_result_to_file(no_counterexample_found('"Enumeration Warning"')),
           print('No counter-example for ASSERTION found (*enumeration warning occured*)'),nl,
           (AllowEnumWarning=true -> true ; error_occurred(cbc_assertions_enumeration_warning)).

process_cbc_assertion_result(counterexample_found,_) :- !,
           write_result_to_file(counterexample_found),
    print_red('*** Counter-example for ASSERTION found ***'),nl,
           error_occurred(cbc_assertions),
           (silent_mode(on) -> true
    ; print('*** STATE = '),nl,
            current_b_expression(DBState), translate:print_bstate(DBState),nl,
            print('*** END ASSERTION counter-example STATE '),nl
           ),
           (get_dot_file('cbc_assertions',DFile) -> generate_dot_from_assertions(DFile) ; true).

process_cbc_assertion_result(Res,A) :-
           write_result_to_file(Res),
           add_internal_error('Unknown: ',process_cbc_assertion_result(Res,A)).

process_ltsmin_result/1

profile_statistics/0

profiling_on/0

recognised_cli_option/4

recognised_option/2

recognised_option('-dot_all',dot_generate_for_all_formulas). % generate dot also for true formulas

recognised_option('-animate_all',cli_random_animate(2147483647,false)).

recognised_option('-execute_all',execute(2147483647,false,current_state)).

recognised_option('-execute_all_inits',execute(2147483647,false,from_all_initial_states)).

recognised_option('-animate_stats',animate_stats).

recognised_option('-execute_monitor',execute_monitoring).

recognised_option('-check_goal',check_goal).

recognised_option('-ltlassertions',ltl_assertions).

recognised_option('-assertions',cli_check_assertions(all,[false/0,unknown/0])).

recognised_option('-main_assertions',cli_check_assertions(main,[false/0,unknown/0])).

recognised_option('-properties',cli_check_properties).

recognised_option('-selfcheck',selfcheck(_)).

recognised_option('-pacheck',pa_check). % predicate analysis for Kodkod

recognised_option('-det_check',det_check). % check if animation is deterministic

recognised_option('-det_constants',det_constants_check). % check if animation for setup_constants is deterministic

recognised_option('-bf',breadth_first).

recognised_option('-breadth',breadth_first).

recognised_option('-df',depth_first).

recognised_option('-depth',depth_first).

recognised_option('-strict',strict_raise_error).

recognised_option('-silent',silent).

recognised_option('-statistics',statistics).

recognised_option('-profile_statistics',profile_statistics).

recognised_option('-reset_profile_statistics',reset_profiler). % mainly for use in REPL

recognised_option('-nodead',no_deadlocks).

recognised_option('-noinv',no_invariant_violations).

recognised_option('-nogoal',no_goal).

recognised_option('-noltl',no_ltl). % just used for TLC at the moment

recognised_option('-noass',no_assertion_violations).

recognised_option('-nocounter',no_counter_examples).

recognised_option('-disable_time_out',set_preference_group(time_out,disable_time_out)).

recognised_option('-disable_timeout',set_preference_group(time_out,disable_time_out)).

recognised_option('-i',animate).

recognised_option('-repl',eval_repl([])). % used to be -eval

recognised_option('-c',coverage(false)).

recognised_option('-cs',coverage(just_summary)).

recognised_option('-coverage',coverage(false)).

recognised_option('-coverage_summary',coverage(just_summary)).

recognised_option('-machine_stats',cli_print_machine_statistics).

recognised_option('-vc',variable_coverage).

recognised_option('-variable_coverage',variable_coverage).

recognised_option('-cv',coverage(true)).

recognised_option('-v',verbose).

recognised_option('-vv',very_verbose).

recognised_option('-verbose',verbose).

recognised_option('-very_verbose',very_verbose).

recognised_option('-profiling_on',profiling_on). % Prolog profiling

recognised_option('-profile',prob_profile). % ProB Operation profiling

recognised_option('-prob_profile',prob_profile). % ProB Operation profiling

recognised_option('-version',print_version).

recognised_option('-svers',print_short_version).

recognised_option('-short_version',print_short_version).

recognised_option('-check_java_version',check_java_version).

recognised_option('-java_version',check_java_version).

recognised_option('-release_java_parser',release_java_parser).

recognised_option('-file_info',file_info).

recognised_option('-t',trace_check).

recognised_option('-trace_check',trace_check).

recognised_option('-init',initialise).

recognised_option('-initialise',initialise).

recognised_option('-ll',log('/tmp/prob_cli_debug.log',prolog)).

recognised_option('-ss',socket(9000)).

recognised_option('-sf',socket(_)).

recognised_option('-help',help).

recognised_option('-h',help).

recognised_option('-rc',runtimechecking).

recognised_option('-test_mode',test_mode).

recognised_option('-check_complete',check_complete).

recognised_option('-check_complete_operation_coverage', check_complete_operation_coverage).

recognised_option('-mc_with_tlc', cli_start_mc_with_tlc).

recognised_option('-mc_with_lts_sym', cli_start_sym_mc_with_lts(symbolic)).

recognised_option('-mc_with_lts_seq', cli_start_sym_mc_with_lts(sequential)).

recognised_option('-core',disprover_options([disprover_option(unsat_core),unsat_core_algorithm/linear])).

recognised_option('-ltsmin',ltsmin).

recognised_option/3

recognised_option('-pref_group',set_preference_group(Group,Val),[Group,Val]).

recognised_option('-prefs',set_prefs_from_file(PREFFILE),[PREFFILE]).

recognised_option('-card',set_card(SET,SCOPE),[SET,SCOPE]).

recognised_option('-argv',set_argv(ARGV),[ARGV]).

recognised_option('-goal',set_goal(GOAL),[GOAL]).

recognised_option('-property',add_additional_property(PRED),[PRED]).

recognised_option('-scope',set_searchscope(GOAL),[GOAL]).

recognised_option('-searchscope',set_searchscope(GOAL),[GOAL]).

recognised_option('-eval',eval_string_or_file(string,E,exists,_,norecheck),[E]).

recognised_option('-evalt',eval_string_or_file(string,E,exists,'TRUE',norecheck),[E]).

recognised_option('-evalf',eval_string_or_file(string,E,exists,'FALSE',norecheck),[E]).

recognised_option('-evalt_rc',eval_string_or_file(string,E,exists,'TRUE',recheck(ascii)),[E]).

recognised_option('-evalf_rc',eval_string_or_file(string,E,exists,'FALSE',recheck(ascii)),[E]).

recognised_option('-evalu',eval_string_or_file(string,E,exists,'UNKNOWN',norecheck),[E]).

recognised_option('-eval_file',eval_string_or_file(file,F,exists,_ANY,norecheck),[F]).

recognised_option('-evalt_file',eval_string_or_file(file,F,exists,'TRUE',norecheck),[F]).

recognised_option('-eval_rule_file',eval_string_or_file(file,F,forall,_ANY,norecheck),[F]).

recognised_option('-parsercp',(L),[L]).

recognised_option('-lg',analyse_log(Log,timestamp,true),[Log]).

recognised_option('-lgr',analyse_log(Log,revision,false),[Log]).

recognised_option('-check_log',check_log(Log),[Log]).

recognised_option('-expcterr',expect_error(Type),[Type]).

recognised_option('-expecterr',expect_error(Type),[Type]).

recognised_option('-expect',expect_error(Type),[Type]).

recognised_option('-opterr',optional_error(Type),[Type]).

recognised_option('-his',history(File),[File]).

recognised_option('-his_option',history_option(Option),[Option]).

recognised_option('-cache',cache_storage(D),[D]).

recognised_option('-show_cache',show_cache,[]).

recognised_option('-MAIN',csp_main(ProcessName),[ProcessName]).

recognised_option('-ltlfile',ltl_file(Filename),[Filename]).

recognised_option('-ltlformula',ltl_formula_model_check(Formula,_),[Formula]).

recognised_option('-ltlformulat',ltl_formula_model_check(Formula,true),[Formula]).

recognised_option('-ltlformulaf',ltl_formula_model_check(Formula,false),[Formula]).

recognised_option('-ctlformula',ctl_formula_model_check(Formula,_),[Formula]).

recognised_option('-ctlformulat',ctl_formula_model_check(Formula,true),[Formula]).

recognised_option('-ctlformulaf',ctl_formula_model_check(Formula,false),[Formula]).

recognised_option('-load_state',load_state(Filename),[Filename]).

recognised_option('-refchk',refinement_check(Filename,0,100000),[Filename]).

recognised_option('-cspref',csp_in_situ_refinement_check(AbsP1,Type,ImplP2),[AbsP1,Type,ImplP2]).

recognised_option('-cspdeadlock',csp_checkAssertion(Proc,Model,'deadlock free'),[Proc,Model]).

recognised_option('-cspdeterministic',csp_checkAssertion(Proc,Model,'deterministic'),[Proc,Model]).

recognised_option('-csplivelock',csp_checkAssertion(Proc,'FD','livelock free'),[Proc]).

recognised_option('-csp_assertion',check_csp_assertion(Assertion),[Assertion]).

recognised_option('-csp_eval', eval_csp_expression(Expr),[Expr]).

recognised_option('-get_csp_assertions_as_string',csp_get_assertions,[]).

recognised_option('-prologOut',csp_translate_to_file(PlFile),[PlFile]).

recognised_option('-csp_guide',add_csp_guide(Filename),[Filename]).

recognised_option('-get_min_max_coverage',get_min_max_coverage(FileName),[FileName]).

recognised_option('-get_coverage_information',get_coverage_information(FileName),[FileName]).

recognised_option('-vacuity_check',vacuity_check,[]).

recognised_option('-cbc',constraint_based_check(OpName),[OpName]).

recognised_option('-cbc_deadlock',cbc_deadlock_check(true),[]).

recognised_option('-cbc_assertions',cbc_assertions(true,[]),[]).

recognised_option('-cbc_main_assertions',cbc_assertions(true,[main_assertions]),[]).

recognised_option('-cbc_assertions_proof',cbc_assertions(false,[]),[]). % do not allow enumeration warnings

recognised_option('-cbc_assertions_tautology_proof',cbc_assertions(false,[tautology_check]),[]). % do not allow enumeration warnings + disregard PROPERTIES, used for Atelier-B proof/disproof

recognised_option('-cbc_assertions_tautology_proof_check',cbc_assertions(false,[tautology_check,contradiction_check]),[]).

recognised_option('-cbc_option',cbc_option(OPT),[OPT]). % should be tautology_check,contradiction_check, unsat_core

recognised_option('-cbc_result_file',cbc_result_file(FILE),[FILE]). % write result to FILE

recognised_option('-cbc_refinement',cbc_refinement,[]).

recognised_option('-cbc_deadlock_pred',cbc_deadlock_check(GoalPred),[GoalPred]).

recognised_option('-cbc_sequence',cbc_sequence(OpSequence,'',single_solution),[OpSequence]).

recognised_option('-cbc_sequence_all',cbc_sequence(OpSequence,'',findall),[OpSequence]).

recognised_option('-cbc_sequence_with_target',cbc_sequence(OpSequence,TargetPredString,single_solution),[OpSequence,TargetPredString]).

recognised_option('-cbc_sequence_with_target_all',cbc_sequence(OpSequence,TargetPredString,findall),[OpSequence,TargetPredString]).

recognised_option('-comment',comment(UserComment),[UserComment]). % not processed by tool, but will be stored in log-file and used by log_analyser

recognised_option('-junit',junit(Dir),[Dir]).

recognised_option('-mcm_cover', mcm_cover(Event),[Event]).

recognised_option('-cbc_cover', cbc_cover(Event),[Event]).

recognised_option('-cbc_cover_match', cbc_cover(match_event(Event)),[Event]). % find events which have Event String occuring somewhere in name

recognised_option('-cbc_cover_all', cbc_cover_all,[]). % is now default if no cbc_cover provided

recognised_option('-cbc_cover_final', cbc_cover_final,[]).

recognised_option('-bmc', cbc_tests(Depth,'#not_invariant',''),[Depth]).

recognised_option('-dot_output',dot_analyse_output_prefix(Path),[Path]).

recognised_option('-evaldot',evaldot(File),[File]).

recognised_option('-enabling_analysis',enabling_analysis_csv(user_output),[]).

recognised_option('-enabling_analysis_csv',enabling_analysis_csv(EnablingCsvFile),[EnablingCsvFile]).

recognised_option('-feasibility_analysis',feasibility_analysis_csv(1000,user_output),[]).

recognised_option('-read_write_matrix',generate_read_write_matrix_csv(user_output),[]).

recognised_option('-state_trace',state_trace(File),[File]).

recognised_option('-typecheckertest',typechecker_test(File),[File]).

recognised_option('-scc_trace',check_scc_for_ltl_formula(LtlFormula,SCC),[LtlFormula,SCC]).

recognised_option('-selfcheck_module',selfcheck(M),[M]).

recognised_option('-mc_mode',depth_breadth_first_mode(M),[M]). % can be mixed, hash, heuristic

recognised_option('-assertion',cli_check_assertions(specific(X),[false/0,unknown/0]),[X]).

recognised_option('-cbc_assertion',cbc_assertions(true,[specific(X)]),[X]). % check only a specific assertion

recognised_option('-symbolic_model_check', cli_symbolic_model_check(Algorithm), [Algorithm]).

recognised_option('-replay',eval_repl([File]),[File]). % used to be -eval

recognised_option('-ltsmin2',ltsmin2(EndpointPath), [EndpointPath]).

recognised_option('-ltsmin_ltl_output',ltsmin_ltl_output(Path), [Path]).

recognised_option('-ltsmin_option', ltsmin_option(X),[X]).

recognised_option/4

recognised_option(X,Opt,[],true) :- recognised_option(X,Opt). % options without arguments

recognised_option(X,Opt,Args,true) :- recognised_option(X,Opt,Args). % options with arguments but no code needed to check arguments

recognised_option('-mc',cli_mc(N),[Arg],user:mc_ok_arg(Arg,N)).

recognised_option('-model_check',cli_mc(LimitNr),[],true) :- max_tagged_integer(LimitNr).

recognised_option('-timeout',timeout(N),[Arg],tools:arg_is_number(Arg,N)). % for model checking, refinement checking and for disprover per PO

recognised_option('-time_out',timeout(N),[Arg],tools:arg_is_number(Arg,N)).

recognised_option('-s',socket(S),[Arg],tools:arg_is_number(Arg,S)).

recognised_option('-cc',coverage(N,N2,just_check_stats),[Arg,Arg2],
    (arg_is_number_or_wildcard(Arg,N),arg_is_number_or_wildcard(Arg2,N2))).

recognised_option('-hash',check_statespace_hash(H,_),[Arg],tools:arg_is_number(Arg,H)).

recognised_option('-hash64',check_statespace_hash(H,'64bit'),[Arg],tools:arg_is_number(Arg,H)).

recognised_option('-hash32',check_statespace_hash(H,'32bit'),[Arg],tools:arg_is_number(Arg,H)).

recognised_option('-ltllimit',ltl_limit(Nr),[Arg], tools:arg_is_number(Arg,Nr)).

recognised_option('-check_disprover_result',cli_check_disprover_result([true-TNr,false-FNr,unknown-UNr,failure-0]),[T,F,U],
    (arg_is_number_or_wildcard(T,TNr),arg_is_number_or_wildcard(F,FNr),arg_is_number_or_wildcard(U,UNr))).

recognised_option('-aa',cli_check_assertions(all,[true/TNr,false/FNr,unknown/UNr]),[T,F,U],
    (arg_is_number_or_wildcard(T,TNr),arg_is_number_or_wildcard(F,FNr),arg_is_number_or_wildcard(U,UNr))).

recognised_option('-ma',cli_check_assertions(main,[true/TNr,false/FNr,unknown/UNr]),[T,F,U],
    (arg_is_number_or_wildcard(T,TNr),arg_is_number_or_wildcard(F,FNr),arg_is_number_or_wildcard(U,UNr))).

recognised_option('-kodkod_comparision',kodkod_comparision(Nr),[Arg],tools:arg_is_number(Arg,Nr)).

recognised_option('-kodkod_performance',kodkod_performance(File,Nr),[File,Arg],tools:arg_is_number(Arg,Nr)).

recognised_option('-animate',cli_random_animate(N,true),[Steps],tools:arg_is_number(Steps,N)).

recognised_option('-execute',execute(N,true,current_state),[Steps],tools:arg_is_number(Steps,N)).

recognised_option('-logxml_write_vars',logxml_write_ids(variables,Prefix),[Prefix],true).

recognised_option('-logxml_write_ids',logxml_write_ids(all,Prefix),[Prefix],true).

recognised_option('-zmq_master',zmq_master(Identifier),[Identifier], true).

recognised_option('-cbc_tests', cbc_tests(Depth,EndPred,Output),[Depth,EndPred,Output],
    tools:check_filename_arg(Output,'cbc_tests')).

recognised_option('-mcm_tests', mcm_tests(Depth,MaxStates,EndPred,Output),[Depth,MaxStates,EndPred,Output],
    tools:check_filename_arg(Output,'mcm_tests')).

recognised_option('-test_description', test_description(File), [File],
    tools:check_filename_arg(File,'test_description')).

recognised_option('-all_paths', all_deadlocking_paths(File), [File],
    tools:check_filename_arg(File,'all_paths')).

recognised_option('-dot',dot_command(Category,File),[Category,File],
    tools:check_filename_arg(File,'dot')).

recognised_option('-spdot',dot_command(state_space,File),[File], tools:check_filename_arg(File,'spdot')). % we keep this : it is shown in Wiki

recognised_option('-dotexpr',dot_command_for_expr(Category,Expr,File,[]),[Category,Expr,File],
    tools:check_filename_arg(File,'dot')).

recognised_option('-csvhist',evaluate_expression_over_history_to_csv_file(Expr,File),[Expr,File],
    tools:check_filename_arg(File,'csvhist')).

recognised_option('-read_write_matrix_csv',generate_read_write_matrix_csv(CsvFile),
    [CsvFile],
    tools:check_filename_arg(CsvFile,'read_write_matrix_csv')).

recognised_option('-feasibility_analysis_csv',feasibility_analysis_csv(TimeOut,EnablingCsvFile),
    [TimeOut,EnablingCsvFile],
    tools:check_filename_arg(EnablingCsvFile,'feasibility_analysis_csv')).

recognised_option('-l',log(Log,prolog),[Log],
    tools:check_filename_arg(Log,'l')).

recognised_option('-log',log(Log,prolog),[Log],
    tools:check_filename_arg(Log,'log')).

recognised_option('-logxml',log(Log,xml),[Log],
    tools:check_filename_arg(Log,'logxml')).

recognised_option('-pp',pretty_print_internal_rep(File,needed,ascii),[File],
    tools:check_filename_arg(File,'pp')).

recognised_option('-ppunicode',pretty_print_internal_rep(File,needed,unicode),[File],
    tools:check_filename_arg(File,'pp')).

recognised_option('-ppf',pretty_print_internal_rep(File,all,ascii),[File],
    tools:check_filename_arg(File,'ppf')).

recognised_option('-ppB',pretty_print_internal_rep_to_B(File),[File],
    tools:check_filename_arg(File,'ppB')).

recognised_option('-save_state',save_state(Filename),[Filename],
    tools:check_filename_arg(Filename,'save_state')).

recognised_option('-save',save_state_for_refinement(Filename),[Filename],
    tools:check_filename_arg(Filename,'save')).

recognised_option('-sptxt',print_values(Filename),[Filename],
    tools:check_filename_arg(Filename,'sptxt')).

recognised_option('-sstxt',print_all_values(Dirname),[Dirname],
    tools:check_filename_arg(Dirname,'sstxt')).

recognised_option('-latex',process_latex_file(In,Out),[In,Out],
    (tools:check_filename_arg(In,'latex'),tools:check_filename_arg(Out,'latex'))).

recognised_option('-zmq_assertions',zmq_assertion(Identifier),[Identifier],true).

recognised_option('-zmq_worker',zmq_worker(Identifier),[Identifier], true).

recognised_option('-p',set_pref(NPREF,PREFVAL),[PREF,PREFVAL],user:normalise_pref_name(PREF,NPREF)).

recognised_option('-pref',set_pref(NPREF,PREFVAL),[PREF,PREFVAL],user:normalise_pref_name(PREF,NPREF)).

recognised_option('-cbc_redundant_invariants',cbc_redundant_invariants(Nr),[X],tools:arg_is_number(X,Nr)).

recognised_option('-expcterrpos',expect_error_pos(Type,LNr,CNr),[Type,Line,Col],
    (tools:arg_is_number(Line,LNr),tools:arg_is_number(Col,CNr))).

reload_mainfile/0

remove_constants/2

repl_multi_read_line/1

repl_multi_read_line_aux/3

reset_cli/0

reset_dot_file_number/0

reset_expected_error_occurred/0

set_current_probcli_command/1

set_dot_file_prefix/1

set_dot_file_prefix_if_option_set/1

set_junit_mode/1

set_new_random_seed/0

set_optional_errors/0

set_pref/2

set_prefs/0

set_random_seed_to_deterministic_start_seed/0

set_repl_input_file/2

show_cache/0

show_initialisation_summary/1

show_last_expression_as_table/0

show_operation_coverage_summary/1

specfile_trans_with_check/5

split_by_seperator/2

split_by_seperator2/2

start_animation_without_computing/0

start_check_disabled/2

start_ltsmin_srv/2

start_probcli_timer/1

start_xml_feature/2

start_xml_feature/4

stop_probcli_debug_timer/2

stop_probcli_timer/2

stop_probcli_timer/3

stop_xml_feature/2

store_last_error_location_for_repl/0

strip_leading_ws/2

strip_ws/2

strip_ws2/2

test_kodkod_and_exit/2

timeout_call/2

Meta: timeout_call(0,-)

translate_exception/2

treat_existence_error/4

trimcore_if_useful/1

truncate_animate_action/2

unset_analyse_hook/0

unset_current_probcli_command/0

we_need_only_static_assertions/1

write_deferred_set_used/1

write_dot_graph_to_new_file/2

write_important_xml_element_to_log/2

write_result_to_file/1

xml_log_machine_statistics/0

zmq_delayed_option/1

zmq_get_important_options/1

zmq_get_initialisation_term/1

zmq_important_option/1

zmq_set_important_options/1

zmq_set_option/1

zmq_start_master/2

zmq_start_master(invariant,Identifier) :-
    start_animation_without_computing,
    zmq_get_initialisation_term(InitTerm),
    (option(strict_raise_error) -> Strict = 1 ; Strict = 0),
    get_preference(port, PortStart),
    get_preference(max_states, Max),
    get_preference(ip, IP),
    get_preference(logdir, LogDir),
    get_preference(tmpdir, TmpDir),
    get_preference(hash_cycle, HashCycle),
    atom_concat(LogDir, '/distb-', ATmp),
    atom_concat(ATmp, Identifier, Logfile),
    atom_concat(TmpDir, '/db-distb-', TTmp),
    atom_concat(TTmp, Identifier, TmpDir2),
    start_master(InitTerm,Max,PortStart,Strict,IP,Logfile,TmpDir2,HashCycle),
    halt.

zmq_start_master(assertion,Identifier) :-
    get_preference(port, PortStart),
    get_preference(logdir, LogDir),
    get_preference(ip, IP),
    get_preference(tmpdir, TmpDir),
    get_preference(hash_cycle, HashCycle),
    atom_concat(LogDir, '/distb-', ATmp),
    atom_concat(ATmp, Identifier, Logfile),
    atom_concat(TmpDir, '/db-distb-', TTmp),
    atom_concat(TTmp, Identifier, TmpDir2),
    current_state_corresponds_to_setup_constants_b_machine,
    animation_mode(b),
    full_b_machine(Machine),
    b_get_assertions(_,static,SAss),
    b_get_assertions(_,dynamic,DAss),
    append(SAss,DAss,Ass),
    count_assertions(Ass,0,N),
    assert(master:assertion_count(N)),
    current_expression(_,State1),
    specfile:state_corresponds_to_set_up_constants(State1,State),
    zmq_get_important_options(Options),
    (option(strict_raise_error) -> Strict = 1 ; Strict = 0),
    %start_master(assertions(classical_b(Machine,Options),State,Ass),2,-1,PortStart,0,Strict,IP,Logfile,TmpDir2),
    start_master(assertions(classical_b(Machine,Options),State,Ass),2,PortStart,Strict,IP,Logfile,TmpDir2,HashCycle),
    halt.

zmq_start_worker/2

zmq_worker_load_model/1

zmq_worker_load_model(classical_b(Machine,Options)) :- !,
    debug_println(20,'ZMQ WORKER: Loading classical B model'),
    zmq_set_important_options(Options),
    bmachine:b_machine_reset, bmachine:assert_main_machine(Machine),
    set_animation_mode(b),
    prob2_interface:start_animation, cli_computeOperations(_)
.

zmq_worker_load_model(classical_b_with_csp(Machine,CspGuide,Options)) :- !,
    debug_println(20,'ZMQ WORKER: Loading CSP || B model'),
    zmq_set_important_options(Options),
    bmachine:b_machine_reset, bmachine:assert_main_machine(Machine),
    set_animation_mode(b),
    prob2_interface:start_animation,
    tcltk_add_csp_file(CspGuide), % TO DO: use CSP Prolog term rather than filename <----------------
    prob2_interface:start_animation,
    cli_computeOperations(_)
.

zmq_worker_load_model(eventb(Machine,Options)) :- !,
    zmq_set_important_options(Options),
    bmachine:b_machine_reset, bmachine:assert_main_machine(Machine),
    set_animation_mode(b), set_animation_minor_mode(eventb),
    prob2_interface:start_animation, cli_computeOperations(_).

zmq_worker_load_model(csp_specification(CSPFile,Options)) :-
    zmq_set_important_options(Options),
    load_cspm_spec_from_cspm_file(CSPFile), % TO DO: pass CSP Prolog term rather than filename
    prob2_interface:start_animation, cli_computeOperations(_).

zmq_worker_load_model(filename(FN)) :- !,
    printsilent('loading file by filename\n'),flush_output,
    ( is_eventb_b(FN) ->
    eclipse_interface:load_eventb_file(FN)
    ; otherwise ->
    bmachine:b_load_machine_probfile(FN)),
    prob2_interface:start_animation.

zmq_worker_load_model(assertions(Machine,State,Assertions)) :- !,
    assert(assertion_counter(-1)),
    println_silent(loaded_model_for_assertion_checking),
    zmq_worker_load_model(Machine),
    assert(worker:assertion_state(State)),
    make_assertionwps(Assertions).

zmq_worker_load_model(Other) :-
    add_internal_error('ZMQ worker: Unexpected machine description', zmq_worker_load_model(Other)),
    fail.

Determinacy Checker

Determinacy Checker:

! 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_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_debug_flag,true)
! Existence error in debug:global_debug_flag/0
! procedure debug:global_debug_flag/0 does not exist
! goal: debug:global_debug_flag
! Existence error in debug:use_timer/0
! procedure debug:use_timer/0 does not exist
! goal: debug:use_timer
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_35495,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/error_manager.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(disable_chr,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),_198539,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/typing_tools.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(cogen,true)
! 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),_242049,[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(b_state_model_check) does not exist
! goal: absolute_file_name(probsrc(b_state_model_check),_242195,[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 probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_235791,[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),_237029,[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(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_242493,[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 extension('regexp/regexp') does not exist
! goal: absolute_file_name(extension('regexp/regexp'),_237651,[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 probcspsrc(haskell_csp) does not exist
! goal: absolute_file_name(probcspsrc(haskell_csp),_238365,[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 user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_observe_runtime,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_profile,true)
! Existence error in argument 1 of absolute_file_name/3
! file prozsrc(z_tools) does not exist
! goal: absolute_file_name(prozsrc(z_tools),_232799,[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'),_232511,[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 probsrc(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_234605,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kodkod/kodkod.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bmachine) does not exist
! goal: absolute_file_name(probsrc(bmachine),_234605,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kodkod/kodkod.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(self_check) does not exist
! goal: absolute_file_name(probsrc(self_check),_234605,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kodkod/kodkod.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_234605,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kodkod/kodkod.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(translate) does not exist
! goal: absolute_file_name(probsrc(translate),_234605,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kodkod/kodkod.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(predicate_analysis) does not exist
! goal: absolute_file_name(probsrc(predicate_analysis),_234605,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kodkod/kodkod.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(btypechecker) does not exist
! goal: absolute_file_name(probsrc(btypechecker),_234605,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kodkod/kodkod.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_global_sets) does not exist
! goal: absolute_file_name(probsrc(b_global_sets),_232657,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kodkod/kodkod.pl')])
! Existence error in debug:global_debug_flag/0
! procedure debug:global_debug_flag/0 does not exist
! goal: debug:global_debug_flag
! Existence error in debug:use_timer/0
! procedure debug:use_timer/0 does not exist
! goal: debug:use_timer
! Existence error in debug:global_debug_flag/0
! procedure debug:global_debug_flag/0 does not exist
! goal: debug:global_debug_flag
! Existence error in debug:use_timer/0
! procedure debug:use_timer/0 does not exist
! goal: debug:use_timer
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_profile,true)
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_198251,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/memoization.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),_194119,[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 debug:global_debug_flag/0
! procedure debug:global_debug_flag/0 does not exist
! goal: debug:global_debug_flag
! 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 chrsrc(chr_integer_inequality) does not exist
! goal: absolute_file_name(chrsrc(chr_integer_inequality),_194407,[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 user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in debug:global_debug_flag/0
! procedure debug:global_debug_flag/0 does not exist
! goal: debug:global_debug_flag
! 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 extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_164641,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/state_space.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_myheap,false)
! Existence error in tools:platform_is_64_bit/0
! procedure tools:platform_is_64_bit/0 does not exist
! goal: tools:platform_is_64_bit
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(debug) does not exist
! goal: absolute_file_name(probsrc(debug),_149629,[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 extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_155145,[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'),_152717,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/value_persistance.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_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file smt_solvers_interface(smt_solvers_interface) does not exist
! goal: absolute_file_name(smt_solvers_interface(smt_solvers_interface),_144081,[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 probcspsrc(haskell_csp) does not exist
! goal: absolute_file_name(probcspsrc(haskell_csp),_134273,[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),_118355,[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(btypechecker) does not exist
! goal: absolute_file_name(probsrc(btypechecker),_97609,[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'),_101563,[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 extension('random_permutations/random_permutations') does not exist
! goal: absolute_file_name(extension('random_permutations/random_permutations'),_88887,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_objects.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_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_data_validation_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(disable_chr,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(enable_time_out_for_constraints,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(enable_time_out_for_constraints,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(enable_time_out_for_constraints,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(enable_time_out_for_constraints,true)
! 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'),_63739,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/clpfd_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(specfile) does not exist
! goal: absolute_file_name(probsrc(specfile),_43267,[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),_43267,[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(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_43267,[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),_43267,[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),_43267,[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),_43267,[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(preferences) does not exist
! goal: absolute_file_name(probsrc(preferences),_43267,[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),_43267,[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(predicate_debugger) does not exist
! goal: absolute_file_name(probsrc(predicate_debugger),_43267,[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),_43267,[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),_43267,[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) does not exist
! goal: absolute_file_name(probsrc(state_space),_43267,[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),_43267,[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'),_19309,[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 probporsrc(static_analysis) does not exist
! goal: absolute_file_name(probporsrc(static_analysis),_32291,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/model_checker.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probcspsrc(haskell_csp) does not exist
! goal: absolute_file_name(probcspsrc(haskell_csp),_32291,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bvisual2.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file smt_solvers_interface(smt_solvers_interface) does not exist
! goal: absolute_file_name(smt_solvers_interface(smt_solvers_interface),_39511,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/solver_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_37137,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/solver_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_32437,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_state_model_check.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('user_signal/user_signal') does not exist
! goal: absolute_file_name(extension('user_signal/user_signal'),_19643,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/eclipse_interface.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'),_41965,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/symmetry_marker.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('user_signal/user_signal') does not exist
! goal: absolute_file_name(extension('user_signal/user_signal'),_40585,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/evalstores.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_myheap,false)
! Existence error in argument 1 of absolute_file_name/3
! file probltlsrc(ltl) does not exist
! goal: absolute_file_name(probltlsrc(ltl),_20691,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/prob2_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('user_signal/user_signal') does not exist
! goal: absolute_file_name(extension('user_signal/user_signal'),_21059,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/prob_socketserver.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probltlsrc(ltl) does not exist
! goal: absolute_file_name(probltlsrc(ltl),_273,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/prob_cli.pl')])

Name: RECURSIVE_CALL/2	Module: prob_cli.pl
Name: accumulated_infos/3	dynamic predicate
Name: assert/1
Name: is/2
Name: =/2
Name: true
Name: retract/1
Name: ->/3
Name: !
Name: >/2
Name: get_info/3	Module: prob_cli.pl

Name: cli_check_assertions/3	Module: prob_cli.pl
Name: cli_check_goal/0	Module: prob_cli.pl
Name: cli_check_properties/1	Module: prob_cli.pl
Name: load_spec_file/3	Module: prob_cli.pl

Name: eval_result/2	dynamic predicate
Name: assert/1
Name: is/2
Name: !
Name: retract/1

Name: fail
Name: add_warning/3	Module: foo_error
Name: nl
Name: model_checking_is_incomplete/6	Module: model_checker

Name: add_error/3	Module: foo_error
Name: translate_bexpression/2	Module: translate

Name: option/1	dynamic predicate
Name: not/1
Name: b_top_level_operation/1	Module: bmachine
Name: b_mode	Module: foo_error

Name: animate_machine2/0	Module: prob_cli.pl
Name: nl
Name: print/1

Name: RECURSIVE_CALL/0	Module: prob_cli.pl
Name: !
Name: fail
Name: cli_animateOperationNr/3	Module: prob_cli.pl
Name: =</2
Name: >/2
Name: number/1
Name: ->/3
Name: read/1
Name: print/1
Name: print_options/2	Module: prob_cli.pl
Name: nl
Name: length/2
Name: cli_computeOperations/1	Module: prob_cli.pl
Name: print_current_state/0	Module: prob_cli.pl

Name: RECURSIVE_CALL/1	Module: prob_cli.pl
Name: assertion_task/2	Module: worker
Name: assert/1
Name: assertion_counter/1	dynamic predicate
Name: is/2
Name: retractall/1

Name: RECURSIVE_CALL/1	Module: prob_cli.pl
Name: assert_option/1	Module: prob_cli.pl

Name: true
Name: set_error_manager_silent_mode/1	Module: foo_error
Name: set_silent_mode/1	Module: foo_error
Name: =/2
Name: ->/3
Name: option/1	dynamic predicate
Name: assert/1

Name: silent/0	Module: prob_cli.pl
Name: zmq_set_option/1	Module: prob_cli.pl
Name: assert_all_options/1	Module: prob_cli.pl
Name: go_cli2/1	Module: prob_cli.pl
Name: call_probcli_option/1	Module: prob_cli.pl

Name: browse_repl_lets	Module: foo_error
Name: browse_machine/1	Module: prob_cli.pl

Name: fail
Name: display_match/4	Module: prob_cli.pl
Name: format/2
Name: get_machine_identifier_names/7	Module: b_machine_hierarchy

Name: display_match/3	Module: prob_cli.pl
Name: get_machine_identifiers/2	Module: prob2_interface
Name: true
Name: =/2
Name: ->/3
Name: print_sets/0	Module: prob_cli.pl

Name: sort/2
Name: findall/3

Name: browse/0	Module: prob_cli.pl
Name: exec_eval_command/2	Module: prob_cli.pl
Name: eval_help/0	Module: prob_cli.pl

Name: on_exception/3
Name: cli_print_statistics/0	Module: prob_cli.pl
Name: !
Name: assert_option/1	Module: prob_cli.pl
Name: true
Name: option/1	dynamic predicate
Name: ->/3
Name: just_assert_option/1	Module: prob_cli.pl

Name: stop_xml_feature/2	Module: prob_cli.pl
Name: write_xml_element_to_log/2	Module: foo_error
Name: error_occurred/1	Module: prob_cli.pl
Name: nl
Name: print_red/1	Module: tools_printing
Name: =/2
Name: write_result_to_file/1	Module: prob_cli.pl
Name: process_cbc_assertion_result/2	Module: prob_cli.pl
Name: cbc_constraint_find_static_assertion_violation/2	Module: foo_error
Name: ->/3
Name: write_prolog_term_as_xml_to_log/1	Module: foo_error
Name: start_xml_feature/4	Module: prob_cli.pl
Name: print_repl_prompt_s/1	Module: prob_cli.pl
Name: check_loaded_not_empty/1	Module: prob_cli.pl
Name: findall/4

Name: fail
Name: cbc_redundant_invariants/1	Module: prob_cli.pl
Name: option/1	dynamic predicate
Name: cbc_refinement/0	Module: prob_cli.pl
Name: cbc_sequence/3	Module: prob_cli.pl
Name: cbc_assertions/2	Module: prob_cli.pl
Name: constraint_based_check/1	Module: prob_cli.pl
Name: cbc_deadlock_check/1	Module: prob_cli.pl

Name: fail
Name: nl
Name: eval_codes/6	Module: foo_error
Name: atom_codes/2
Name: format_with_colour/4	Module: tools_printing
Name: format/3
Name: functor/3
Name: lookup_value_for_existing_id/3	Module: store
Name: abstract_constant/2	Module: b_machine_hierarchy
Name: expand_const_and_vars_to_full_store/2	Module: foo_error
Name: current_expression/2	Module: state_space

Name: cli_load_files3/4	Module: prob_cli.pl
Name: cli_load_files/2	Module: prob_cli.pl
Name: halt_prob/1	Module: prob_cli.pl

Name: get_state_errors/1	Module: prob_cli.pl
Name: fail
Name: error_occurred_with_msg/2	Module: prob_cli.pl
Name: print_state_silent/1	Module: prob_cli.pl
Name: visited_expression/2	Module: state_space
Name: format/2
Name: ajoin/2	Module: tools_strings
Name: get_preference/2	Module: foo_error
Name: option/1	dynamic predicate
Name: not/1
Name: invariant_violated/1	Module: state_space

Name: add_error/2	Module: foo_error
Name: check_parser_version/0	Module: prob_cli.pl
Name: =/2
Name: ->/3
Name: format/2
Name: check_java_version/2	Module: parsercall

Name: check_loaded_not_empty/1	Module: prob_cli.pl
Name: cli_process_loaded_file_afer_start_animation/1	Module: prob_cli.pl

Name: check_loaded/1	Module: prob_cli.pl
Name: fail
Name: error_occurred/1	Module: prob_cli.pl
Name: add_error/3	Module: foo_error
Name: !
Name: file_loaded/2	dynamic predicate

prob_prolog/src/prob_cli.pl

Modules

Predicates of prob_cli.pl

Module Information

4288 Lines

382 Predicates

0 Exports

174 specified Imports

Predicates:

Name: if_option_set_loaded/3	Module: prob_cli.pl
Name: cbc_sequence/3	Module: prob_cli.pl
Name: cbc_redundant_invariants/1	Module: prob_cli.pl
Name: cbc_refinement/0	Module: prob_cli.pl
Name: constraint_based_check/1	Module: prob_cli.pl
Name: cbc_assertions/2	Module: prob_cli.pl

Name: cli_check_csp_assertion/2	Module: prob_cli.pl
Name: cli_checkAssertion/4	Module: prob_cli.pl

Name: cli_csp_in_situ_refinement_check/4	Module: prob_cli.pl
Name: cli_start_refinement_check/4	Module: prob_cli.pl

Name: add_internal_error/2	Module: foo_error
Name: check_expected/3	Module: prob_cli.pl
Name: nl
Name: print/1
Name: add_error/3	Module: foo_error
Name: format_with_colour/4	Module: tools_printing
Name: ==/2
Name: ->/3
Name: !
Name: =/2
Name: format/2
Name: add_warning/3	Module: foo_error
Name: incomplete_warning/2	Module: prob_cli.pl
Name: flush_output/1

Name: cli_ctl_model_check/3	Module: prob_cli.pl
Name: cli_ltl_model_check/3	Module: prob_cli.pl

Name: true
Name: clear_loaded_machines_wo_errors	Module: foo_error
Name: file_loaded/1	Module: prob_cli.pl
Name: ->/3

Name: reload_mainfile/0	Module: prob_cli.pl
Name: cli_load_files2/3	Module: prob_cli.pl

Name: add_additional_property/1	Module: bmachine
Name: debug_println/2	Module: foo_error

Name: executeOperationNr_on_computed_node/1	Module: foo_error
Name: true
Name: format/2
Name: >/2
Name: ->/3
Name: truncate_animate_action/2	Module: prob_cli.pl
Name: nth1/3	Module: lists
Name: option/1	dynamic predicate

Name: animate_machine2/0	Module: prob_cli.pl
Name: perform_random_step/4	Module: prob_cli.pl