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 prob_summary/1 expected_error_occurred/1 error_did_not_occur/1 current_probcli_command/1 accumulated_infos/3 individual_file_infos/3 merged_individual_file_infos/3 option/1

5633 Lines

471 Predicates

Imported Modules: module_information preferences lists system codesio debug error_manager specfile basic_unit_tests logger tcltk_interface eclipse_interface predicate_evaluator version alloy2b_benchmarks smt_solver_benchmarks eval_strings

9 Exports

227 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_memory_used_wo_gc/1 Module: tools Name: print_memory_used_wo_gc/0 Module: tools Name: split_atom/3 Module: tools Name: get_options/5 Module: tools 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: print_error/1 Module: tools_printing Name: format_with_colour/4 Module: tools_printing Name: format_with_colour_nl/4 Module: tools_printing Name: atom_split/4 Module: tools_strings Name: convert_atom_to_number/2 Module: tools_strings Name: safe_time_out/3 Module: tools_meta Name: count_occurences/2 Module: tools_lists Name: file_exists/1 Module: file_systems Name: between/3 Module: between Name: term_hash/2 Module: terms Name: random/3 Module: random Name: setrand/1 Module: random 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: pretty_type/2 Module: translate Name: safe_absolute_file_name/2 Module: tools Name: safe_absolute_file_name/3 Module: tools Name: convert_ms_time_to_string/2 Module: tools Name: counter_init/0 Module: counter/counter Name: new_counter/1 Module: counter/counter Name: get_counter/2 Module: counter/counter Name: inc_counter/1 Module: counter/counter Name: inc_counter/2 Module: counter/counter Name: reset_counter/1 Module: counter/counter Name: current_expression/2 Module: state_space Name: set_junit_dir/1 Module: junit_tests Name: create_and_print_junit_result/4 Module: junit_tests 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_check_sequence_from_file/3 Module: b_trace_checking Name: get_default_trace_file/3 Module: b_trace_checking Name: tcltk_save_history_as_trace_file/2 Module: b_trace_checking Name: tcltk_save_history_as_trace_file/3 Module: b_trace_checking Name: store_virtual_event/1 Module: eventhandling Name: b_set_initial_machine/0 Module: bmachine Name: run_typecheck_testcase/2 Module: test_typechecker Name: size_of_conjunction/2 Module: bsyntaxtree Name: get_texpr_id/2 Module: bsyntaxtree Name: get_texpr_description/2 Module: bsyntaxtree Name: conjunction_to_list/2 Module: bsyntaxtree Name: get_texpr_label/2 Module: bsyntaxtree Name: predicate_components/2 Module: bsyntaxtree Name: get_texpr_pos/2 Module: bsyntaxtree Name: b_write_machine_representation_to_file/3 Module: bmachine Name: full_b_machine/1 Module: bmachine Name: b_write_eventb_machine_to_classicalb_to_file/1 Module: bmachine Name: current_state_id/1 Module: state_space Name: get_state_space_stats/4 Module: state_space Name: compute_full_state_space_hash/1 Module: state_space Name: set_cspm_main_process/1 Module: xtl_interface 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: start_master/8 Module: zmq/master/master Name: start_worker/5 Module: zmq/worker/worker Name: start_ltsmin/4 Module: ltsmin/ltsmin Name: ltsmin_init/3 Module: ltsmin/ltsmin Name: ltsmin_loop/1 Module: ltsmin/ltsmin Name: ltsmin_teardown/2 Module: ltsmin/ltsmin Name: ltsmin_generate_ltlfile/2 Module: ltsmin/ltsmin Name: set_storage_directory/1 Module: value_persistance Name: start_prob_socketserver/2 Module: prob_socketserver Name: start_animation/0 Module: prob2_interface Name: is_initialised_state/1 Module: prob2_interface Name: reset_animator/0 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: load_xtl_spec_from_prolog_file/1 Module: prob2_interface Name: translate_error_term/2 Module: translate Name: statistics_memory_used/1 Module: tools Name: show_cache_file_contents/1 Module: value_persistance Name: print_runtime_profile/0 Module: runtime_profiler Name: print_source_profile/0 Module: source_profiler Name: print_memo_profile/0 Module: memoization Name: print_state_packing_profile/0 Module: state_packing Name: print_external_function_instantiation_profile/0 Module: external_functions Name: reset_memo_with_statistics/0 Module: memoization Name: print_mb/1 Module: tools Name: not_all_transitions_added/1 Module: state_space Name: not_invariant_checked/1 Module: state_space Name: not_interesting/1 Module: state_space Name: get_operation_name_coverage_infos/4 Module: state_space 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: get_specification_description/2 Module: specfile Name: static_cannot_enable/2 Module: static_enabling_analysis Name: add_new_transition_to_cache_from_expanded_state/3 Module: value_persistance 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: b_test_boolean_expression_for_ground_state/4 Module: b_interpreter Name: get_assertions_from_machine/2 Module: bmachine Name: b_get_machine_goal/1 Module: bmachine Name: b_get_assertions/3 Module: bmachine Name: replay_json_trace_file/2 Module: b_intelligent_trace_replay Name: extended_static_check_machine/1 Module: bmachine_static_checks 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: set_user_defined_scope/2 Module: b_global_sets Name: convert_cli_arg/2 Module: tools_strings 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: platform_is_64_bit/0 Module: tools_platform Name: b_machine_statistics/2 Module: bmachine Name: b_get_main_filename/1 Module: bmachine Name: b_get_all_used_filenames/1 Module: bmachine Name: get_full_b_machine_sha_hash/1 Module: bmachine Name: get_hex_bytes/2 Module: tools_strings Name: raw_sha_hash_file/3 Module: probhash/probhash Name: get_hex_bytes/2 Module: tools_strings Name: get_machine_file_number/4 Module: bmachine Name: b_absolute_file_name_relative_to_main_machine/2 Module: bmachine Name: get_parent_directory/2 Module: tools Name: get_tail_filename/2 Module: tools 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: load_spec_file_requires_extension/2 Module: pathes_extensions_db Name: available_extension/1 Module: pathes_lib Name: unavailable_extension/2 Module: pathes_lib Name: check_java_version/2 Module: parsercall Name: get_parser_version/1 Module: parsercall Name: ensure_console_parser_launched/0 Module: parsercall Name: connect_to_external_console_parser_on_port/1 Module: parsercall Name: install_lib_component/2 Module: pathes_lib Name: get_parser_version/1 Module: parsercall Name: get_java_command_path/1 Module: parsercall Name: get_java_fullversion/1 Module: parsercall Name: check_lib_contents/2 Module: pathes_lib Name: host_platform/1 Module: tools_platform Name: host_processor/1 Module: tools_platform Name: compile_time_flags/1 Module: compile_time_flags Name: relevant_prolog_flags/1 Module: compile_time_flags Name: get_cpp_version/1 Module: regexp/regexp Name: set_user_defined_scope/2 Module: b_global_sets Name: set_depth_breadth_first_mode/1 Module: state_space_exploration_modes Name: get_current_breadth_first_level/1 Module: state_space_exploration_modes Name: convert_cli_arg/2 Module: tools_strings Name: get_possible_preferences_matches_msg/2 Module: tools_matching 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: safe_open_file/4 Module: tools_io Name: print_bexpr/1 Module: translate Name: print_error/1 Module: tools_printing Name: format_error_with_nl/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: toggle_perfmessages/0 Module: performance_messages Name: show_dot_file/1 Module: tools_commands Name: show_pdf_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: open_file/1 Module: tools_commands Name: extract_file_line_col/6 Module: error_manager Name: source_code_for_identifier/6 Module: bmachine Name: read_atom_from_file/3 Module: tools Name: get_machine_identifiers/2 Module: bmachine 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: lookup_value_for_existing_id/3 Module: store Name: abstract_constant/2 Module: b_machine_hierarchy Name: is_interval_closure/3 Module: custom_explicit_sets Name: cbc_constants_det_check/1 Module: b_state_model_check Name: set_unicode_mode/0 Module: translate Name: unset_unicode_mode/0 Module: translate Name: set_atelierb_mode/1 Module: translate Name: unset_atelierb_mode/0 Module: translate Name: tcltk_nested_read_prolog_file_as_codes/2 Module: tools_printing Name: truncate_atom/3 Module: tools_strings Name: visited_expression/2 Module: state_space Name: b_machine_has_constants_or_properties/0 Module: bmachine Name: tcltk_read_write_matrix/1 Module: b_read_write_info Name: safe_intelligent_open_file/3 Module: tools_io Name: gen_relative_path_to_cur_dir/2 Module: tools Name: max_tagged_integer/1 Module: tools_platform Name: probcli_command_requires_extension/2 Module: pathes_extensions_db Name: set_no_color/1 Module: tools_printing Name: reset_no_color_to_default/0 Module: tools_printing Name: fuzzy_match_codes_lower_case/2 Module: tools_matching Name: get_possible_completions_msg/3 Module: tools_matching Name: safe_intelligent_open_file/3 Module: tools_io Name: announce_event/1 Module: eventhandling	Name: go_cli/0 Name: run_probcli/2 Name: run_probcli_with_argv_string/1 Name: reset_cli/0 Name: recognised_cli_option/4 Name: recognised_option/2 Name: go_proxy/0 Name: print_version/1 Name: cli_print_statistics/1

Imports

Exports

Name: startup_prob/0

Module: prob_startup

Name: string_concatenate/3

Module: tools

Name: arg_is_number/2

Module: tools

Name: print_memory_used_wo_gc/1

Module: tools

Name: print_memory_used_wo_gc/0

Module: tools

Name: split_atom/3

Module: tools

Name: get_options/5

Module: tools

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: print_error/1

Module: tools_printing

Name: format_with_colour/4

Module: tools_printing

Name: format_with_colour_nl/4

Module: tools_printing

Name: atom_split/4

Module: tools_strings

Name: convert_atom_to_number/2

Module: tools_strings

Name: safe_time_out/3

Module: tools_meta

Name: count_occurences/2

Module: tools_lists

Name: file_exists/1

Module: file_systems

Name: between/3

Module: between

Name: term_hash/2

Module: terms

Name: random/3

Module: random

Name: setrand/1

Module: random

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: pretty_type/2

Module: translate

Name: safe_absolute_file_name/2

Module: tools

Name: safe_absolute_file_name/3

Module: tools

Name: convert_ms_time_to_string/2

Module: tools

Name: counter_init/0

Module: counter/counter

Name: new_counter/1

Module: counter/counter

Name: get_counter/2

Module: counter/counter

Name: inc_counter/1

Module: counter/counter

Name: inc_counter/2

Module: counter/counter

Name: reset_counter/1

Module: counter/counter

Name: current_expression/2

Module: state_space

Name: set_junit_dir/1

Module: junit_tests

Name: create_and_print_junit_result/4

Module: junit_tests

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_check_sequence_from_file/3

Module: b_trace_checking

Name: get_default_trace_file/3

Module: b_trace_checking

Name: tcltk_save_history_as_trace_file/2

