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

3959 Lines

358 Predicates

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

0 Exports

113 specified Imports

Imports	Exports
Name: startup_prob/0 Module: prob_startup Name: string_concatenate/3 Module: tools Name: arg_is_number/2 Module: tools Name: print_error/1 Module: tools_printing Name: start_animation/0 Module: prob2_interface Name: is_initialised_state/1 Module: prob2_interface Name: set_eclipse_preference/2 Module: prob2_interface Name: update_preferences_from_spec/0 Module: prob2_interface Name: load_cspm_spec_from_cspm_file/1 Module: prob2_interface Name: compute_the_coverage/5 Module: coverage_statistics Name: set_storage_directory/1 Module: value_persistance Name: unset_storage_directory/0 Module: value_persistance Name: check_default_trace_for_specfile/1 Module: b_trace_checking Name: tcltk_check_state_sequence_from_file/1 Module: b_trace_checking Name: tcltk_save_history_as_trace_file/2 Module: b_trace_checking Name: file_exists/1 Module: file_systems Name: make_directory/1 Module: file_systems Name: run_typecheck_testcase/2 Module: test_typechecker Name: disable_interaction_on_errors/0 Module: self_check Name: perform_self_check/1 Module: self_check Name: turn_off_run_time_type_checks/0 Module: self_check Name: turn_on_run_time_type_checks/0 Module: self_check Name: b_write_machine_representation_to_file/2 Module: bmachine Name: full_b_machine/1 Module: bmachine Name: b_write_eventb_machine_to_classicalb_to_file/1 Module: bmachine Name: set_cspm_main_process/1 Module: xtl_interface Name: is_dot_command/1 Module: meta_interface Name: call_dot_command/3 Module: meta_interface Name: is_dot_command_for_expr/1 Module: meta_interface Name: call_dot_command_for_expr/4 Module: meta_interface Name: command_description/3 Module: meta_interface Name: test_predicate_analysis/0 Module: predicate_analysis Name: write_history_to_file/2 Module: b_show_history Name: write_values_to_file/1 Module: b_show_history Name: write_all_values_to_dir/1 Module: b_show_history Name: write_history_to_user_output/1 Module: b_show_history Name: check_if_predicates_were_evaluated/1 Module: external_functions Name: write_all_deadlocking_paths_to_xml/1 Module: sap Name: test_generation_by_xml_description/1 Module: sap Name: run_disprover_on_all_pos/1 Module: disprover_test_runner Name: load_po_file/1 Module: disprover_test_runner Name: print_disprover_stats/0 Module: disprover_test_runner Name: set_disprover_timeout/1 Module: disprover_test_runner Name: set_disprover_options/1 Module: disprover_test_runner Name: reset_disprover_timeout/0 Module: disprover_test_runner Name: process_latex_file/2 Module: latex_processor Name: safe_time_out/3 Module: tools_meta Name: set_junit_dir/1 Module: junit_tests Name: print_junit/2 Module: junit_tests Name: create_junit_result/6 Module: junit_tests Name: store_virtual_event/1 Module: eventhandling Name: show_cache_file_contents/0 Module: value_persistance Name: show_cache_file_constants/0 Module: value_persistance Name: print_op_cache/0 Module: b_operation_cache Name: not_all_transitions_added/1 Module: state_space Name: not_invariant_checked/1 Module: state_space Name: current_expression/2 Module: state_space Name: count_occurences/2 Module: tools_lists Name: reset_side_effect_occurred/0 Module: external_functions Name: side_effect_occurred/1 Module: external_functions Name: get_assertions_from_machine/2 Module: bmachine Name: current_state_corresponds_to_setup_constants_b_machine/0 Module: state_space Name: system_call/4 Module: system_call Name: csv_to_trace/3 Module: ltsmin/ltsmin_trace Name: b_machine_name/1 Module: bmachine Name: write_lines_to_file/2 Module: tools_files Name: pretty_print_coverage_information_to_file/1 Module: coverage_statistics Name: term_hash/2 Module: terms Name: state_error/3 Module: state_space Name: invariant_violated/1 Module: state_space Name: time_out_for_invariant/1 Module: state_space Name: time_out_for_assertions/1 Module: state_space Name: time_out_for_node/3 Module: state_space Name: check_java_version/2 Module: parsercall Name: get_parser_version/1 Module: parsercall Name: ensure_console_parser_launched/0 Module: parsercall Name: get_parser_version/1 Module: parsercall Name: get_java_command_path/1 Module: parsercall Name: get_java_fullversion/1 Module: parsercall Name: set_depth_breadth_first_mode/1 Module: state_space_exploration_modes Name: model_checking_is_incomplete/6 Module: model_checker Name: predicate_uses_unfixed_deferred_set/2 Module: solver_interface Name: unfixed_typed_id_in_list/3 Module: solver_interface Name: get_texpr_id/2 Module: bsyntaxtree Name: safe_open_file/4 Module: tools_io Name: infeasible_operation_cache/1 Module: enabling_analysis Name: explore_and_generate_testcases/7 Module: sap Name: cbc_gen_test_cases_from_string/5 Module: sap Name: tcl_get_stored_test_cases/1 Module: sap Name: ensure_console_parser_launched/0 Module: parsercall Name: interruptable_call/1 Module: user_interrupts Name: start_terminal_colour/2 Module: tools_printing Name: reset_terminal_colour/1 Module: tools_printing Name: print_red/1 Module: tools_printing Name: print_green/1 Module: tools_printing Name: safe_open_file/4 Module: tools_io Name: format_with_colour/4 Module: tools_printing Name: toggle_perfmessages/0 Module: performance_messages Name: show_dot_file/1 Module: tools_commands Name: show_ps_file/1 Module: tools_commands Name: gen_dot_output/4 Module: tools_commands Name: edit_file/2 Module: tools_commands Name: extract_file_line_col/6 Module: error_manager Name: get_machine_identifiers/2 Module: prob2_interface Name: get_machine_identifier_names/7 Module: b_machine_hierarchy Name: visited_expression/2 Module: state_space Name: tcltk_cbc_enabling_analysis/1 Module: enabling_analysis Name: print_enable_table/1 Module: enabling_analysis Name: is_timeout_enabling_result/1 Module: enabling_analysis Name: feasible_operation_with_timeout/3 Module: enabling_analysis Name: tcltk_read_write_matrix/1 Module: b_read_write_info Name: print_runtime_profile/0 Module: runtime_profiler Name: print_source_profile/0 Module: source_profiler

Imports

Exports

Name: startup_prob/0

Module: prob_startup

Name: string_concatenate/3

Module: tools

Name: arg_is_number/2

Module: tools

Name: print_error/1

Module: tools_printing

Name: start_animation/0

Module: prob2_interface

Name: is_initialised_state/1

Module: prob2_interface

Name: set_eclipse_preference/2

Module: prob2_interface

Name: update_preferences_from_spec/0

Module: prob2_interface

Name: load_cspm_spec_from_cspm_file/1

Module: prob2_interface

Name: compute_the_coverage/5

Module: coverage_statistics

Name: set_storage_directory/1

Module: value_persistance

