Dynamic Predicates: prob2_formula/3

3478 Lines

323 Predicates

Imported Modules: module_information sets typechecker self_check random lists lists

154 Exports

205 specified Imports

Imports	Exports
Name: time_out_for_node/1 Module: state_space Name: time_out_for_node/3 Module: state_space Name: time_out_for_invariant/1 Module: state_space Name: max_reached_for_node/1 Module: state_space Name: max_reached_or_timeout_for_node/1 Module: state_space Name: visited_expression/2 Module: state_space Name: transition/4 Module: state_space Name: visited_expression_id/1 Module: state_space Name: set_context_state/2 Module: state_space Name: clear_context_state/0 Module: state_space Name: state_error/3 Module: state_space Name: current_state_id/1 Module: state_space Name: set_current_state_id/1 Module: state_space Name: get_state_space_stats/3 Module: state_space Name: try_set_trace_by_transition_ids/1 Module: state_space Name: set_current_state_for_external_fun/1 Module: external_functions Name: clear_state_for_external_fun/0 Module: external_functions Name: announce_event/1 Module: eventhandling Name: version/4 Module: version Name: revision/1 Module: version Name: lastchangeddate/1 Module: version Name: b_get_preferences_from_specification/0 Module: pref_definitions Name: b_get_preferences_from_specification/1 Module: pref_definitions Name: conjunct_predicates/2 Module: bsyntaxtree Name: get_texpr_type/2 Module: bsyntaxtree Name: get_texpr_expr/2 Module: bsyntaxtree Name: find_identifier_uses/3 Module: bsyntaxtree Name: set_depth_breadth_first_mode/1 Module: state_space_exploration_modes Name: b_type_expression/5 Module: bmachine Name: b_get_machine_operation/4 Module: bmachine Name: b_get_machine_operation/6 Module: bmachine Name: b_type_open_predicate/5 Module: bmachine Name: b_top_level_operation/1 Module: bmachine Name: get_machine_operation_additional_identifiers/2 Module: bmachine Name: b_load_machine_from_list_of_facts/2 Module: bmachine Name: b_set_eventb_project_flat/3 Module: bmachine Name: load_additional_information/1 Module: bmachine Name: b_machine_precompile/0 Module: bmachine Name: other_spec_precompile/0 Module: bmachine Name: b_set_parsed_typed_machine_goal/1 Module: bmachine Name: b_is_variable/2 Module: bmachine Name: b_is_constant/1 Module: bmachine Name: b_is_variable/1 Module: bmachine Name: b_is_constant/2 Module: bmachine Name: b_test_boolean_expression_cs/5 Module: b_interpreter Name: b_compute_expression_nowf/6 Module: b_interpreter Name: add_prob_deferred_set_elements_to_store/3 Module: b_global_sets Name: user_interruptable_call_det/2 Module: user_signal/user_signal Name: ignore_user_interrupt_det/1 Module: user_signal/user_signal Name: maplist/2 Module: lists Name: maplist/3 Module: lists Name: maplist/4 Module: lists Name: read_from_codes/2 Module: codesio Name: write_term_to_codes/4 Module: codesio Name: expand_const_and_vars_to_full_store/2 Module: specfile Name: animation_mode/1 Module: specfile Name: csp_mode/0 Module: specfile Name: b_or_z_mode/0 Module: specfile Name: xtl_mode/0 Module: specfile Name: set_currently_opened_file/1 Module: specfile Name: set_currently_opened_b_file/1 Module: specfile Name: set_minor_animation_mode_from_file/1 Module: specfile Name: set_currently_opening_file/1 Module: specfile Name: set_failed_to_open_file/1 Module: specfile Name: set_currently_opened_package/1 Module: specfile Name: set_animation_mode/1 Module: specfile Name: set_animation_minor_mode/1 Module: specfile Name: with_translation_mode/2 Module: translate Name: get_language_mode/1 Module: translate Name: with_language_mode/2 Module: translate Name: translate_bvalue_for_expression/3 Module: translate Name: suppress_rodin_positions/1 Module: translate Name: reset_suppress_rodin_positions/1 Module: translate Name: translate_event/2 Module: translate Name: translate_bstate/2 Module: translate Name: translate_state_error/2 Module: translate Name: translate_bexpression/2 Module: translate Name: translate_bvalue_with_limit/3 Module: translate Name: translate_event_error/2 Module: translate Name: explain_event_trace/3 Module: translate Name: explain_state_error/3 Module: translate Name: add_error_and_fail/3 Module: error_manager Name: get_all_errors_with_span_info_and_reset/1 Module: error_manager Name: get_all_errors_with_span_and_context_and_reset/1 Module: error_manager Name: add_error/3 Module: error_manager Name: add_error/2 Module: error_manager Name: add_message/2 Module: error_manager Name: add_message/3 Module: error_manager Name: reset_errors/0 Module: error_manager Name: add_warning/3 Module: error_manager Name: add_all_perrors/1 Module: error_manager Name: no_real_perror_occurred/1 Module: error_manager Name: get_error/2 Module: error_manager Name: catch_enumeration_warning_exceptions/2 Module: error_manager Name: real_error_occurred/0 Module: error_manager Name: warning_occurred/0 Module: error_manager Name: string_concatenate/3 Module: tools Name: split_atom/3 Module: tools Name: safe_atom_codes/2 Module: tools Name: ajoin/2 Module: tools Name: eclipse_preference/2 Module: preferences Name: get_preference/2 Module: preferences Name: preference_description/2 Module: preferences Name: preference_val_type/2 Module: preferences Name: preference_default_value/2 Module: preferences Name: preference_category/2 Module: preferences Name: set_preference/2 Module: preferences Name: advanced_eclipse_preference/2 Module: preferences Name: deprecated_eclipse_preference/4 Module: preferences Name: obsolete_eclipse_preference/1 Module: preferences Name: solve_predicate/5 Module: solver_interface Name: call_with_smt_mode_enabled/1 Module: solver_interface Name: parse_and_load_cspm_file/1 Module: haskell_csp Name: debug_println/2 Module: debug Name: get_user_signal_ref/1 Module: user_signal/user_signal Name: get_total_number_of_errors/1 Module: error_manager Name: b_set_typed_machine/2 Module: bmachine Name: call_fuzz_parser/2 Module: parsercall Name: open_xtl_file/1 Module: xtl_interface Name: b_set_empty_machine/0 Module: bmachine Name: load_alloy_model/2 Module: alloy2b/alloy2b Name: get_id_of_node_and_add_if_required/6 Module: state_space_exploration_modes Name: b_is_operation_name/1 Module: bmachine Name: b_is_initialisation_name/1 Module: bmachine Name: get_operation_name/2 Module: specfile Name: is_concrete_constants_state_id/1 Module: state_space Name: succeed_max_call_id/3 Module: succeed_max Name: execute_operation_by_predicate_in_state/5 Module: b_state_model_check Name: inline_prob_deferred_set_elements_into_bexpr/2 Module: b_global_sets Name: assert_temp_typed_predicate/1 Module: bmachine Name: reset_temp_predicate/0 Module: bmachine Name: visited_state_corresponds_to_setup_constants_b_machine/1 Module: state_space Name: visited_state_corresponds_to_initialised_b_machine/1 Module: state_space Name: xtl_invariant_violated/1 Module: xtl_interface Name: extract_span_description/2 Module: error_manager Name: evaluate_parsed_csp_expression_with_timing/2 Module: haskell_csp Name: extend_state_with_stored_lets/2 Module: eval_let_store Name: b_is_variable/2 Module: bmachine Name: b_is_constant/2 Module: bmachine Name: b_type_expression_for_full_b_machine/6 Module: bmachine Name: get_stored_let_typing_scope/1 Module: eval_let_store Name: reset_let_values/0 Module: eval_let_store Name: safe_time_out/3 Module: tools_meta Name: catch_clpfd_overflow_call2/2 Module: clpfd_interface Name: enter_new_error_scope/2 Module: error_manager Name: exit_error_scope/3 Module: error_manager Name: clear_all_errors_in_error_scope/1 Module: error_manager Name: event_occurred_in_error_scope/1 Module: error_manager Name: abort_error_occured_in_error_scope/0 Module: error_manager Name: normalise_value_for_var/4 Module: store Name: safe_create_texpr/4 Module: bsyntaxtree Name: determine_type_of_formula/2 Module: bmachine Name: catch_clpfd_overflow_call1/1 Module: clpfd_interface Name: cbc_deadlock_freedom_check/3 Module: b_state_model_check Name: cbc_find_redundant_invariants/2 Module: b_state_model_check Name: b_set_up_valid_state_with_pred/4 Module: b_state_model_check Name: get_state_for_b_formula/3 Module: specfile Name: solver_pp_bvalue/4 Module: solver_interface Name: solve_predicate_with_satsolver_free/4 Module: satsolver/b2sat Name: solve_predicate_with_satsolver_in_state/4 Module: satsolver/b2sat Name: temporary_set_preference/3 Module: preferences Name: reset_temporary_preference/2 Module: preferences Name: convert_cli_arg/2 Module: tools_strings Name: get_possible_preferences_matches_msg/2 Module: tools_matching Name: specfile_possible_trans_name_for_successors/2 Module: specfile Name: prepare_state_for_specfile_trans/3 Module: specfile Name: specfile_trans_or_partial_trans/7 Module: specfile Name: throw_enumeration_warnings_in_current_scope/0 Module: error_manager Name: add_internal_error/2 Module: error_manager Name: error_occurred_in_error_scope/0 Module: error_manager Name: safe_time_out/3 Module: tools_meta Name: start_ms_timer/1 Module: tools Name: stop_ms_walltimer_with_msg/2 Module: tools Name: get_internal_representation/1 Module: specfile Name: get_internal_representation/3 Module: specfile Name: set_print_type_infos/1 Module: translate Name: b_get_machine_operation/4 Module: bmachine Name: b_get_machine_operation_for_animation/4 Module: bmachine Name: b_get_initialisation_from_machine/2 Module: bmachine Name: call_with_preference/3 Module: preferences Name: channel/2 Module: haskell_csp Name: get_texpr_id/2 Module: bsyntaxtree Name: b_get_operation_non_det_modifies/2 Module: bmachine Name: b_get_operation_normalized_read_write_info/3 Module: bmachine Name: b_filenumber/4 Module: bmachine Name: get_machine_identifiers/2 Module: bmachine Name: get_machine_identifiers_with_pp_type/2 Module: bmachine Name: get_cspm_identifier/2 Module: haskell_csp Name: fuzzy_match_codes_lower_case/2 Module: tools_matching Name: codes_to_lower_case/2 Module: tools_matching Name: get_current_expr_keywords/1 Module: tools_matching Name: get_current_keywords/1 Module: tools_matching Name: get_all_svg_attributes/1 Module: tools_matching Name: is_svg_color_name/1 Module: tools_matching Name: get_all_dot_attributes/1 Module: tools_matching Name: common_prefix_atom/2 Module: tools_lists Name: ord_union/3 Module: ordsets Name: get_latex_keywords/1 Module: translate Name: get_latex_keywords_with_backslash/1 Module: translate Name: ascii_to_unicode/2 Module: translate Name: latex_to_unicode/2 Module: translate Name: extended_static_check_machine/0 Module: bmachine_static_checks Name: ensure_wd/2 Module: banditfuzz/welldef Name: clean_up_pred/3 Module: b_ast_cleanup Name: replay_json_trace_file/5 Module: b_intelligent_trace_replay	Name: initialise_specification/0 Name: get_version/7 Name: get_user_signal_reference/1 Name: get_prob_total_number_of_errors/1 Name: load_classical_b_from_list_of_facts/2 Name: update_preferences_from_spec/0 Name: update_preferences_from_spec/1 Name: load_event_b_project/4 Name: load_cspm_spec_from_cspm_file/1 Name: load_z_spec_from_fuzz_file/1 Name: load_z_spec_from_tex_file/1 Name: load_xtl_spec_from_prolog_file/1 Name: load_alloy_spec_from_term/2 Name: prob2_reset_prob/0 Name: reset_animator/0 Name: clear_animator/0 Name: start_animation/0 Name: serialize/2 Name: deserialize/2 Name: get_state/2 Name: get_b_state/2 Name: compute_operations_for_state/2 Name: prob2_execute_custom_operations/6 Name: get_op_from_id/4 Name: is_initialised_state/1 Name: is_initialised_b_state/1 Name: state_property/3 Name: op_timeout_occurred/2 Name: prob2_get_state_errors/2 Name: prob2_evaluate_formulas/3 Name: register_prob2_formulas/2 Name: unregister_prob2_formulas/1 Name: get_animation_image_list/1 Name: get_animation_image_matrix_for_state/6 Name: get_react_to_item_right_click_options_for_state/4 Name: react_to_item_right_click_option_for_state/6 Name: prob2_get_formula_type/3 Name: get_states_for_predicate/3 Name: filter_states_for_predicate/3 Name: get_top_level_formulas/1 Name: insert_formula_for_expansion/2 Name: prob2_evaluate_bvisual2_formulas/3 Name: prob2_evaluate_bvisual2_formulas/4 Name: prob2_expand_bvisual2_formula/3 Name: do_modelchecking/5 Name: set_goal_for_model_checking/1 Name: compute_efficient_statespace_stats/3 Name: compute_coverage/5 Name: get_modelchecking_coverage/5 Name: get_statistics/2 Name: prob2_deadlock_freedom_check/2 Name: prob2_invariant_check/2 Name: prob2_redundant_invariants/2 Name: get_enable_matrix/2 Name: prob2_do_ltl_modelcheck/3 Name: prob2_do_ltl_modelcheck/4 Name: prob2_do_ctl_modelcheck/4 Name: prob2_do_ctl_modelcheck/6 Name: find_trace_to_node/2 Name: find_trace_from_node_to_node/3 Name: find_state_for_predicate/3 Name: cbc_disprove/5 Name: cbc_disprove/6 Name: cbc_solve_with_opts/5 Name: cbc_timed_solve_with_opts/6 Name: pretty_print_predicate/3 Name: cbc_generate_test_cases/3 Name: prob2_find_test_path/4 Name: ast_leaf_walks/2 Name: check_csp_assertions/3 Name: list_eclipse_preferences/1 Name: list_all_eclipse_preferences/1 Name: list_current_eclipse_preferences/1 Name: get_eclipse_preference/2 Name: set_eclipse_preference/2 Name: get_signature_merge_state_space/2 Name: get_transition_diagram/2 Name: write_dotty_transition_diagram/2 Name: write_dotty_signature_merge/2 Name: write_dot_for_state_viz/2 Name: write_dotty_state_space/1 Name: is_dotty_command/1 Name: write_dotty/2 Name: is_dotty_command_for_expr/1 Name: write_dotty_for_expr/3 Name: get_dot_commands_in_state/2 Name: call_dot_command_in_state/4 Name: get_dot_commands_with_trace/2 Name: call_dot_command_with_trace/4 Name: get_plantuml_commands_in_state/2 Name: call_plantuml_command_in_state/4 Name: get_plantuml_commands_with_trace/2 Name: call_plantuml_command_with_trace/4 Name: get_table_commands_in_state/2 Name: call_table_command_in_state/4 Name: get_table_commands_with_trace/2 Name: call_table_command_with_trace/4 Name: get_error_messages_with_span_info/1 Name: generate_trace_until_condition_fulfilled/4 Name: execute_model/5 Name: execute_model/6 Name: get_unsat_core_with_fixed_conjuncts/3 Name: get_minimum_unsat_core_with_fixed_conjuncts/3 Name: prob2_construct_trace/6 Name: prob2_find_trace/5 Name: prob2_refine_trace/8 Name: symbolic_model_check/2 Name: start_synthesis_from_ui_/13 Name: start_synthesis_single_operation_from_ui_/11 Name: get_valid_and_invalid_equality_predicates_for_operation_/6 Name: get_valid_and_invalid_equality_predicates_for_invariants_/4 Name: get_invariant_violating_vars_from_examples_/3 Name: adapt_machine_code_for_operations_/2 Name: reset_synthesis_context_/0 Name: generate_data_from_machine_operation_/6 Name: generate_synthesis_data_from_predicate_untyped_/5 Name: generate_operation_data_from_machine_path_/4 Name: get_pretty_print/1 Name: get_pretty_print_unicode/1 Name: get_machine_internal_representation/2 Name: get_operations_and_names/2 Name: get_primed_predicate/2 Name: get_nonquantifying_primed_predicate/2 Name: get_weakest_precondition/3 Name: before_after_predicate/2 Name: get_machine_operation_names/1 Name: get_machine_operation_infos/1 Name: get_machine_operation_infos_typed/1 Name: get_machine_identifiers/2 Name: get_machine_files/1 Name: get_possible_completions/3 Name: get_possible_completion/3 Name: get_possible_fuzzy_matches/2 Name: prob2_extended_static_check/1 Name: prob2_check_well_definedness/2 Name: prob2_ensure_wd/2 Name: prob2_load_visb_file/1 Name: prob2_get_loaded_visb_file/1 Name: prob2_visb_file_loaded/2 Name: prob2_visb_attributes_for_state/2 Name: prob2_visb_click_events_and_hovers/2 Name: prob2_visb_perform_click/4 Name: prob2_visb_items/1 Name: prob2_visb_svg_objects/1 Name: prob2_visb_default_svg_file_contents/1 Name: prob2_read_visb_path_from_definitions/1 Name: prob2_export_visb_html_for_history/2 Name: prob2_export_visb_html_for_history/3 Name: prob2_export_visb_for_current_state/1 Name: prob2_export_visb_html_for_states/3 Name: prob2_get_visb_html_for_states/3 Name: prob2_replay_json_trace_file/4 Name: get_constants_predicate/1 Name: replay_state_trace_from_file/3