Module: b_trace_checking

Name: tcltk_save_history_as_trace_file/3

Module: b_trace_checking

Name: store_virtual_event/1

Module: eventhandling

Name: b_set_initial_machine/0

Module: bmachine

Name: run_typecheck_testcase/2

Module: test_typechecker

Name: size_of_conjunction/2

Module: bsyntaxtree

Name: get_texpr_id/2

Module: bsyntaxtree

Name: get_texpr_description/2

Module: bsyntaxtree

Name: conjunction_to_list/2

Module: bsyntaxtree

Name: get_texpr_label/2

Module: bsyntaxtree

Name: predicate_components/2

Module: bsyntaxtree

Name: get_texpr_pos/2

Module: bsyntaxtree

Name: b_write_machine_representation_to_file/3

Module: bmachine

Name: full_b_machine/1

Module: bmachine

Name: b_write_eventb_machine_to_classicalb_to_file/1

Module: bmachine

Name: current_state_id/1

Module: state_space

Name: get_state_space_stats/4

Module: state_space

Name: compute_full_state_space_hash/1

Module: state_space

Name: set_cspm_main_process/1

Module: xtl_interface

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: start_master/8

Module: zmq/master/master

Name: start_worker/5

Module: zmq/worker/worker

Name: start_ltsmin/4

Module: ltsmin/ltsmin

Name: ltsmin_init/3

Module: ltsmin/ltsmin

Name: ltsmin_loop/1

Module: ltsmin/ltsmin

Name: ltsmin_teardown/2

Module: ltsmin/ltsmin

Name: ltsmin_generate_ltlfile/2

Module: ltsmin/ltsmin

Name: set_storage_directory/1

Module: value_persistance

Name: start_prob_socketserver/2

Module: prob_socketserver

Name: start_animation/0

Module: prob2_interface

Name: is_initialised_state/1

Module: prob2_interface

Name: reset_animator/0

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: load_xtl_spec_from_prolog_file/1

Module: prob2_interface

Name: translate_error_term/2

Module: translate

Name: statistics_memory_used/1

Module: tools

Name: show_cache_file_contents/1

Module: value_persistance

Name: print_runtime_profile/0

Module: runtime_profiler

Name: print_source_profile/0

Module: source_profiler

Name: print_memo_profile/0

Module: memoization

Name: print_state_packing_profile/0

Module: state_packing

Name: print_external_function_instantiation_profile/0

Module: external_functions

Name: reset_memo_with_statistics/0

Module: memoization

Name: print_mb/1

Module: tools

Name: not_all_transitions_added/1

Module: state_space

Name: not_invariant_checked/1

Module: state_space

Name: not_interesting/1

Module: state_space

Name: get_operation_name_coverage_infos/4

Module: state_space

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: get_specification_description/2

Module: specfile

Name: static_cannot_enable/2

Module: static_enabling_analysis

Name: add_new_transition_to_cache_from_expanded_state/3

Module: value_persistance

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: b_test_boolean_expression_for_ground_state/4

Module: b_interpreter

Name: get_assertions_from_machine/2

Module: bmachine

Name: b_get_machine_goal/1

Module: bmachine

Name: b_get_assertions/3

Module: bmachine

Name: replay_json_trace_file/2

Module: b_intelligent_trace_replay

Name: extended_static_check_machine/1

Module: bmachine_static_checks

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: set_user_defined_scope/2

Module: b_global_sets

Name: convert_cli_arg/2

Module: tools_strings

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: platform_is_64_bit/0

Module: tools_platform

Name: b_machine_statistics/2

Module: bmachine

Name: b_get_main_filename/1

Module: bmachine

Name: b_get_all_used_filenames/1

Module: bmachine

Name: get_full_b_machine_sha_hash/1

Module: bmachine

Name: get_hex_bytes/2

Module: tools_strings

Name: raw_sha_hash_file/3

Module: probhash/probhash

Name: get_hex_bytes/2

Module: tools_strings

Name: get_machine_file_number/4

Module: bmachine

Name: b_absolute_file_name_relative_to_main_machine/2

Module: bmachine

Name: get_parent_directory/2

Module: tools

Name: get_tail_filename/2

Module: tools

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: load_spec_file_requires_extension/2

Module: pathes_extensions_db

Name: available_extension/1

Module: pathes_lib

Name: unavailable_extension/2

Module: pathes_lib

Name: check_java_version/2

Module: parsercall

Name: get_parser_version/1

Module: parsercall

Name: ensure_console_parser_launched/0

Module: parsercall

Name: connect_to_external_console_parser_on_port/1

Module: parsercall

Name: install_lib_component/2

Module: pathes_lib

Name: get_parser_version/1

Module: parsercall

Name: get_java_command_path/1

Module: parsercall

Name: get_java_fullversion/1

Module: parsercall

Name: check_lib_contents/2

Module: pathes_lib

Name: host_platform/1

Module: tools_platform

Name: host_processor/1

Module: tools_platform

Name: compile_time_flags/1

Module: compile_time_flags

Name: relevant_prolog_flags/1

Module: compile_time_flags

Name: get_cpp_version/1

Module: regexp/regexp

Name: set_user_defined_scope/2

Module: b_global_sets

Name: set_depth_breadth_first_mode/1

Module: state_space_exploration_modes

Name: get_current_breadth_first_level/1

Module: state_space_exploration_modes

Name: convert_cli_arg/2

Module: tools_strings

Name: get_possible_preferences_matches_msg/2

Module: tools_matching

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: safe_open_file/4

Module: tools_io

Name: print_bexpr/1

Module: translate

Name: print_error/1

Module: tools_printing

Name: format_error_with_nl/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: toggle_perfmessages/0

Module: performance_messages

Name: show_dot_file/1

Module: tools_commands

Name: show_pdf_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: open_file/1

Module: tools_commands

Name: extract_file_line_col/6

Module: error_manager

Name: source_code_for_identifier/6

Module: bmachine

Name: read_atom_from_file/3

Module: tools

Name: get_machine_identifiers/2

Module: bmachine

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: lookup_value_for_existing_id/3

Module: store

Name: abstract_constant/2

Module: b_machine_hierarchy

Name: is_interval_closure/3

Module: custom_explicit_sets

Name: cbc_constants_det_check/1

Module: b_state_model_check

Name: set_unicode_mode/0

Module: translate

Name: unset_unicode_mode/0

Module: translate

Name: set_atelierb_mode/1

Module: translate

Name: unset_atelierb_mode/0

Module: translate

Name: tcltk_nested_read_prolog_file_as_codes/2

Module: tools_printing

Name: truncate_atom/3

Module: tools_strings

Name: visited_expression/2

Module: state_space

Name: b_machine_has_constants_or_properties/0

Module: bmachine

Name: tcltk_read_write_matrix/1

Module: b_read_write_info

Name: safe_intelligent_open_file/3

Module: tools_io

Name: gen_relative_path_to_cur_dir/2

Module: tools

Name: max_tagged_integer/1

Module: tools_platform

Name: probcli_command_requires_extension/2

Module: pathes_extensions_db

Name: set_no_color/1

Module: tools_printing

Name: reset_no_color_to_default/0

Module: tools_printing

Name: fuzzy_match_codes_lower_case/2

Module: tools_matching

Name: get_possible_completions_msg/3

Module: tools_matching

Name: safe_intelligent_open_file/3

Module: tools_io

Name: announce_event/1

Module: eventhandling

Name: go_cli/0

Name: run_probcli/2

Name: run_probcli_with_argv_string/1

Name: reset_cli/0

Name: recognised_cli_option/4

Name: recognised_option/2

Name: go_proxy/0

Name: print_version/1

Name: cli_print_statistics/1

Predicates

Predicates:

:/2

accumulate_file_infos/3

accumulate_infos/2

accumulate_infos_2/2

add_eval_result/1

add_model_checking_warnings/4

add_vacuous_invariant/1

allow_filter_unused_constants/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_for_option/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_atom_looks_like_file/1

check_codes_look_like_file/2

check_codes_resembles_command/2

check_complete/0

check_complete_operation_coverage/0

check_deadlock_fail/1

check_expected/3

check_failures_mode/2

check_loaded_not_empty/1

check_machine_file_sha/2

check_model_result/2

check_nr_of_steps/1

check_parser_version/0

check_partial_trans/2

check_ref_result/1

check_required_infos/3

check_unavailable_options/0

clear_loaded_files/0

cli_add_additional_property/1

cli_animateOperationNr/3

cli_assertions_ko/3

cli_assertions_ko2/3

cli_checkAssertion/4

cli_check_assertions/2

cli_check_assertions/3

cli_check_csp_assertion/2

cli_check_goal/0

cli_check_op_cache/1

cli_check_properties/0

cli_check_properties/1

cli_check_scc_for_ltl_formula/2

cli_check_statespace_hash/2

cli_computeOperations/1

cli_core_properties/1

cli_csp_get_assertions/0

cli_csp_in_situ_refinement_check/4

cli_csp_translate_to_file/1

cli_ctl_model_check/4

cli_eval_csp_expression/1

cli_execute/3

cli_execute2/3

cli_execute_add_virtual_transition/3

cli_execute_add_virtual_transition/4

cli_generate_all_traces_until/2

cli_get_coverage_information/1

cli_ltl_model_check/4

cli_mc/2

cli_option_not_available/3

cli_print_all_values/1

cli_print_history/1

cli_print_junit_results/1

cli_print_machine_info/1

cli_print_pred_info/1

cli_print_statistics/1

cli_print_values/1

cli_process_loaded_file/2

cli_process_loaded_file_afer_start_animation/1

cli_process_options_for_alrady_fully_processed_file/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_start_animation/1

cli_start_default_trace_check/1

cli_start_initialisation/1

cli_start_logging/5

cli_start_mc_with_tlc/0

cli_start_model_check/3

cli_start_refinement_check/4

cli_start_selfcheck/0

cli_start_socketserver/2

cli_start_sym_mc_with_lts/1

cli_start_trace_check/3

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

compute_average/1

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

csv_table_command/4

default_json_trace_save/0

default_trace_check/0

definite_error_occurred/0

det_check_constants/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

dot_command/3

dot_command_for_expr/5

dot_file_number/1

dot_file_prefix/1

edit_main_file/0

empty_machine_loaded/0

error_occurred/1

error_occurred/2

error_occurred/4

error_occurred_with_msg/2

error_occurred_with_msg/3

eval_gen_enum_warning/1

eval_help/0

eval_line/1

eval_probcli_repl_line/1

eval_string_or_file/5

evaluate_from_commandline/0

exec_eval_command/2

execute/3

expected_error/1

file_extension_can_be_loaded/2

generate_read_write_matrix/1

generate_time_stamp/2

get_additional_infos/2

get_additional_stats/2

get_all_options/1

get_comma_or_space_separated_options/2

get_dot_file/2

get_error_category_and_type/3

get_error_or_warning_span/4

get_error_sources/0

get_errors/0

get_full_machine_file_path/2

get_info/3

get_next_nr/1

get_possible_fuzzy_match_options/2