Name: unset_storage_directory/0

Module: value_persistance

Name: check_default_trace_for_specfile/1

Module: b_trace_checking

Name: tcltk_check_state_sequence_from_file/1

Module: b_trace_checking

Name: tcltk_save_history_as_trace_file/2

Module: b_trace_checking

Name: file_exists/1

Module: file_systems

Name: make_directory/1

Module: file_systems

Name: run_typecheck_testcase/2

Module: test_typechecker

Name: disable_interaction_on_errors/0

Module: self_check

Name: perform_self_check/1

Module: self_check

Name: turn_off_run_time_type_checks/0

Module: self_check

Name: turn_on_run_time_type_checks/0

Module: self_check

Name: b_write_machine_representation_to_file/2

Module: bmachine

Name: full_b_machine/1

Module: bmachine

Name: b_write_eventb_machine_to_classicalb_to_file/1

Module: bmachine

Name: set_cspm_main_process/1

Module: xtl_interface

Name: is_dot_command/1

Module: meta_interface

Name: call_dot_command/3

Module: meta_interface

Name: is_dot_command_for_expr/1

Module: meta_interface

Name: call_dot_command_for_expr/4

Module: meta_interface

Name: command_description/3

Module: meta_interface

Name: test_predicate_analysis/0

Module: predicate_analysis

Name: write_history_to_file/2

Module: b_show_history

Name: write_values_to_file/1

Module: b_show_history

Name: write_all_values_to_dir/1

Module: b_show_history

Name: write_history_to_user_output/1

Module: b_show_history

Name: check_if_predicates_were_evaluated/1

Module: external_functions

Name: write_all_deadlocking_paths_to_xml/1

Module: sap

Name: test_generation_by_xml_description/1

Module: sap

Name: run_disprover_on_all_pos/1

Module: disprover_test_runner

Name: load_po_file/1

Module: disprover_test_runner

Name: print_disprover_stats/0

Module: disprover_test_runner

Name: set_disprover_timeout/1

Module: disprover_test_runner

Name: set_disprover_options/1

Module: disprover_test_runner

Name: reset_disprover_timeout/0

Module: disprover_test_runner

Name: process_latex_file/2

Module: latex_processor

Name: safe_time_out/3

Module: tools_meta

Name: set_junit_dir/1

Module: junit_tests

Name: print_junit/2

Module: junit_tests

Name: create_junit_result/6

Module: junit_tests

Name: store_virtual_event/1

Module: eventhandling

Name: show_cache_file_contents/0

Module: value_persistance

Name: show_cache_file_constants/0

Module: value_persistance

Name: print_op_cache/0

Module: b_operation_cache

Name: not_all_transitions_added/1

Module: state_space

Name: not_invariant_checked/1

Module: state_space

Name: current_expression/2

Module: state_space

Name: count_occurences/2

Module: tools_lists

Name: reset_side_effect_occurred/0

Module: external_functions

Name: side_effect_occurred/1

Module: external_functions

Name: get_assertions_from_machine/2

Module: bmachine

Name: current_state_corresponds_to_setup_constants_b_machine/0

Module: state_space

Name: system_call/4

Module: system_call

Name: csv_to_trace/3

Module: ltsmin/ltsmin_trace

Name: b_machine_name/1

Module: bmachine

Name: write_lines_to_file/2

Module: tools_files

Name: pretty_print_coverage_information_to_file/1

Module: coverage_statistics

Name: term_hash/2

Module: terms

Name: state_error/3

Module: state_space

Name: invariant_violated/1

Module: state_space

Name: time_out_for_invariant/1

Module: state_space

Name: time_out_for_assertions/1

Module: state_space

Name: time_out_for_node/3

Module: state_space

Name: check_java_version/2

Module: parsercall

Name: get_parser_version/1

Module: parsercall

Name: ensure_console_parser_launched/0

Module: parsercall

Name: get_parser_version/1

Module: parsercall

Name: get_java_command_path/1

Module: parsercall

Name: get_java_fullversion/1

Module: parsercall

Name: set_depth_breadth_first_mode/1

Module: state_space_exploration_modes

Name: model_checking_is_incomplete/6

Module: model_checker

Name: predicate_uses_unfixed_deferred_set/2

Module: solver_interface

Name: unfixed_typed_id_in_list/3

Module: solver_interface

Name: get_texpr_id/2

Module: bsyntaxtree

Name: safe_open_file/4

Module: tools_io

Name: infeasible_operation_cache/1

Module: enabling_analysis

Name: explore_and_generate_testcases/7

Module: sap

Name: cbc_gen_test_cases_from_string/5

Module: sap

Name: tcl_get_stored_test_cases/1

Module: sap

Name: ensure_console_parser_launched/0

Module: parsercall

Name: interruptable_call/1

Module: user_interrupts

Name: start_terminal_colour/2

Module: tools_printing

Name: reset_terminal_colour/1

Module: tools_printing

Name: print_red/1

Module: tools_printing

Name: print_green/1

Module: tools_printing

Name: safe_open_file/4

Module: tools_io

Name: format_with_colour/4

Module: tools_printing

Name: toggle_perfmessages/0

Module: performance_messages

Name: show_dot_file/1

Module: tools_commands

Name: show_ps_file/1

Module: tools_commands

Name: gen_dot_output/4

Module: tools_commands

Name: edit_file/2

Module: tools_commands

Name: extract_file_line_col/6

Module: error_manager

Name: get_machine_identifiers/2

Module: prob2_interface

Name: get_machine_identifier_names/7

Module: b_machine_hierarchy

Name: visited_expression/2

Module: state_space

Name: tcltk_cbc_enabling_analysis/1

Module: enabling_analysis

Name: print_enable_table/1

Module: enabling_analysis

Name: is_timeout_enabling_result/1

Module: enabling_analysis

Name: feasible_operation_with_timeout/3

Module: enabling_analysis

Name: tcltk_read_write_matrix/1

Module: b_read_write_info

Name: print_runtime_profile/0

Module: runtime_profiler

Name: print_source_profile/0

Module: source_profiler

Predicates

Predicates:

accumulate_infos/2

add_eval_result/1

add_model_checking_warnings/4

add_vacuous_invariant/1

animate_machine/0

animate_machine2/0

animation_mode_does_not_support_animation/1

append_assertion/1

assert_all_options/1

assert_option/1

atom_contains_codes/2

available_commands/1

browse/0

browse_all_machines/1

browse_machine/1

call_probcli_option/1

cbc_assertions/2

cbc_check/1

cbc_deadlock_check/1

cbc_redundant_invariants/1

cbc_refinement/0

cbc_sequence/3

cbc_test_case_generation/3

check_all_expected_errors_occurred/1

check_complete/0

check_complete_operation_coverage/0

check_parser_version/0

check_ref_result/1

check_required_infos/3

check_status/4

check_totals/4

clear_loaded_files/0

cli_add_additional_property/1

cli_animateOperationNr/3

cli_assertions_ok/2

cli_checkAssertion/4

cli_check_assertions/2

cli_check_assertions/3

cli_check_csp_assertion/2

cli_check_goal/0