Imports

Exports

Name: time_out_for_node/1

Module: state_space

Name: time_out_for_node/3

Module: state_space

Name: time_out_for_invariant/1

Module: state_space

Name: max_reached_for_node/1

Module: state_space

Name: max_reached_or_timeout_for_node/1

Module: state_space

Name: visited_expression/2

Module: state_space

Name: transition/4

Module: state_space

Name: visited_expression_id/1

Module: state_space

Name: set_context_state/2

Module: state_space

Name: clear_context_state/0

Module: state_space

Name: state_error/3

Module: state_space

Name: current_state_id/1

Module: state_space

Name: set_current_state_id/1

Module: state_space

Name: get_state_space_stats/3

Module: state_space

Name: try_set_trace_by_transition_ids/1

Module: state_space

Name: set_current_state_for_external_fun/1

Module: external_functions

Name: clear_state_for_external_fun/0

Module: external_functions

Name: announce_event/1

Module: eventhandling

Name: version/4

Module: version

Name: revision/1

Module: version

Name: lastchangeddate/1

Module: version

Name: b_get_preferences_from_specification/0

Module: pref_definitions

Name: b_get_preferences_from_specification/1

Module: pref_definitions

Name: conjunct_predicates/2

Module: bsyntaxtree

Name: get_texpr_type/2

Module: bsyntaxtree

Name: get_texpr_expr/2

Module: bsyntaxtree

Name: find_identifier_uses/3

Module: bsyntaxtree

Name: set_depth_breadth_first_mode/1

Module: state_space_exploration_modes

Name: b_type_expression/5

Module: bmachine

Name: b_get_machine_operation/4

Module: bmachine

Name: b_get_machine_operation/6

Module: bmachine

Name: b_type_open_predicate/5

Module: bmachine

Name: b_top_level_operation/1

Module: bmachine

Name: get_machine_operation_additional_identifiers/2

Module: bmachine

Name: b_load_machine_from_list_of_facts/2

Module: bmachine

Name: b_set_eventb_project_flat/3

Module: bmachine

Name: load_additional_information/1

Module: bmachine

Name: b_machine_precompile/0

Module: bmachine

Name: other_spec_precompile/0

Module: bmachine

Name: b_set_parsed_typed_machine_goal/1

Module: bmachine

Name: b_is_variable/2

Module: bmachine

Name: b_is_constant/1

Module: bmachine

Name: b_is_variable/1

Module: bmachine

Name: b_is_constant/2

Module: bmachine

Name: b_test_boolean_expression_cs/5

Module: b_interpreter

Name: b_compute_expression_nowf/6

Module: b_interpreter

Name: add_prob_deferred_set_elements_to_store/3

Module: b_global_sets

Name: user_interruptable_call_det/2

Module: user_signal/user_signal

Name: ignore_user_interrupt_det/1

Module: user_signal/user_signal

Name: maplist/2

Module: lists

Name: maplist/3

Module: lists

Name: maplist/4

Module: lists

Name: read_from_codes/2

Module: codesio

Name: write_term_to_codes/4

Module: codesio

Name: expand_const_and_vars_to_full_store/2

Module: specfile

Name: animation_mode/1

Module: specfile

Name: csp_mode/0

Module: specfile

Name: b_or_z_mode/0

Module: specfile

Name: xtl_mode/0

Module: specfile

Name: set_currently_opened_file/1

Module: specfile

Name: set_currently_opened_b_file/1

Module: specfile

Name: set_minor_animation_mode_from_file/1

Module: specfile

Name: set_currently_opening_file/1

Module: specfile

Name: set_failed_to_open_file/1

Module: specfile

Name: set_currently_opened_package/1

Module: specfile

Name: set_animation_mode/1

Module: specfile

Name: set_animation_minor_mode/1

Module: specfile

Name: with_translation_mode/2

Module: translate

Name: get_language_mode/1

Module: translate

Name: with_language_mode/2

Module: translate

Name: translate_bvalue_for_expression/3

Module: translate

Name: suppress_rodin_positions/1

Module: translate

Name: reset_suppress_rodin_positions/1

Module: translate

Name: translate_event/2

Module: translate

Name: translate_bstate/2

Module: translate

Name: translate_state_error/2

Module: translate

Name: translate_bexpression/2

Module: translate

Name: translate_bvalue_with_limit/3

Module: translate

Name: translate_event_error/2

Module: translate

Name: explain_event_trace/3

Module: translate

Name: explain_state_error/3

Module: translate

Name: add_error_and_fail/3

Module: error_manager

Name: get_all_errors_with_span_info_and_reset/1

Module: error_manager

Name: get_all_errors_with_span_and_context_and_reset/1

Module: error_manager

Name: add_error/3

Module: error_manager

Name: add_error/2

Module: error_manager

Name: add_message/2