get_possible_next_operation_for_execute/3

get_possible_options_completion_msg/2

get_probcli_elapsed_runtime/2

get_probcli_elapsed_walltime/2

get_quoted_atom/4

get_state_errors/1

get_state_space_errors/0

get_value_type/2

get_xml_add_description/2

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

install_prob_lib/2

interactive_animate_machine/0

irrelevant_xml_if_zero/1

irrelevant_xml_info/1

is_constant_binding/1

known_spec_file_extension/2

load_b_file_with_options/1

load_main_file/3

load_prob_file_with_options/1

loaded_root_filename/1

logxml_write_ids/2

ltl_check_assertions/0

mcm_test_case_generation/4

member_with_last/4

memory_intensive_option/1

merge_acc/4

merge_acc_infos/4

merge_accumulated_infos/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

options_can_eval_any_cst/0

parse_eval_command/3

perform/1

perform_feedback_options_after_exception/0

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

plantuml_command/2

plantuml_command_for_expr/4

pr_acc_infos_aux/3

pracc/2

pred_eval_hook/5

pretty_print_internal_rep/4

pretty_print_internal_rep_to_B/1

pretty_print_prolog_file/1

print_accumulated_infos/1

print_bindings/1

print_cbc_stats/2

print_compile_time_flags/0

print_cpp_version/1

print_csv_prefs/1

print_current_state/0

print_eval_command_help/1

print_individual_file/2

print_individual_file_infos_csv/2

print_memory_statistics/1

print_probcli_error_non_strict/2

print_probcli_version/1

print_prolog_flags/1

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/1

print_state_silent/1

print_titles/2

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_exception/2

process_ltsmin_result/2

profiling_on/0

recognised_cli_option/4

recognised_option/2

recognised_option/3

recognised_option/4

regular_safety_model_check/3

regular_safety_model_check_now/5

reload_mainfile/0

remove_constants/2

repl_evaluate_expressions/1

repl_multi_read_line/1

repl_multi_read_line/2

repl_multi_read_line_aux/4

reset_cli/0

reset_dot_file_number/0

reset_expected_error_occurred/0

run_probcli_with_argv_string/1

run_probcli_with_junit_check/1

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/1

show_initialisation_summary/1

show_last_expression_as_table/0

show_operation_coverage_summary/1

show_origin/1

show_source/1

sicstus_profile_statistics/0

silent/0

sort_assertions/2

specfile_trans_with_check/5

split_argv_string/2

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_repl_even_after_failure/0

start_repl_if_required/0

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

stop_xml_probcli_run/1

store_last_error_location_for_repl/0

test_kodkod_and_exit/2

translate_exception/2

translate_solver_result/2

treat_existence_error/4

treat_option/1

trim_quotes/2

trimcore_if_useful/1

truncate_animate_action/2

unset_analyse_hook/0

unset_current_probcli_command/0

we_need_only_static_assertions/1

write_cbc_check_result/1

write_cbc_check_result/2

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_animation/0

zmq_start_master/2

zmq_start_worker/2

zmq_worker_load_model/1

:/2

accumulate_file_infos/3

accumulate_infos/2

accumulate_infos_2/2

add_eval_result/1

add_model_checking_warnings/4

add_vacuous_invariant/1

allow_filter_unused_constants/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_for_option/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' -> BMC=invariant_violation
    ; TargetString = '#deadlock' -> BMC=deadlock
    ; BMC = 'none'),
    (BMC \= 'none' ->
    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),
    !,
    format('constraint based test case generation finished~n',[]),
    (BMC \= 'none'
    -> tcl_get_stored_test_cases(list(Tests)), %print(tests(Tests)),nl,
    (Tests=[] -> print_green('No counterexample found'),nl
    ; Tests = [_|_], BMC=deadlock -> add_error(deadlock,'Deadlock found by bmc')
    ; 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('Constraint based test case generation failed!'),
    error_occurred(cbc_tests).

check_abstract_constants/0

check_all_expected_errors_occurred/1

check_atom_looks_like_file/1

check_codes_look_like_file/2

check_codes_resembles_command/2

check_complete/0

check_complete_operation_coverage/0

check_deadlock_fail/1

check_expected/3

check_failures_mode/2

check_loaded_not_empty/1

check_machine_file_sha/2

check_model_result/2

check_nr_of_steps/1

check_parser_version/0

check_partial_trans/2

check_ref_result/1

check_required_infos/3

check_unavailable_options/0

clear_loaded_files/0

cli_add_additional_property/1

cli_animateOperationNr/3

cli_assertions_ko/3

cli_assertions_ko2/3

cli_checkAssertion/4

cli_check_assertions/2

cli_check_assertions/3

cli_check_csp_assertion/2

cli_check_goal/0

cli_check_op_cache/1

cli_check_properties/0

cli_check_properties/1

cli_check_scc_for_ltl_formula/2

cli_check_statespace_hash/2

cli_computeOperations/1

cli_core_properties/1

cli_csp_get_assertions/0

cli_csp_in_situ_refinement_check/4

cli_csp_translate_to_file/1

cli_ctl_model_check/4

cli_eval_csp_expression/1

cli_execute/3

cli_execute2/3

cli_execute2(Steps,ErrorOnDeadlock,FromWhere) :-
    FromWhere=from_all_initial_states,!,
    % try out all initial states and from each of those perform deterministic execution
    start_ms_timer(Start),
    format('Running execute from all initial states~n',[]),
    reset_counter(cli_execute_inits),
    findall(Result,
    (cli_trans(root,Action,CurState,0,'$NO_OPERATION'), %print(Action),nl,
    (\+ functor(Action,'$setup_constants',_)
    -> inc_counter(cli_execute_inits,Nr),
    format('~nExecuting model from initial state ~w~n',[Nr]),
    (option(animate_stats) -> print_state_silent(CurState) ; true),
    (cli_execute_from(CurState,Steps,ErrorOnDeadlock,1,Result) -> true)
    ; format('~nInitialising state~n',[]), % we need to execute initialise_machine
    cli_trans(CurState,_ActionName,NewState,0,'$NO_OPERATION'),
    inc_counter(cli_execute_inits,Nr),
    format('~nExecuting model from initial state ~w with constants~n',[Nr]),
    (option(animate_stats) -> print_state_silent(NewState) ; true),
    (cli_execute_from(NewState,Steps,ErrorOnDeadlock,2,Result) -> true)
    )), Results),
    get_counter(cli_execute_inits,Nr),
    format('---------~nTotal runtime for all ~w executions:',[Nr]),nl,
    stop_ms_timer(Start),
    count_occurences(Results,Occs), format('Results: ~w~n',[Occs]).

cli_execute2(Steps,ErrorOnDeadlock,current_state(Repetitions)) :-
    current_expression(ID,CurState),
    start_xml_feature(execute,max_steps,Steps,FINFO),
    start_ms_timer(Start),
    (between(1,Repetitions,RepNr),
    % with -strict option we will stop after first error found
    % for repetitions you should probably set RANDOMISE_OPERATION_ORDER and RANDOMISE_ENUMERATION_ORDER to TRUE
    debug_format(19,'Starting execute (~w/~w) from state ~w with maximum number of steps ~w~n',[RepNr,Repetitions,ID,Steps]),
    (cli_execute_from(CurState,Steps,ErrorOnDeadlock,1,_Result) -> fail ; fail)
    ; Repetitions>1 -> stop_ms_timer_with_msg(Start,'-execute-repeat')
    ; true),
    stop_xml_feature(execute,FINFO).

cli_execute_add_virtual_transition/3

cli_execute_add_virtual_transition/4

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: '),print_memory_used_wo_gc,flush_output,nl %nl_time
    ; true),
    prepare_state_for_specfile_trans(CurState0,unknown,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,NewID),
    %(option_verbose -> b_interpreter:analyse_invariant_for_state(NewID) ; true)
    b_interpreter:analyse_invariant_for_state(NewID)
    ; cli_assertions_ko(CurState,LastActionName,AssRes) -> % also recognises no_inv command
    N1 is Nr-1,
    format('ASSERTIONS ~w after ~w steps (after ~w).~n',[AssRes,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,LastActionName), % Compute new transition
    !,
    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/5

cli_find_ltl_ap/1

cli_generate_all_traces_until/2

cli_get_coverage_information/1

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
    ; assertz(file_loaded(true,MainFile)),
    trimcore_if_useful(Rest),
    writeln_log_time(start_processing(NOW)),
    start_probcli_timer(Timer),
    catch((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),
    start_repl_even_after_failure
    ),
    user_interrupt_signal, % catch CTRL-C by user but give chance to enter REPL
    start_repl_even_after_failure
    ),
    writeln_log_time(finished_processing(NOW))
    )
    ;
    assertz(file_loaded(error,MainFile)),
    print_error('Loading Specification Failed'),
    writeln_log_time(loading_failed(NOW,MainFile)),
    error_occurred(load_main_file)
    %start_repl_even_after_failure : TODO: fix issues with bmachine not precompiled and counter extension
    ),
    nls,
    ifm_option_set(indent_b_file(PPFILE0),
    indent_b_file(PPFILE0)),
    ifm_option_set(pretty_print_prolog_file(PPFILE0),
    pretty_print_prolog_file(PPFILE0))
    ; % not file_exists
    nl, assertz(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)
    ; get_filename_extension(MainFile,Ext), \+ known_spec_file_extension(Ext,_)
    -> (Ext = '' -> EMsg = 'Specified file does not exist and has no file extension:'
    ; ajoin(['Specified file does not exist and has an unrecognised file extension ".',Ext,'" :'], EMsg)
    ),
    add_error(load_main_file,EMsg,MainFile)
    ; add_error(load_main_file,'Specified file does not exist:',MainFile)
    )
    ),
    check_all_expected_errors_occurred(NOW),
    stop_xml_feature(process_file,FINFO),

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

cli_ltl_model_check/4

cli_mc/2

cli_option_not_available/3

cli_print_all_values/1

cli_print_history/1

cli_print_junit_results/1

cli_print_machine_info/1

cli_print_pred_info/1

cli_print_statistics/1

cli_print_values/1

cli_process_loaded_file/2

cli_process_loaded_file_afer_start_animation/1

Description:
TODO: replace