cli_check_properties/0

cli_check_properties/1

cli_check_scc_for_ltl_formula/2

cli_check_statespace_hash/2

cli_computeOperations/1

cli_csp_get_assertions/0

cli_csp_in_situ_refinement_check/4

cli_csp_translate_to_file/1

cli_ctl_model_check/3

cli_eval_csp_expression/1

cli_execute/3

cli_execute_add_virtual_transition/3

cli_get_coverage_information/1

cli_get_min_max_coverage/1

cli_ltl_model_check/3

cli_mc/1

cli_print_all_values/1

cli_print_history/1

cli_print_junit_results/1

cli_print_machine_statistics/0

cli_print_statistics/0

cli_print_values/1

cli_process_loaded_file/2

cli_process_loaded_file_afer_start_animation/1

cli_random_animate/2

cli_random_animate/3

cli_set_empty_machine/0

cli_set_goal/1

cli_set_searchscope/1

cli_show_coverage/2

cli_show_coverage/4

cli_show_help/2

cli_show_variable_coverage/1

cli_start_animation/1

cli_start_initialisation/1

cli_start_logging/5

cli_start_mc_with_tlc/0

cli_start_model_check/2

cli_start_refinement_check/4

cli_start_selfcheck/0

cli_start_socketserver/1

cli_start_sym_mc_with_lts/1

cli_start_trace_check/1

cli_start_trace_state_check/1

cli_symbolic_model_check/1

close_repl_input_stream/1

command_option/1

compare_kodkod_performance1/3

compile_time_flag/1

computeOperations_for_root_required/0

constraint_based_check/1

construct_and_execute_tlc_command/1

convert_dash_to_underscore/2

count_assertions/3

coverage/1

create_state_error_description/2

definite_error_occurred/0

display_match/3

display_match/4

do_det_checking/0

do_enabling_analysis_csv/2

do_feasibility_analysis/2

do_not_execute_automatically/1

do_one_gui_event/0

dot_command/2

dot_command_for_expr/4

error_occurred_with_msg/2

eval_probcli_repl_line/1

eval_string_or_file/4

evalchecklist/2

evalchecklist2/2

evalchecklist3/3

evaluate_expressions/1

evaluate_from_commandline/0

generate_read_write_matrix/1

generate_time_stamp/2

get_comma_or_space_separated_options/2

get_dot_file/2

get_error_category_and_type/3

get_error_or_warning_span/4

get_probcli_elapsed_walltime/2

get_quoted_atom/4

get_state_errors/1

get_state_space_errors/0

go_cli/0

go_cli/1

go_cli2/1

go_cli_with_junit_check/1

handle_symbolic_model_check_result/1

help/0

if_option_set/2

if_option_set/3

if_option_set_loaded/3

if_options_set/2

ifm_option_set/2

ifm_option_set/3

ifm_option_set_loaded/3

initialise_required/0

irrelevant_xml_info/1

is_constant_binding/1

loaded_root_filename/1

logxml_write_vars/1

ltl_check_assertions/0

mcm_test_case_generation/4

normalise_option_atom/2

normalise_pref_name/2

not_command_option/1

open_file_at_position/1

option_only_works_for_single_file/1

option_requires_all_properties/1

option_verbose/0

options_allow_start_without_file/0

parse_eval_command/3

perform/1

perform_random_init_after_setup_constants/0

perform_random_initialisation/0

perform_random_initialisation/1

perform_random_initialisation_if_necessary/1

perform_random_step/1

perform_random_step/4

perform_random_steps/2

perform_random_steps_aux/3

perform_symbolic_model_checking/2

portray_message/2

pracc/1

pred_eval_hook/5

pretty_print_all_types/1

pretty_print_internal_rep/1

pretty_print_internal_rep_to_B/1

print_accumulated_infos/1

print_bindings/1

print_cbc_stats/2

print_compile_time_flags/0

print_current_state/0

print_eval_command_help/1

print_probcli_error_non_strict/2

print_short_version/0

print_state_silent/1

print_total_probcli_timer/0

probcli_add_light_warning/2

probcli_startup/0

process_cbc_assertion_result/2

process_ltsmin_result/1

profiling_on/0

recognised_cli_option/4

repl_multi_read_line/1

repl_multi_read_line_aux/3

reset_cli/0

reset_dot_file_number/0

reset_expected_error_occurred/0

set_current_probcli_command/1

set_dot_file_prefix/1

set_dot_file_prefix_if_option_set/1

set_junit_mode/1

set_new_random_seed/0

set_optional_errors/0

set_pref/2

set_prefs/0

set_random_seed_to_deterministic_start_seed/0

set_repl_input_file/2

show_cache/0

show_initialisation_summary/1

show_last_expression_as_table/0

show_operation_coverage_summary/1

split_by_seperator2/2

start_animation_without_computing/0

start_ltsmin_srv/2

start_probcli_timer/1

start_xml_feature/2

start_xml_feature/4

stop_probcli_debug_timer/2

stop_probcli_timer/2

stop_probcli_timer/3

stop_xml_feature/2

store_last_error_location_for_repl/0

strip_leading_ws/2

strip_ws/2

strip_ws2/2

test_kodkod_and_exit/2

translate_exception/2

treat_existence_error/4

truncate_animate_action/2

unset_analyse_hook/0

unset_current_probcli_command/0

we_need_only_static_assertions/1

write_deferred_set_used/1

write_dot_graph_to_new_file/2

write_important_xml_element_to_log/2

write_result_to_file/1

xml_log_machine_statistics/0

zmq_delayed_option/1

zmq_get_important_options/1

zmq_get_initialisation_term/1

zmq_important_option/1

zmq_set_important_options/1

zmq_set_option/1

zmq_start_master/2

zmq_start_worker/2

zmq_worker_load_model/1

accumulate_infos/2

add_eval_result/1

add_model_checking_warnings/4

add_vacuous_invariant/1

animate_machine/0

animate_machine2/0

animation_mode_does_not_support_animation/1

append_assertion/1

assert_all_options/1

assert_option/1

atom_contains_codes/2

available_commands/1

browse/0

browse_all_machines/1

browse_machine/1

call_probcli_option/1

Meta: call_probcli_option(0)

cbc_assertions/2

cbc_check/1

cbc_deadlock_check/1

cbc_redundant_invariants/1

cbc_refinement/0

cbc_sequence/3

cbc_test_case_generation/3

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

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

check_all_expected_errors_occurred/1

check_complete/0

check_complete_operation_coverage/0

check_parser_version/0

check_ref_result/1

check_required_infos/3

check_status/4

check_totals/4

clear_loaded_files/0

cli_add_additional_property/1

cli_animateOperationNr/3

cli_assertions_ok/2

cli_checkAssertion/4

cli_check_assertions/2

cli_check_assertions/3

cli_check_csp_assertion/2

cli_check_goal/0

cli_check_properties/0

cli_check_properties/1

cli_check_scc_for_ltl_formula/2

cli_check_statespace_hash/2

cli_computeOperations/1

cli_csp_get_assertions/0

cli_csp_in_situ_refinement_check/4