Module: error_manager

Name: add_message/3

Module: error_manager

Name: reset_errors/0

Module: error_manager

Name: add_warning/3

Module: error_manager

Name: add_all_perrors/1

Module: error_manager

Name: no_real_perror_occurred/1

Module: error_manager

Name: get_error/2

Module: error_manager

Name: catch_enumeration_warning_exceptions/2

Module: error_manager

Name: real_error_occurred/0

Module: error_manager

Name: warning_occurred/0

Module: error_manager

Name: string_concatenate/3

Module: tools

Name: split_atom/3

Module: tools

Name: safe_atom_codes/2

Module: tools

Name: ajoin/2

Module: tools

Name: eclipse_preference/2

Module: preferences

Name: get_preference/2

Module: preferences

Name: preference_description/2

Module: preferences

Name: preference_val_type/2

Module: preferences

Name: preference_default_value/2

Module: preferences

Name: preference_category/2

Module: preferences

Name: set_preference/2

Module: preferences

Name: advanced_eclipse_preference/2

Module: preferences

Name: deprecated_eclipse_preference/4

Module: preferences

Name: obsolete_eclipse_preference/1

Module: preferences

Name: solve_predicate/5

Module: solver_interface

Name: call_with_smt_mode_enabled/1

Module: solver_interface

Name: parse_and_load_cspm_file/1

Module: haskell_csp

Name: debug_println/2

Module: debug

Name: get_user_signal_ref/1

Module: user_signal/user_signal

Name: get_total_number_of_errors/1

Module: error_manager

Name: b_set_typed_machine/2

Module: bmachine

Name: call_fuzz_parser/2

Module: parsercall

Name: open_xtl_file/1

Module: xtl_interface

Name: b_set_empty_machine/0

Module: bmachine

Name: load_alloy_model/2

Module: alloy2b/alloy2b

Name: get_id_of_node_and_add_if_required/6

Module: state_space_exploration_modes

Name: b_is_operation_name/1

Module: bmachine

Name: b_is_initialisation_name/1

Module: bmachine

Name: get_operation_name/2

Module: specfile

Name: is_concrete_constants_state_id/1

Module: state_space

Name: succeed_max_call_id/3

Module: succeed_max

Name: execute_operation_by_predicate_in_state/5

Module: b_state_model_check

Name: inline_prob_deferred_set_elements_into_bexpr/2

Module: b_global_sets

Name: assert_temp_typed_predicate/1

Module: bmachine

Name: reset_temp_predicate/0

Module: bmachine

Name: visited_state_corresponds_to_setup_constants_b_machine/1

Module: state_space

Name: visited_state_corresponds_to_initialised_b_machine/1

Module: state_space

Name: xtl_invariant_violated/1

Module: xtl_interface

Name: extract_span_description/2

Module: error_manager

Name: evaluate_parsed_csp_expression_with_timing/2

Module: haskell_csp

Name: extend_state_with_stored_lets/2

Module: eval_let_store

Name: b_is_variable/2

Module: bmachine

Name: b_is_constant/2

Module: bmachine

Name: b_type_expression_for_full_b_machine/6

Module: bmachine

Name: get_stored_let_typing_scope/1

Module: eval_let_store

Name: reset_let_values/0

Module: eval_let_store

Name: safe_time_out/3

Module: tools_meta

Name: catch_clpfd_overflow_call2/2

Module: clpfd_interface

Name: enter_new_error_scope/2

Module: error_manager

Name: exit_error_scope/3

Module: error_manager

Name: clear_all_errors_in_error_scope/1

Module: error_manager

Name: event_occurred_in_error_scope/1

Module: error_manager

Name: abort_error_occured_in_error_scope/0

Module: error_manager

Name: normalise_value_for_var/4

Module: store

Name: safe_create_texpr/4

Module: bsyntaxtree

Name: determine_type_of_formula/2

Module: bmachine

Name: catch_clpfd_overflow_call1/1

Module: clpfd_interface

Name: cbc_deadlock_freedom_check/3

Module: b_state_model_check

Name: cbc_find_redundant_invariants/2

Module: b_state_model_check

Name: b_set_up_valid_state_with_pred/4

Module: b_state_model_check

Name: get_state_for_b_formula/3

Module: specfile

Name: solver_pp_bvalue/4

Module: solver_interface

Name: solve_predicate_with_satsolver_free/4

Module: satsolver/b2sat

Name: solve_predicate_with_satsolver_in_state/4

Module: satsolver/b2sat

Name: temporary_set_preference/3

Module: preferences

Name: reset_temporary_preference/2

Module: preferences

Name: convert_cli_arg/2

Module: tools_strings

Name: get_possible_preferences_matches_msg/2

Module: tools_matching

Name: specfile_possible_trans_name_for_successors/2

Module: specfile

Name: prepare_state_for_specfile_trans/3

Module: specfile

Name: specfile_trans_or_partial_trans/7

Module: specfile

Name: throw_enumeration_warnings_in_current_scope/0

Module: error_manager

Name: add_internal_error/2

Module: error_manager

Name: error_occurred_in_error_scope/0

Module: error_manager

Name: safe_time_out/3

Module: tools_meta

Name: start_ms_timer/1

Module: tools

Name: stop_ms_walltimer_with_msg/2

Module: tools

Name: get_internal_representation/1

Module: specfile

Name: get_internal_representation/3

Module: specfile

Name: set_print_type_infos/1

Module: translate

Name: b_get_machine_operation/4

Module: bmachine

Name: b_get_machine_operation_for_animation/4

Module: bmachine

Name: b_get_initialisation_from_machine/2

Module: bmachine

Name: call_with_preference/3

Module: preferences

Name: channel/2

Module: haskell_csp

Name: get_texpr_id/2

Module: bsyntaxtree

Name: b_get_operation_non_det_modifies/2

Module: bmachine

Name: b_get_operation_normalized_read_write_info/3

Module: bmachine

Name: b_filenumber/4

Module: bmachine

Name: get_machine_identifiers/2

Module: bmachine

Name: get_machine_identifiers_with_pp_type/2

Module: bmachine

Name: get_cspm_identifier/2

Module: haskell_csp

Name: fuzzy_match_codes_lower_case/2

Module: tools_matching

Name: codes_to_lower_case/2

Module: tools_matching

Name: get_current_expr_keywords/1

Module: tools_matching

Name: get_current_keywords/1

Module: tools_matching

Name: get_all_svg_attributes/1

Module: tools_matching

Name: is_svg_color_name/1

Module: tools_matching

Name: get_all_dot_attributes/1

Module: tools_matching

Name: common_prefix_atom/2

Module: tools_lists

Name: ord_union/3

Module: ordsets

Name: get_latex_keywords/1

Module: translate

Name: get_latex_keywords_with_backslash/1

Module: translate

Name: ascii_to_unicode/2

Module: translate

Name: latex_to_unicode/2

Module: translate

Name: extended_static_check_machine/0

Module: bmachine_static_checks

Name: ensure_wd/2

Module: banditfuzz/welldef

Name: clean_up_pred/3

Module: b_ast_cleanup

Name: replay_json_trace_file/5

Module: b_intelligent_trace_replay

Name: initialise_specification/0

Name: get_version/7

Name: get_user_signal_reference/1

Name: get_prob_total_number_of_errors/1

Name: load_classical_b_from_list_of_facts/2

Name: update_preferences_from_spec/0

Name: update_preferences_from_spec/1

Name: load_event_b_project/4

Name: load_cspm_spec_from_cspm_file/1

Name: load_z_spec_from_fuzz_file/1

Name: load_z_spec_from_tex_file/1

Name: load_xtl_spec_from_prolog_file/1

Name: load_alloy_spec_from_term/2

Name: prob2_reset_prob/0

Name: reset_animator/0

Name: clear_animator/0

Name: start_animation/0

Name: serialize/2

Name: deserialize/2

Name: get_state/2

Name: get_b_state/2

Name: compute_operations_for_state/2

Name: prob2_execute_custom_operations/6

Name: get_op_from_id/4

Name: is_initialised_state/1

Name: is_initialised_b_state/1

Name: state_property/3

Name: op_timeout_occurred/2

Name: prob2_get_state_errors/2

Name: prob2_evaluate_formulas/3

Name: register_prob2_formulas/2

Name: unregister_prob2_formulas/1

Name: get_animation_image_list/1

Name: get_animation_image_matrix_for_state/6

Name: get_react_to_item_right_click_options_for_state/4

Name: react_to_item_right_click_option_for_state/6

Name: prob2_get_formula_type/3

Name: get_states_for_predicate/3

Name: filter_states_for_predicate/3

Name: get_top_level_formulas/1

Name: insert_formula_for_expansion/2

Name: prob2_evaluate_bvisual2_formulas/3

Name: prob2_evaluate_bvisual2_formulas/4

Name: prob2_expand_bvisual2_formula/3

Name: do_modelchecking/5

Name: set_goal_for_model_checking/1

Name: compute_efficient_statespace_stats/3

Name: compute_coverage/5

Name: get_modelchecking_coverage/5

Name: get_statistics/2

Name: prob2_deadlock_freedom_check/2

Name: prob2_invariant_check/2

Name: prob2_redundant_invariants/2

Name: get_enable_matrix/2

Name: prob2_do_ltl_modelcheck/3

Name: prob2_do_ltl_modelcheck/4

Name: prob2_do_ctl_modelcheck/4

Name: prob2_do_ctl_modelcheck/6

Name: find_trace_to_node/2

Name: find_trace_from_node_to_node/3

Name: find_state_for_predicate/3

Name: cbc_disprove/5

Name: cbc_disprove/6

Name: cbc_solve_with_opts/5

Name: cbc_timed_solve_with_opts/6

Name: pretty_print_predicate/3

Name: cbc_generate_test_cases/3

Name: prob2_find_test_path/4

Name: ast_leaf_walks/2

Name: check_csp_assertions/3

Name: list_eclipse_preferences/1

Name: list_all_eclipse_preferences/1

Name: list_current_eclipse_preferences/1

Name: get_eclipse_preference/2

Name: set_eclipse_preference/2

Name: get_signature_merge_state_space/2

Name: get_transition_diagram/2

Name: write_dotty_transition_diagram/2

Name: write_dotty_signature_merge/2

Name: write_dot_for_state_viz/2

Name: write_dotty_state_space/1

Name: is_dotty_command/1

Name: write_dotty/2

Name: is_dotty_command_for_expr/1

Name: write_dotty_for_expr/3

Name: get_dot_commands_in_state/2

Name: call_dot_command_in_state/4

Name: get_dot_commands_with_trace/2

Name: call_dot_command_with_trace/4

Name: get_plantuml_commands_in_state/2

Name: call_plantuml_command_in_state/4

Name: get_plantuml_commands_with_trace/2

Name: call_plantuml_command_with_trace/4

Name: get_table_commands_in_state/2

Name: call_table_command_in_state/4

Name: get_table_commands_with_trace/2

Name: call_table_command_with_trace/4

Name: get_error_messages_with_span_info/1

Name: generate_trace_until_condition_fulfilled/4

Name: execute_model/5

Name: execute_model/6

Name: get_unsat_core_with_fixed_conjuncts/3

Name: get_minimum_unsat_core_with_fixed_conjuncts/3

Name: prob2_construct_trace/6