cli_process_loaded_file_afer_start_animation(NOW) :-
    ifm_option_set(cli_print_machine_info(IKind),
    cli_print_machine_info(IKind)),
    ifm_option_set(pretty_print_internal_rep(PPFILE1,MachName1,TYPES1,ASCII1),
    pretty_print_internal_rep(PPFILE1,MachName1,TYPES1,ASCII1)),
    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(check_abstract_constants,
    check_abstract_constants),

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

    if_option_set(cli_lint,cli_lint(_)),
    ifm_option_set_loaded(cli_lint(LintCheck),cli_lint,cli_lint(LintCheck)),
    if_option_set(cli_wd_check(Disch,TotPos),cli_wd_check(Disch,TotPos)),
    if_option_set(cli_wd_inv_proof(UnchangedNr,ProvenNr,TotPOsNr),cli_wd_inv_proof(UnchangedNr,ProvenNr,TotPOsNr)),
    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,MCOpts),model_check,
    cli_start_model_check(Nr,NOW,MCOpts)),
    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,init,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_coverage_information(CovFileName),cli_get_coverage_information(CovFileName)), %% TODO: replace
    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,
    (interactive_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)),
    if_options_set(run_benchmark(Kind,Option,Path), run_benchmark(Kind,Option,Path)),
    evaluate_from_commandline,
    if_option_set_loaded(ltl_assertions,check_ltl_assertions,
    (timeout_call(ltl_check_assertions,NOW,check_ltl_assertions) -> 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,init,Expected,_),NOW,check_ltl_assertions)
    -> true; true)),
    ifm_option_set_loaded(ltl_file(LtlFilename),check_ltl_file,
    (ltl_check_file(LtlFilename) -> true; true)),
    ifm_option_set_loaded(visb_history(VJSONFile,VHTMLFile,Options),visb,
    cli_visb_history(VJSONFile,VHTMLFile,Options)),
    ifm_option_set_loaded(history(HistoryFilename),history,
    cli_print_history(HistoryFilename)),
    ifm_option_set_loaded(print_values(ValuesFilename),sptxt,
    cli_print_values(ValuesFilename)),
    ifm_option_set_loaded(print_all_values(ValuesDirname),print_all_values,
    cli_print_all_values(ValuesDirname)),
    ifm_option_set_loaded(generate_all_traces_until(LTL_Stop_AsAtom,FilePrefix),generate_all_traces_until,
    cli_generate_all_traces_until(LTL_Stop_AsAtom,FilePrefix)),
    if_options_set(save_state_for_refinement(SaveRefF),
    tcltk_save_specification_state_for_refinement(SaveRefF)),
    if_options_set(rule_report(File),
    rule_validation:generate_report(File)),
    if_options_set(dot_command(DCommand1,DotFile1,DotEngine1),
    dot_command(DCommand1,DotFile1,DotEngine1)),
    if_options_set(dot_command_for_expr(DECommand,Expr,DotFile,Opts,DotEngine),
    dot_command_for_expr(DECommand,Expr,DotFile,Opts,DotEngine)),
    if_options_set(plantuml_command(PCommand1,UmlFile1),
    plantuml_command(PCommand1,UmlFile1)),
    if_options_set(plantuml_command_for_expr(PECommand,Expr,UmlFile,Opts),
    plantuml_command_for_expr(PECommand,Expr,UmlFile,Opts)),
    if_options_set(csv_table_command(TECommand,TableFormulas,TableOptions,TableCSVFile),
    csv_table_command(TECommand,TableFormulas,TableOptions,TableCSVFile)),
    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(check_op_cache(ExpectedC),
    cli_check_op_cache(ExpectedC)),
    ifm_option_set(coverage(ShowEnabledInfo),
    cli_show_coverage(ShowEnabledInfo,NOW)),
    if_option_set(save_state_space(StateFile),
    save_state_space(StateFile)),
    ifm_option_set(cli_print_statistics(SPARA),
    cli_print_statistics(SPARA)),
    if_option_set(show_cache(SCVM),
    show_cache(SCVM)),
    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_process_options_for_alrady_fully_processed_file/1

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_start_animation/1

cli_start_default_trace_check/1

cli_start_initialisation/1

cli_start_logging/5

cli_start_mc_with_tlc/0

cli_start_model_check/3

cli_start_refinement_check/4

cli_start_selfcheck/0

cli_start_socketserver/2

cli_start_sym_mc_with_lts/1

cli_start_trace_check/3

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

compute_average/1

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_cbc_check_result(Result,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_cbc_check_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

csv_table_command/4

default_json_trace_save/0

default_trace_check/0

definite_error_occurred/0

det_check_constants/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

dot_command/3

dot_command_for_expr/5

dot_file_number/1

Dynamic: true

dot_file_prefix/1

Dynamic: true

edit_main_file/0

empty_machine_loaded/0

error_occurred/1

error_occurred/2

error_occurred/4

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]),
    assertz(expected_error_occurred(Type)),
    (get_error_or_warning_span(ExtractedSpan,Type,EL,EC)
    -> (option(expect_error_pos(Type,EL,EC))
    -> debug_println(9,expect_error_pos_ok(Type,EL,EC))
    ; format('*** Unexpected line ~w and column ~w for error ~w!~n*** 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]),
    assertz(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]),
    formatsilent('% Optional error occured: ~w~n',[Type])
    ;
    write_xml_element_to_log(error_occurred,[category/Type, (type)/ErrOrWarning, message/Msg|XML]),
    (ErrOrWarning = warning -> safe_inc_counter(cli_warnings) ; safe_inc_counter(cli_errors)),
    flush_output, % ensure we can later associate position of error message
    (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("q",quit).

eval_command("quit",quit).

eval_command("halt",quit).

eval_command("x",exit).

eval_command("exit",exit).

eval_command("f",find).

eval_command("find",find).

eval_command("*",apropos).

eval_command("apropos",apropos).

eval_command("help",help).

eval_command("h",help).

eval_command("?",help).

eval_command("ctl",ctl). % :ctl

eval_command("ctlh",ctl_starthere). % :ctlh

eval_command("ltl",ltl). % :ltl

eval_command("ltlh",ltl_starthere). % :ltlh

eval_command("reset",reset_animator(hard)). % :reset

eval_command("reset-history",reset_animator(history_only)). % :reset

eval_command("statistics",statistics).

eval_command("stats",statistics). % :stats

eval_command("states",state_space_stats). % :states

eval_command("state",show_state_info(2000)). % :state

eval_command("statespace",state_space_display). % :statespace

eval_command("u",unsat_core).

eval_command("show",show_last_as_table). % :show

eval_command("dot",show_last_as_dot(no_dot_viewing)). % :dot

eval_command("dotty",show_last_as_dot(dotty)).

eval_command("dotpdf",show_last_as_dot(dot)).

eval_command("sfdp",show_last_as_dot(sfdp)).

eval_command("browse",browse). % :browse

eval_command("abstract_constants",check_abstract_constants). % :abstract_constants

eval_command("det_check_constants",det_check_constants). % :det_check_constants

eval_command("b",browse).

eval_command("hbrowse",hbrowse). % :hbrowse

eval_command("comp",show_components). % :comp

eval_command("replay",replay_repl_file). % :replay

eval_command("trim",trimcore). % :trim

eval_command("src",show_source). %:src

eval_command("source",show_source). %:source

eval_command("origin",show_origin). %:origin

eval_command("edit",edit_main_file).

eval_command("e",edit_main_file). % :e

eval_command("comment",comment).

eval_command("machine",show_machine_info(statistics)). %:machine

eval_command("machine-stats",show_machine_info(statistics)). %:machine

eval_command("files",show_machine_info(files)). %:files

eval_command("syntax",syntax_help). % :syntax

eval_command("open",open_file). % :open

eval_command_help/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(ltl_starthere,['F'],'Check LTL formula F starting from current state').

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

eval_command_help(ctl_starthere,['F'],'Check CTL formula F starting from current state').

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(det_check_constants,[],'Check if values of CONSTANTS are forced and explain if they are').

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(reset_animator(_),[],'Reset history and statespace of animator').

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(show_machine_info(_),[],'Show statistics about loaded machine and files').

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('z3-free',['P'],'Solve predicate P using Z3 solver (ignoring current state)').

eval_command_help('z3-file',['F'],'Solve predicate in File F using Z3 solver').

eval_command_help('z3-free-file',['F'],'Solve predicate in File F using Z3 solver (ignoring current state)').

eval_command_help(cdclt,['P'],'Solve predicate P using Prolog CDCL(T) solver').

eval_command_help(cdclt-free,['P'],'Solve predicate P using Prolog CDCL(T) solver (ignoring current state)').

eval_command_help(prob,['P'],'Solve predicate P using ProB solver (ignoring current state)').

eval_command_help('prob-file',['F'],'Solve predicate in File F using ProB solver (ignoring current state)').

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_command_help(syntax_help,[],'Show a summary of the B syntax accepted by the REPL').

eval_command_help(open_file,['FILE'],'Open FILE in preferred application.').

eval_gen_enum_warning/1

eval_help/0

eval_help :-
    print('ProB Interactive Expression and Predicate Evaluator '), nl,
    print('Type a valid B expressions or predicates, followed by RETURN or ENTER.'),nl,
    print('You can spread input over multiple lines by ending lines with "\\".'),nl,
    browse_machine([]),
    print('You can also type one of the following commands: '),nl,
    (option_verbose ->
    print(' + to save last expression to ProB unit tests.'),nl,
    print(' ! to go to deterministic propagation only mode.'),nl,
    print(' $ to print evaluation time for last expression.'),nl,
    print(' $$ to pretty-print last expression and its type.'),nl,
    print(' $$$ to pretty-print last expression in nested fashion.'),nl,
    print(' !p to toggle performance messages.'),nl,
    print(' !norm to toggle normalisation of results.'),nl,
    print(' :col to toggle colorizing of results.'),nl
    ; true),
    print(' :let x = E to define a new local variable x'),nl, % : optional for let
    print(' :unlet x to un-define a local variable'),nl,
    print(' #file=MYFILE to evaluate the formula in MYFILE'),nl,
    print(' @INVARIANT to evaluate or obtain invariant predicate'),nl,
    print(' @PROPERTIES, @GUARD-OpName ditto for properties and guards'),nl, % @FUZZ, @RANDOMISE also exist
    print(' :b or :b Prefix to browse the available identifiers'),nl,
    print(' :t E to get the type of an expression'),nl,
    print(' :r to reload the machine'),nl,
    print(' :show to display the last result as a table (if possible)'),nl,
    print(' :list CAT to display information with CAT : {files,variables,help,...}'),nl,
    print(' :* P to display constants/variables containing pattern P'),nl,
    print(' :core Pred to compute the unsat core for Pred'),nl,
    print(' :u to compute the unsat core for last evaluated result'),nl,
    print(' :stats to print the type and evaluation time for last query'),nl,
    print(' -PROBCLIARGS to pass command-line probcli arguments to the REPL'),nl,
    print(' (e.g., -v to switch to verbose mode or -p PREF VAL to set a preference)'),nl,
    print(' :ctl F or :ltl F to check a CTL or LTL formula.'),nl,
    print(' :f F to find a state satisfying LTL atomic property.'),nl,
    print(' :find-value PAT to find a value in current state matching PAT.'),nl,
    print(' :exec S to execute an operation or substitution S.'),nl,
    print(' :replay FILE to replay a file of commands.'),nl,
    print(' :z3 P, :cvc4 P, :kodkod P to solve predicate P using alternate solver'),nl,
    print(' :forall P to prove predicate P as universally quantified with default solver'),nl,
    print(' :prove P to prove predicate P using ProB\'s own WD prover'),nl,
    (option_verbose ->
    print(' :krt P, :pp P, :ml P to prove predicate P using Atelier-B provers if installed'),nl
    ; true),
    print(' :print P to pretty print predicate in a nested fashion'),nl,
    print(' :min P, :max P to find a minimal/maximal model for predicate P or %x.(P|E)'),nl,
    print(' :prefs to print current value of preferences'),nl,
    print(' :reset to reset the state space of the animator.'),nl, % :reset-history only resets history
    print(' :help CMD to obtain more help about a command.'),nl,
    print(' :state, :statespace, :states,'),nl,
    print(' :machine, :files, :source, :orgin, :machine-stats,'),nl,
    print(' :apropos, :hbrowse, :abstract_constants, :det_check_constants,'),nl,
    print(' :dot, :dotty, :sfdp, :trim, :comp - use :help CMD for more info'),nl,
    print(' :syntax to show a summary of the B syntax accepted by the REPL'),nl,
    print(' :q to exit.'),nl.

eval_line/1

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

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),
    eval0.

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

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(prob_cli:call_probcli_option,Options) -> true
    ; print_red('Failed to execute probcli arguments'),nl),
    eval0.

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

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

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

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

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

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_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,eval0.

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

eval_line("!print_coverage") :- !, nl,print_repl_prompt('PROLOG COVERAGE INFORMATION:'), nl,
    (current_prolog_flag(source_info,on) -> true ; print_red('Only useful when current_prolog_flag(source_info,on)!'),nl),
    catch(print_coverage,
    error(existence_error(_,_),_),
    print_red('CAN ONLY BE USED WHEN RUNNING PROB FROM SOURCE')),
    nl,
    eval0.

eval_line("!profile_reset") :- !, nl,print_repl_prompt('RESETTING PROLOG PROFILE INFORMATION'), nl,
    catch(profile_reset,
    error(existence_error(_,_),_),
    print_red('CAN ONLY BE USED WHEN RUNNING PROB FROM SOURCE')),
    eval0.

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

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

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) , eval0.

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

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

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

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

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
    ; nonvar(Expected) -> format('eval(~w): ~w~n',[Expected,String])
    ; format('eval: ~w~n',[String])
    ),
    reset_error_spans, % avoid underlining previous errors in eval_string
    (eval_string_with_time_out(String,StringResult,EnumWarning,_LS) -> true
    ; print_error('Eval string failed: '), print_error(String),
    error_occurred(eval_string)
    ),
    add_eval_result(StringResult),
    eval_check_result(StringResult,Expected,EnumWarning,eval_string,String),
    (Recheck=recheck(Mode) -> recheck_pp_of_last_expression(Mode,_,_) ; true),
    unset_current_probcli_command.