cli_csp_translate_to_file/1

cli_ctl_model_check/3

cli_eval_csp_expression/1

cli_execute/3

cli_execute_add_virtual_transition/3

cli_execute_aux/6

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,CurState,ErrorOnDeadlock,LastActionName,Result) :-
    ((Nr mod 50000 =:= 0,\+option(animate_stats),\+option(silent))
    -> format('Step ~w (after ~w)~n',[Nr,LastActionName]),
    (option(verbose) -> print_state_silent(CurState) ; true),
    print('Memory used: '),tools:print_memory_used_wo_gc,flush_output,nl ; true),
    (\+ cli_invariant_ok(CurState,LastActionName) -> % also recognises no_inv command
    N1 is Nr-1,
    tools:ajoin(['INVARIANT VIOLATED after ',N1,' steps (after ',LastActionName,').'],ErrMsg),
    format('~w~n',[ErrMsg]),!,
    print_state_silent(CurState),
    error_occurred_with_msg(invariant_violation,ErrMsg),
    Result=invariant_violation,
    cli_execute_add_virtual_transition(N1,CurState,Result)
    ; \+ cli_assertions_ok(CurState,LastActionName) -> % also recognises no_inv command
    N1 is Nr-1,
    format('ASSERTION VIOLATED after ~w steps (after ~w).~n',[N1,LastActionName]),!,
    print_state_silent(CurState),
    error_occurred(assertion_violation), Result=assertion_violation,
    cli_execute_add_virtual_transition(N1,CurState,Result)
    ; cli_goal_found(CurState) -> % also recognizes no_goal command
    N1 is Nr-1,
    format('GOAL FOUND after ~w steps (after ~w).~n',[N1,LastActionName]),!,
    print_state_silent(CurState), Result=goal_found,
    cli_execute_add_virtual_transition(N1,CurState,Result)
    ; reset_side_effect_occurred,
    cli_trans(CurState,ActionName,NewState,Nr),
    !,
    N1 is Nr+1,
    (NewState=CurState, \+ side_effect_occurred(file)
    -> formatsilent('Infinite loop reached after ~w steps (looping on ~w).~n',[N1,ActionName]),
    Result=loop
    ; cli_execute_aux(N1,Steps,NewState,ErrorOnDeadlock,ActionName,Result))
).

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

cli_execute_from/5

cli_execute_trans/4

cli_find_ltl_ap/1

cli_get_coverage_information/1

cli_get_min_max_coverage/1

cli_goal_found/1

cli_init_options/2

cli_init_options2/2

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

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

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

cli_ltl_model_check/3

cli_mc/1

cli_print_all_values/1

cli_print_history/1

cli_print_junit_results/1

cli_print_machine_statistics/0

cli_print_statistics/0

cli_print_values/1

cli_process_loaded_file/2

cli_process_loaded_file_afer_start_animation/1

cli_process_loaded_file_afer_start_animation(NOW) :-
    ifm_option_set(cli_print_machine_statistics,
    cli_print_machine_statistics),
    ifm_option_set(pretty_print_internal_rep(PPFILE1),
    b_write_machine_representation_to_file(needed,PPFILE1)),
    ifm_option_set(pretty_print_all_types(PPFILE2),
    b_write_machine_representation_to_file(all,PPFILE2)),
    ifm_option_set(pretty_print_internal_rep_to_B(PPFILE3),
    b_write_eventb_machine_to_classicalb_to_file(PPFILE3)),

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

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

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

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

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

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

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

    cbc_check(NOW),
    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_forumla_model_check(Formula,Expected),cli_ctl_model_check(Formula,Expected,_)),
    % TO DO print ctl/ltl statistics
    if_options_set(csp_get_assertions,cli_csp_get_assertions),
    if_options_set(eval_csp_expression(CspExpr),cli_eval_csp_expression(CspExpr)),
    if_options_set(csp_translate_to_file(PlFile),cli_csp_translate_to_file(PlFile)),
    if_options_set(get_min_max_coverage(MinMxFileName),cli_get_min_max_coverage(MinMxFileName)),
    if_options_set(get_coverage_information(CovFileName),cli_get_coverage_information(CovFileName)),
    if_options_set(vacuity_check,cli_vacuity_check),
    if_option_set_loaded(check_goal,check_goal,cli_check_goal),
    if_option_set_loaded(animate,animate,
    (animate_machine -> true ; true)),
    if_option_set(ltsmin, start_ltsmin_srv('/tmp/ltsmin.probz', NOW)),
    if_option_set(ltsmin2(EndpointPath), start_ltsmin_srv(EndpointPath, NOW)),
    if_option_set(ltsmin_ltl_output(Path), ltsmin_ltl_output(Path, NOW)),
    evaluate_from_commandline,
    if_option_set_loaded(ltl_assertions,check_ltl_assertions,
    (timeout_call(ltl_check_assertions,NOW) -> true; true)),
    ifm_option_set_loaded(ltl_formula_model_check(Formula,Expected),check_ltl_assertions,
    (option(cli_start_sym_mc_with_lts(_))-> true % we request LTSMin, do not start prob model check
    ; timeout_call(cli_ltl_model_check(Formula,Expected,_),NOW) -> true; true)),
    ifm_option_set_loaded(ltl_file(LtlFilename),check_ltl_file,
    (ltl_check_file(LtlFilename) -> true; true)),
    ifm_option_set_loaded(history(HistoryFilename),history,
    cli_print_history(HistoryFilename)),
    ifm_option_set_loaded(print_values(ValuesFilename),values,
    cli_print_values(ValuesFilename)),
    ifm_option_set_loaded(print_all_values(ValuesDirname),values,
    cli_print_all_values(ValuesDirname)),
    if_options_set(save_state_for_refinement(SaveRefF),
    refinement_checker:tcltk_save_specification_state_for_refinement(SaveRefF)),
    if_options_set(dot_command(DCommand,DotFile),
    dot_command(DCommand,DotFile)),
    if_options_set(dot_command_for_expr(DECommand,Expr,DotFile,Opts),
    dot_command_for_expr(DECommand,Expr,DotFile,Opts)),
    if_options_set(evaluate_expression_over_history_to_csv_file(HistExpr,HistDotFile),
    user: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)),
    if_options_set(expect_evaluation(EEvals),
    check_if_predicates_were_evaluated(EEvals)),
    ifm_option_set(coverage(Nodes,Operations,ShowEnabledInfo),
    cli_show_coverage(Nodes,Operations,ShowEnabledInfo,NOW)),
    ifm_option_set(check_statespace_hash(ExpectedHash,Kind),
    cli_check_statespace_hash(ExpectedHash,Kind)),
    ifm_option_set(variable_coverage,
    cli_show_variable_coverage(NOW)),
    ifm_option_set(coverage(ShowEnabledInfo),
    cli_show_coverage(ShowEnabledInfo,NOW)),
    if_option_set(save_state(StateFile),
    save_state(StateFile)),
    if_option_set(prob_profile,
    prob_profile),
    if_option_set(statistics,
    cli_print_statistics),
    if_option_set(profile_statistics,
    profile_statistics),
    if_option_set(show_cache,
    show_cache),
    if_option_set(check_complete, check_complete),
    if_option_set(check_complete_operation_coverage, check_complete_operation_coverage),
    if_option_set(check_scc_for_ltl_formula(LtlFormula,SCC),cli_check_scc_for_ltl_formula(LtlFormula,SCC)).