Name: prob2_find_trace/5

Name: prob2_refine_trace/8

Name: symbolic_model_check/2

Name: start_synthesis_from_ui_/13

Name: start_synthesis_single_operation_from_ui_/11

Name: get_valid_and_invalid_equality_predicates_for_operation_/6

Name: get_valid_and_invalid_equality_predicates_for_invariants_/4

Name: get_invariant_violating_vars_from_examples_/3

Name: adapt_machine_code_for_operations_/2

Name: reset_synthesis_context_/0

Name: generate_data_from_machine_operation_/6

Name: generate_synthesis_data_from_predicate_untyped_/5

Name: generate_operation_data_from_machine_path_/4

Name: get_pretty_print/1

Name: get_pretty_print_unicode/1

Name: get_machine_internal_representation/2

Name: get_operations_and_names/2

Name: get_primed_predicate/2

Name: get_nonquantifying_primed_predicate/2

Name: get_weakest_precondition/3

Name: before_after_predicate/2

Name: get_machine_operation_names/1

Name: get_machine_operation_infos/1

Name: get_machine_operation_infos_typed/1

Name: get_machine_identifiers/2

Name: get_machine_files/1

Name: get_possible_completions/3

Name: get_possible_completion/3

Name: get_possible_fuzzy_matches/2

Name: prob2_extended_static_check/1

Name: prob2_check_well_definedness/2

Name: prob2_ensure_wd/2

Name: prob2_load_visb_file/1

Name: prob2_get_loaded_visb_file/1

Name: prob2_visb_file_loaded/2

Name: prob2_visb_attributes_for_state/2

Name: prob2_visb_click_events_and_hovers/2

Name: prob2_visb_perform_click/4

Name: prob2_visb_items/1

Name: prob2_visb_svg_objects/1

Name: prob2_visb_default_svg_file_contents/1

Name: prob2_read_visb_path_from_definitions/1

Name: prob2_export_visb_html_for_history/2

Name: prob2_export_visb_html_for_history/3

Name: prob2_export_visb_for_current_state/1

Name: prob2_export_visb_html_for_states/3

Name: prob2_get_visb_html_for_states/3

Name: prob2_replay_json_trace_file/4

Name: get_constants_predicate/1

Name: replay_state_trace_from_file/3

Predicates

Predicates:

adapt_machine_code_for_operations_/2

add_artificial_transition/5

add_id_type_kind/3

add_unknown_preference_error_and_fail/2

apply_refinement_variants/5

ast_leaf_walks/2

b_get_machine_op_for_anim_with_otype/5

b_is_op_or_init/1

before_after_predicate/2

before_after_predicate_aux/2

build_modelcheck_return/2

build_modelcheck_return2/2

bvisual2_formula_attribute/3

bvisual2_formula_children_attribute/3

call_dot_command_for_dotfile/3

call_dot_command_in_state/4

call_dot_command_with_trace/4

call_plantuml_command_for_pumlfile/3

call_plantuml_command_in_state/4

call_plantuml_command_with_trace/4

call_table_command_in_state/4

call_table_command_with_trace/4

category_pattern/2

cbc_disprove/5

cbc_disprove/6

cbc_generate_test_cases/3

cbc_solve_with_opts/5

cbc_timed_solve_with_opts/6

check_cbc_solve_opts/1

check_csp_assertion/3

check_csp_assertions/3

clean_targets/3

clear_animator/0

cli_trans_aux/7

completion_add_backquotes_if_required/2

compute_coverage/5

compute_efficient_statespace_stats/3

compute_enable_matrix_entry/3

compute_operations_for_state/2

create_simple_op_terms/3

create_traces/4

csp_channel_or_start/1

eval_predicate2_fail_result/2

evaluate_csp_expression_aux/2

evaluate_csp_expression_string/2

evaluate_expression/4

evaluate_formula_eval/5

evaluate_formula_in_state/8

evaluate_formula_in_state_aux/8

evaluate_typechecked_b_formula_in_state/5

evaluate_typechecked_b_formula_in_state/7

execute_model/5

execute_model/6

execute_model_steps/7

execute_nr_of_custom_operations/7

execute_until_disabled/6

execute_until_disabled/7

expand_bvisual2_formula_internal/3

expression_typecheck_for_eval/2

expression_typecheck_for_eval/3

expression_typecheck_for_eval/5

extract_b_op/4

extract_b_op_infos/4

extract_csp_name_and_args/3

filter_states_for_predicate/3

filter_states_for_typed_predicate/3

find_eclipse_preference/2

find_new_ids/2

find_path/8

find_state_for_predicate/3

find_state_for_predicate1/3

find_trace/7

find_trace1/6

find_trace_aux/9

find_trace_from_node_to_node/3

find_trace_iterator/7

find_trace_to_node/2

formula_typecheck2_for_eval/5

formula_typecheck_for_eval/4

gen_exec_error_message/4

gen_op_triples/3

generate_data_from_machine_operation_/6

generate_operation_data_from_machine_path_/4

generate_synthesis_data_from_predicate_untyped_/5

generate_trace_until_condition_fulfilled/4

get_all_spec_identifiers/1

get_all_special_categories/1

get_animation_image_list/1

get_animation_image_matrix_for_state/6

get_b_state/2

get_bstate_with_deferred_sets/5

get_commands_in_state/3

get_commands_with_trace/3

get_constants_id/3

get_constants_predicate/1

get_constants_type/2

get_dot_commands_in_state/2

get_dot_commands_with_trace/2

get_eclipse_preference/2

get_eclipse_preference_infos/5

get_enable_matrix/2

get_error_messages_with_span_and_contxt/1

get_error_messages_with_span_info/1

get_eval_scope/1

get_eval_scope/2

get_eval_scope_with_opts/2

get_invariant_violating_vars_from_examples_/3

get_libraries/2

get_machine_files/1

get_machine_internal_representation/2

get_machine_operation_infos/1

get_machine_operation_infos_typed/1

get_machine_operation_names/1

get_main_eval_scope/1

get_match_ids/2

get_match_ids2/3

get_minimum_unsat_core_with_fixed_conjuncts/3

get_modelchecking_coverage/5

get_nonquantifying_primed_predicate/2

get_nonquantifying_primed_predicate_2/2

get_op_from_id/4

get_operations_and_names/2

get_plantuml_commands_in_state/2

get_plantuml_commands_with_trace/2

get_possible_completion/3

get_possible_completions/3

get_possible_fuzzy_matches/2

get_pretty_print/1

get_pretty_print_unicode/1

get_primed_predicate/2

get_prob_total_number_of_errors/1

get_react_to_item_right_click_options_for_state/4

get_signature_merge_state_space/2

get_spec_identifiers2/1

get_state/2

get_state/4

get_state2/3

get_state_for_predicate/2

get_states_for_predicate/3

get_statistics/2

get_table_commands_in_state/2

get_table_commands_with_trace/2

get_top_level_formulas/1

get_transition_diagram/2

get_unknown_error_result/1

get_unsat_core_with_fixed_conjuncts/3

get_user_signal_reference/1

get_valid_and_invalid_equality_predicates_for_invariants_/4

get_valid_and_invalid_equality_predicates_for_operation_/6

get_variable_type/2

get_version/7

get_weakest_precondition/3

get_weakest_precondition_aux/3

ignore_type/2

initialise_specification/0

insert_formula_for_expansion/2

inv_timeout_occurred/1

invariantKO/1

is_a_command/7

is_constants_set_up_state/1

is_dotty_command/1

is_dotty_command_for_expr/1

is_initialised_b_state/1

is_initialised_state/1

is_special_op/2

is_universal_quantifier/4

limit_for_pretty_print/2

list_all_eclipse_preferences/1

list_current_eclipse_preferences/1

list_eclipse_preferences/1

load_alloy_spec_from_term/2

load_classical_b_from_list_of_facts/2

load_cspm_spec_from_cspm_file/1

load_event_b_project/4

load_fuzz_file_internal/1

load_xtl_spec_from_prolog_file/1

load_z_spec_from_fuzz_file/1

load_z_spec_from_tex_file/1

longest_match/3

match/3

max_operations_reached/1

op_id/1

op_timeout_occurred/2

option_set/3

options_to_translation_mode/2

predicate_typecheck_for_eval/2

predicate_typecheck_for_eval/3

predicate_typecheck_for_eval/5

pretty_print_bvalue/3

pretty_print_predicate/3

prettyprint_solutions/3

prob2_check_well_definedness/2

prob2_construct_trace/6

prob2_deadlock_freedom_check/2

prob2_deadlock_freedom_check1/2

prob2_deadlock_freedom_check2/2

prob2_do_ctl_modelcheck/4

prob2_do_ctl_modelcheck/6

prob2_do_ltl_modelcheck/3

prob2_do_ltl_modelcheck/4

prob2_ensure_wd/2

prob2_evaluate_bvisual2_formulas/3

prob2_evaluate_bvisual2_formulas/4

prob2_evaluate_formulas/3

prob2_exec_custom_aux/4

prob2_exec_custom_pred_aux/5

prob2_execute_custom_operation/4

prob2_execute_custom_operation_with_predicate/5

prob2_execute_custom_operation_with_predicate_aux/5

prob2_execute_custom_operations/6

prob2_execute_custom_operations_aux/6

prob2_expand_bvisual2_formula/3

prob2_export_visb_for_current_state/1

prob2_export_visb_html_for_history/2

prob2_export_visb_html_for_history/3

prob2_export_visb_html_for_states/3

prob2_extended_static_check/1

prob2_find_test_path/4

prob2_find_test_path_aux/4

prob2_find_trace/5

prob2_get_formula_type/3

prob2_get_loaded_visb_file/1

prob2_get_state_errors/2

prob2_get_visb_html_for_states/3

prob2_invariant_check/2

prob2_invariant_check2/2

prob2_invariant_check3/3

prob2_invariant_check_for_single_op/3

prob2_load_visb_file/1

prob2_ltl_adapt_ce/2

prob2_ltl_adapt_ce2/3

prob2_ltl_adapt_operations/2

prob2_read_visb_path_from_definitions/1

prob2_redundant_invariants/2

prob2_refine_trace/8

prob2_replay_json_trace_file/4

prob2_reset_prob/0

prob2_visb_attributes_for_state/2

prob2_visb_click_events_and_hovers/2

prob2_visb_default_svg_file_contents/1

prob2_visb_file_loaded/2

prob2_visb_items/1

prob2_visb_perform_click/4

prob2_visb_svg_objects/1

raw_equals/2

raw_truth/1

react_to_item_right_click_option_for_state/6

recognised_smt_solver/2

refine_trace_main_loop/8

refine_trace_start_kick_off/8

refine_trace_step/12

register_prob2_formula1/3

register_prob2_formulas/2

replay_state_trace_from_file/3

requirements_met/2

reset_animator/0

reset_synthesis_context_/0

set_default_eval_opts/1

set_default_pp_opts/1

set_eclipse_preference/2

set_goal_for_model_checking/1

solve_free_aux/3

solve_in_state_aux/4

solve_in_state_sat_aux/4

special_id_match_pattern/3

start_animation/0

start_synthesis_from_ui_/13

start_synthesis_single_operation_from_ui_/11

state_property/3

state_property2/2

strip_ID/2

symbolic_model_check/2

take_best/2

test_bool_exists/4