eval_string_or_file(file(bench),File,Quantifier,Expected,Recheck) :- !,
    ( member(Solver,[prob,kodkod,sat,'sat-z3','z3', 'cdclt']),
    (eval_string_or_file(file(Solver),File,Quantifier,Expected,Recheck) -> fail)
    ; true).

eval_string_or_file(file(Solver),File,Quantifier,Expected,_) :-
    % evaluate a single formula stored in a file
    set_current_probcli_command(eval_file(Solver,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,_]),
    statistics(walltime,[W1,_]),
    (Expected=='TRUE' -> TypeInfo=predicate(_) % avoids parsing as expression
    ; true),
    (eval_file(Solver,File,Quantifier,Result,EnumWarning,TypeInfo)
    -> statistics(walltime,[W2,_]), WT is W2-W1,
    translate_solver_result(Result,Infos),
    accumulate_file_infos(File,Solver,[walltime-WT|Infos]),
    add_eval_result(Result),
    eval_check_result(Result,Expected,EnumWarning,eval_file,File)
    ; statistics(walltime,[W2,_]), WT is W2-W1,
    accumulate_file_infos(File,Solver,[failure-1,false-0,true-0,unknown-1,walltime-WT]),
    add_eval_result(eval_file_failed),
    print_error('Eval from file failed: '), print_error(File),
    error_occurred(eval_file)
    ),
    statistics(runtime,[Stop,_]), Time is Stop - Start,
    debug_format(19,'Time for ~w : ~w ms (~w ms walltime)~n',[File,Time,WT]),
    turn_show_error_source_on,
    unset_current_probcli_command.

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 (hbrowse 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(det_check_constants,_) :-
    det_check_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) :- % :ctl
    atom_codes(F,FORMULA),
    (cli_ctl_model_check(F,init,_,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(ctl_starthere,FORMULA) :- % :ctlh for ctl here
    atom_codes(F,FORMULA),
    (cli_ctl_model_check(F,starthere,_,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) :- % :ltl
    atom_codes(F,FORMULA),
    (cli_ltl_model_check(F,init,_,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(ltl_starthere,FORMULA) :- % :ltl
    atom_codes(F,FORMULA),
    (cli_ltl_model_check(F,starthere,_,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(reset_animator(Hard),_) :- !,
    get_state_space_stats(TotalNodeSum,TotalTransSum,_,_),
    (Hard=hard ->
    format('Resetting statespace (~w states, ~w transitions)~n',[TotalNodeSum,TotalTransSum]),
    reset_animator
    ; format('Resetting animation history (keeping statespace: ~w states, ~w transitions)~n',[TotalNodeSum,TotalTransSum]),
    tcltk_reset % only resets animation history,...

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

exec_eval_command(state_space_stats,_) :- !, % :states
    get_state_space_stats(TotalNodeSum,TotalTransSum,Processed,Ignored),
    (Ignored>0
    -> format('Statespace: ~w states (~w processed, ~w ignored) and ~w transitions.~n',
    [TotalNodeSum,Processed,Ignored,TotalTransSum])
    ; format('Statespace: ~w states (~w processed) and ~w transitions.~n',[TotalNodeSum,Processed,TotalTransSum])).

exec_eval_command(state_space_display,_) :- !, % :statespace
    ( 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(Limit),_) :- !, % :state
    current_expression(ID,CurState),
    expand_const_and_vars_to_full_store(CurState,EState),
    format('Current state id ~w : ~n',[ID]), % MAX_DISPLAY_SET
    translate:print_bstate_limited(EState,Limit,-1),nl.

exec_eval_command(unsat_core,_) :- !, % :core :u
    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(syntax_help,_) :- !, % :syntax
    syntax_help.

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_pdf_file(PDFFile)
)).

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

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

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

exec_eval_command(show_machine_info(X),_) :- !, % :machine
    cli_print_machine_info(X).

exec_eval_command(edit_main_file,Arg) :- !, % :e
    (Arg=[] -> edit_main_file
    ; trim_quotes(Arg,FC), atom_codes(File,FC), file_exists(File) -> edit_file(File,unknown)
    ; exec_eval_command(show_origin,Arg)).

exec_eval_command(open_file,FILEC) :- !, % :open
    (FILEC=[] -> open_file('.')
    ; atom_codes(File,FILEC),
    open_file(File)
).

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

execute/3

expected_error/1

file_extension_can_be_loaded/2

generate_read_write_matrix/1

generate_time_stamp/2

get_additional_infos/2

get_additional_stats/2

get_all_options/1

get_comma_or_space_separated_options/2

get_dot_file/2

get_error_category_and_type/3

get_error_or_warning_span/4

get_error_sources/0

get_errors/0

get_full_machine_file_path/2

get_info/3

get_next_nr/1

get_possible_fuzzy_match_options/2

get_possible_next_operation_for_execute/3

get_possible_options_completion_msg/2

get_probcli_elapsed_runtime/2

get_probcli_elapsed_walltime/2

get_quoted_atom/4

get_state_errors/1

get_state_space_errors/0

get_value_type/2

get_xml_add_description/2

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

Meta: ifm_option_set(-,-,0)

ifm_option_set_loaded/3

Meta: ifm_option_set_loaded(-,-,0)

initialise_required/0

install_prob_lib/2

interactive_animate_machine/0

irrelevant_xml_if_zero/1

irrelevant_xml_info/1

is_constant_binding/1

known_spec_file_extension/2

load_b_file_with_options/1

load_main_file/3

load_prob_file_with_options/1

load_spec_file/2

load_spec_file('csp',MainFile) :- !, load_cspm_spec_from_cspm_file(MainFile).

load_spec_file('cspm',MainFile) :- !, load_cspm_spec_from_cspm_file(MainFile).

load_spec_file('P',MainFile) :- !, load_xtl_spec_from_prolog_file(MainFile).

load_spec_file('p',MainFile) :- !, load_xtl_spec_from_prolog_file(MainFile). % sometimes windows is confused about the upper case letter....

load_spec_file('eventb',MainFile) :- !, load_eventb_file(MainFile).

load_spec_file('v',MainFile) :- !,
    print('Warning: .v proof rule file format no longer supported, use -eval_rule_file FILE'),nl,
    % but even that may not work; some older rule files required predicate variables
    load_b_file_with_options(MainFile). % Siemens Rule File; now use -eval_rule_file

load_spec_file('prob',MainFile) :- !,load_prob_file_with_options(MainFile). % .prob files

load_spec_file('mch',MainFile) :- !,load_b_file_with_options(MainFile).

load_spec_file('sys',MainFile) :- !,load_b_file_with_options(MainFile).

load_spec_file('ref',MainFile) :- !,load_b_file_with_options(MainFile).

load_spec_file('imp',MainFile) :- !,load_b_file_with_options(MainFile).

load_spec_file('rmch',MainFile) :- !,load_b_file_with_options(MainFile).

load_spec_file('def',MainFile) :- !,load_b_file_with_options(MainFile). % .def DEFINITIONS file

load_spec_file('fuzz',MainFile) :- !,tcltk_open_z_file(MainFile).

load_spec_file('tex',MainFile) :- !,tcltk_open_z_tex_file(MainFile).

load_spec_file('zed',MainFile) :- !,tcltk_open_z_tex_file(MainFile). % proz .zed file

load_spec_file('als',MainFile) :- !,tcltk_open_alloy_file(MainFile).

load_spec_file('pla',MainFile) :- !,tcltk_open_alloy_prolog_ast_file(MainFile). % maybe we should detect .als.pl

load_spec_file('tla',MainFile) :- !, load_tla_file(MainFile).

load_spec_file('eval',File) :- !, % .eval file
    cli_set_empty_machine,
    assertz(option(eval_string_or_file(file(default),File,exists,_,norecheck))).

load_spec_file('pb',File) :- !, cli_set_empty_machine, % .pb file
    cli_set_empty_machine,
    assertz(option(eval_string_or_file(file(default),File,exists,_,norecheck))).

load_spec_file(EXT,MainFile) :- print_error('Unknown file extension, assuming B machine:'),
    print_error(EXT),
    load_b_file_with_options(MainFile).

load_spec_file/3

load_state/1

loaded_main_file/1

loaded_root_filename/1

logxml_write_ids/2

ltl_check_assertions/0

mcm_test_case_generation/4

member_with_last/4

memory_intensive_option/1

merge_acc/4

merge_acc_infos/4

merge_accumulated_infos/1

merge_value/5

model_check_aux/5

model_check_aux(Nr,T1,W1,Time,ErrRes) :-
    (option(no_deadlocks) -> FindDeadlocks=0 ; FindDeadlocks=1),
    (option(no_invariant_violations) -> FindInvViolations=0 ; FindInvViolations=1),
    (option(no_goal) -> FindGoal=0 ; FindGoal=1),
    (option(no_state_errors) -> FindStateErrors=0 ; FindStateErrors=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,
    find_state_errors/FindStateErrors,
    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,FindStateErrors,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, AnalysisTime=0),
    formatsilent('Model checking time: ~w ms (~w ms walltime)~n',[Time,WTime]),
    formatsilent('States analysed: ~w~n',[NodesAnalysed]),
    get_state_space_stats(_,NrTransitions,_,_),
    printsilent('Transitions fired: '),printsilent(NrTransitions),nls,
    (get_current_breadth_first_level(Level)
    -> formatsilent('Breadth-first levels: ~w~n',[Level]) % is this the equivalent of TLC's diameter?
    ; true),
    write_xml_element_to_log(model_checking_statistics,
    [result/ErrRes,runtime/Time,walltime/WTime,
    states/NodesAnalysed,transitions/NrTransitions,staticAnalysisTime/AnalysisTime]),
    (ErrRes = no
    -> print('No counter example Found, not all states visited'),nl,
    add_warning(model_check_incomplete,'Not all states examined due to limit set by user: ',Nr)
    ; ErrRes=all
    -> (tcltk_find_max_reached_node
    -> (not_interesting(_)
    -> print('No counter example found. However, not all transitions were computed (and some states not satisfying SCOPE predicate were ignored) !')
    ; print('No counter example found. However, not all transitions were computed !')
    )
    ; not_interesting(_)
    -> print_green('No counter example found. ALL states (satisfying SCOPE predicate) visited.')
    % b_get_machine_searchscope(Scope)
    ; print_green('No counter example found. ALL states visited.')
    ),nl,
    add_model_checking_warnings(FindInvViolations,FindDeadlocks,FindGoal,FindAssViolations)
    ; % ErrRes is not no or all
    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 % -nocounter
    ; tcltk_interface:tcltk_get_history(list(Hist)),
    length(Hist,Len),
    format('*** TRACE (length=~w):~n',[Len]),
    reverse(Hist,Trace),
    print_nr_list(Trace),
    (silent_mode(off),
    current_state_id(ID),invariant_violated(ID)
    -> b_interpreter:analyse_invariant_for_state(ID)
    ; true)
    ),
    error_occurred(TclTkRes)
    ),nl
    )
    ; % do_model_check failed
    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
).

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

options_can_eval_any_cst/0

parse_eval_command/3

perform/1

perform_feedback_options_after_exception/0

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

plantuml_command/2

plantuml_command_for_expr/4

pr_acc_infos_aux/3

pracc/2

pred_eval_hook/5

pretty_print_internal_rep/4

pretty_print_internal_rep_to_B/1

pretty_print_prolog_file/1

print_accumulated_infos/1

print_bindings/1

print_cbc_stats/2

print_compile_time_flags/0

print_cpp_version/1

print_csv_prefs/1

print_current_state/0

print_eval_command_help/1

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(full),
    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,size'),nl, % dlk stands for out_degree_hash
    print(' -global_time_out 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 G S set group G of preferences to predefined value set S'),nl,
    print(' -card GS Val set cardinality (aka 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(' (only states satsifying this predicate will be examined)'),nl,
    print(' -property "PRED" virtually add predicate to PROPERTIES'),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,
    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(' -ppAB FILE like -ppf, but make output readable by Atelier-B'),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 TLC (see also TLC_WORKERS preference)'),nl,
    print(' -mc_with_lts_sym model check using LTSmin (symbolic)'),nl,
    print(' -mc_with_lts_seq model check using 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(' -feasibility_analysis_csv FILE write feasibility result to file'),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(' -puml CMD File write a graph to a plantuml file, with CMD being one of:'),nl,
    (is_plantuml_command(Cmd),command_description(Cmd,_,Desc),
    format(' ~w : ~w~n',[Cmd,Desc]),fail
    ; true),
    print(' -pumlexpr CMD Expr File write a graph for Expr to a plantuml file, with CMD:'),nl,
    (is_plantuml_command_for_expr(Cmd),command_description(Cmd,_,Desc),
    format(' ~w : ~w~n',[Cmd,Desc]),fail
    ; true),
    print(' -csv CMD File write a table to a CSV file, with CMD being one of:'),nl,
    (is_table_command(Cmd),command_description(Cmd,_,Desc),
    format(' ~w : ~w~n',[Cmd,Desc]),fail
    ; true),
    print(' -csvexpr CMD Expr File write a table for Expr to a CSV file, with CMD:'),nl,
    (is_table_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(' -rule_report generate HTML validation report for rules machines (.rmch)'),nl,
    print(' -csvhist E File evaluate expression over history and generate CSV file.'),nl,
    print(' -load_state File load state of ProB from a saved state space (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
    ;
    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: https://prob.hhu.de/w/index.php/ProB_Cli'),nl,
    nl.

print_host_version/1

print_individual_file/2

print_individual_file_infos_csv/2

print_memory_statistics/1

print_probcli_error_non_strict/2

print_probcli_version/1

print_prolog_flags/1

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/1

print_state_silent/1

print_titles/2

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_exception/2

process_ltsmin_result/2

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(1))).

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('-properties_core',cli_core_properties(_)). % variable as arg: try various algorithms in order

recognised_option('-properties_core_wd',cli_core_properties(wd_prover)).

recognised_option('-properties_core_z2',cli_core_properties(z3_bup(2))).

recognised_option('-properties_core_z3',cli_core_properties(z3_bup(3))).

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('-quiet',silent).

recognised_option('-q',silent).

recognised_option('-force_no_silent',force_no_silent). % override provided silent flag; useful for gitlab test debugging

recognised_option('-statistics',cli_print_statistics(full)).

recognised_option('-stats',cli_print_statistics(full)).

recognised_option('-memory_stats',cli_print_statistics(memory)).

recognised_option('-memory_statistics',cli_print_statistics(memory)).

recognised_option('-memory',cli_print_statistics(memory)).

recognised_option('-profile_stats',cli_print_statistics(sicstus_profile)).

recognised_option('-profile_statistics',cli_print_statistics(sicstus_profile)).

recognised_option('-op_cache_profile',cli_print_statistics(op_cache_profile)).

recognised_option('-hit_profile',cli_print_statistics(hit_profile)). % mainly for ProB developers

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

recognised_option('-nodead',no_deadlocks).

recognised_option('-no_dead',no_deadlocks).

recognised_option('-no_deadlocks',no_deadlocks).

recognised_option('-noinv',no_invariant_violations).

recognised_option('-no_inv',no_invariant_violations).

recognised_option('-no_invariant_violations',no_invariant_violations).

recognised_option('-nogoal',no_goal).

recognised_option('-no_goal',no_goal).

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

recognised_option('-no_ltl',no_ltl).

recognised_option('-noass',no_assertion_violations).

recognised_option('-no_ass',no_assertion_violations).

recognised_option('-no_assertion_violations',no_assertion_violations).

recognised_option('-no_state_errors',no_state_errors). % disable checking for general_errors and transition related state_errors

recognised_option('-nocounter',no_counter_examples).

recognised_option('-no_counter_examples',no_counter_examples).

recognised_option('-nocolor',no_color).

recognised_option('-no_color',no_color).

recognised_option('-no_colour',no_color).

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_info(statistics)).

recognised_option('-machine_statistics',cli_print_machine_info(statistics)).

recognised_option('-machine_files',cli_print_machine_info(files(no_sha))).

recognised_option('-machine_files_sha',cli_print_machine_info(files(with_sha))).

recognised_option('-machine_hash',cli_print_machine_info(hash(_))).

recognised_option('-check_abstract_constants',check_abstract_constants).

recognised_option('-op_cache_stats',check_op_cache([])).

recognised_option('-op_cache_statistics',check_op_cache([])).

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

recognised_option('-v',verbose).

recognised_option('-vv',very_verbose).

recognised_option('-verbose',verbose).

recognised_option('-debug',verbose).

recognised_option('-verbose_off',verbose_off). % mainly useful in REPL

recognised_option('-voff',verbose_off). % mainly useful in REPL

recognised_option('-very_verbose',very_verbose).

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

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

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

recognised_option('-version',print_version(full)).

recognised_option('-cpp_version',print_version(cpp)).

recognised_option('-V',print_version(full)).

recognised_option('-svers',print_version(short)).

recognised_option('-short_version',print_version(short)).

recognised_option('-check_lib',print_version(lib)).

recognised_option('-check_java_version',check_java_version).

recognised_option('-java_version',print_version(java)).

recognised_option('-release_java_parser',release_java_parser).

recognised_option('-fast_read_prob',fast_read_prob).

recognised_option('-file_info',file_info).

recognised_option('-t',default_trace_check).

recognised_option('-init',initialise).

recognised_option('-initialise',initialise).

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

recognised_option('-ss',socket(9000,true)). % standard socket 9000

recognised_option('-sf',socket(_,true)). % free socket

recognised_option('-local_socketserver',socket(_,true)). % do not allow remote socket connections

recognised_option('-remote_socketserver',socket(_,false)). % allow remote socket connections

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('-export_po',disprover_options([disprover_option(export_po_as_machine(user_output))])).

recognised_option('-ltsmin',ltsmin).

recognised_option('-trace',prolog_trace). % enter Prolog debugger on development system after starting up ProB

recognised_option/3

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('-search_scope',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('-evalnwd',eval_string_or_file(string,E,exists,'NOT-WELL-DEFINED',norecheck),[E]).

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

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

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_option',history_option(Option),[Option]). % trace_file, json, show_init, show_states

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

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

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

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

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('-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('-variable_coverage',csv_table_command(variable_coverage,[],[text_output],user_output),[]).

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

recognised_option('-wd_check',cli_wd_check(_,_),[]).

recognised_option('-wd_check_all',cli_wd_check(X,X),[]).

recognised_option('-well_definedness_check',cli_wd_check(_,_),[]).

recognised_option('-wd_inv_proof',cli_wd_inv_proof(_,_,_),[]).

recognised_option('-lint',cli_lint,[]). % extended static check (ESC, esc)

recognised_option('-lint_operations',cli_lint(operations),[]).

recognised_option('-lint_variables',cli_lint(variables),[]).

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

recognised_option('-cbc_invariant',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; TO DO: also call WD prover

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('-bdc', cbc_tests(Depth,'#deadlock',''),[Depth]).

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

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

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

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('-ltsmin2',ltsmin2(EndpointPath), [EndpointPath]).

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

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

recognised_option('-machine_hash_check',cli_print_machine_info(hash(X)),[X]).

recognised_option('-install',install_prob_lib(X,[]),[X]).

recognised_option('-install_dry_run',install_prob_lib(X,[dryrun]),[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],prob_cli:mc_ok_arg(Arg,N)).

recognised_option('-bench_model_check',cli_mc(LimitNr,[reset_state_space,repeat(Rep)]),[Arg],tools:arg_is_number(Arg,Rep)) :- max_tagged_integer(LimitNr).

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('-global_time_out',timeout(N),[Arg],tools:arg_is_number(Arg,N)). % better name, to avoid conflict with -p timeout N which also works

recognised_option('-s',socket(S,true),[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('-csp_guide',add_csp_guide(File),[File],
    prob_cli:check_file_arg(File,'csp_guide')).

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

recognised_option('-load_state',load_state(Filename),[Filename],
    prob_cli:check_file_arg(Filename,'load_state')).

recognised_option('-refchk',refinement_check(Filename,trace,100000),[Filename],
    prob_cli:check_file_arg(Filename,'refchk')).

recognised_option('-ref_check',refinement_check(Filename,FailuresModel,100000),[Shortcut,Filename],
    (prob_cli:check_file_arg(Filename,'ref_check'),
    prob_cli:check_failures_mode(Shortcut,FailuresModel))).

recognised_option('-refinement_check',Option,Args,Code) :- recognised_option('-refchk',Option,Args,Code).

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('-check_op_cache_stats',
    check_op_cache([next_state_calls-H1,inv_check_calls-H2,
    operations_cached-H3,invariants_cached-H4]),[Arg1,Arg2,Arg3,Arg4],
    (tools:arg_is_number_or_wildcard(Arg1,H1), tools:arg_is_number_or_wildcard(Arg2,H2),
    tools:arg_is_number_or_wildcard(Arg3,H3), tools:arg_is_number_or_wildcard(Arg4,H4))).

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

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

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('-wd',cli_wd_check(DNr,TNr),[D,T],
    (arg_is_number_or_wildcard(T,TNr),arg_is_number_or_wildcard(D,DNr))).

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(1)),[Steps],tools:arg_is_number(Steps,N)).

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

recognised_option('-execute_expect_steps',execute_expect_steps(N),[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],
    prob_cli:check_file_arg(Output,'cbc_tests')).

recognised_option('-mcm_tests', mcm_tests(Depth,MaxStates,EndPred,Output),[Depth,MaxStates,EndPred,Output],
    prob_cli:check_file_arg(Output,'mcm_tests')).

recognised_option('-test_description', test_description(File), [File],
    prob_cli:check_file_arg(File,'test_description')).

recognised_option('-all_paths', all_deadlocking_paths(File), [File],
    prob_cli:check_file_arg(File,'all_paths')).

recognised_option('-dot',dot_command(Category,File,default),[Category,File],
    prob_cli:check_file_arg(File,'dot')).

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

recognised_option('-dotexpr',dot_command_for_expr(Category,Expr,File,[],default),[Category,Expr,File],
    prob_cli:check_file_arg(File,'dotexpr')).

recognised_option('-dot_expr',Opt,Args,Call) :- recognised_option('-dotexpr',Opt,Args,Call).

recognised_option('-puml',plantuml_command(Category,File),[Category,File],
    prob_cli:check_file_arg(File,'plantuml')).

recognised_option('-pumlexpr',plantuml_command(Category,File,[Expr]),[Category,Expr,File],
    prob_cli:check_file_arg(File,'plantuml')).

recognised_option('-puml_expr',Opt,Args,Call) :- recognised_option('-pumlexpr',Opt,Args,Call).

recognised_option('-csv',csv_table_command(Category,[],[],File),[Category,File],
    prob_cli:check_file_arg(File,'csv')).

recognised_option('-csvexpr',csv_table_command(Category,[Expr],[],File),[Category,Expr,File],
    prob_cli:check_file_arg(File,'csvexpr')).

recognised_option('-csv_expr',Opt,Args,Call) :- recognised_option('-csvexpr',Opt,Args,Call).

recognised_option('-csv_hist',Opt,Args,Call) :- recognised_option('-csvhist',Opt,Args,Call).

recognised_option('-csvhist',evaluate_expression_over_history_to_csv_file(Expr,File),[Expr,File],
    prob_cli:check_file_arg(File,'csvhist')).

recognised_option('-min_max_coverage',csv_table_command(minmax_table,[],[text_output],File),[File],
    prob_cli:check_file_arg(File,'min_max_coverage')).

recognised_option('-get_coverage_information',get_coverage_information(File),[File],
    prob_cli:check_file_arg(File,'get_coverage_information')).

recognised_option('-read_write_matrix_csv',generate_read_write_matrix_csv(CsvFile),
    [CsvFile],
    prob_cli:check_file_arg(CsvFile,'read_write_matrix_csv')).

recognised_option('-feasibility_analysis_csv',feasibility_analysis_csv(TimeOut,EnablingCsvFile),
    [TimeOut,EnablingCsvFile],
    prob_cli:check_file_arg(EnablingCsvFile,'feasibility_analysis_csv')).

recognised_option('-l',log(Log,prolog),[Log],
    prob_cli:check_file_arg(Log,'l')).

recognised_option('-log',log(Log,prolog),[Log],
    prob_cli:check_file_arg(Log,'log')).

recognised_option('-logxml',log(Log,xml),[Log],
    prob_cli:check_file_arg(Log,'logxml')). % see cli_start_logging

recognised_option('-logtlc',logtlc(Log),[Log],
    prob_cli:check_file_arg(Log,'logtlc')).

recognised_option('-pp',pretty_print_internal_rep(File,'$auto',needed,ascii),[File],
    prob_cli:check_file_arg(File,'pp')).

recognised_option('-ppunicode',pretty_print_internal_rep(File,'$auto',needed,unicode),[File],
    prob_cli:check_file_arg(File,'pp')).

recognised_option('-ppf',pretty_print_internal_rep(File,'$auto',all,ascii),[File],
    prob_cli:check_file_arg(File,'ppf')).

recognised_option('-ppAB',pretty_print_internal_rep(File,'$auto',all,atelierb),[File],
    prob_cli:check_file_arg(File,'ppAB')).

recognised_option('-pp_with_name',pretty_print_internal_rep(File,MachName,all,ascii),[MachName,File],
    prob_cli:check_file_arg(File,'pp_with_name')). % provide explicit machine name

recognised_option('-ppB',pretty_print_internal_rep_to_B(File),[File],
    prob_cli:check_file_arg(File,'ppB')). % deprecated; is now superseded by ppAB for Event-B machines

recognised_option('-pppl',pretty_print_prolog_file(File),[File],
    prob_cli:check_file_arg(File,'pppl')).

recognised_option('-ppi',indent_b_file(File),[File],
    prob_cli:check_file_arg(File,'ppi')).

recognised_option('-save_state',save_state_space(Filename),[Filename],
    prob_cli:check_file_arg(Filename,'save_state')). % possibly save_state_space would be a better name

recognised_option('-save',save_state_for_refinement(Filename),[Filename],
    prob_cli:check_file_arg(Filename,'save')).

recognised_option('-sptxt',print_values(Filename),[Filename],
    prob_cli:check_file_arg(Filename,'sptxt')).

recognised_option('-sstxt',print_all_values(Dirname),[Dirname],
    prob_cli:check_file_arg(Dirname,'sstxt')).

recognised_option('-latex',process_latex_file(In,Out),[In,Out],
    (prob_cli:check_file_arg(In,'latex'),prob_cli:check_file_arg(Out,'latex'))).

recognised_option('-bench_csv',benchmark_info_csv_output(File,write),[File],prob_cli:check_file_arg(File,'bench_csv')).

recognised_option('-bench_csv_append',benchmark_info_csv_output(File,append),[File],prob_cli:check_file_arg(File,'bench_csv')).

recognised_option('-trace_replay',trace_check(Style,File,default_trace_replay),[Style,File],prob_cli:check_file_arg(File,'trace_replay')). % can be json, ..

recognised_option('-det_trace_replay',trace_check(Style,File,deterministic_trace_replay),[Style,File],prob_cli:check_file_arg(File,'det_trace_replay')).

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

recognised_option('-state_trace',state_trace(File),[File],prob_cli:check_file_arg(File,'state_trace')).

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

recognised_option('-enabling_analysis_csv',enabling_analysis_csv(EnablingCsvFile),[EnablingCsvFile],
    prob_cli:check_file_arg(EnablingCsvFile,'enabling_analysis_csv')).

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

recognised_option('-evaldot',evaldot(File),[File],prob_cli:check_file_arg(File,'evaldot')).

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

recognised_option('-visb_click',visb_click(SVGID),[SVGID],true).

recognised_option('-visb',visb_history(JSONFile,HTMLFile,[]),[JSONFile,HTMLFile],
    (prob_cli:check_file_arg(JSONFile,'visb'),prob_cli:check_file_arg(HTMLFile,'visb'))).

recognised_option('-visb_with_vars',
    visb_history(JSONFile,HTMLFile,[show_constants(all),show_sets(all),show_variables(all)]),
    [JSONFile,HTMLFile],
    (prob_cli:check_file_arg(JSONFile,'visb_with_vars'),prob_cli:check_file_arg(HTMLFile,'visb_with_vars'))).

recognised_option('-rule_report',rule_report(File), [File], prob_cli:check_file_arg(File,'rule_report')).

recognised_option('-bench_alloy_cmd',run_benchmark(alloy,CmdNames,AlloyFilePath),[CmdNames,AlloyFilePath],prob_cli:check_file_arg(AlloyFilePath,'bench_alloy_cmd')).

recognised_option('-bench_smt_cbc_inv',run_benchmark(smt,cbc_inv,Folder),[Folder],prob_cli:check_file_arg(Folder,'bench_smt_cbc_inv')).

recognised_option('-bench_smt_cbc_deadlock',run_benchmark(smt,cbc_deadlock,Folder),[Folder],prob_cli:check_file_arg(Folder,'bench_smt_cbc_deadlock')).

recognised_option('-bench_smt_bmc',run_benchmark(smt,bmc,Folder),[Folder],prob_cli:check_file_arg(Folder,'bench_smt_bmc')).

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

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

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

recognised_option('-solve_file',eval_string_or_file(file(Solver),F,exists,_ANY,norecheck),[Solver,F],prob_cli:check_file_arg(F,'eval_file')).

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],prob_cli:normalise_pref_name(PREF,NPREF)).

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

recognised_option('-prob_application_type',set_application_type(T),[T],true).

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))).

recognised_option('-pref_group',set_preference_group(NGroup,Val),[Group,Val],
    (prob_cli:normalise_option_atom(Group,NGroup))).

recognised_option('-save_all_traces_until',generate_all_traces_until(Formula,FilePrefix),
    [Formula,FilePrefix],
    true). % we could check LTL formula and FilePrefix

recognised_option('-check_machine_file_sha',check_machine_file_sha(FILE,SHA1),[FILE,SHA1],
    prob_cli:check_file_arg(FILE,'check_machine_file_sha')).

recognised_option('-sha1sum',Command,Args,Call) :-
    recognised_option('-check_machine_file_sha',Command,Args,Call).

regular_safety_model_check/3

regular_safety_model_check_now/5

reload_mainfile/0

remove_constants/2

repl_evaluate_expressions/1

repl_multi_read_line/1

repl_multi_read_line/2

repl_multi_read_line_aux/4

reset_cli/0

reset_dot_file_number/0

reset_expected_error_occurred/0

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

run_probcli3/2

Description:
set_verbose_mode -> does tcltk_turn_debugging_on(19),

run_probcli3(ArgV,RemArgV) :-
    ( 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(1)))
    ; true),
    if_option_set(set_application_type(PAT),set_prob_application_type(PAT)),
    if_option_set(test_mode,set_random_seed_to_deterministic_start_seed, set_new_random_seed),
    if_option_set(verbose,
    verbose, %% set_verbose_mode -> does 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),
    (add_message(parsercp,'Command -parcercp PATH deprecated, use -p JAVA_PARSER_PATH PATH',''),
    set_preference(path_to_java_parser,ParserLoc))
    ),
    if_option_set(parserport(ParserPort),
    connect_to_external_console_parser_on_port(ParserPort)),
    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,
    (option_verbose, (option(set_prefs_from_file(_)) ; option(set_preference_group(_,_))),
    get_non_default_preferences(list(NDPrefs))
    -> format('Non-default preferences:~n',[]),print_list(NDPrefs),nl ; true),
    set_optional_errors,
    check_unavailable_options,
    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,0); halt_prob(NOW,1))),
    if_option_set(install_prob_lib(LIBTOINSTALL,INSTALLOPTS), install_prob_lib(LIBTOINSTALL,INSTALLOPTS)),
    if_options_set(print_version(VERSIONKIND), print_version(VERSIONKIND)),
    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)),
    % process remaining arguments as files to load
    debug_println(6,processing(RemArgV)),
    cli_load_files(RemArgV,NOW), % all CLI arguments which are not understood are supposed to be files to be treated
    debug_println(19,finished_loading(RemArgV)),
    if_option_set(socket(Port,Loopback),
    cli_start_socketserver(Port,Loopback)),
    % check_all_expected_errors_occurred(NOW), % is now checked for each file; socket_server should not generate errors ?
    debug_println(20,'% probcli execution finished'),
    cli_print_junit_results(ArgV),
    debug_println(20,'% Stored Junit results'),
    stop_xml_probcli_run(NOW),
    debug_println(20,'% ProB Finished').