cli_random_animate/2

cli_random_animate/3

cli_set_empty_machine/0

cli_set_goal/1

cli_set_searchscope/1

cli_show_coverage/2

cli_show_coverage/4

cli_show_help/2

cli_show_variable_coverage/1

cli_start_animation/1

cli_start_initialisation/1

cli_start_logging/5

cli_start_mc_with_tlc/0

cli_start_model_check/2

cli_start_refinement_check/4

cli_start_selfcheck/0

cli_start_socketserver/1

cli_start_sym_mc_with_lts/1

cli_start_trace_check/1

cli_start_trace_state_check/1

cli_symbolic_model_check/1

close_repl_input_stream/1

command_option/1

compare_kodkod_performance1/3

compile_time_flag/1

computeOperations_for_root_required/0

constraint_based_check/1

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

constraint_based_check(OpName) :- OpName\=all, % -cbc OpName
    check_loaded(constraint_based_check),
    print_repl_prompt('% 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_get_machine_operation(OpName,_,_,_) -> true
    ; add_error(probcli,'Unknown Operation Name: ',OpName)),
    definite_error_occurred
        ),nl,
    write_xml_element_to_log(cbc_check_result,[result/Result]),
    stop_xml_feature(cbc_operation_check,FINFO).

construct_and_execute_tlc_command/1

convert_dash_to_underscore/2

count_assertions/3

coverage/1

create_state_error_description/2

definite_error_occurred/0

display_match/3

display_match/4

do_det_checking/0

do_enabling_analysis_csv/2

do_feasibility_analysis/2

do_not_execute_automatically/1

do_one_gui_event/0

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

dot_command/2

dot_command_for_expr/4

Dynamic: true

Dynamic: true

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

error_occurred(Type,ErrOrWarning,_,Msg) :-
    option(expect_error(Type)),!,
    write_xml_element_to_log(expected_error_occurred,[category/Type, type/ErrOrWarning, message/Msg]),
    assert(expected_error_occurred(Type)).

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

error_occurred_with_msg/2

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

eval_help/0

eval_line/1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

eval_probcli_repl_line/1

eval_string_or_file/4

eval_string_or_file(string,String,_,Expected) :-
    set_current_probcli_command(eval_string(String)),
    print('eval: '), print(String),nl,
    reset_error_spans, % avoid underlining previous errors in eval_string
    eval_string_with_time_out(String,StringResult,EnumWarning,_LS),
    % print(enumwarning(EnumWarning,Expected)),nl,
    add_eval_result(StringResult),
    (Expected\=StringResult
    -> print_error('### Error, expected result to be: '), print_error(Expected),
    error_occurred(eval_string)
    ; EnumWarning = false -> true
    ; gen_enum_warning(Expected) % now also generate enum warnings when Expected not set (eval instead of evalt/evalf)
    ),
    unset_current_probcli_command.

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

evalchecklist/2

evalchecklist2/2

evalchecklist3/3

evaluate_expressions/1

evaluate_from_commandline/0

exec_eval_command/2

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

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

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

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

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

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

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

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

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

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

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

exec_eval_command(show_state_info,_) :- !,
    current_expression(ID,CurState),
    format('Current state ~w : ',[ID]),translate:print_bstate(CurState),nl.

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

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

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

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

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

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

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

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

generate_read_write_matrix/1

generate_time_stamp/2

get_comma_or_space_separated_options/2

get_dot_file/2

get_error_category_and_type/3

get_error_or_warning_span/4

get_probcli_elapsed_walltime/2

get_quoted_atom/4

get_state_errors/1

get_state_space_errors/0

go_cli/0

go_cli/1

go_cli2/1

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

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

go_cli_with_junit_check/1

handle_symbolic_model_check_result/1

help/0

if_option_set/2

Meta: if_option_set(-,0)

if_option_set/3

Meta: if_option_set(-,0,0)

if_option_set_loaded/3

Meta: if_option_set_loaded(-,-,0)

if_options_set/2

Meta: if_options_set(-,0)

ifm_option_set/2

Meta: ifm_option_set(-,0)

ifm_option_set/3

ifm_option_set_loaded/3

Meta: ifm_option_set_loaded(-,-,0)

initialise_required/0

irrelevant_xml_info/1

is_constant_binding/1

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_file(MainFile).

load_spec_file('p',MainFile) :- !, load_xtl_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('---------------------------------'),nl,
    print('Loading: '),print(MainFile),nl,
    load_b_file(MainFile). % Siemens Rule File; maybe in future use -eval_rule_file

load_spec_file('prob',MainFile) :- !,load_prob_file(MainFile).

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

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

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

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

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

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

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

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

load_spec_file('eval',File) :- !, cli_set_empty_machine, cli_start_animation(eval_file), eval_string_or_file(file,File,exists,_).

load_spec_file('pb',File) :- !, cli_set_empty_machine, cli_start_animation(pb_file), eval_string_or_file(file,File,exists,_).

load_spec_file('pml',MainFile) :- !,parsercall:call_promela_parser(MainFile),
    parsercall:promela_prolog_filename(MainFile,PrologFile),
    println_silent(consulting(PrologFile)),
    tcltk_open_promela_file(PrologFile).

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

load_spec_file/3

loaded_main_file/1

loaded_root_filename/1

logxml_write_vars/1

ltl_check_assertions/0

mcm_test_case_generation/4

model_check/3

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

model_check/4

my_tell/1

no_command_issued/0

normalise_option_atom/2

normalise_pref_name/2

not_command_option/1

open_file_at_position/1

option_only_works_for_single_file/1

option_requires_all_properties/1

option_verbose/0

options_allow_start_without_file/0

parse_eval_command/3

perform/1

perform_random_init_after_setup_constants/0

perform_random_initialisation/0

perform_random_initialisation/1

perform_random_initialisation_if_necessary/1

perform_random_step/1

perform_random_step/4

perform_random_steps/2

perform_random_steps_aux/3

perform_symbolic_model_checking/2

portray_message/2

pracc/1

pred_eval_hook/5

pretty_print_all_types/1

pretty_print_internal_rep/1

pretty_print_internal_rep_to_B/1

print_accumulated_infos/1

print_bindings/1

print_cbc_stats/2

print_compile_time_flags/0

print_current_state/0

print_eval_command_help/1

print_eval_results/0

print_file_info/1

print_help/0

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