timed_solve_predicate/6

timeout_occurred/1

trace_to_op_terms/3

translate_cbc_cdclt_result/2

typecheck_pred_for_unsat_core/2

unpack_operation/2

unpack_operation_aux/2

unregister_prob2_formula/1

unregister_prob2_formulas/1

update_preferences_from_spec/0

update_preferences_from_spec/1

valid_op_name/1

write_dot_for_state_viz/2

write_dotty/2

write_dotty_for_expr/3

write_dotty_signature_merge/2

write_dotty_state_space/1

write_dotty_transition_diagram/2

adapt_machine_code_for_operations_/2

add_artificial_transition/5

Description:
add_artificial_transition(+SrcId,+Operation,+DstState,+DstId,-TransitionTuple)

creates a helper transition that is artificially added to the state space (e.g. during deadlock checking)
This transition is added to the state space.
A triple TransitionTuple in the form op(TransId,OpName,SrcId,DstId) for this transition is generated.

add_id_type_kind/3

add_unknown_preference_error_and_fail/2

apply_refinement_variants/5

Description:
We want to catch all possiblities, we do not care for an failing option

ast_leaf_walks/2

b_get_machine_op_for_anim_with_otype/5

b_is_op_or_init/1

before_after_predicate/2

before_after_predicate_aux/2

build_modelcheck_return/2

Description:
build_modelcheck_return(+MCRes, -JavaResult)

build_modelcheck_return2/2

bvisual2_formula_attribute/3

bvisual2_formula_children_attribute/3

call_dot_command_for_dotfile/3

call_dot_command_in_state/4

call_dot_command_with_trace/4

call_plantuml_command_for_pumlfile/3

call_plantuml_command_in_state/4

call_plantuml_command_with_trace/4

call_table_command_in_state/4

call_table_command_with_trace/4

category_pattern/2

cbc_disprove/5

Description:
cbc_disprove(+Goal,+AllHypotheses,+SelectedHypotheses,+TimeoutFactor,-OutResult)

#### called by:
ProB Plugin (de.prob.eventb.disprover.core): DisproverCommand

cbc_disprove/6

Description:
cbc_disprove(+Goal,+AllHypotheses,+SelectedHypotheses,+TimeoutFactor,-OutResult)

the same with explicit Options:

cbc_generate_test_cases/3

cbc_solve_with_opts/5

Description:
cbc_solve_with_opts(+Solver,+Options,+Predicate,-Identifiers,-Result)

cbc_timed_solve_with_opts/6

check_cbc_solve_opts/1

check_csp_assertion/3

check_csp_assertions/3

Description:
check_csp_assertions(+Assertions,-Results,-ResultTraces)

Takes a list of assertions and produce a list of results and result traces.

TODO: We should modify the result traces so that they are useful for ProB 2.0. (or at least document what the result traces mean)

#### called by:
ProB 2.0: CSPAssertionsCommand

clean_targets/3

clear_animator/0

cli_trans_aux/7

completion_add_backquotes_if_required/2

compute_coverage/5

Description:
compute_coverage(-TotalNodeNr,-TotalTransSum,-NodeStat,-OpStat,-Uncovered)

compute_efficient_statespace_stats/3

Description:
compute_efficient_statespace_stats(-NrNodes, -NrTrans, -NrProcessed)

Computes the coverage statistics of the current state space at any given time.
The information of interest includes the total number of nodes and transitions, as well as
a list of statistics about the nodes and operations and a list of the operations that have been uncovered sofar.

#### called by:
ProB Plugin: ComputeCoverageCommand
* ProB 2.0: ComputeCoverageCommand

compute_enable_matrix_entry/3

compute_operations_for_state/2

Description:
compute_operations_for_state(+StateID,-Transitions)

Compute the enabled operations (without the backtrack options) for a given state id.
Transitions is a list of operation tuples with the form op(TransitionId, Name,SrcId,DestId)

#### called by:
ProB 2.0: GetEnabledOperationsCommand

Description:
create_op_tuple(+OpTerm, +PPOpts, -Params, -RetVals)

Creates an operation tuple from transition id, source id, an op term, and a destination id.
If creation is unsuccessful, an error is added and the predicate fails.
See comment for extract_op_tuple for a description of OpTuple

create_simple_op_terms/3

create_traces/4

csp_channel_or_start/1

default_eval_opts/1

deserialize/2

Description:
deserialize(-NewId,+SerializedState)

Deserialize a state and add it if necessary

#### called by:
ProB 2.0: DeserializeStateCommand

do_modelchecking/5

Description:
do_modelchecking(+MaxNumberOfStatesToCheck,+Time,+Options,-Result,-Stats)

#### do_modelchecking(+MaxNumberOfStatesToCheck, +Time,+Options,-Result,stats(-NrNodes,-NrTrans,-NrProcessed))
+MaxNumberOfStatesToCheck : maximum number of states to be checked
* +Time : Timeout specified by the user in ms
* +Options : List of options specified by the user. Used for predicate do_modelchecking(Time,Options,Result)
* -NrNodes : total number of nodes in state space. Calculated with get_state_space_stats
* -NrTrans : total number of nodes in state space. Calculated with get_state_space_stats
* -NrProcessed : total number of calculated nodes in state space. Calculated with get_state_space_stats
When Time Milliseconds have elapsed the modelchecker should stop after its next step

#### called by:
* ProB Plugin: ModelCheckingCommand
* ProB 2.0: ModelCheckingStepCommand

eval_predicate/4

eval_predicate2/4

eval_predicate2_fail_result/2

evaluate_csp_expression_aux/2

evaluate_csp_expression_string/2

evaluate_expression/4

evaluate_formula_eval/5

evaluate_formula_in_state/8

evaluate_formula_in_state_aux/8

evaluate_typechecked_b_formula_in_state/5

evaluate_typechecked_b_formula_in_state/7

execute_model/5

Description:
execute_model(+CurStateID,+MaxNrSteps,-TransitionInfo,-ExecutedSteps,-Result)

an execution engine with minimal overhead: states are not stored in visited_expression database, only first enabled operation is taken

execute_model/6

Description:
execute_model(+CurStateID,+MaxNrSteps,+Options,-TransitionInfo,-ExecutedSteps,-Result)

Options can contain continue_after_errors, timeout(MS)
Result is either maximum_nr_of_steps_reached, deadlock, error, internal_error, time_out

execute_model_steps/7

execute_nr_of_custom_operations/7

execute_until_disabled/6

execute_until_disabled/7

expand_bvisual2_formula_internal/3

expression_typecheck_for_eval/2

expression_typecheck_for_eval/3

expression_typecheck_for_eval/5

extract_b_op/4

Description:
extract_b_op(+OpTerm, +PPOpts, -Params, -RetVals)

Extracts information for a B operation.

extract_b_op_infos/4

Description:
extract_b_op_infos(+Term, -Name, -Arguments, -RetVals)

extract_csp_name_and_args/3

Description:
extract_csp_name_and_args(+OpTerm, -Name, -Args)

extract_csp_op/3

Description:
extract_csp_op(+OpTerm, -Params, -RetVals)

Extracts information for a CSP operation.

extract_node_info/5

Description:
extract_node_info(+NodeId,-Count,-Color,+LabelGenerator,-Labels)

Generates information about the nodes found during state space reduction

#### Generated Information:
Count - number of concrete states combined in the abstract state
* Color - the color used to represent this state type in a visualization
* Labels - determine the labels that should appear on a node in a visualization

extract_op_name/2

extract_op_tuple/4

Description:
extract_op_tuple(+OpTerm, +PPOpts, -Params, -RetVals)

Extracts the parameters and return values of the operations

extract_opid/2

extract_result/6

extract_trans_info/7

Description:
extract_trans_info(+ShowSelfLoops,+TransId,-Src,-Dest,-Label,-Style,-Color)

Generates information about the transitions created during state space reduction

#### Generated Information:
Src - ID corresponding to the abstract state that is the source of the abstract transition with TransId
* Dest - ID corresponding to the abstract state that is the destination of the abstract transition with TransId
* Label - the label that should appear on a transition in a visualization
* Style - the style that should be applied to a transition of this type in a visualization (e.g. dashed)
* Color - the color used to represent a transition of this type in a visualization

filter_states_for_predicate/3

Description:
filter_states_for_predicate(+Raw,+States,-Filtered)

Takes a list of state ids and a predicate and finds all of the states
for which the predicate is true

#### called by:
ProB 2.0: FilterStatesForPredicateCommand

filter_states_for_typed_predicate/3

find_eclipse_preference/2

find_new_ids/2

find_path/8

find_state_for_predicate/3

Description:
Takes a given predicate and finds a state in the state space that satisfies the predicate.
A helper transition is then added to go to the goal state.

#### called by:
ProB 2.0: FindValidStateCommand

find_state_for_predicate1/3

find_trace/7

Description:
No transitions found -> return with the current state
Start a new exploration path for each solution

find_trace1/6

find_trace_aux/9

find_trace_from_node_to_node/3

Description:
find_trace_from_node_to_node(+FromId,+ToId,-Trace)

Finds a trace from one state to a goal state in the current state space.

#### Parameters:
FromId - Id of source node
* ToId - Id of destination node
* Trace - List of op tuples op(OpId,SrcId,DestId) corresponding to the trace calculated by ProB or atom no_trace_found if the call was unsuccessful

#### called by:
* ProB 2.0: GetShortestTraceCommand

find_trace_iterator/7

find_trace_to_node/2

Description:
find_trace_to_node(+StateId,-Trace)

Finds a trace from the root state to the specified state in the current state space.

#### Parameters:
StateId
* Trace - List of op tuples op(OpId,SrcId,DestId) corresponding to the trace calculated by ProB or atom no_trace_found if the call was unsuccessful

#### called by:
* ProB 2.0: GetShortestTraceCommand

formula_typecheck2_for_eval/5

Description:
formula_typecheck2_for_eval(+PredOrExpr,+EvalOpts,?Machine,+RawFormula,-TypedFormula,-Type,-Errors)

formula_typecheck_for_eval/4

gen_exec_error_message/4

gen_op_triples/3

generate_data_from_machine_operation_/6

generate_operation_data_from_machine_path_/4

generate_synthesis_data_from_predicate_untyped_/5

generate_trace_until_condition_fulfilled/4

Description:
generate_trace_until_condition_fulfilled(+CurState,+Condition,-Trace,-Result)

Animates randomly number of steps until a certain (LTL?) condition is fulfilled.

#### Called by:
ProB 2.0: ExecuteUntilCommand

#### Arguments
* CurState - the ID of the current state
* Condition - a condition that should be satisfied at some point (this come as parsed term from the ProB2)

#### Generated Information:
* Trace - a list of triples representing a trace in the state space of the model being analysed
* Result - the result found: ltl_found, typeerror, max_nr_of_steps_reached, deadlock

get_all_spec_identifiers/1

get_all_special_categories/1

get_animation_image_list/1

get_animation_image_matrix_for_state/6

get_b_state/2

Description:
Get the predicate representation of a BState

#### called by:
ProB 2.0: GetBStateCommand

get_bstate_with_deferred_sets/5

get_commands_in_state/3

get_commands_with_trace/3

get_constants_id/3

get_constants_predicate/1

get_constants_type/2

Description:
note exclude return the elements where the predicate is not succesful