run_probcli_with_argv_string/1

run_probcli_with_junit_check/1

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/1

show_initialisation_summary/1

show_last_expression_as_table/0

show_operation_coverage_summary/1

show_origin/1

show_source/1

sicstus_profile_statistics/0

silent/0

sort_assertions/2

specfile_trans_with_check/5

split_argv_string/2

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_repl_even_after_failure/0

start_repl_if_required/0

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

stop_xml_probcli_run/1

store_last_error_location_for_repl/0

test_kodkod_and_exit/2

timeout_call/3

Meta: timeout_call(0,-,-)

top_level_eval/0

top_level_eval1/0

translate_err_type/2

translate_exception/2

translate_solver_result/2

treat_existence_error/4

treat_option/1

trim_quotes/2

trimcore_if_useful/1

truncate_animate_action/2

unset_analyse_hook/0

unset_current_probcli_command/0

we_need_only_static_assertions/1

write_cbc_check_result/1

write_cbc_check_result/2

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_animation/0

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),
    assertz(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),
    zmq_start_animation.

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 <----------------
    zmq_start_animation.

zmq_worker_load_model(eventb(Machine,Options)) :- !,
    print(loading_eventb(Options)),nl,
    zmq_set_important_options(Options),
    bmachine:b_machine_reset, bmachine:assert_main_machine(Machine),
    set_animation_mode(b), set_animation_minor_mode(eventb),
    zmq_start_animation.

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
    zmq_start_animation.

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