print_help :- print_version,
    print('Usage: probcli FILE [OPTIONS]'),nl,
    print(' OPTIONS are: '),nl,
    print(' -mc Nr model check; checking at most Nr states'),nl,
    print(' -model_check model check without limit on states explored'),nl,
    ( \+ option_verbose ->
    print(' -noXXX XXX=dead,inv,goal,ass (for model check)'),nl % -nodead, -noinv, -nogoal, -noass
    ;
    print(' -nodead do not look for deadlocks (for model check, animate, execute)'),nl,
    print(' -noinv do not look for invariant violations (for model check, animate, execute)'),nl,
    print(' -nogoal do not look for GOAL predicate (for model check, execute)'),nl,
    print(' -noass do not look for ASSERTION violations (for model check, execute)'),nl
    ),
    print(' -bf proceed breadth-first'),nl,
    print(' -df proceed depth-first'),nl,
    print(' -mc_mode M M=hash,heuristic,random,breadth-first,depth-first,mixed'),nl,
    print(' -timeout N total timeout in ms for model and refinement checking'),nl, % also for disprover
    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 executed'),nl,
    print(' -execute Nr execute first operation found without storing states (max. Nr steps)'),nl,
    print(' -execute_all execute first operation found until a deadlock is reached'),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(' -card GS Val set scope of B deferred set'),nl,
    print(' -goal "PRED" set GOAL predicate for model checker'),nl,
    print(' -check_goal check GOAL (after -mc, -t, or -animate)'),nl,
    print(' -scope "PRED"set scope predicate for model checker'),nl,
    print(' -s Port start socket server on given port'),nl,
    print(' -ss start socket server on port 9000'),nl,
    print(' -sf start socket server on some free port'),nl,
    print(' -l LogFile log activities in LogFile'),nl,
    print(' -ll log activities in /tmp/prob_cli_debug.log'),nl,
    print(' -lg LogFile analyse logfile using gnuplot'),nl,
    print(' -pp FILE pretty-print internal representation to file'), nl,
    print(' -ppf FILE like -pp, but force printing of all type infos'),nl,
    print(' -ppB FILE pretty-print internal representation to file in valid B syntax'),nl,
    print(' -v verbose'),nl,
    print(' -mc_with_tlc model check using the model checker TLC'),nl,
    print(' -mc_with_lts_sym model check using the model checker LTSmin (symbolic)'),nl,
    print(' -mc_with_lts_seq model check using the model checker LTSmin (sequential)'),nl,
    %% print(' -vv very verbose'),nl, % no effect when debugging calls disabled

    ( \+ 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(' -version print version information (-svers for short info)'),nl,
    print(' -check_java_version check that Java version compatible with ProB parser'),nl,
    print(' -assertions check ASSERTIONS'),nl,
    print(' -main_assertions check ASSERTIONS from main file only'),nl,
    print(' -properties check PROPERTIES'),nl,
    print(' -cache Dir use directory "Dir" to cache constants and variables'),nl,
    print(' -ltlfile F check LTL formulas in file F'),nl,
    print(' -ltlassertions check LTL assertions (in DEFINITIONS)'),nl,
    print(' -ltllimit L explore at most L states when model-checking LTL or CTL'),nl,
    print(' -ltlformula \"F\" check the LTL formula F'),nl,
    print(' -ctlformula \"F\" check the CTL formula F'),nl,
    print(' -save File save state space for later refinement check'),nl,
    print(' -refchk File refinement check against previous saved state space'),nl,
    print(' -mcm_tests Depth MaxStates EndPredicate File'),nl,
    print(' generate test cases with maximum length Depth, explore'),nl,
    print(' maximally MaxStates, the last state satisfies EndPredicate'),nl,
    print(' and the test cases are written to File'),nl,
    print(' -mcm_cover Operation'),nl,
    print(' when generating MCM test cases, Operation should be covered'),nl,
    print(' -cbc_tests Depth EndPredicate File'),nl,
    print(' generate test cases by constraint solving with maximum'),nl,
    print(' length Depth, the last state satisfies EndPredicate'),nl,
    print(' and the test cases are written to File'),nl,
    print(' -cbc_cover Operation'),nl,
    print(' when generating CBC test cases, Operation should be covered'),nl,
    % print(' -cbc_cover_all try and cover all operations'),nl, % is now default if no cbc_cover provided
    print(' -test_description File'),nl,
    print(' read information for test generation from File'),nl,
    print(' -dot CMD File write a graph to a dot file, with CMD being one of:'),nl,
    (is_dot_command(Cmd),command_description(Cmd,_,Desc),
    format(' ~w : ~w~n',[Cmd,Desc]),fail
    ; true),
    print(' -dotexpr CMD Expr File write a graph for Expr to a dot file, with CMD:'),nl,
    (is_dot_command_for_expr(Cmd),command_description(Cmd,_,Desc),
    format(' ~w : ~w~n',[Cmd,Desc]),fail
    ; true),
    print(' -dot_output Path generate dot files for false assertions/properties'),nl,
    print(' -dot_all also generate dot files for true assertions/properties'),nl,
    print(' -csvhist E File evaluate expression over history and generate CSV file.'),nl,
    print(' -load_state File load state from a saved state (generated by PrB 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(' -expcteval Evals expect that the given predicates have been evaluated or not (see external predicate IS_EVALUATED)'),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(' .csp, .cspm for CSP-M files, same format as FDR'),nl,
    print(' .eventb for Event-B packages exported from Rodin ProB Plugin'),nl,
    print(' .tla for TLA+ models'),nl,
    ( option_verbose ->
    print(' Preferences PREF are: '),nl,
    print_eclipse_prefs
    ; otherwise ->
    print(' Use --help -v to print avalaible preferences PREF'),nl
    ),
    print(' More info at: http://www.stups.hhu.de/ProB/'),nl,
    print(' and at: http://www.prob2.de/probcli/'),nl,
    % http://www.stups.hhu.de/ProB/index.php5/Using_the_Command-Line_Version_of_ProB
    nl.

print_probcli_error_non_strict/2

print_short_version/0

print_state_silent/1

print_total_probcli_timer/0

probcli_add_light_warning/2

probcli_startup/0

process_cbc_assertion_result/2

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

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

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

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

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

process_ltsmin_result/1

profiling_on/0

recognised_cli_option/4

recognised_option/2

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

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

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

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

recognised_option('-animate_stats',animate_stats).

recognised_option('-check_goal',check_goal).

recognised_option('-ltlassertions',ltl_assertions).

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

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

recognised_option('-properties',cli_check_properties).

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

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

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

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

recognised_option('-bf',breadth_first).

recognised_option('-breadth',breadth_first).

recognised_option('-df',depth_first).

recognised_option('-depth',depth_first).

recognised_option('-strict',strict_raise_error).

recognised_option('-silent',silent).

recognised_option('-statistics',statistics).

recognised_option('-profile_statistics',profile_statistics).

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

recognised_option('-nodead',no_deadlocks).

recognised_option('-noinv',no_invariant_violations).

recognised_option('-nogoal',no_goal).

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

recognised_option('-noass',no_assertion_violations).

recognised_option('-nocounter',no_counter_examples).

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

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

recognised_option('-i',animate).

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

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

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

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

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

recognised_option('-machine_stats',cli_print_machine_statistics).

recognised_option('-vc',variable_coverage).

recognised_option('-variable_coverage',variable_coverage).

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

recognised_option('-v',verbose).

recognised_option('-vv',very_verbose).

recognised_option('-verbose',verbose).

recognised_option('-very_verbose',very_verbose).

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

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

recognised_option('-version',print_version).

recognised_option('-svers',print_short_version).

recognised_option('-short_version',print_short_version).

recognised_option('-check_java_version',check_java_version).

recognised_option('-java_version',check_java_version).

recognised_option('-file_info',file_info).

recognised_option('-t',trace_check).

recognised_option('-trace_check',trace_check).

recognised_option('-init',initialise).

recognised_option('-initialise',initialise).

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

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

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

recognised_option('-help',help).

recognised_option('-h',help).

recognised_option('-rc',runtimechecking).

recognised_option('-test_mode',test_mode).

recognised_option('-check_complete',check_complete).

recognised_option('-check_complete_operation_coverage', check_complete_operation_coverage).

recognised_option('-mc_with_tlc', cli_start_mc_with_tlc).

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

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

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

recognised_option('-ltsmin',ltsmin).

recognised_option/3

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

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

recognised_option('-plugin',plugin(Plugin), [Plugin]).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

recognised_option/4

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

recognised_option('-expcteval',expect_evaluation(List),[Arg],user:evalchecklist(Arg,List)).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

repl_multi_read_line/1

repl_multi_read_line_aux/3

reset_cli/0

reset_dot_file_number/0

reset_expected_error_occurred/0

set_current_probcli_command/1

set_dot_file_prefix/1

set_dot_file_prefix_if_option_set/1

set_junit_mode/1

set_new_random_seed/0

set_optional_errors/0

set_pref/2

set_prefs/0

set_random_seed_to_deterministic_start_seed/0

set_repl_input_file/2

show_cache/0

show_initialisation_summary/1

show_last_expression_as_table/0

show_operation_coverage_summary/1

split_by_seperator2/2

start_animation_without_computing/0

start_ltsmin_srv/2

start_probcli_timer/1

start_xml_feature/2

start_xml_feature/4

stop_probcli_debug_timer/2

stop_probcli_timer/2

stop_probcli_timer/3

stop_xml_feature/2

store_last_error_location_for_repl/0

strip_leading_ws/2

strip_ws/2

strip_ws2/2

test_kodkod_and_exit/2

timeout_call/2

Meta: timeout_call(0,-)

translate_exception/2

treat_existence_error/4

truncate_animate_action/2

unset_analyse_hook/0

unset_current_probcli_command/0

we_need_only_static_assertions/1

write_deferred_set_used/1

write_dot_graph_to_new_file/2

write_important_xml_element_to_log/2

write_result_to_file/1

xml_log_machine_statistics/0

zmq_delayed_option/1

zmq_get_important_options/1

zmq_get_initialisation_term/1

zmq_important_option/1

zmq_set_important_options/1

zmq_set_option/1

zmq_start_master/2

zmq_start_worker/2

zmq_worker_load_model/1

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_machine(Machine),
    set_animation_mode(b),
    prob2_interface:start_animation, cli_computeOperations(_)
.

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

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

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

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

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

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

Determinacy Checker

Determinacy Checker:

! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_terminal_colors,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in debug:global_debug_flag/0
! procedure debug:global_debug_flag/0 does not exist
! goal: debug:global_debug_flag
! Existence error in debug:use_timer/0
! procedure debug:use_timer/0 does not exist
! goal: debug:use_timer
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_34947,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/error_manager.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(specfile) does not exist
! goal: absolute_file_name(probsrc(specfile),_20741,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(translate) does not exist
! goal: absolute_file_name(probsrc(translate),_20741,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_20741,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_enumerate) does not exist
! goal: absolute_file_name(probsrc(b_enumerate),_20741,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_state_model_check) does not exist
! goal: absolute_file_name(probsrc(b_state_model_check),_20741,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bmachine) does not exist
! goal: absolute_file_name(probsrc(bmachine),_20741,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(debug) does not exist
! goal: absolute_file_name(probsrc(debug),_20741,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(preferences) does not exist
! goal: absolute_file_name(probsrc(preferences),_20741,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_interpreter) does not exist
! goal: absolute_file_name(probsrc(b_interpreter),_20741,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(predicate_debugger) does not exist
! goal: absolute_file_name(probsrc(predicate_debugger),_20741,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_trace_checking) does not exist
! goal: absolute_file_name(probsrc(b_trace_checking),_20741,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! 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 extension('random_permutations/random_permutations') does not exist
! goal: absolute_file_name(extension('random_permutations/random_permutations'),_122117,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/clpfd_interface.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'),_128081,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/state_space.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_myheap,false)
! Existence error in argument 1 of absolute_file_name/3
! file extension('random_permutations/random_permutations') does not exist
! goal: absolute_file_name(extension('random_permutations/random_permutations'),_171719,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/fd_utils_clpfd.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(clpfd_interface) does not exist
! goal: absolute_file_name(probsrc(clpfd_interface),_173477,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/typing_tools.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_wd_checking,true)
! Existence error in argument 1 of absolute_file_name/3
! file prob_rewrite_rules(b_ast_cleanup_rewrite_rules) does not exist
! goal: absolute_file_name(prob_rewrite_rules(b_ast_cleanup_rewrite_rules),_196633,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/b_ast_cleanup.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(partially_evaluate,true)
! Existence error in debug:global_debug_flag/0
! procedure debug:global_debug_flag/0 does not exist
! goal: debug:global_debug_flag
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(partially_evaluate,true)
! Existence error in debug:use_timer/0
! procedure debug:use_timer/0 does not exist
! goal: debug:use_timer
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(partially_evaluate,true)
! Existence error in debug:global_debug_flag/0
! procedure debug:global_debug_flag/0 does not exist
! goal: debug:global_debug_flag
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(disable_chr,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_wd_checking,true)
! Existence error in debug:global_debug_flag/0
! procedure debug:global_debug_flag/0 does not exist
! goal: debug:global_debug_flag
! Existence error in debug:use_timer/0
! procedure debug:use_timer/0 does not exist
! goal: debug:use_timer
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_201759,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/kernel_strings.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_196633,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/external_functions.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(custom_explicit_sets) does not exist
! goal: absolute_file_name(probsrc(custom_explicit_sets),_192501,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/b_compiler.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_wd_checking,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,xxxtrue)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file extension('random_permutations/random_permutations') does not exist
! goal: absolute_file_name(extension('random_permutations/random_permutations'),_169437,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/kernel_objects.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(disable_chr,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_146575,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/kodkod/kodkod.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bmachine) does not exist
! goal: absolute_file_name(probsrc(bmachine),_146575,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/kodkod/kodkod.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(self_check) does not exist
! goal: absolute_file_name(probsrc(self_check),_146575,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/kodkod/kodkod.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_146575,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/kodkod/kodkod.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(translate) does not exist
! goal: absolute_file_name(probsrc(translate),_146575,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/kodkod/kodkod.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(predicate_analysis) does not exist
! goal: absolute_file_name(probsrc(predicate_analysis),_146575,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/kodkod/kodkod.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(btypechecker) does not exist
! goal: absolute_file_name(probsrc(btypechecker),_146575,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/kodkod/kodkod.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_global_sets) does not exist
! goal: absolute_file_name(probsrc(b_global_sets),_144627,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/kodkod/kodkod.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'),_150143,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/succeed_max.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_148191,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/b_machine_hierarchy.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_147715,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/value_persistance.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_state_model_check) does not exist
! goal: absolute_file_name(probsrc(b_state_model_check),_147485,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/b_read_write_info.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file smt_solvers_interface(smt_solvers_interface) does not exist
! goal: absolute_file_name(smt_solvers_interface(smt_solvers_interface),_138795,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/b_interpreter.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(module_information) does not exist
! goal: absolute_file_name(probsrc(module_information),_144729,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/promela/h_int.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probcspsrc(haskell_csp) does not exist
! goal: absolute_file_name(probcspsrc(haskell_csp),_138795,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/xtl_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probcspsrc(haskell_csp) does not exist
! goal: absolute_file_name(probcspsrc(haskell_csp),_128987,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/specfile.pl')])
! Existence error in tools:platform_is_64_bit/0
! procedure tools:platform_is_64_bit/0 does not exist
! goal: tools:platform_is_64_bit
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_94145,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/pragmas.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(module_information) does not exist
! goal: absolute_file_name(probsrc(module_information),_95383,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/bmachine_static_checks.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file prozsrc(z_tools) does not exist
! goal: absolute_file_name(prozsrc(z_tools),_91295,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/bmachine_eventb.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(gensym) does not exist
! goal: absolute_file_name(probsrc(gensym),_46957,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/translate.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(btypechecker) does not exist
! goal: absolute_file_name(probsrc(btypechecker),_27347,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/bsyntaxtree.pl')])
! Existence error in debug:global_debug_flag/0
! procedure debug:global_debug_flag/0 does not exist
! goal: debug:global_debug_flag
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,xtrue)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_20741,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(state_space) does not exist
! goal: absolute_file_name(probsrc(state_space),_20741,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(state_space_exploration_modes) does not exist
! goal: absolute_file_name(probsrc(state_space_exploration_modes),_20741,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('plspec/plspec/plspec') does not exist
! goal: absolute_file_name(extension('plspec/plspec/plspec'),_19329,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probporsrc(static_analysis) does not exist
! goal: absolute_file_name(probporsrc(static_analysis),_32027,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/model_checker.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probcspsrc(haskell_csp) does not exist
! goal: absolute_file_name(probcspsrc(haskell_csp),_32027,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/bvisual2.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(specfile) does not exist
! goal: absolute_file_name(probsrc(specfile),_33439,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(translate) does not exist
! goal: absolute_file_name(probsrc(translate),_33439,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_33439,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_enumerate) does not exist
! goal: absolute_file_name(probsrc(b_enumerate),_33439,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_state_model_check) does not exist
! goal: absolute_file_name(probsrc(b_state_model_check),_33439,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bmachine) does not exist
! goal: absolute_file_name(probsrc(bmachine),_33439,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(debug) does not exist
! goal: absolute_file_name(probsrc(debug),_33439,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(preferences) does not exist
! goal: absolute_file_name(probsrc(preferences),_33439,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_interpreter) does not exist
! goal: absolute_file_name(probsrc(b_interpreter),_33439,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(predicate_debugger) does not exist
! goal: absolute_file_name(probsrc(predicate_debugger),_33439,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_trace_checking) does not exist
! goal: absolute_file_name(probsrc(b_trace_checking),_33439,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_33439,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(state_space) does not exist
! goal: absolute_file_name(probsrc(state_space),_33439,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(state_space_exploration_modes) does not exist
! goal: absolute_file_name(probsrc(state_space_exploration_modes),_33439,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('plspec/plspec/plspec') does not exist
! goal: absolute_file_name(extension('plspec/plspec/plspec'),_32027,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/tcltk_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file smt_solvers_interface(smt_solvers_interface) does not exist
! goal: absolute_file_name(smt_solvers_interface(smt_solvers_interface),_38537,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/solver_interface.pl')])
! 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(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_32173,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/b_state_model_check.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('user_signal/user_signal') does not exist
! goal: absolute_file_name(extension('user_signal/user_signal'),_19663,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/eclipse_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_40281,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/symmetry_marker.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('user_signal/user_signal') does not exist
! goal: absolute_file_name(extension('user_signal/user_signal'),_38901,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/evalstores.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_myheap,false)
! Existence error in argument 1 of absolute_file_name/3
! file probltlsrc(ltl) does not exist
! goal: absolute_file_name(probltlsrc(ltl),_20711,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/prob2_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('user_signal/user_signal') does not exist
! goal: absolute_file_name(extension('user_signal/user_signal'),_21079,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/prob_socketserver.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_profile,true)
! Existence error in argument 1 of absolute_file_name/3
! file probltlsrc(ltl) does not exist
! goal: absolute_file_name(probltlsrc(ltl),_273,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/src/prob_cli.pl')])

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Name: sort/2
Name: findall/3

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

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

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

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

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

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

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

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

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

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

../../prolog/src/prob_cli.pl

Modules

Predicates of prob_cli.pl

Module Information

3959 Lines

358 Predicates

0 Exports

113 specified Imports

Predicates:

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

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

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

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

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

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

Name: stop_probcli_debug_timer/2	Module: prob_cli.pl
Name: maplist/2	Module: lists
Name: start_probcli_timer/1	Module: prob_cli.pl
Name: !
Name: get_assertions_from_machine/2	Module: bmachine
Name: state_corresponds_to_initialised_b_machine/2	Module: foo_error
Name: option/1	dynamic predicate

Name: cli_check_assertions/3	Module: prob_cli.pl
Name: probcli_time_stamp/1	dynamic predicate

Name: check_required_infos/3	Module: prob_cli.pl
Name: write_important_xml_element_to_log/2	Module: prob_cli.pl
Name: accumulate_infos/2	Module: prob_cli.pl
Name: debug_println/2	Module: foo_error
Name: tcltk_analyse_goal/2	Module: foo_error
Name: nl
Name: print/1
Name: error_occurred/1	Module: prob_cli.pl
Name: add_error/2	Module: foo_error
Name: !
Name: b_get_machine_goal/1	Module: foo_error
Name: not/1

Name: formatsilent/2	Module: foo_error
Name: loaded_root_filename/1	Module: prob_cli.pl
Name: writeln_log_time/1	Module: foo_error
Name: error_occurred/1	Module: prob_cli.pl
Name: nl
Name: print/1
Name: tcltk_debug_properties/3	Module: foo_error
Name: ->/3
Name: otherwise
Name: ->/2
Name: print_error/1	Module: tools_printing
Name: true
Name: check_summary_all_true/1	Module: predicate_evaluator
Name: write_important_xml_element_to_log/2	Module: prob_cli.pl
Name: accumulate_infos/2	Module: prob_cli.pl
Name: unset_analyse_hook/0	Module: prob_cli.pl
Name: tcltk_analyse_properties/2	Module: predicate_evaluator
Name: set_analyse_hook/1	Module: prob_cli.pl
Name: current_state_corresponds_to_setup_constants_b_machine/0	Module: state_space