get_dot_commands_in_state/2

get_dot_commands_with_trace/2

get_eclipse_preference/2

Description:
Returns the current value of a specified preference.

#### called by:
ProB 2.0: GetPreferenceCommand

get_eclipse_preference_infos/5

get_enable_matrix/2

Description:
computes the enabling relation information for the provided operations of interest
get_enable_matrix(-PairsOfOperations,+EnableResult)
PairsOfOperations: list of pair(Op1,Op2) of operations pairs for which the enable relation is to be computed
EnableResult: list of terms enable_edges(Op1,Op2,enable_edges(E,KE,D,KD)) of same length

get_error_messages_with_span_and_contxt/1

get_error_messages_with_span_info/1

Description:
get_error_messages_with_span_info(-ListOfErrMsgTerms)

each error is of the form: error(ErrMsg,ErrType,ErrLocations)
ErrMsg is an atom (aka string)
ErrType is warning, internal_error or error
ErrLocations is a list of terms error_span(Filename,StartLine,StartCol,EndLine,EndCol)
Note: Filename is '' when not known

#### called by:
ProB 2.0: GetErrorItemsCommand

get_eval_scope/1

get_eval_scope/2

get_eval_scope_with_opts/2

get_invariant_violating_vars_from_examples_/3

get_libraries/2

get_machine_files/1

get_machine_internal_representation/2

Description:
Pretty-print the machine's internal representation in B syntax.

#### called by:
ProB 2.0: GetInternalRepresentationCommand

get_machine_operation_infos/1

get_machine_operation_infos_typed/1

Description:
Same as untyped

get_machine_operation_infos_typed(MachineOperationInfos) :- b_or_z_mode,!,
    % TODO: ensure that we do not need to consider preference(show_eventb_any_arguments,EVENTB)
    % TODO: examine what happens for CSP||B
    findall(operation_info(Name,ResultNames,ParameterNames,TopLevel,OTypeF,Read,Modified,NonDetModifies, TypeMap),
    (b_get_machine_op_for_anim_with_otype(Name, Results, AnimParameters,_, OType),

    maplist(get_texpr_id,Results,ResultNames),
    maplist(get_texpr_type, Results,ResultTypes),
    keys_and_values(ResultMap, ResultNames, ResultTypes),
    maplist(get_texpr_id,AnimParameters,ParameterNames),
    maplist(get_texpr_type, AnimParameters,ParameterTypes),
    keys_and_values(ParameterMap, ParameterNames, ParameterTypes),

    functor(OType,OTypeF,_),
    % TO DO: obtain machine file or machine name
    (b_top_level_operation(Name) -> TopLevel = true ; TopLevel=false),
    (b_get_operation_normalized_read_write_info(Name,OpRead,Modified)
    -> exclude(op_id,OpRead,Read),
    get_constants_type(OpRead, ConstReadType),
    get_variable_type(OpRead, VarReadType), % TO DO: ids appear multiple times in TypeMap if read and written
    get_variable_type(Modified, ModifiedType),
    append([ConstReadType, VarReadType, ModifiedType], VarMap)
    % exclude query operations called in expressions (allow_operation_calls_in_expr);
    %ProB2 Java cannot deal with it and raises exception for non-atomic identifiers
    ; Read=unknown,Modified=unknown,
    VarMap = []
    ),
    (b_get_operation_non_det_modifies(Name,NonDetModifies)
    -> maplist(b_is_variable, NonDetModifies, NonDetModifiesType),
    keys_and_values(NonDetModifiedMap, NonDetModifies, NonDetModifiesType)
    ; NonDetModifies=unknown,
    NonDetModifiedMap = []
    ),
    append([ResultMap, ParameterMap, VarMap, NonDetModifiedMap], TypeMap)
    ),
    MachineOperationInfos).

get_machine_operation_infos_typed(ChannelInfos) :- csp_mode,!,
    findall(operation_info(Name,[],[],true,csp,[],[],[],[]), csp_channel_or_start(Name),ChannelInfos).

get_machine_operation_infos_typed([]).

get_machine_operation_names/1

get_main_eval_scope/1

get_match_ids/2

get_match_ids2/3

get_minimum_unsat_core_with_fixed_conjuncts/3

get_modelchecking_coverage/5

get_nonquantifying_primed_predicate/2

get_nonquantifying_primed_predicate_2/2

get_op_from_id/4

Description:
get_op_from_id(+Id,+Options,-Params,-RetVals)

Extracts information about the parameters and return values for the
specified transition.

#### called by:
ProB 2.0: GetOpFromId

get_operations_and_names/2

get_plantuml_commands_in_state/2

get_plantuml_commands_with_trace/2

get_possible_completion/3

get_possible_completions/3

get_possible_fuzzy_matches/2

get_pretty_print/1

Description:
Access information about the current version of the ProB core.

#### called by:
ProB 2.0: GetInternalRepresentationPrettyPrintCommand

get_pretty_print_unicode/1

get_primed_predicate/2

get_prob_total_number_of_errors/1

get_react_to_item_right_click_options_for_state/4

get_signature_merge_state_space/2

Description:
get_signature_merge_state_space(+IgnoredEvents,-Space)

Takes a list of ignored events, and applies the signature merge algorithm
from module `state_space_reduction` to the current state space.

#### called by:
ProB 2.0: ApplySignatureMergeCommand

get_spec_identifiers2/1

get_state/2

get_state/4

get_state2/3

get_state_for_predicate/2

get_states_for_predicate/3

Description:
get_states_for_predicate(+Raw,-States,-Errors)

Takes a predicate and finds a list of all state ids for which the
predicate holds. The states that are not intitialized (i.e. root) are
included in the list. The list that is returned is therefore the union
of the uninitialised states and the states for which the predicate holds.

#### called by:
ProB 2.0: GetStatesFromPredicate

get_statistics/2

Description:
get_statistics(+Option,-Value)

Takes an option for the statistics and returns the corresponding value.

#### called by:
ProB 2.0: GetStatisticsCommand

get_table_commands_in_state/2

get_table_commands_with_trace/2

get_top_level_formulas/1

Description:
get_top_level_formulas(-TopIds)

Gets all top-level formula IDs from bvisual2.

#### called by:
ProB 2.0: GetTopLevelFormulasCommand

get_transition_diagram/2

Description:
get_transition_diagram(+ParsedExpr,-Space)

Takes a list of ignored events, and calculates a transition diagram
using module `state_space_reduction` for the current state space.

#### called by:
ProB 2.0: CalculateTransitionDiagramCommand

get_unknown_error_result/1

get_unsat_core_with_fixed_conjuncts/3

get_user_signal_reference/1

get_valid_and_invalid_equality_predicates_for_invariants_/4

get_valid_and_invalid_equality_predicates_for_operation_/6

get_variable_type/2

get_version/7

Description:
Access information about the current version of the ProB core.

#### called by:
ProB 2.0: GetVersionCommand

get_weakest_precondition/3

get_weakest_precondition_aux/3

ignore_type/2

initialise_specification/0

insert_formula_for_expansion/2

Description:
insert_formula_for_expansion(+AST,-Id)

Inserts a formula into bvisual2 module
The formula is inserted as a child of level "user" in bvisual2

#### called by:
ProB 2.0: InsertFormulaForVisualizationCommand

inv_timeout_occurred/1

invariantKO/1

is_a_command/7

is_constants_set_up_state/1

is_dotty_command/1

is_dotty_command_for_expr/1

is_initialised_b_state/1

is_initialised_state/1

is_special_op/2

is_universal_quantifier/4

limit_for_pretty_print/2

list_all_eclipse_preferences/1

Description:
list_all_eclipse_preferences(-L)

also includes advanced eclipse preferences

list_current_eclipse_preferences/1

Description:
list_current_eclipse_preferences(-L)

Returns a list of all the preferences with their current values

#### called by:
ProB 2.0: GetCurrentPreferencesCommand

list_eclipse_preferences/1

Description:
list_eclipse_preferences(-L)

Returns a list of all normal eclipse preferences as well as their information
(i.e. type, description, category, and default value)

#### called by:
ProB Plugin: GetPreferencesCommand
* ProB 2.0: GetDefaultPreferencesCommand

load_alloy_spec_from_term/2

load_classical_b_from_list_of_facts/2

Description:
load_classical_b_from_list_of_facts(+MainFilename,+ListOfFacts)

Loads a classical b model.

#### called by:
ProB 2.0: LoadBProjectCommand

load_cspm_spec_from_cspm_file/1

Description:
load_cspm_spec_from_cspm_file(+CSPMFile)

Takes a path to a CSPM specification and loads the file using the CSPM parser.

#### called by:
ProB 2.0: LoadCSPCommand

load_event_b_project/4

Description:
Loads an Event-B model.

#### called by:
ProB Plugin: de.prob.eventb.translator.internal.EventBTranslator, DisproverLoadCommand
* ProB 2.0: de.prob.model.eventb.translate.EventBModelTranslator (LoadEventBProjectCommand)

load_fuzz_file_internal/1

load_xtl_spec_from_prolog_file/1

load_z_spec_from_fuzz_file/1

load_z_spec_from_tex_file/1

longest_match/3

match/3

max_operations_reached/1

op_id/1

op_timeout_occurred/2

Description:
Takes a state id and finds all of the operations for which a timeout occurred

#### called by:
ProB Plugin: GetTimeoutedOperationsCommand
* ProB 2.0: GetOperationsWithTimeout

option_set/3

Description:
option_set(+Element, +List, -Result)

Takes an atom and unifies Result with 1 if the atom is in the List.
Otherwise, Result is unified with 0.

options_to_translation_mode/2

pack_as_list/2

parse_eval_opts/3

Description:
parse_eval_opts(-EvalOpts, +Options, -Options0)

Supported options:
state(StateId): state in which to evaluate the formulas
* provide_stored_let_values: make stored let values visible to the formulas (see eval_let_store module)
* eval_expand(EvalExpand): any of the expand modes supported by store:normalise_value_for_var/4
* timeout(TimeoutMs): per-formula evaluation timeout in milliseconds

parse_pp_opts/3

Description:
parse_pp_opts(-PPOpts, +Options, -Options0)

Supported options:
truncate(Truncate): either truncate or expand - controls whether result strings are truncated
* translation_mode(TransMode): any of the modes supported by set_translation_mode/1
* language(Language): any of the languages supported by set_language_mode/1

pick_action/5

predicate_typecheck_for_eval/2

predicate_typecheck_for_eval/3

predicate_typecheck_for_eval/5

pretty_print_bvalue/3

pretty_print_predicate/3

Description:
Takes a predicates and generates a pretty printed string

prettyprint_solutions/3

Description:
This cycles through all of the solutions and extracts the string
representation of the solutions.

prob2_check_well_definedness/2

Description:
prob2_check_well_definedness(-NrDischarged,-NrTotal)

prob2_construct_trace/6

Description:
Calculates a trace given a list of operation names and a list of guards.
In case of errors, a partial trace is generated that jumps over the errornous operation / event.
In addition, a list of integers should be given as argument that make possible to execute some
operations in the oprations list multiple times or as long as they are disabled (in this case one should give -1).
E.g. by calling prob2_construct_trace(0,[e1,e2,e3],[TRUE,TRUE,TRUE],[2,1,-1],OpsOut,ErrOut) the predicate calculates
a trace starting at the state with the ID 0 where e1 is executed sequentially 2 times, after that e2 once,
and finally e3 until it becomes disabled.