zmq_worker_load_model(assertions(Machine,State,Assertions)) :- !,
    assertz(assertion_counter(-1)),
    println_silent(loaded_model_for_assertion_checking),
    zmq_worker_load_model(Machine),
    assertz(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_release,true)
! Existence error in argument 1 of absolute_file_name/3
! file extension('dll_path/dll_path') does not exist
! goal: absolute_file_name(extension('dll_path/dll_path'),_22773,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pathes.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(plspec_patch_libraries,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_terminal_colors,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_enter_debugger_upon_error,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_use_timer,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_74071,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(debug) does not exist
! goal: absolute_file_name(probsrc(debug),_72407,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_src_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_core_only,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_myheap,false)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(disable_chr,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_53899,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pathes_lib.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_22915,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/error_manager.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('user_signal/user_signal') does not exist
! goal: absolute_file_name(extension('user_signal/user_signal'),_21055,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/prob_startup.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(json_parser) does not exist
! goal: absolute_file_name(extrasrc(json_parser),_31781,[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 extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/prob_cli.pl')])

Name: assertz/1
Name: sort/2
Name: get_additional_stats/2	Module: prob_cli

Name: accumulate_infos_2/2	Module: prob_cli
Name: fail
Name: assertz/1
Name: debug_println/2	Module: foo_error
Name: sort/2
Name: get_additional_infos/2	Module: prob_cli
Name: file_loaded/2	dynamic predicate
Name: option/1	dynamic predicate

Name: load_spec_file/3	Module: prob_cli
Name: cli_core_properties/1	Module: prob_cli
Name: cli_start_model_check/3	Module: prob_cli
Name: construct_and_execute_tlc_command/1	Module: prob_cli
Name: cli_wd_check/2	Module: prob_cli
Name: cli_check_properties/1	Module: prob_cli
Name: cli_start_sym_mc_with_lts/1	Module: prob_cli
Name: cli_check_goal/0	Module: prob_cli
Name: cli_check_op_cache/1	Module: prob_cli
Name: cli_trans/5	Module: prob_cli
Name: cli_check_assertions/3	Module: prob_cli
Name: cli_wd_inv_proof/3	Module: prob_cli

Name: RECURSIVE_CALL/2	Module: prob_cli
Name: assertz/1
Name: is/2
Name: =/2
Name: true
Name: accumulated_infos/3	dynamic predicate
Name: retract/1
Name: ->/3
Name: !
Name: fail
Name: add_internal_error/2	Module: foo_error
Name: >/2
Name: number/1
Name: get_info/3	Module: prob_cli

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

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

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

Name: options_can_eval_any_cst/0	Module: prob_cli
Name: not/1
Name: b_top_level_operation/1	Module: bmachine
Name: b_or_z_mode	Module: foo_error

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

Name: RECURSIVE_CALL/1	Module: prob_cli
Name: assertz/1
Name: is/2
Name: retractall/1
Name: assertion_counter/1	dynamic predicate

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

Name: treat_option/1	Module: prob_cli
Name: assertz/1
Name: !
Name: option/1	dynamic predicate

Name: assert_all_options/1	Module: prob_cli
Name: run_probcli3/2	Module: prob_cli
Name: zmq_set_option/1	Module: prob_cli
Name: silent/0	Module: prob_cli
Name: call_probcli_option/1	Module: prob_cli

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

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

Name: display_match/3	Module: prob_cli
Name: get_machine_identifiers/2	Module: bmachine
Name: true
Name: =/2
Name: ->/3
Name: print_sets/0	Module: prob_cli

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

Name: if_option_set_loaded/3	Module: prob_cli
Name: if_option_set/3	Module: prob_cli
Name: perform/1	Module: prob_cli
Name: ifm_option_set/3	Module: prob_cli

Name: catch/3
Name: cli_print_statistics/1	Module: prob_cli
Name: !
Name: assert_option/1	Module: prob_cli
Name: true
Name: option/1	dynamic predicate
Name: ->/3
Name: just_assert_option/1	Module: prob_cli

Name: stop_xml_feature/2	Module: prob_cli
Name: write_cbc_check_result/1	Module: prob_cli
Name: error_occurred/1	Module: prob_cli
Name: nl
Name: print_red/1	Module: tools_printing
Name: =/2
Name: write_result_to_file/1	Module: prob_cli
Name: process_cbc_assertion_result/2	Module: prob_cli
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
Name: print_repl_prompt_s/1	Module: prob_cli
Name: check_loaded_not_empty/1	Module: prob_cli
Name: findall/4

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

Name: stop_xml_feature/2	Module: prob_cli
Name: write_xml_element_to_log/2	Module: foo_error
Name: error_occurred/1	Module: prob_cli
Name: format_with_colour_nl/4	Module: tools_printing
Name: true
Name: =/2
Name: ->/3
Name: nl
Name: prnt/2	Module: prob_cli
Name: format/2
Name: print_green/1	Module: tools_printing
Name: length/2
Name: cbc_find_redundant_invariants/2	Module: b_state_model_check
Name: start_xml_feature/2	Module: prob_cli
Name: print_repl_prompt_s/1	Module: prob_cli
Name: check_loaded_not_empty/1	Module: prob_cli

Name: fail
Name: nl
Name: eval_codes/6	Module: foo_error
Name: atom_codes/2
Name: format_with_colour_nl/4	Module: tools_printing
Name: translate_bvalue/2	Module: translate
Name: true
Name: debug_mode/1	Module: foo_error
Name: ->/3
Name: format/3
Name: get_value_type/2	Module: prob_cli
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: format/2

Name: cli_load_files3/4	Module: prob_cli
Name: cli_load_files/2	Module: prob_cli

Name: check_codes_look_like_file/2	Module: prob_cli
Name: atom_codes/2
Name: add_warning/3	Module: foo_error
Name: !
Name: number/1

prob_prolog/src/prob_cli.pl

Modules

Predicates of prob_cli

Module Information

5633 Lines

471 Predicates

Imported Modules: module_information preferences lists system codesio debug error_manager specfile basic_unit_tests logger tcltk_interface eclipse_interface predicate_evaluator version alloy2b_benchmarks smt_solver_benchmarks eval_strings

9 Exports

227 specified Imports

Predicates:

Name: add_message/3	Module: foo_error
Name: !
Name: nonmember/2
Name: =</2
Name: >=/2
Name: check_codes_resembles_command/2	Module: prob_cli

Name: check_filename_arg/2	Module: tools
Name: add_warning/3	Module: foo_error
Name: ajoin/2	Module: tools_strings
Name: !
Name: recognised_option/4	Module: prob_cli
Name: normalise_option_atom/2	Module: prob_cli

Name: get_state_errors/1	Module: prob_cli
Name: fail
Name: error_occurred_with_msg/2	Module: prob_cli
Name: print_state_silent/1	Module: prob_cli
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
Name: =/2
Name: ->/3
Name: format/2
Name: check_java_version/2	Module: parsercall

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

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

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

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

Name: add_internal_error/2	Module: foo_error
Name: check_expected/3	Module: prob_cli
Name: nl
Name: debug_format/3	Module: foo_error
Name: print/1
Name: add_error/3	Module: foo_error
Name: format_with_colour_nl/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
Name: flush_output/1

Name: cli_ctl_model_check/4	Module: prob_cli
Name: cli_ltl_model_check/4	Module: prob_cli