#### called by:
ProB 2.0: ConstructTraceCommand

prob2_deadlock_freedom_check/2

Description:
prob2_deadlock_freedom_check(+Predicate,-Result)

Performs deadlock freedom checking with constraint Predicate and calulates the Result.

#### called by:
ProB 2.0: ConstraintBasedDeadlockCheckCommand

prob2_deadlock_freedom_check1/2

prob2_deadlock_freedom_check2/2

prob2_do_ctl_modelcheck/4

Description:
prob2_do_ctl_modelcheck(+Formula, +Options, -Result, -CE)

Performs an CTL model checking step.

Supported options:
max_new_states(Max) - maximum number of new states that will be explored, or -1 (the default) for no limit
* mode(Mode) - init (the default) to check starting from every initialized state, or specific_node(StateID) to check starting from one specific state

#### called by:
* ProB 2.0: CtlCheckingCommand

prob2_do_ctl_modelcheck/6

prob2_do_ltl_modelcheck/3

Description:
prob2_do_ltl_modelcheck(+Formula,+Options,-Result)

Performs an LTL model checking step.

Supported options:
max_new_states(Max) - maximum number of new states that will be explored, or -1 (the default) for no limit
* mode(Mode) - init (the default) to check starting from every initialized state, or specific_node(StateID) to check starting from one specific state

#### called by:
* ProB 2.0: LtlCheckingCommand

prob2_do_ltl_modelcheck/4

prob2_ensure_wd/2

prob2_evaluate_bvisual2_formulas/3

Description:
prob2_evaluate_bvisual2_formulas(+Ids,+StateId,-Values)

Uses the bvisual2 module to evaluate the given formulas.
Unlike expand_formula_nonrecursive/6, this predicate only evaluates the formulas,
but doesn't return their label, description, or subformulas.

#### called by:
ProB 2.0: EvaluateBVisual2FormulasCommand

prob2_evaluate_bvisual2_formulas/4

Description:
prob2_evaluate_bvisual2_formulas(+Ids,+StateId,+Options,-Values)

New version of the above predicate which also supports options.
Currently supported options:
- unlimited: does not truncate terms

prob2_evaluate_formulas/3

Description:
prob2_evaluate_formulas(+Formulas, +Options, -Results)

Evaluate a list of formulas.
This is more efficient than evaluating each formula individually,
because some calculations (e. g. expanding the current state) don't have to be repeated for each formula.

Supported formula types:
bpred(Raw)
* bexpr(Raw)
* csp(TermCodes)

Supported options:
* all options supported by parse_eval_opts/3
* all options supported by parse_pp_opts/3

Possible results:
* result(Value,Solutions,Errors): evaluation succeeded
* Value: String rep of the value calculated by ProB
* Solutions: List of solutions as a triple: bind(Name,PPSol)
* Name: Free variable from formula
* PPSol: String representation of the solution bound to the name
* Errors: List of error/3 terms for non-fatal errors (warnings or messages) that occurred during evaluation
* errors(Value,Errors): Typechecking or evaluation failed
* Value: Short description of error type (e. g. 'NOT-WELL-DEFINED', 'UNKNOWN')
* Errors: List of error/3 terms for all errors that occurred
* enum_warning: An enumeration warning was thrown during evaluation

prob2_exec_custom_aux/4

prob2_exec_custom_pred_aux/5

prob2_execute_custom_operation/4

prob2_execute_custom_operation_with_predicate/5

prob2_execute_custom_operation_with_predicate_aux/5

prob2_execute_custom_operations/6

Description:
prob2_execute_custom_operations(+CurID, +OpName, +ParsedPredicate, +MaxNrOfSolutions, -TOperations, -Errors)

Calculates an operation given a predicate from the user.

#### called by:
ProB 2.0: GetOperationByPredicateCommand

prob2_execute_custom_operations_aux/6

prob2_expand_bvisual2_formula/3

Description:
prob2_expand_bvisual2_formula(+FormulaId,+Options,-ExpandedFormula)

Uses the bvisual2 module to expand a specified formula,
optionally also expanding child formulas recursively and/or evaluating all expanded formulas.
FormulaId must be a bvisual2 formula ID,
as returned for example by get_top_level_formulas/1, insert_formula_for_expansion/2, or prob2_expand_bvisual2_formula/3.

#### called by:
ProB 2.0: ExpandBVisual2FormulaCommand

prob2_export_visb_for_current_state/1

prob2_export_visb_html_for_history/2

prob2_export_visb_html_for_history/3

prob2_export_visb_html_for_states/3

prob2_extended_static_check/1

Description:
prob2_extended_static_check(-Problems)

prob2_find_test_path/4

Description:
prob2_find_test_path(+Events,+EndPredicate,+TimeoutMs,-ResultOpTerms)

example call | ?- prob2_interface:prob2_find_test_path([enter1],truth(unknown),200,R).

Result is either errors(Errors), timeout, interrupt, infeasible_path, or list of Operation IDs

prob2_find_test_path_aux/4

prob2_find_trace/5

prob2_get_formula_type/3

Description:
prob2_get_formula_type(+Formula,-PPType,-Errors)

Type checks the given untyped formula to determine its type and any type errors.

#### Params:
Formula - bexpr(Raw) or bpred(Raw), where Raw is the Prolog representation of non-typechecked expression or predicate
* PPType - pretty-printed type of formula
* Errors - any errors that have occured during typechecking

#### called by:
ProB 2.0: FormulaTypecheckCommand

prob2_get_loaded_visb_file/1

prob2_get_state_errors/2

Description:
prob2_get_state_errors(+StateId,-Errors)

Takes a id for a given state in the state space and produces a list of all
state based errors.

#### called by:
ProB 2.0: GetStateBasedErrorsCommand

prob2_get_visb_html_for_states/3

prob2_invariant_check/2

Description:
prob2_invariant_check(+Ops,-Result)

Performs invariant cbc checking for either for all operations or a list of operations.

#### called by:
ProB 2.0: ConstraintBasedInvariantCheckCommand

prob2_invariant_check2/2

prob2_invariant_check3/3

prob2_invariant_check_for_single_op/3

prob2_load_visb_file/1

prob2_ltl_adapt_ce/2

prob2_ltl_adapt_ce2/3

prob2_ltl_adapt_operations/2

prob2_read_visb_path_from_definitions/1

prob2_redundant_invariants/2

prob2_refine_trace/8

Description:
StartingPoint, Operations, Predicates, 1:n refinemets, Refinements that are actually use refines, Skip events, Results, Maximum search depth

prob2_replay_json_trace_file/4

prob2_reset_prob/0

Description:
prob2_reset_prob

Reset ProB to a clean state as if it was newly started
(except for total_number_of_errors).

#### called by:
ProB 2.0: ResetProBCommand

prob2_visb_attributes_for_state/2

prob2_visb_click_events_and_hovers/2

prob2_visb_default_svg_file_contents/1

prob2_visb_file_loaded/2

prob2_visb_items/1

prob2_visb_perform_click/4

prob2_visb_svg_objects/1

raw_equals/2

raw_truth/1

react_to_item_right_click_option_for_state/6

recognised_smt_solver/2

refine_trace_main_loop/8

refine_trace_start_kick_off/8

refine_trace_step/12

Description:
Current max depth

register_prob2_formula1/3

register_prob2_formulas/2

Description:
register_prob2_formulas(+FormulaUUIDs, +Formulas)

replay_state_trace_from_file/3

requirements_met/2

reset_animator/0

reset_synthesis_context_/0

Description:
serialize(+Id,-SerializedState)

Produces a prolog serialization of a given state id

#### called by:
ProB 2.0: SerializeStateCommand

set_current_state/1

set_default_eval_opts/1

set_default_pp_opts/1

set_eclipse_preference/2

Description:
set_eclipse_preference(+PrefS,+PrefVal)

Sets a preference

#### called by:
ProB Plugin: SetPreferenceCommand
* ProB 2.0: SetPreferenceCommand

set_goal_for_model_checking/1

Description:
set_goal_for_model_checking(+Goal)

Sets the goal for model checking. The Option search_for_goal needs to be set when starting
model checking in order for this to have an effect on the model checking.

#### called by:
ProB 2.0: SetBGoalCommand

solve_free_aux/3

solve_in_state_aux/4

solve_in_state_sat_aux/4

special_id_match_pattern/3

start_animation/0

start_synthesis_from_ui_/13

Description:
Synthesis Commands:

#### b_synthesis:start_synthesis_from_ui/13 called by:
* ProB 2.0: BSynthesisCommand

start_synthesis_single_operation_from_ui_/11

state_property/3

Description:
state_property(+Property,+StateId,-Status)

Finds the status for a given property
Properties can be: invariantKO, timeout_occurred, max_operations_reached, initialised
Statuses are expected to be boolean values: either true or false

#### called by:
ProB Plugin: CheckBooleanPropertyCommand
* ProB 2.0: CheckBooleanPropertyCommand

state_property2/2

strip_ID/2

symbolic_model_check/2

take_best/2

test_bool_exists/4

timed_solve_predicate/6

timeout_occurred/1

trace_to_op_terms/3

Description:
trace_to_op_terms(+ListOpIds,+CurID,-ListOpTerms)

Translates a list of transition ids to a list of terms op(TransId,OpName,SrcId,DestId).
The list must represent a trace,
i. e. the first transition must lead to the source state of the second one,
the second transition to the source state of the third, etc.

translate_cbc_cdclt_result/2

typecheck_pred_for_unsat_core/2

unpack_operation/2

unpack_operation_aux/2

unregister_prob2_formula/1

unregister_prob2_formulas/1

update_preferences_from_spec/0

Description:
update preferences from SET_PREF Definitions in B machines:
should be called after loading a model and before start_animation

update_preferences_from_spec/1

valid_op_name/1

write_dot_for_state_viz/2

Description:
write_dot_for_state_viz(+StateId, +Filename)

Writes a dot representation of the given state to the specified file.

write_dotty/2

write_dotty_for_expr/3

write_dotty_signature_merge/2

write_dotty_state_space/1

write_dotty_transition_diagram/2

Determinacy Checker

Determinacy Checker:

! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(plspec_patch_libraries,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_terminal_colors,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_enter_debugger_upon_error,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_use_timer,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_avl_custom,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_core_only,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_src_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_core_only,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_myheap,false)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(disable_chr,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_96977,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pathes_lib.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_66135,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/error_manager.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_59181,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(debug) does not exist
! goal: absolute_file_name(probsrc(debug),_57517,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_29083,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/state_space.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(json_parser) does not exist
! goal: absolute_file_name(extrasrc(json_parser),_34861,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/translate.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file covsrc(coverage_tools_annotations) does not exist
! goal: absolute_file_name(covsrc(coverage_tools_annotations),_34861,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_waitflags.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_152967,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_records.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_lists) does not exist
! goal: absolute_file_name(probsrc(tools_lists),_181529,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_tools.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_watch_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_waitflags) does not exist
! goal: absolute_file_name(probsrc(kernel_waitflags),_183673,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/runtime_profiler.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(closures) does not exist
! goal: absolute_file_name(probsrc(closures),_189793,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/memoization.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file chrsrc(chr_integer_inequality) does not exist
! goal: absolute_file_name(chrsrc(chr_integer_inequality),_226637,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/clpfd_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(preferences) does not exist
! goal: absolute_file_name(probsrc(preferences),_232607,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_z.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_use_timer,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_watch_flag,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_reals) does not exist
! goal: absolute_file_name(probsrc(kernel_reals),_212821,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_interpreter_check.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(clpfd_interface) does not exist
! goal: absolute_file_name(probsrc(clpfd_interface),_207127,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_equality.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_wd_checking,true)
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(atts))
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(atts))
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(atts))
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(avl_tools) does not exist
! goal: absolute_file_name(probsrc(avl_tools),_190215,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bsets_clp.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_202729,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/succeed_max.pl')])
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(logarr))
! Existence error in argument 1 of absolute_file_name/3
! file probcspsrc(haskell_csp) does not exist
! goal: absolute_file_name(probcspsrc(haskell_csp),_202583,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xtl_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'),_205863,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_machine_hierarchy.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_202729,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/value_persistance.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(avl_tools) does not exist
! goal: absolute_file_name(probsrc(avl_tools),_202871,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/state_packing.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(btypechecker) does not exist
! goal: absolute_file_name(probsrc(btypechecker),_190503,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/specfile.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_190215,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_reals.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_183673,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_interpreter.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_waitflags) does not exist
! goal: absolute_file_name(probsrc(kernel_waitflags),_181529,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/delay.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(performance_messages) does not exist
! goal: absolute_file_name(probsrc(performance_messages),_181529,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_compiler.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_wd_checking,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,xxxtrue)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_156243,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/custom_explicit_sets.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file prob_rewrite_rules(b_ast_cleanup_rewrite_rules) does not exist
! goal: absolute_file_name(prob_rewrite_rules(b_ast_cleanup_rewrite_rules),_152679,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_ast_cleanup.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_152967,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/input_syntax_tree.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),_152825,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_read_write_info.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_152825,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/parsercall.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bmachine_eventb) does not exist
! goal: absolute_file_name(probsrc(bmachine_eventb),_145427,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/btypechecker.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_145427,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pragmas.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(module_information) does not exist
! goal: absolute_file_name(probsrc(module_information),_147233,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine_static_checks.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_145427,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine_static_checks.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_142293,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine_eventb.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_110897,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('random_permutations/random_permutations') does not exist
! goal: absolute_file_name(extension('random_permutations/random_permutations'),_111621,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/fd_utils_clpfd.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_109619,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/partition_detection.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_73385,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_objects.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_67691,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_freetypes.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(clpfd_interface) does not exist
! goal: absolute_file_name(probsrc(clpfd_interface),_64127,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/typing_tools.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(custom_explicit_sets) does not exist
! goal: absolute_file_name(probsrc(custom_explicit_sets),_34861,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bsyntaxtree.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(external_functions_reals) does not exist
! goal: absolute_file_name(extrasrc(external_functions_reals),_34385,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(external_functions_svg) does not exist
! goal: absolute_file_name(extrasrc(external_functions_svg),_34385,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.pl')])
! Existence error in user:check_arithmetic_function/1
! procedure user:check_arithmetic_function/1 does not exist
! goal: user:check_arithmetic_function(log(2,4))
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_36001,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_strings.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_freetypes) does not exist
! goal: absolute_file_name(probsrc(kernel_freetypes),_29739,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.pl')])
! Existence error in user: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 probporsrc(static_analysis) does not exist
! goal: absolute_file_name(probporsrc(static_analysis),_43977,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/model_checker.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(bvisual2) does not exist
! goal: absolute_file_name(extrasrc(bvisual2),_36441,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/eclipse_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file symsrc(state_permuter) does not exist
! goal: absolute_file_name(symsrc(state_permuter),_33161,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/state_space_exploration_modes.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probltlsrc(ctl) does not exist
! goal: absolute_file_name(probltlsrc(ctl),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/prob2_interface.pl')])

Name: =/2
Name: extract_op_name/2	Module: prob2_interface
Name: tcltk_add_new_transition_transid/6	Module: tcltk_interface

Name: prob2_deadlock_freedom_check2/2	Module: prob2_interface
Name: prob2_invariant_check_for_single_op/3	Module: prob2_interface
Name: find_state_for_predicate1/3	Module: prob2_interface

Name: append/3
Name: RECURSIVE_CALL/5	Module: prob2_interface
Name: prob2_execute_custom_operations/6	Module: prob2_interface

Name: leaf_paths/2	Module: foo_error
Name: cbc_solve_type2/3	Module: prob2_interface

Name: =/2
Name: current_state_id/1	Module: state_space
Name: nl
Name: print/1
Name: true
Name: build_modelcheck_return2/2	Module: prob2_interface
Name: ->/3

Name: translate_bexpression/2	Module: translate
Name: before_after_predicate_for_operation/2	Module: foo_error

Name: =/2
Name: !
Name: max_reached_or_timeout_for_node/1	Module: state_space
Name: current_state_id/1	Module: state_space
Name: is/2

Name: bvisual2_formula_children_attribute/3	Module: prob2_interface
Name: =/2
Name: bv_expand_formula/3	Module: foo_error
Name: bv_is_typed_formula/1	Module: foo_error
Name: ->/3
Name: bv_is_typed_predicate/1	Module: foo_error
Name: bv_get_values/3	Module: foo_error
Name: memberchk/2
Name: bv_formula_discharged_info/2	Module: foo_error
Name: bv_formula_labels/2	Module: foo_error
Name: bv_get_formula_functor_symbol/2	Module: foo_error
Name: bv_formula_description/2	Module: foo_error

Name: fail
Name: add_internal_error/2	Module: error_manager
Name: call_dot_command_for_expr/4	Module: foo_error
Name: =/2
Name: !
Name: is_dot_command_for_expr/1	Module: foo_error
Name: call_dot_command/3	Module: foo_error
Name: is_dot_command/1	Module: foo_error

Name: call_dot_command_for_dotfile/3	Module: prob2_interface
Name: tcltk_try_goto_node_with_id/1	Module: tcltk_interface

Name: call_plantuml_command_for_pumlfile/3	Module: prob2_interface
Name: tcltk_try_goto_node_with_id/1	Module: tcltk_interface

Name: is/2
Name: statistics/2
Name: solve_free_aux/3	Module: prob2_interface
Name: solve_in_state_aux/4	Module: prob2_interface
Name: member/2
Name: ->/3
Name: timed_solve_predicate/6	Module: prob2_interface

Name: cbc_solve_typed/6	Module: prob2_interface
Name: cbc_timed_solve_with_opts/6	Module: prob2_interface

Name: cbc_solve_type2/3	Module: prob2_interface
Name: call_cleanup/2
Name: temporary_set_preference/3	Module: preferences
Name: !

Name: ast_leaf_walks/2	Module: prob2_interface
Name: cbc_solve_type/4	Module: prob2_interface

Name: cbc_solve_timed/7	Module: prob2_interface
Name: =/2
Name: true
Name: select/3	Module: foo_error
Name: ->/3
Name: find_identifier_uses/3	Module: bsyntaxtree
Name: cbc_solve_type/4	Module: prob2_interface
Name: maplist/2	Module: lists

Name: =/2
Name: ->/3
Name: checkAssertion/5	Module: tcltk_interface
Name: read_from_codes/2	Module: codesio

Name: RECURSIVE_CALL/3	Module: prob2_interface
Name: memberchk/2
Name: not/1

Name: =/2
Name: true
Name: nonvar/1
Name: ->/3
Name: add_internal_error/2	Module: error_manager
Name: catch_enumeration_warning_exceptions/2	Module: error_manager
Name: specfile_possible_trans_name_for_successors/2	Module: specfile

Name: findall/3
Name: compute_the_coverage/5	Module: foo_error

Name: RECURSIVE_CALL/8	Module: prob2_interface
Name: append/3
Name: execute_nr_of_custom_operations/7	Module: prob2_interface

Name: prob2_ltl_adapt_operations/2	Module: prob2_interface
Name: compute_operations_for_state/2	Module: prob2_interface

Name: find_path/8	Module: prob2_interface
Name: refine_trace_start_kick_off/8	Module: prob2_interface

Name: set_default_eval_opts/1	Module: prob2_interface
Name: =/2

Name: register_prob2_formula1/3	Module: prob2_interface
Name: prob2_get_formula_type/3	Module: prob2_interface

prob_prolog/src/prob2_interface.pl

Modules

Predicates of prob2_interface

Module Information

Dynamic Predicates: prob2_formula/3

3478 Lines

323 Predicates

Imported Modules: module_information sets typechecker self_check random lists lists

154 Exports

205 specified Imports

Predicates:

Name: get_state_space_stats/3	Module: state_space
Name: build_modelcheck_return/2	Module: prob2_interface
Name: do_model_check/13	Module: tcltk_interface
Name: get_preference/2	Module: preferences
Name: option_set/3	Module: prob2_interface
Name: set_depth_breadth_first_mode/1	Module: state_space_exploration_modes
Name: ->/3
Name: =/2
Name: is/2
Name: statistics/2

Name: =/2
Name: !
Name: is_universal_quantifier/4	Module: prob2_interface

Name: add_error_and_fail/3	Module: error_manager
Name: translate_cspm_expression/2	Module: translate
Name: evaluate_parsed_csp_expression_with_timing/2	Module: haskell_csp

Name: evaluate_csp_expression_aux/2	Module: prob2_interface
Name: read_from_codes/2	Module: codesio

Name: exit_error_scope/3	Module: error_manager
Name: get_unknown_error_result/1	Module: prob2_interface
Name: =/2
Name: ->/3
Name: normalise_value_for_var/4	Module: store
Name: !
Name: catch_clpfd_overflow_call2/2	Module: clpfd_interface
Name: clear_all_errors_in_error_scope/1	Module: error_manager
Name: enter_new_error_scope/2	Module: error_manager

Name: evaluate_expression/4	Module: prob2_interface
Name: eval_predicate/4	Module: prob2_interface
Name: !
Name: get_texpr_type/2	Module: bsyntaxtree

Name: extract_result/6	Module: prob2_interface
Name: get_all_errors_with_span_info_and_reset/1	Module: error_manager
Name: =/2
Name: real_error_occurred/0	Module: error_manager
Name: ->/3
Name: true
Name: safe_time_out/3	Module: tools_meta

Name: =/2
Name: tcltk_goto_state/2	Module: tcltk_interface
Name: debug_println/2	Module: debug
Name: tcltk_add_new_transition_transid/6	Module: tcltk_interface
Name: >/2
Name: ->/3
Name: execute_model_steps/7	Module: prob2_interface
Name: prepare_state_for_specfile_trans/3	Module: specfile
Name: visited_expression/2	Module: state_space

Name: RECURSIVE_CALL/7	Module: prob2_interface
Name: =/2
Name: nonvar/1
Name: ->/3
Name: is/2
Name: debug_println/2	Module: debug
Name: !
Name: cli_trans_aux/7	Module: prob2_interface
Name: >=/2

Name: b_type_expression_for_full_b_machine/6	Module: bmachine
Name: get_eval_scope_with_opts/2	Module: prob2_interface
Name: =/2
Name: !
Name: b_is_constant/2	Module: bmachine
Name: b_is_variable/2	Module: bmachine