Dynamic Predicates: bmachine_is_precompiled/0 machine/2 discharged/3 discharged_theorem/3 wd_po/3 wp_untyped/3 nonchanging_guard/2 discharged_guard_strengthening/4 b_specialized_invariant_for_op/2 b_operation_preserves_invariant/2 b_nth1_invariant/3 b_invariant_number_list/1 b_specialized_invariant_mask_for_op/2 get_proven_invariant/2 complete_discharged_info/0 discharged2/2 also_discharged/3 b_operation_reads_output_variables/3 b_operation_cannot_modify_state/1 b_get_operation_normalized_read_write_info/3 b_get_operation_unchanged_variables/2 b_get_operation_non_det_modifies/2 b_get_all_used_filenames/1 b_get_main_filename/1 b_get_main_filenumber/1 b_filenumber/4 b_machine_name/1 b_get_named_machine_set/3 b_enumerated_sets_precompiled/0 b_get_machine_set/2 b_get_machine_constants/1 b_get_machine_all_constants/1 b_get_machine_variables/1 b_get_machine_variables_in_original_order/1 b_is_constant/2 b_is_variable/2 b_get_constant_variable_description/2 b_get_invariant_from_machine/1 b_get_linking_invariant_from_machine/1 b_get_properties_from_machine/1 b_get_static_assertions_from_machine/1 b_extract_values_clause_assignment/3 b_get_unproven_static_assertions_from_machine/1 b_get_dynamic_assertions_from_machine/1 b_get_unproven_dynamic_assertions_from_machine/1 b_get_assertions_from_main_machine/2 b_get_initialisation_from_machine/2 b_get_machine_operation/6 b_top_level_operation/1 b_get_machine_operation_for_animation/7 b_is_operation_name/1 b_get_promoted_machine_operations/1 b_machine_has_static_assertions/0 b_machine_has_dynamic_assertions/0 b_machine_operation_names_in_reverse_order/1 get_operation_info/2 get_operation_description_template_expr/2 b_top_level_feasible_operation/1 b_get_machine_setscope/2 b_get_machine_operation_max/2 b_get_machine_goal/1 b_get_machine_searchscope/1 b_get_definition_string_from_machine/3 b_get_machine_animation_function/2 b_get_machine_heuristic_function/1 b_get_machine_animation_expression/2 b_get_machine_custom_nodes_function/2 b_get_machine_custom_edges_function/2 b_get_machine_custom_graph_function/2 b_get_constant_represented_inside_global_set/2 b_get_disjoint_constants_of_type/3 b_get_all_used_identifiers_in_section/2 b_get_all_used_identifiers/1 b_is_unused_constant/1 b_machine_temp_predicate/1 b_machine_additional_property/1 b_machine_statistics/2

3228 Lines

342 Predicates

Imported Modules: lists ordsets self_check error_manager debug bsyntaxtree parsercall tools b_machine_hierarchy debug specfile state_packing

204 Exports

81 specified Imports

Imports	Exports
Name: check_machine/4 Module: bmachine_construction Name: type_in_machine_l/6 Module: bmachine_construction Name: type_open_predicate_with_quantifier/6 Module: bmachine_construction Name: get_section/3 Module: bmachine_structure Name: write_section/4 Module: bmachine_structure Name: get_section_texprs/3 Module: bmachine_structure Name: translate_machine/3 Module: translate Name: translate_eventb_to_classicalb/3 Module: translate Name: check_event_b_project/4 Module: bmachine_eventb Name: is_eventb_additional_info/1 Module: bmachine_eventb Name: register_freetypes/1 Module: kernel_freetypes Name: find_inequal_global_set_identifiers/4 Module: b_global_sets Name: b_get_prob_deferred_set_elements/2 Module: b_global_sets Name: b_check_and_precompile_enumerated_sets/0 Module: b_global_sets Name: b_check_and_precompile_deferred_sets/0 Module: b_global_sets Name: b_check_and_precompile_global_set_symmetry/0 Module: b_global_sets Name: replace_sets_by_records/2 Module: record_detection Name: detect_partitions/2 Module: partition_detection Name: module_info/2 Module: module_information Name: raw_sha_hash/2 Module: probhash/probhash Name: static_check_main_machine/1 Module: bmachine_static_checks Name: count_occurences/2 Module: tools_lists Name: get_accessed_vars/4 Module: b_read_write_info Name: get_global_identifiers/1 Module: bsyntaxtree Name: get_nondet_modified_vars/3 Module: b_read_write_info Name: codes_to_lower_case/2 Module: tools_matching Name: same_file_name/2 Module: tools Name: safe_absolute_file_name/3 Module: tools Name: get_parent_directory/2 Module: tools Name: reset_typechecker/0 Module: btypechecker Name: b_clear_global_set_type_definitions/0 Module: b_global_sets Name: reset_bmachine_construction/0 Module: bmachine_construction Name: register_event_listener/3 Module: eventhandling Name: get_preference/2 Module: preferences Name: atom_prefix/2 Module: tools_strings Name: animation_minor_mode/1 Module: specfile Name: classical_b_mode/0 Module: specfile Name: type_open_formula/8 Module: bmachine_construction Name: b_global_set/1 Module: b_global_sets Name: is_b_global_constant/3 Module: b_global_sets Name: registered_freetype/2 Module: kernel_freetypes Name: freetype_case_db/3 Module: kernel_freetypes Name: stored_operator/2 Module: bmachine_eventb Name: get_texpr_id/2 Module: bsyntaxtree Name: get_texpr_type/2 Module: bsyntaxtree Name: pretty_type/2 Module: translate Name: b_global_deferred_set/1 Module: b_global_sets Name: all_elements_of_type/2 Module: b_global_sets Name: get_raw_position_info/2 Module: input_syntax_tree Name: split_last/4 Module: tools Name: lookup_global_constant/2 Module: b_global_sets Name: prob_deferred_set_element/4 Module: b_global_sets Name: extract_file_number_and_name/3 Module: error_manager Name: b_or_z_mode/0 Module: specfile Name: safe_number_codes/2 Module: tools Name: is_set_type/2 Module: bsyntaxtree Name: ord_union/2 Module: ordsets Name: unify_types_strict/2 Module: btypechecker Name: safe_create_texpr/4 Module: bsyntaxtree Name: pretty_type/2 Module: translate Name: unset_animation_minor_modes/1 Module: specfile Name: reset_animation_minor_modes/1 Module: specfile Name: set_unicode_mode/0 Module: translate Name: unset_unicode_mode/0 Module: translate Name: set_print_type_infos/1 Module: translate Name: nested_write_term_to_codes/2 Module: tools_printing Name: get_tail_filename/2 Module: tools Name: split_filename/3 Module: tools Name: safe_atom_chars/3 Module: tools Name: set_print_type_infos/1 Module: translate Name: write_to_utf8_file_or_user_output/2 Module: tools_files Name: temporary_set_preference/3 Module: preferences Name: reset_temporary_preference/2 Module: preferences Name: start_ms_timer/1 Module: tools Name: stop_ms_walltimer_with_msg/2 Module: tools Name: prime_atom0/2 Module: btypechecker Name: extend_typing_scope_for_stored_lets/2 Module: eval_let_store Name: create_couple/3 Module: bsyntaxtree Name: prime_atom0/2 Module: btypechecker Name: find_typed_identifier_uses/2 Module: bsyntaxtree Name: get_texpr_id/2 Module: bsyntaxtree	Name: bmachine_is_precompiled/0 Name: b_enumerated_sets_precompiled/0 Name: b_set_initial_machine/0 Name: b_set_empty_machine/0 Name: b_set_machine/3 Name: b_set_typed_machine/2 Name: b_load_eventb_project/1 Name: b_set_eventb_project_flat/3 Name: get_full_b_machine/2 Name: full_b_machine/1 Name: get_full_b_machine_sha_hash/1 Name: b_machine_is_loaded/0 Name: get_proven_invariant/2 Name: get_unproven_invariants/1 Name: get_invariant_list_with_proof_info/1 Name: load_additional_information/1 Name: get_operation_info/2 Name: b_get_operation_description/2 Name: get_operation_description_template_expr/2 Name: b_load_machine_from_file/1 Name: b_load_machine_from_file/2 Name: b_load_machine_probfile/1 Name: b_load_machine_probfile/2 Name: b_load_machine_from_list_of_facts/2 Name: b_load_machine_from_term/2 Name: b_machine_precompile/0 Name: other_spec_precompile/0 Name: b_machine_reset/0 Name: b_machine_name/1 Name: b_get_all_used_filenames/1 Name: b_get_main_filename/1 Name: add_additional_filename/2 Name: set_additional_filename_as_parsing_default/3 Name: reset_filename_parsing_default/2 Name: b_get_main_filenumber/1 Name: b_filenumber/4 Name: portray_filenumbers/0 Name: get_machine_file_number/4 Name: b_absolute_file_name_relative_to_main_machine/2 Name: b_get_animated_sections/1 Name: b_get_machine_set/1 Name: b_get_machine_set/2 Name: b_get_named_machine_set/2 Name: b_get_named_machine_set/3 Name: b_get_disjoint_constants_of_type/3 Name: b_get_constant_represented_inside_global_set/2 Name: b_get_machine_constants/1 Name: b_get_machine_all_constants/1 Name: b_machine_has_constants/0 Name: b_machine_has_constants_or_properties/0 Name: b_is_constant/2 Name: b_is_constant/1 Name: b_is_unused_constant/1 Name: get_constant_span/2 Name: b_machine_has_variables/0 Name: b_is_variable/1 Name: b_is_variable/2 Name: b_get_constant_variable_description/2 Name: constant_variable_marked_as_memo/1 Name: constant_variable_marked_as_expand/1 Name: b_get_machine_variables_in_original_order/1 Name: b_get_machine_variables/1 Name: get_primed_machine_variables/1 Name: get_nr_of_machine_variables/1 Name: get_nr_of_machine_constants/1 Name: b_get_all_used_identifiers/1 Name: b_get_all_used_identifiers_in_section/2 Name: get_machine_identifiers/2 Name: get_machine_identifiers_with_pp_type/2 Name: source_code_for_identifier/6 Name: b_get_properties_from_machine/1 Name: b_get_invariant_from_machine/1 Name: b_get_linking_invariant_from_machine/1 Name: b_machine_has_assertions/0 Name: b_get_static_assertions_from_machine/1 Name: b_machine_has_static_assertions/0 Name: b_get_unproven_static_assertions_from_machine/1 Name: b_get_dynamic_assertions_from_machine/1 Name: b_machine_has_dynamic_assertions/0 Name: b_get_unproven_dynamic_assertions_from_machine/1 Name: b_get_assertions_from_main_machine/2 Name: b_main_machine_has_no_assertions/0 Name: b_machine_has_unproven_assertions/0 Name: get_assertions_from_machine/2 Name: get_all_assertions_from_machine/1 Name: b_machine_has_proven_invariants/0 Name: b_get_assertions/3 Name: b_get_assertion_count/3 Name: is_discharged_assertion/1 Name: b_get_initialisation_from_machine/2 Name: b_machine_has_operations/0 Name: b_get_machine_operation/4 Name: b_get_machine_operation/6 Name: b_get_machine_operation_for_animation/6 Name: b_get_machine_operation_for_animation/7 Name: b_get_promoted_machine_operations/1 Name: b_top_level_operation/1 Name: b_top_level_feasible_operation/1 Name: b_is_initialisation_name/1 Name: b_is_operation_name/1 Name: b_get_operation_pos/2 Name: b_get_machine_operation_parameter_types/2 Name: b_get_machine_operation_parameter_names/2 Name: b_get_machine_operation_result_names/2 Name: b_get_machine_operation_typed_parameters/2 Name: b_get_machine_operation_typed_results/2 Name: b_get_machine_operation_signature/2 Name: b_machine_operation_names_in_reverse_order/1 Name: b_get_operation_variant/3 Name: b_get_machine_setscope/2 Name: b_get_machine_operation_max/2 Name: b_get_machine_goal/1 Name: b_set_machine_goal/1 Name: b_set_machine_goal/2 Name: b_set_machine_searchscope/1 Name: b_set_machine_searchscope/2 Name: b_set_parsed_typed_machine_goal/1 Name: b_unset_machine_goal/0 Name: b_reset_machine_goal_from_DEFINITIONS/0 Name: b_parse_machine_expression_from_codes/2 Name: b_parse_machine_expression_from_codes_with_prob_ids/2 Name: b_parse_machine_expression_from_codes_with_prob_ids/3 Name: b_parse_machine_expression_from_codes_with_prob_ids/4 Name: b_parse_machine_expression_from_codes/5 Name: b_parse_machine_expression_from_codes/6 Name: b_parse_machine_subsitutions_from_codes/6 Name: b_parse_machine_formula/3 Name: b_parse_machine_formula_from_codes/7 Name: b_parse_machine_predicate/2 Name: b_parse_machine_predicate/3 Name: b_parse_optional_machine_predicate/2 Name: b_parse_machine_predicate_from_codes/3 Name: b_parse_machine_predicate_from_codes_open/5 Name: b_parse_machine_operation_pre_post_predicate/3 Name: b_parse_machine_operation_pre_post_predicate/5 Name: get_machine_operation_additional_identifiers/2 Name: determine_type_of_formula/2 Name: determine_type_of_formula/3 Name: parse_expression_raw_or_atom_with_prob_ids/2 Name: b_parse_wo_type_machine_predicate_from_codes_to_raw_expr/2 Name: b_type_check_raw_expr/4 Name: b_get_machine_searchscope/1 Name: b_get_machine_animation_function/2 Name: b_get_machine_heuristic_function/1 Name: b_get_machine_animation_expression/2 Name: b_get_machine_custom_edges_function/2 Name: b_get_machine_custom_nodes_function/2 Name: b_get_machine_custom_graph_function/2 Name: b_machine_temp_predicate/1 Name: assert_temp_typed_predicate/1 Name: reset_temp_predicate/0 Name: add_additional_property/2 Name: b_machine_additional_property/1 Name: get_animation_image/2 Name: get_animation_image_source_file/2 Name: b_get_definition/5 Name: b_get_definition_with_pos/6 Name: b_get_definition_string_from_machine/2 Name: b_get_definition_string_from_machine/3 Name: b_definition_prefixed/5 Name: b_sorted_b_definition_prefixed/4 Name: b_get_typed_definition/3 Name: b_get_typed_predicate_definition/3 Name: b_get_typed_expression_definition/3 Name: b_get_true_expression_definition/1 Name: b_nth1_invariant/3 Name: b_invariant_number_list/1 Name: b_specialized_invariant_for_op/2 Name: b_specialized_invariant_mask_for_op/2 Name: b_operation_preserves_full_invariant/1 Name: b_operation_preserves_invariant/2 Name: tcltk_get_specialized_invariant_for_op/2 Name: tcltk_get_specialized_invariants_for_ops/1 Name: b_get_operation_normalized_read_write_info/3 Name: b_get_operation_unchanged_variables/2 Name: b_operation_cannot_modify_state/1 Name: b_operation_reads_output_variables/3 Name: b_get_operation_non_det_modifies/2 Name: b_extract_values_clause_assignment/3 Name: b_type_expression/5 Name: b_type_expression_for_full_b_machine/6 Name: b_type_open_predicate/5 Name: b_type_open_predicate_with_errors/4 Name: b_type_open_exists_predicate/3 Name: type_with_errors/4 Name: b_show_machine_representation_unicode/4 Name: b_show_machine_representation/4 Name: b_get_internal_prolog_representation_as_codes/1 Name: b_write_machine_representation_to_file/2 Name: b_write_machine_representation_to_file/3 Name: b_write_eventb_machine_to_classicalb_to_file/1 Name: b_show_eventb_as_classicalb/2 Name: b_get_machine_refinement_hierarchy/1 Name: b_get_refined_machine/1 Name: b_get_refined_machine_name/1 Name: b_get_refined_ancestors_names/1 Name: b_get_machine_header_position/2 Name: b_get_model_type/1 Name: b_machine_statistics/2 Name: discharged_guard_strengthening/4 Name: wp_untyped/3 Name: clear_wp/0 Name: nonchanging_guard/2 Name: typecheck_predicates/4

Imports

Exports

Name: check_machine/4

Module: bmachine_construction

Name: type_in_machine_l/6

Module: bmachine_construction

Name: type_open_predicate_with_quantifier/6

Module: bmachine_construction

Name: get_section/3

Module: bmachine_structure

Name: write_section/4

Module: bmachine_structure

Name: get_section_texprs/3

Module: bmachine_structure

Name: translate_machine/3

Module: translate

Name: translate_eventb_to_classicalb/3

Module: translate

Name: check_event_b_project/4

Module: bmachine_eventb

Name: is_eventb_additional_info/1

Module: bmachine_eventb

Name: register_freetypes/1

Module: kernel_freetypes

Name: find_inequal_global_set_identifiers/4

Module: b_global_sets

Name: b_get_prob_deferred_set_elements/2

Module: b_global_sets

Name: b_check_and_precompile_enumerated_sets/0

Module: b_global_sets

Name: b_check_and_precompile_deferred_sets/0

Module: b_global_sets

Name: b_check_and_precompile_global_set_symmetry/0

Module: b_global_sets

Name: replace_sets_by_records/2

Module: record_detection

Name: detect_partitions/2

Module: partition_detection

Name: module_info/2

Module: module_information

Name: raw_sha_hash/2

Module: probhash/probhash

Name: static_check_main_machine/1

Module: bmachine_static_checks

Name: count_occurences/2

Module: tools_lists

Name: get_accessed_vars/4

Module: b_read_write_info

Name: get_global_identifiers/1

Module: bsyntaxtree

Name: get_nondet_modified_vars/3

Module: b_read_write_info

Name: codes_to_lower_case/2

Module: tools_matching

Name: same_file_name/2

Module: tools

Name: safe_absolute_file_name/3

Module: tools

Name: get_parent_directory/2

Module: tools

Name: reset_typechecker/0

Module: btypechecker

Name: b_clear_global_set_type_definitions/0

Module: b_global_sets

Name: reset_bmachine_construction/0

Module: bmachine_construction

Name: register_event_listener/3

Module: eventhandling

Name: get_preference/2

Module: preferences

Name: atom_prefix/2

Module: tools_strings

Name: animation_minor_mode/1

Module: specfile

Name: classical_b_mode/0

Module: specfile

Name: type_open_formula/8

Module: bmachine_construction

Name: b_global_set/1

Module: b_global_sets

Name: is_b_global_constant/3

Module: b_global_sets

Name: registered_freetype/2

Module: kernel_freetypes

Name: freetype_case_db/3

Module: kernel_freetypes

Name: stored_operator/2

Module: bmachine_eventb

Name: get_texpr_id/2

Module: bsyntaxtree

Name: get_texpr_type/2

Module: bsyntaxtree

Name: pretty_type/2

Module: translate

Name: b_global_deferred_set/1

Module: b_global_sets

Name: all_elements_of_type/2

Module: b_global_sets

Name: get_raw_position_info/2

Module: input_syntax_tree

Name: split_last/4

Module: tools

Name: lookup_global_constant/2

Module: b_global_sets

Name: prob_deferred_set_element/4

Module: b_global_sets

Name: extract_file_number_and_name/3

Module: error_manager

Name: b_or_z_mode/0

Module: specfile

Name: safe_number_codes/2

Module: tools

Name: is_set_type/2

Module: bsyntaxtree

Name: ord_union/2

Module: ordsets

Name: unify_types_strict/2

Module: btypechecker

Name: safe_create_texpr/4

Module: bsyntaxtree

Name: pretty_type/2

Module: translate

Name: unset_animation_minor_modes/1

Module: specfile

Name: reset_animation_minor_modes/1

Module: specfile

Name: set_unicode_mode/0

Module: translate

Name: unset_unicode_mode/0

Module: translate

Name: set_print_type_infos/1

Module: translate

Name: nested_write_term_to_codes/2

Module: tools_printing

Name: get_tail_filename/2

Module: tools

Name: split_filename/3

Module: tools

Name: safe_atom_chars/3

Module: tools

Name: set_print_type_infos/1

Module: translate

Name: write_to_utf8_file_or_user_output/2

Module: tools_files

Name: temporary_set_preference/3

Module: preferences

Name: reset_temporary_preference/2

Module: preferences

Name: start_ms_timer/1

Module: tools

Name: stop_ms_walltimer_with_msg/2

Module: tools

Name: prime_atom0/2

Module: btypechecker

Name: extend_typing_scope_for_stored_lets/2

Module: eval_let_store

Name: create_couple/3

Module: bsyntaxtree

Name: prime_atom0/2

Module: btypechecker

Name: find_typed_identifier_uses/2

Module: bsyntaxtree

Name: get_texpr_id/2

Module: bsyntaxtree

Name: bmachine_is_precompiled/0

Name: b_enumerated_sets_precompiled/0

Name: b_set_initial_machine/0

Name: b_set_empty_machine/0

Name: b_set_machine/3

Name: b_set_typed_machine/2

Name: b_load_eventb_project/1

Name: b_set_eventb_project_flat/3

Name: get_full_b_machine/2

Name: full_b_machine/1

Name: get_full_b_machine_sha_hash/1

Name: b_machine_is_loaded/0

Name: get_proven_invariant/2

Name: get_unproven_invariants/1

Name: get_invariant_list_with_proof_info/1

Name: load_additional_information/1

Name: get_operation_info/2

Name: b_get_operation_description/2

Name: get_operation_description_template_expr/2

Name: b_load_machine_from_file/1

Name: b_load_machine_from_file/2

Name: b_load_machine_probfile/1

Name: b_load_machine_probfile/2

Name: b_load_machine_from_list_of_facts/2

Name: b_load_machine_from_term/2

Name: b_machine_precompile/0

Name: other_spec_precompile/0

Name: b_machine_reset/0

Name: b_machine_name/1

Name: b_get_all_used_filenames/1

Name: b_get_main_filename/1

Name: add_additional_filename/2

Name: set_additional_filename_as_parsing_default/3

Name: reset_filename_parsing_default/2

Name: b_get_main_filenumber/1

Name: b_filenumber/4

Name: portray_filenumbers/0

Name: get_machine_file_number/4

Name: b_absolute_file_name_relative_to_main_machine/2

Name: b_get_animated_sections/1

Name: b_get_machine_set/1

Name: b_get_machine_set/2

Name: b_get_named_machine_set/2

Name: b_get_named_machine_set/3

Name: b_get_disjoint_constants_of_type/3

Name: b_get_constant_represented_inside_global_set/2

Name: b_get_machine_constants/1

Name: b_get_machine_all_constants/1

Name: b_machine_has_constants/0

Name: b_machine_has_constants_or_properties/0

Name: b_is_constant/2

Name: b_is_constant/1

Name: b_is_unused_constant/1

Name: get_constant_span/2

Name: b_machine_has_variables/0

Name: b_is_variable/1

Name: b_is_variable/2

Name: b_get_constant_variable_description/2

Name: constant_variable_marked_as_memo/1

Name: constant_variable_marked_as_expand/1

Name: b_get_machine_variables_in_original_order/1

Name: b_get_machine_variables/1

Name: get_primed_machine_variables/1

Name: get_nr_of_machine_variables/1

Name: get_nr_of_machine_constants/1

Name: b_get_all_used_identifiers/1

Name: b_get_all_used_identifiers_in_section/2

Name: get_machine_identifiers/2

Name: get_machine_identifiers_with_pp_type/2

Name: source_code_for_identifier/6

Name: b_get_properties_from_machine/1

Name: b_get_invariant_from_machine/1

Name: b_get_linking_invariant_from_machine/1

Name: b_machine_has_assertions/0

Name: b_get_static_assertions_from_machine/1

Name: b_machine_has_static_assertions/0

Name: b_get_unproven_static_assertions_from_machine/1

Name: b_get_dynamic_assertions_from_machine/1

Name: b_machine_has_dynamic_assertions/0

Name: b_get_unproven_dynamic_assertions_from_machine/1

Name: b_get_assertions_from_main_machine/2

Name: b_main_machine_has_no_assertions/0

Name: b_machine_has_unproven_assertions/0

Name: get_assertions_from_machine/2

Name: get_all_assertions_from_machine/1

Name: b_machine_has_proven_invariants/0

Name: b_get_assertions/3

Name: b_get_assertion_count/3

Name: is_discharged_assertion/1

Name: b_get_initialisation_from_machine/2

Name: b_machine_has_operations/0

Name: b_get_machine_operation/4

Name: b_get_machine_operation/6

Name: b_get_machine_operation_for_animation/6

Name: b_get_machine_operation_for_animation/7

Name: b_get_promoted_machine_operations/1

Name: b_top_level_operation/1

Name: b_top_level_feasible_operation/1

Name: b_is_initialisation_name/1

Name: b_is_operation_name/1

Name: b_get_operation_pos/2

Name: b_get_machine_operation_parameter_types/2

Name: b_get_machine_operation_parameter_names/2

Name: b_get_machine_operation_result_names/2

Name: b_get_machine_operation_typed_parameters/2

Name: b_get_machine_operation_typed_results/2

Name: b_get_machine_operation_signature/2

Name: b_machine_operation_names_in_reverse_order/1

Name: b_get_operation_variant/3

Name: b_get_machine_setscope/2

Name: b_get_machine_operation_max/2

Name: b_get_machine_goal/1

Name: b_set_machine_goal/1

Name: b_set_machine_goal/2

Name: b_set_machine_searchscope/1

Name: b_set_machine_searchscope/2

Name: b_set_parsed_typed_machine_goal/1

Name: b_unset_machine_goal/0

Name: b_reset_machine_goal_from_DEFINITIONS/0

Name: b_parse_machine_expression_from_codes/2

Name: b_parse_machine_expression_from_codes_with_prob_ids/2

Name: b_parse_machine_expression_from_codes_with_prob_ids/3

Name: b_parse_machine_expression_from_codes_with_prob_ids/4

Name: b_parse_machine_expression_from_codes/5

Name: b_parse_machine_expression_from_codes/6

Name: b_parse_machine_subsitutions_from_codes/6

Name: b_parse_machine_formula/3

Name: b_parse_machine_formula_from_codes/7

Name: b_parse_machine_predicate/2

Name: b_parse_machine_predicate/3

Name: b_parse_optional_machine_predicate/2

Name: b_parse_machine_predicate_from_codes/3

Name: b_parse_machine_predicate_from_codes_open/5

Name: b_parse_machine_operation_pre_post_predicate/3

Name: b_parse_machine_operation_pre_post_predicate/5

Name: get_machine_operation_additional_identifiers/2

Name: determine_type_of_formula/2

Name: determine_type_of_formula/3

Name: parse_expression_raw_or_atom_with_prob_ids/2

Name: b_parse_wo_type_machine_predicate_from_codes_to_raw_expr/2

Name: b_type_check_raw_expr/4

Name: b_get_machine_searchscope/1

Name: b_get_machine_animation_function/2

Name: b_get_machine_heuristic_function/1

Name: b_get_machine_animation_expression/2

Name: b_get_machine_custom_edges_function/2

Name: b_get_machine_custom_nodes_function/2

Name: b_get_machine_custom_graph_function/2

Name: b_machine_temp_predicate/1

Name: assert_temp_typed_predicate/1

Name: reset_temp_predicate/0

Name: add_additional_property/2

Name: b_machine_additional_property/1

Name: get_animation_image/2

Name: get_animation_image_source_file/2

Name: b_get_definition/5

Name: b_get_definition_with_pos/6

Name: b_get_definition_string_from_machine/2

Name: b_get_definition_string_from_machine/3

Name: b_definition_prefixed/5

Name: b_sorted_b_definition_prefixed/4

Name: b_get_typed_definition/3

Name: b_get_typed_predicate_definition/3

Name: b_get_typed_expression_definition/3

Name: b_get_true_expression_definition/1

Name: b_nth1_invariant/3

Name: b_invariant_number_list/1

Name: b_specialized_invariant_for_op/2

Name: b_specialized_invariant_mask_for_op/2

Name: b_operation_preserves_full_invariant/1

Name: b_operation_preserves_invariant/2

Name: tcltk_get_specialized_invariant_for_op/2

Name: tcltk_get_specialized_invariants_for_ops/1

Name: b_get_operation_normalized_read_write_info/3

Name: b_get_operation_unchanged_variables/2

Name: b_operation_cannot_modify_state/1

Name: b_operation_reads_output_variables/3

Name: b_get_operation_non_det_modifies/2

Name: b_extract_values_clause_assignment/3

Name: b_type_expression/5

Name: b_type_expression_for_full_b_machine/6

Name: b_type_open_predicate/5

Name: b_type_open_predicate_with_errors/4

Name: b_type_open_exists_predicate/3

Name: type_with_errors/4

Name: b_show_machine_representation_unicode/4

Name: b_show_machine_representation/4

Name: b_get_internal_prolog_representation_as_codes/1

Name: b_write_machine_representation_to_file/2

Name: b_write_machine_representation_to_file/3

Name: b_write_eventb_machine_to_classicalb_to_file/1

Name: b_show_eventb_as_classicalb/2

Name: b_get_machine_refinement_hierarchy/1

Name: b_get_refined_machine/1

Name: b_get_refined_machine_name/1

Name: b_get_refined_ancestors_names/1

Name: b_get_machine_header_position/2

Name: b_get_model_type/1

Name: b_machine_statistics/2

Name: discharged_guard_strengthening/4

Name: wp_untyped/3

Name: clear_wp/0

Name: nonchanging_guard/2

Name: typecheck_predicates/4

Predicates

Predicates:

add_additional_filename/2

add_additional_property/2

add_all_perrors_in_context_of_used_filenames/2

add_discharged_po_infos/2

all_operations_have_valid_read_modifies_infos/0

apply_machine_transformations-->/2

apply_transformation_step/4

assert_bmachine_is_precompiled/0

assert_main_machine/1

assert_temp_typed_predicate/1

auto_precompile/0

auto_precompile2/3

auto_precompile_phase2/0

b_absolute_file_name_relative_to_main_machine/2

b_definition_prefixed/5

b_enumerated_sets_precompiled_calc/0

b_extract_values_clause_assignment_calc/3

b_find_operation/5

b_get_abstract_events/3

b_get_all_used_filenames/1

b_get_all_used_identifiers_calc/1

b_get_all_used_identifiers_in_section_calc/2

b_get_animated_sections/1

b_get_assertion_count/3

b_get_assertions/3

b_get_assertions_from_main_machine_calc/2

b_get_constant_represented_inside_global_set_calc/2

b_get_constant_variable_description_calc/2

b_get_definition/5

b_get_definition_string_from_machine/2

b_get_definition_string_from_machine_calc/3

b_get_definition_with_pos/6

b_get_disjoint_constants_of_type_calc/3

b_get_dynamic_assertions_from_machine_calc/1

b_get_initialisation_from_machine_calc/2

b_get_internal_prolog_representation_as_codes/1

b_get_invariant_from_machine_calc/1

b_get_linking_invariant_from_machine_calc/1

b_get_machine_all_constants_calc/1

b_get_machine_animation_expression_calc/2

b_get_machine_animation_function_calc/2

b_get_machine_constants_calc/1

b_get_machine_custom_edges_function_calc/2

b_get_machine_custom_graph_function_calc/2

b_get_machine_custom_nodes_function_calc/2

b_get_machine_goal_calc/1

b_get_machine_header_position/2

b_get_machine_heuristic_function_calc/1

b_get_machine_operation/4

b_get_machine_operation_calc/6

b_get_machine_operation_for_animation/6

b_get_machine_operation_for_animation_calc/7

b_get_machine_operation_max_calc/2

b_get_machine_operation_parameter_names/2

b_get_machine_operation_parameter_types/2

b_get_machine_operation_result_names/2

b_get_machine_operation_signature/2

b_get_machine_operation_typed_parameters/2

b_get_machine_operation_typed_parameters_aux/2

b_get_machine_operation_typed_results/2

b_get_machine_refinement_hierarchy/1

b_get_machine_searchscope_calc/1

b_get_machine_set/1

b_get_machine_set_calc/2

b_get_machine_setscope_calc/2

b_get_machine_variables_calc/1

b_get_machine_variables_in_original_order_calc/1

b_get_model_type/1

b_get_named_machine_set/2

b_get_named_machine_set_calc/3

b_get_operation_description/2

b_get_operation_non_det_modifies_calc/2

b_get_operation_normalized_read_write_info_calc/3

b_get_operation_pos/2

b_get_operation_unchanged_variables_calc/2

b_get_operation_variant/3

b_get_promoted_machine_operations_calc/1

b_get_properties_from_machine_calc/1

b_get_refined_ancestors_names/1

b_get_refined_machine/1

b_get_refined_machine_name/1

b_get_static_assertions_from_machine_calc/1

b_get_true_expression_definition/1

b_get_typed_definition/3

b_get_typed_expression_definition/3

b_get_typed_predicate_definition/3

b_get_unproven_dynamic_assertions_from_machine_calc/1

b_get_unproven_static_assertions_from_machine_calc/1

b_invariant_number_list_calc/1

b_is_constant/1

b_is_constant_calc/2

b_is_initialisation_name/1

b_is_operation_name_calc/1

b_is_unused_constant_calc/1

b_is_variable/1

b_is_variable_calc/2

b_limit_abstract_level_to_zero/2

b_load_eventb_project/1

b_load_machine_from_file/1

b_load_machine_from_file/2

b_load_machine_from_list_of_facts/2

b_load_machine_from_term/2

b_load_machine_probfile/1

b_load_machine_probfile/2

b_machine_clear/0

b_machine_has_assertions/0

b_machine_has_constants/0

b_machine_has_constants_or_properties/0

b_machine_has_dynamic_assertions_calc/0

b_machine_has_operations/0

b_machine_has_proven_invariants/0

b_machine_has_static_assertions_calc/0

b_machine_has_unproven_assertions/0

b_machine_has_variables/0

b_machine_is_loaded/0

b_machine_name_calc/1

b_machine_precompile/0

b_machine_reset/0

b_machine_statistics_calc/2

b_main_machine_has_no_assertions/0

b_nth1_invariant_calc/3

b_operation_cannot_modify_state_calc/1

b_operation_preserves_full_invariant/1

b_operation_preserves_invariant_calc/2

b_operation_reads_output_variables_calc/3

b_parse_machine_expression_from_codes/2

b_parse_machine_expression_from_codes/5

b_parse_machine_expression_from_codes/6

b_parse_machine_expression_from_codes4/4

b_parse_machine_expression_from_codes_with_prob_ids/2

b_parse_machine_expression_from_codes_with_prob_ids/3

b_parse_machine_expression_from_codes_with_prob_ids/4

b_parse_machine_formula/3

b_parse_machine_formula_from_codes/7

b_parse_machine_operation_pre_post_predicate/3

b_parse_machine_operation_pre_post_predicate/5

b_parse_machine_predicate/2

b_parse_machine_predicate/3

b_parse_machine_predicate_from_codes/3

b_parse_machine_predicate_from_codes2/5

b_parse_machine_predicate_from_codes_open/5

b_parse_machine_subsitutions_from_codes/6

b_parse_only/5

b_parse_optional_machine_predicate/2

b_parse_predicate/3

b_parse_wo_type_machine_predicate_from_codes_to_raw_expr/2

b_reset_filenames_and_numbers/0

b_reset_machine_goal_from_DEFINITIONS/0

b_set_empty_machine/0

b_set_eventb_project_flat/3

b_set_initial_machine/0

b_set_machine/3

b_set_machine_goal/1

b_set_machine_goal/2

b_set_machine_searchscope/1

b_set_machine_searchscope/2

b_set_parsed_typed_machine_goal/1

b_set_parsed_typed_machine_searchscope/1

b_set_to_level_zero/2

b_set_typed_machine/2

b_show_eventb_as_classicalb/2

b_show_eventb_as_classicalb1/3

b_show_machine_representation/4

b_show_machine_representation_unicode/4

b_sorted_b_definition_prefixed/4

b_specialized_invariant_for_op_calc/2

b_specialized_invariant_mask_for_op_calc/2

b_top_level_feasible_operation_calc/1

b_top_level_operation_calc/1

b_type_check_raw_expr/4

b_type_expression/5

b_type_expression_for_full_b_machine/6

b_type_expressions_l/6

b_type_literal/3

b_type_only/5

b_type_open_exists_predicate/3

b_type_open_predicate/5

b_type_open_predicate_for_full_b_machine/6

b_type_open_predicate_with_errors/4

b_unset_machine_goal/0

b_write_eventb_machine_to_classicalb_to_file/1

b_write_machine_representation_to_file/2

b_write_machine_representation_to_file/3

b_write_machine_representation_to_file3/3

check_valid_machine_name/1

check_wd_discharged_inv_or_thm/4

check_write/2

clear_wp/0

comparison/3

complete_discharged_info2/0

complete_discharged_info3/3

complete_discharged_info_calc/0

constant_variable_marked_as_expand/1

constant_variable_marked_as_memo/1

determine_type_of_formula/2

determine_type_of_formula/3

determine_type_of_formula2/2

discharged_info_exists/0

discharged_invariant/3

do_machine_consistency_check/0

empty/1

empty_machine/2

eventb_load_command/5

extension_kind/2

extract_id_and_pp_type/2

filter_out_proven_assertions/2

filter_syntactically_relevant_invariants/4

filter_syntactically_relevant_invariants2/4

find_constants_of_type/4

find_id_uses_for_maplist/2

find_main_file_name/3

find_used_identifier_in_machine_section/3

flexible_atom_codes/2

full_b_machine/1

gen_couple_from_list/2

generate_no_parse_errors/1

generate_parse_errors_for/2

get_all_assertions_from_machine/1

get_animation_image/2

get_animation_image_source_file/2

get_assertions_from_machine/2

get_bottom_event/2

get_constant_definition/2

get_constant_predicate/2

get_constant_span/2

get_constant_type_and_origin/4

get_definition_with_nr_suffix/3

get_full_b_machine/2

get_full_b_machine_sha_hash/1

get_goal/1

get_invariant_list_with_proof_info/1

get_invariant_list_with_used_ids/2

get_invariant_with_proof_status_calc/2

get_machine_file_number/4

get_machine_identifiers/2

get_machine_identifiers_with_pp_type/2

get_machine_operation_additional_identifiers/2

get_machine_operation_typing_scope/3

get_modifies_from_info/2

get_multi_sections/2

get_nr_of_machine_constants/1

get_nr_of_machine_variables/1

get_op_desc_template_expr_calc2/2

get_op_or_init_and_syntax_filter/5

get_operation_description_template_expr_calc/2

get_operation_info_calc/2

get_operation_type/4

get_primed_machine_variables/1

get_proven_invariant_calc/2

get_proz_animation_function/3

get_proz_settings/1

get_section_from_current_machine/2

get_tc_scope/2

get_unproven_invariants/1

get_variable_type_and_origin/4

invariant_proof_status_for_event/4

involves_id/2

involves_id_aux/2

is_abstract_event_in_list/3

is_discharged_assertion/1

is_empty_string/1

is_empty_string2/1

is_ground/2

is_initialisation_op/1

is_not_main_assertion/1

is_precompiled_predicate/1

is_proven_invariant/2

is_proven_invariant_for_model/3

is_syntactically_relevant_inv/3

is_syntactically_relevant_invariant_for_event/2

known_identifier/1

l_weigh_term/2

load_additional_information/1

load_additional_information_fact/1

minor_mode_to_check/0

operation_has_valid_read_modifies_infos/1

operation_has_valid_read_modifies_infos2/1

other_spec_precompile/0

parse_expression_raw_or_atom3/3

parse_expression_raw_or_atom_with_prob_ids/2

portray_defs/0

portray_filenumbers/0

precompile_operation_names_in_reverse_order/0

precompiled_predicate/1

precompiled_predicate_no_error_when_not_precompiled/1

precompiled_predicate_phase2/1

predicate_uses_variables/1

prime_variable/2

process_eventb_project_term/4

proof_status_for_inv2/4

read_eventb_project_from_file/6

read_eventb_project_from_stream/4

remove_weights/2

replace_prob_set_elements_in_scope/2

reset_filename_parsing_default/2

reset_temp_predicate/0

rewrite_complete_machine/3

safe_read/3

select_proven_invariants/4

set_additional_filename_as_parsing_default/3

set_all_used_filenames/1

set_stored_prefs/1

sort_properties/2

sorted_list_of_defs/3

source_code_for_definition/5

source_code_for_identifier/6

startup_precompiled/0

store_filenumbers/1

store_filenumbers/2

tcltk_get_proven_invariant_for_op/2

tcltk_get_specialized_invariant_for_op/2

tcltk_get_specialized_invariant_for_op_single/3

tcltk_get_specialized_invariants_for_ops/1

translate_any_into_parameters/3

translate_any_into_parameters_aux/5

translate_machine_to_classicalb/3

try_kodkod/0

type_check_definitions/0

type_check_definitions2/0

type_with_errors/4

type_with_errors_in_context/5

type_without_errors/4

typecheck_predicates/4

unify_args/3

useful_animation_expression/1

add_additional_filename/2

add_additional_property/2

add_all_perrors_in_context_of_used_filenames/2

add_discharged_po_infos/2

all_operations_have_valid_read_modifies_infos/0

apply_machine_transformations-->/2

apply_transformation_step/4

Meta: apply_transformation_step(*,2,*,*)

assert_bmachine_is_precompiled/0

Description:
generate_specialized_invariants/0, %% no longer exists

assert_main_machine/1

assert_temp_typed_predicate/1

Description:
set a temporary predicate as additional guard

auto_precompile/0

auto_precompile2/3

auto_precompile_phase2/0

b_absolute_file_name_relative_to_main_machine/2

b_definition_prefixed/5

b_enumerated_sets_precompiled_calc/0

b_extract_values_clause_assignment_calc/3

b_find_operation/5

b_get_abstract_events/3

b_get_all_used_filenames/1

Dynamic: true

b_get_all_used_identifiers_calc/1

b_get_all_used_identifiers_in_section_calc/2

b_get_animated_sections/1

b_get_assertion_count/3

b_get_assertions/3

b_get_assertions_from_main_machine_calc/2

b_get_constant_represented_inside_global_set_calc/2

b_get_constant_variable_description_calc/2

b_get_definition/5

b_get_definition_string_from_machine/2

b_get_definition_string_from_machine_calc/3

b_get_definition_with_pos/6

b_get_disjoint_constants_of_type_calc/3

b_get_dynamic_assertions_from_machine_calc/1

b_get_initialisation_from_machine_calc/2

b_get_internal_prolog_representation_as_codes/1

b_get_invariant_from_machine_calc/1

b_get_linking_invariant_from_machine_calc/1

b_get_machine_all_constants_calc/1

b_get_machine_animation_expression_calc/2

b_get_machine_animation_function_calc/2

b_get_machine_constants_calc/1

b_get_machine_custom_edges_function_calc/2

b_get_machine_custom_graph_function_calc/2

b_get_machine_custom_nodes_function_calc/2

b_get_machine_goal_calc/1

b_get_machine_header_position/2

b_get_machine_heuristic_function_calc/1

b_get_machine_operation/4

b_get_machine_operation_calc/6

b_get_machine_operation_for_animation/6

b_get_machine_operation_for_animation_calc/7

b_get_machine_operation_max_calc/2

b_get_machine_operation_parameter_names/2

b_get_machine_operation_parameter_types/2

b_get_machine_operation_result_names/2

b_get_machine_operation_signature/2

b_get_machine_operation_typed_parameters/2

b_get_machine_operation_typed_parameters_aux/2

b_get_machine_operation_typed_results/2

b_get_machine_refinement_hierarchy/1

b_get_machine_searchscope_calc/1

b_get_machine_set/1

b_get_machine_set_calc/2

b_get_machine_setscope_calc/2

b_get_machine_variables_calc/1

b_get_machine_variables_in_original_order_calc/1

b_get_model_type/1

b_get_named_machine_set/2

b_get_named_machine_set_calc/3

b_get_operation_description/2

b_get_operation_non_det_modifies_calc/2

b_get_operation_normalized_read_write_info_calc/3

b_get_operation_pos/2

b_get_operation_unchanged_variables_calc/2

Description:
, print(read_write_set(Event,ReadVariables,WrittenVariables)),nl.

b_get_operation_variant/3

b_get_promoted_machine_operations_calc/1

b_get_properties_from_machine_calc/1

b_get_refined_ancestors_names/1

b_get_refined_machine/1

b_get_refined_machine_name/1

b_get_static_assertions_from_machine_calc/1

b_get_true_expression_definition/1

b_get_typed_definition/3

b_get_typed_expression_definition/3

b_get_typed_predicate_definition/3

b_get_unproven_dynamic_assertions_from_machine_calc/1

b_get_unproven_static_assertions_from_machine_calc/1

b_invariant_number_list_calc/1

b_is_constant/1

b_is_constant_calc/2

b_is_initialisation_name/1

b_is_operation_name_calc/1

b_is_unused_constant_calc/1

b_is_variable/1

b_is_variable_calc/2

b_limit_abstract_level_to_zero/2

b_load_eventb_project/1

b_load_machine_from_file/1

b_load_machine_from_file/2

b_load_machine_from_list_of_facts/2

b_load_machine_from_term/2

b_load_machine_probfile/1

b_load_machine_probfile/2

b_machine_clear/0

b_machine_has_assertions/0

b_machine_has_constants/0

b_machine_has_constants_or_properties/0

b_machine_has_dynamic_assertions_calc/0

b_machine_has_operations/0

b_machine_has_proven_invariants/0

b_machine_has_static_assertions_calc/0

b_machine_has_unproven_assertions/0

b_machine_has_variables/0

b_machine_is_loaded/0

b_machine_name_calc/1

b_machine_precompile/0

b_machine_reset/0

b_machine_statistics_calc/2

b_main_machine_has_no_assertions/0

b_nth1_invariant_calc/3

b_operation_cannot_modify_state_calc/1

b_operation_preserves_full_invariant/1

b_operation_preserves_invariant_calc/2

b_operation_reads_output_variables_calc/3

b_parse_machine_expression_from_codes/2

b_parse_machine_expression_from_codes/5

b_parse_machine_expression_from_codes/6

b_parse_machine_expression_from_codes4/4

b_parse_machine_expression_from_codes_with_prob_ids/2

b_parse_machine_expression_from_codes_with_prob_ids/3

b_parse_machine_expression_from_codes_with_prob_ids/4

b_parse_machine_formula/3

b_parse_machine_formula_from_codes/7

b_parse_machine_operation_pre_post_predicate/3

b_parse_machine_operation_pre_post_predicate/5

b_parse_machine_predicate/2

b_parse_machine_predicate/3

b_parse_machine_predicate_from_codes/3

b_parse_machine_predicate_from_codes2/5

b_parse_machine_predicate_from_codes_open/5

b_parse_machine_subsitutions_from_codes/6

b_parse_only/5

b_parse_optional_machine_predicate/2

b_parse_predicate/3

b_parse_wo_type_machine_predicate_from_codes_to_raw_expr/2

b_reset_filenames_and_numbers/0

b_reset_machine_goal_from_DEFINITIONS/0

b_set_empty_machine/0

b_set_eventb_project_flat/3

b_set_initial_machine/0

b_set_machine/3

Description:
get_memory_used(M1), %%
, get_memory_used(M2),print_memory_used(M2), print_memory_used_difference(M1,M2),nl %%

b_set_machine_goal/1

b_set_machine_goal/2

b_set_machine_searchscope/1

b_set_machine_searchscope/2

b_set_parsed_typed_machine_goal/1

b_set_parsed_typed_machine_searchscope/1

b_set_to_level_zero/2

b_set_typed_machine/2

b_show_eventb_as_classicalb/2

b_show_eventb_as_classicalb1/3

b_show_machine_representation/4

b_show_machine_representation_unicode/4

b_sorted_b_definition_prefixed/4

b_specialized_invariant_for_op_calc/2

b_specialized_invariant_mask_for_op_calc/2

b_top_level_feasible_operation_calc/1

b_top_level_operation_calc/1

b_type_check_raw_expr/4

b_type_expression/5

b_type_expression_for_full_b_machine/6

b_type_expressions_l/6

b_type_literal/3

b_type_only/5

b_type_open_exists_predicate/3

b_type_open_predicate/5

b_type_open_predicate_for_full_b_machine/6

b_type_open_predicate_with_errors/4

b_unset_machine_goal/0

b_write_eventb_machine_to_classicalb_to_file/1

b_write_machine_representation_to_file/2

b_write_machine_representation_to_file/3

b_write_machine_representation_to_file3/3

check_valid_machine_name/1

check_wd_discharged_inv_or_thm/4

check_write/2

clear_wp/0

comparison/3

complete_discharged_info2/0

complete_discharged_info3/3

complete_discharged_info_calc/0

constant_variable_marked_as_expand/1

constant_variable_marked_as_memo/1

determine_type_of_formula/2

determine_type_of_formula/3

determine_type_of_formula2/2

discharged_info_exists/0

discharged_invariant/3

do_machine_consistency_check/0

empty/1

empty_machine/2

eventb_load_command/5

extension_kind/2

extract_id_and_pp_type/2

filter_out_proven_assertions/2

filter_syntactically_relevant_invariants/4

filter_syntactically_relevant_invariants2/4

find_constants_of_type/4

find_id_uses_for_maplist/2

find_main_file_name/3

find_used_identifier_in_machine_section/3

flexible_atom_codes/2

full_b_machine/1

gen_couple_from_list/2

generate_no_parse_errors/1

generate_parse_errors_for/2

get_all_assertions_from_machine/1

get_animation_image/2

get_animation_image_source_file/2

get_assertions_from_machine/2

get_bottom_event/2

get_constant_definition/2

get_constant_predicate/2

get_constant_span/2

get_constant_type_and_origin/4

get_definition_with_nr_suffix/3

get_full_b_machine/2

get_full_b_machine_sha_hash/1

get_goal/1

get_invariant_list_with_proof_info/1

get_invariant_list_with_used_ids/2

get_invariant_with_proof_status_calc/2

get_machine_file_number/4

get_machine_identifiers/2

Description:
mode get_machine_identifiers(+Category, -ListOfIdentifiers)

get_machine_identifiers_with_pp_type/2

get_machine_operation_additional_identifiers/2

get_machine_operation_typing_scope/3

get_modifies_from_info/2

get_multi_sections/2

get_nr_of_machine_constants/1

get_nr_of_machine_variables/1

get_op_desc_template_expr_calc2/2

get_op_or_init_and_syntax_filter/5

get_operation_description_template_expr_calc/2

get_operation_info_calc/2

get_operation_type/4

get_primed_machine_variables/1

get_proven_invariant_calc/2

get_proz_animation_function/3

get_proz_settings/1

get_section_from_current_machine/2

get_tc_scope/2

get_unproven_invariants/1

get_variable_type_and_origin/4

initial_machine(phonebook,[M]) :-
    M = abstract_machine(none,machine(none),machine_header(none,phonebook,[]),Body),
    Body = [sets(none, [deferred_set(none,'Name'),
    deferred_set(none,'Code')]),
    definitions(none,[ScopeName,ScopeCode,TraceTest0]),
    variables(none, [identifier(none, db)]),
    invariant(none, member(none,
    identifier(none, db),
    partial_function(none,
    identifier(none, 'Name'),
    identifier(none, 'Code')))),
    initialisation(none,
    assign(none, [identifier(none, db)], [empty_set(none)])),
    operations(none, [Add,Lookup,Update,Reset])],

    % definitions
    ScopeName = expression_definition(none,
    scope_Name,
    [],
    interval(none, integer(none, 1), integer(none, 3))),
    ScopeCode = expression_definition(none,
    scope_Code,
    [],
    interval(none, integer(none, 1), integer(none, 2))),
    TraceTest0 = expression_definition(none, trace_Test0, [], empty_sequence(none)),

    % add operation
    Add = operation(none,
    identifier(none, add),
    [],
    [identifier(none,cc),identifier(none,nn)],
    precondition(none, AddPre, AddAssign)),
    AddPre = conjunct(none,
    conjunct(none,
    member(none, identifier(none,nn), identifier(none,'Name')),
    member(none, identifier(none,cc), identifier(none,'Code'))),
    not_member(none,
    identifier(none,nn),
    domain(none, identifier(none,db)))),
    AddAssign = assign(none,
    [identifier(none,db)],
    [union(none,
    identifier(none,db),
    set_extension(none,
    [couple(none,[identifier(none,nn),
    identifier(none,cc)])]))]),

    % lookup operation
    Lookup = operation(none,
    identifier(none, lookup),
    [identifier(none, cc)],
    [identifier(none, nn)],
    precondition(none, LookupPre, LookupAssign)),
    LookupPre = member(none, identifier(none,nn), domain(none,identifier(none,db))),
    LookupAssign = assign(none,
    [identifier(none, cc)],
    [function(none, identifier(none, db), identifier(none, nn))]),

    % update operation
    Update = operation(none,
    identifier(none, update),
    [],
    [identifier(none,nn),identifier(none,cc)],
    precondition(none, UpdatePre, UpdateAssign)),
    UpdatePre = conjunct(none,
    conjunct(none,
    member(none, identifier(none,nn), identifier(none,'Name')),
    member(none, identifier(none,cc), identifier(none,'Code'))),
    member(none,
    identifier(none,nn),
    domain(none, identifier(none,db)))),
    UpdateAssign = assign(none,
    [function(none, identifier(none,db), identifier(none,nn))],
    [identifier(none, cc)]),

    % reset operation
    Reset = operation(none,
    identifier(none,reset),
    [],
    [],
    precondition(none, ResetPre, ResetAssign)),
    ResetPre = member(none,
    identifier(none, db),
    total_function(none, identifier(none,'Name'), identifier(none,'Code'))),
    ResetAssign = assign(none,[identifier(none,db)],[empty_set(none)]).

invalid_chars/1

invariant_proof_status_for_event/4

involves_id/2

involves_id_aux/2

is_abstract_event_in_list/3

is_discharged_assertion/1

is_empty_string/1

is_empty_string2/1

is_ground/2

is_initialisation_op/1

is_not_main_assertion/1

is_precompiled_predicate/1

is_proven_invariant/2

Description:
print('DISCHARGED'(Model,Event,Name)),nl.

is_proven_invariant_for_model/3

is_syntactically_relevant_inv/3

is_syntactically_relevant_invariant_for_event/2

known_identifier/1

l_weigh_term/2

load_additional_information/1

load_additional_information_fact/1

load_additional_information_fact(discharged(Machine,Theorem)) :- % a discharged theorem
    debug_println(9,discharged_theorem(Machine,old_style_proof_info,Theorem)),
    assertz(discharged_theorem(Machine,invariant,Theorem)).

load_additional_information_fact(discharged(Machine,Event,Invariant)) :-
    debug_println(9,discharged(Machine,Event,Invariant)),
    assertz(discharged(Machine,Event,Invariant)).

load_additional_information_fact(Term) :- % theories are handled in bmachine_eventb.pl already
    is_eventb_additional_info(Term).

load_additional_information_fact(po(Machine,'Invariant preservation',Source,true)) :- % invariant preservation
    add_discharged_po_infos(Source,Machine).

load_additional_information_fact(po(Machine,'Invariant establishment',Source,true)) :- % invariant establishment
    add_discharged_po_infos(Source,Machine).

load_additional_information_fact(po(Machine,Text,Source,Proven)) :- % invariant or theorem wd
    ( Text = 'Well-definedness of Invariant'
    ; Text = 'Well-definedness of Theorem'),
    member(invariant(Invariant),Source),
    debug_println(9,wd_po(Machine,Invariant,Proven)),
    assertz(wd_po(Machine,Invariant,Proven)).

load_additional_information_fact(po(Machine,Text,Source,Proven)) :- % axiom or axiom theorem wd
    ( Text = 'Well-definedness of Axiom'
    ; Text = 'Well-definedness of Theorem'),
    member(axiom(Axiom),Source),
    debug_println(9,wd_axiom(Machine,Axiom,Proven)). % TO DO: assert and use

load_additional_information_fact(po(Machine,Text,Source,Proven)) :- % proven theorem as guard
    Text = 'Well-definedness of Theorem',
    member(guard(Grd),Source),
    member(event(Evt),Source),
    debug_println(9,wd_axiom(Machine,Evt/Grd,Proven)). % TO DO: assert and use

load_additional_information_fact(po(Machine,Text,Source,Proven)) :- % wd of action
    Text = 'Well-definedness of action',
    (member(action(ACT),Source) % probably the guard in the last event with discharged info ??
    -> debug_println(9,wd_action(Machine,ACT,Proven)) % TO DO: assert and use, if false: discard proven invariants?!
    ; format('Illegal Rodin PO source in ~w for ~w: ~w~n',[Machine,Text,Source])
).

load_additional_information_fact(po(Machine,Text,Source,Proven)) :- % wd of guard
    Text = 'Well-definedness of Guard',
    (member(guard(GRD),Source) % probably the guard in the last event with discharged info ??
    -> debug_println(9,wd_guard(Machine,GRD,Proven)) % TO DO: assert and use
    ; format('Illegal Rodin PO source in ~w for ~w: ~w~n',[Machine,Text,Source])
).

load_additional_information_fact(po(Machine,'Theorem',[invariant(Theorem)],true)) :- % a theorem
    debug_println(9,discharged_theorem(Machine,invariant,Theorem)),
    assertz(discharged_theorem(Machine,invariant,Theorem)).

load_additional_information_fact(po(Machine,'Theorem',[axiom(Theorem)],true)) :- % a theorem
    debug_println(9,discharged_theorem(Machine,axiom,Theorem)),
    assertz(discharged_theorem(Machine,axiom,Theorem)).

load_additional_information_fact(po(Machine,'Theorem',[guard(GuardTheorem),event(Event)],true)) :- % a theorem in a guard
    debug_println(9,discharged_theorem(Machine,guard(Event),GuardTheorem)),
    assertz(discharged_theorem(Machine,guard(Event),GuardTheorem)).

load_additional_information_fact(po(Machine,Text,Infos,Proven)) :-
    ( Text = 'Guard strengthening (split)'
    ; Text = 'Guard strengthening (merge)'
    ; Text = 'Guard strengthening' ),
    !,
    (Proven=true, Infos = [event(AbsEvent),guard(Guard),event(ConcreteEvent)]
    -> assertz(discharged_guard_strengthening(Machine,AbsEvent,Guard,ConcreteEvent)),
    debug_println(19,discharged_guard_strengthening(Machine,AbsEvent,Guard,ConcreteEvent))
    ; true
).

load_additional_information_fact(po(_,'Variant of event',_,_)).

load_additional_information_fact(po(_,'Natural number variant of event',_,_)).

load_additional_information_fact(po(_,'Action simulation',_,_)).

load_additional_information_fact(po(_,'Feasibility of witness',_,_)).

load_additional_information_fact(po(_,'Feasibility of action',_,_)).

load_additional_information_fact(po(_,'Well-definedness of witness',_,_)).

load_additional_information_fact(po(_,'Well-definedness of variant',_,_)).

load_additional_information_fact(po(_,'Finiteness of variant',_,_)).

load_additional_information_fact(po(_,'Equality of common variables',_,_)).

load_additional_information_fact(po(_Machine,_Kind,_Source,false)). % ignore everything that is not proven

load_additional_information_fact(po(_Machine,_Kind,_Source,reviewed)). % ignore everything that is only reviewed

load_additional_information_fact(exporter_version(V)) :- V=2 ; V=3.

load_additional_information_fact(pragma(_Type,_Source,_AttachedTo,_Content)).

load_additional_information_fact(wp(S,D,P)) :-
    assertz( wp_untyped(S,D,P) ).

load_additional_information_fact(nonchanging_guard(E,P)) :-
    typecheck_predicates(P,TypedPred,E,_),
    assertz(nonchanging_guard(E,TypedPred)).

load_additional_information_fact(invariant(_I)). %ignore

minor_mode_to_check/0

operation_has_valid_read_modifies_infos/1

operation_has_valid_read_modifies_infos2/1

other_spec_precompile/0

parse_expression_raw_or_atom3/3

parse_expression_raw_or_atom_with_prob_ids/2

portray_defs/0

portray_filenumbers/0

precompile_operation_names_in_reverse_order/0

precompiled_predicate/1

precompiled_predicate(b_machine_name/1).

precompiled_predicate(b_get_named_machine_set/3).

precompiled_predicate(b_enumerated_sets_precompiled/0).

precompiled_predicate(b_get_properties_from_machine/1).

precompiled_predicate(b_get_machine_all_constants/1).

precompiled_predicate(b_get_machine_set/2).

precompiled_predicate(b_get_disjoint_constants_of_type/3).

precompiled_predicate(b_get_constant_represented_inside_global_set/2).

precompiled_predicate(b_get_machine_constants/1).

precompiled_predicate(b_get_machine_variables_in_original_order/1).

precompiled_predicate(b_get_machine_variables/1).

precompiled_predicate(b_get_invariant_from_machine/1).

precompiled_predicate(b_get_linking_invariant_from_machine/1).

precompiled_predicate(b_is_constant/2).

precompiled_predicate(b_is_variable/2).

precompiled_predicate(b_get_constant_variable_description/2).

precompiled_predicate(b_get_static_assertions_from_machine/1).

precompiled_predicate(b_machine_has_static_assertions/0).

precompiled_predicate(b_get_unproven_static_assertions_from_machine/1).

precompiled_predicate(b_get_dynamic_assertions_from_machine/1).

precompiled_predicate(b_machine_has_dynamic_assertions/0).

precompiled_predicate(b_get_unproven_dynamic_assertions_from_machine/1).

precompiled_predicate(b_get_assertions_from_main_machine/2).

precompiled_predicate(b_get_initialisation_from_machine/2).

precompiled_predicate(b_get_machine_operation/6).

precompiled_predicate(b_top_level_operation/1).

precompiled_predicate(b_is_operation_name/1).

precompiled_predicate(b_top_level_feasible_operation/1).

precompiled_predicate(b_get_promoted_machine_operations/1).

precompiled_predicate(get_operation_info/2).

precompiled_predicate(b_get_machine_operation_for_animation/7).

precompiled_predicate(get_operation_description_template_expr/2).

precompiled_predicate(b_get_machine_goal/1).

precompiled_predicate(b_get_machine_setscope/2).

precompiled_predicate(b_get_machine_operation_max/2).

precompiled_predicate(b_get_machine_searchscope/1).

precompiled_predicate(b_get_definition_string_from_machine/3).

precompiled_predicate(b_get_machine_animation_function/2).

precompiled_predicate(b_get_machine_heuristic_function/1).

precompiled_predicate(b_get_machine_animation_expression/2).

precompiled_predicate(b_get_machine_custom_nodes_function/2).

precompiled_predicate(b_get_machine_custom_edges_function/2).

precompiled_predicate(b_get_machine_custom_graph_function/2).

precompiled_predicate(complete_discharged_info/0). % just call it before calling b_specialized_invariant_for_op_calc !

precompiled_predicate(get_proven_invariant/2).

precompiled_predicate(b_nth1_invariant/3).

precompiled_predicate(b_invariant_number_list/1).

precompiled_predicate(b_specialized_invariant_mask_for_op/2).

precompiled_predicate(b_specialized_invariant_for_op/2).

precompiled_predicate(b_operation_preserves_invariant/2).

precompiled_predicate(b_get_all_used_identifiers_in_section/2).

precompiled_predicate(b_get_all_used_identifiers/1).

precompiled_predicate(b_is_unused_constant/1).

precompiled_predicate(b_extract_values_clause_assignment/3). % depends on b_is_constant/1

precompiled_predicate(b_machine_statistics/2).

precompiled_predicate_no_error_when_not_precompiled/1

precompiled_predicate_phase2/1

predicate_uses_variables/1

prime_variable/2

process_eventb_project_term/4

proof_status_for_inv2/4

read_eventb_project_from_file/6

read_eventb_project_from_stream/4

remove_weights/2

replace_prob_set_elements_in_scope/2

reset_filename_parsing_default/2

reset_temp_predicate/0

rewrite_complete_machine/3

safe_read/3

select_proven_invariants/4

set_additional_filename_as_parsing_default/3

set_all_used_filenames/1

set_stored_prefs/1

sort_properties/2

sorted_list_of_defs/3

source_code_for_definition/5

source_code_for_identifier/6

source_code_for_identifier(ID,constant,Type,OriginStr,OriginTerm,Source) :- b_is_constant(ID),!,
    get_constant_type_and_origin(ID,Type,OriginStr,OriginTerm),
    findall(Def,get_constant_definition(ID,Def),AllDefs),
    (AllDefs=[_|_] -> conjunct_predicates(AllDefs,Source)
    ; % try and find other type of predicates defining ID
    findall(Pred,get_constant_predicate(ID,Pred),AllPreds),
    conjunct_predicates(AllPreds,Source)).

source_code_for_identifier(ID,variable,Type,OriginStr,OriginTerm,Source) :- b_is_variable(ID),!,
    get_variable_type_and_origin(ID,Type,OriginStr,OriginTerm),
    Source = b(truth,pred,[]). % TO DO: improve

source_code_for_identifier(ID,Kind,Type,OriginStr,OriginTerm,Source) :- b_get_machine_set(ID,TID),!,
    (b_global_deferred_set(ID) -> Kind = deferred_set ; Kind = enumerated_set),
    Type = set(global(ID)),
    all_elements_of_type(ID,All),
    translate:translate_span_with_filename(TID,OriginStr), OriginTerm=TID,
    Source = b(equal(TID,b(value(All),Type,[])),pred,[]).

source_code_for_identifier(ID,Kind,Type,OriginStr,OriginTerm,Source) :-
    global_set_element(ID,GID),!,
    (b_global_deferred_set(GID)
    -> Kind = deferred_set_element ; Kind = enumerated_set_element),
    b_get_machine_set(GID,TGID),
    Type = global(ID),
    all_elements_of_type(GID,All),
    translate:translate_span_with_filename(TGID,OriginStr), OriginTerm=TGID,
    Source = b(equal(TGID,b(value(All),set(Type),[])),pred,[]).

source_code_for_identifier(ID,definition,Type,OriginStr,OriginTerm,Source) :-
    b_get_definition(ID,DefType,Args,RawExpr,_Deps),!,
    Type = DefType,
    % Definitions are only present in RAW form
    get_raw_position_info(RawExpr,PosInfo),
    translate:translate_span_with_filename(PosInfo,OriginStr), % the position info does not always seem to be valid (when coming from DEFINITION FILE) !??! TO DO fix
    OriginTerm=PosInfo,
    source_code_for_definition(DefType,ID,Args,RawExpr,Source).

source_code_for_identifier(ID,file,Type,OriginStr,OriginTerm,b(string(Source),string,[])) :-
    b_filenumber(ID,Kind,_,Filename),
    extension_kind(Kind,Type),
    !,
    ajoin([Type,' ',ID],Source),
    OriginTerm =src_position_with_filename(1,0,0,Filename),
    OriginStr = Filename.

source_code_for_identifier(ID,Kind,subst,OriginStr,OriginTerm,Source) :-
    b_find_operation(ID,Res,TParas,Body,OType),
    (OType=classic -> Kind = operation ; Kind=event),
    translate:translate_span_with_filename(Body,OriginStr),Body=OriginTerm,
    get_texpr_info(Body,Info),
    Source=b(operation(b(identifier(ID),subst,[]),Res,TParas,Body),subst,Info).

source_code_for_identifier(ID,assertion,pred,OriginStr,OriginTerm,Assertion) :-
    b_get_assertions(all,_,Ass), member(Assertion,Ass),
    get_texpr_label(Assertion,ID), OriginTerm = Assertion,
    translate:translate_span_with_filename(Assertion,OriginStr).

source_code_for_identifier(ID,invariant,pred,OriginStr,OriginTerm,Invariant) :-
    b_get_invariant_from_machine(C), conjunction_to_list(C,L), member(Invariant,L),
    get_texpr_label(Invariant,ID), OriginTerm = Invariant,
    translate:translate_span_with_filename(Invariant,OriginStr).

startup_precompiled/0

store_filenumbers/1

store_filenumbers/2

tcltk_get_proven_invariant_for_op/2

tcltk_get_specialized_invariant_for_op/2

tcltk_get_specialized_invariant_for_op_single/3

tcltk_get_specialized_invariants_for_ops/1

translate_any_into_parameters/3

translate_any_into_parameters_aux/5

translate_machine_to_classicalb/3

try_kodkod/0

type_check_definitions/0

type_check_definitions2/0

type_with_errors/4

type_with_errors_in_context/5

type_without_errors/4

typecheck_predicates/4

unify_args/3

useful_animation_expression/1

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_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),_80941,[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'),_50667,[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),_43713,[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),_42049,[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(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_44901,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_records.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file covsrc(coverage_tools_annotations) does not exist
! goal: absolute_file_name(covsrc(coverage_tools_annotations),_136843,[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 extension('random_permutations/random_permutations') does not exist
! goal: absolute_file_name(extension('random_permutations/random_permutations'),_136843,[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 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),_161987,[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),_164131,[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),_170109,[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 prob_rewrite_rules(b_ast_cleanup_rewrite_rules) does not exist
! goal: absolute_file_name(prob_rewrite_rules(b_ast_cleanup_rewrite_rules),_170251,[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 extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_175519,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/state_space.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(external_functions_reals) does not exist
! goal: absolute_file_name(extrasrc(external_functions_reals),_174755,[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),_174755,[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 chrsrc(chr_integer_inequality) does not exist
! goal: absolute_file_name(chrsrc(chr_integer_inequality),_176051,[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),_175377,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_z.pl')])
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(atts))
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_176371,[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),_170109,[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_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),_193137,[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),_187443,[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 argument 1 of absolute_file_name/3
! file probsrc(avl_tools) does not exist
! goal: absolute_file_name(probsrc(avl_tools),_170531,[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'),_183045,[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),_182899,[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'),_186179,[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'),_183045,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/value_persistance.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(btypechecker) does not exist
! goal: absolute_file_name(probsrc(btypechecker),_170819,[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'),_170531,[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),_164131,[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),_161987,[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(custom_explicit_sets) does not exist
! goal: absolute_file_name(probsrc(custom_explicit_sets),_161987,[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),_136843,[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 extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_111131,[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),_106005,[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),_102583,[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),_73601,[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 probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_73747,[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 probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_68795,[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(gensym) does not exist
! goal: absolute_file_name(probsrc(gensym),_44613,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/translate.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_state_model_check) does not exist
! goal: absolute_file_name(probsrc(b_state_model_check),_44759,[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(bmachine_eventb) does not exist
! goal: absolute_file_name(probsrc(bmachine_eventb),_37787,[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),_37787,[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),_39167,[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),_37787,[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),_37907,[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),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine.pl')])

Name: format/2
Name: is/2
Name: b_get_all_used_filenames/1	Module: bmachine
Name: assert/1
Name: append/3
Name: length/2
Name: retract/1
Name: =/2
Name: !
Name: nth1/3	Module: foo_error
Name: functor/3

Name: assertz/1
Name: add_texpr_info_if_new/3	Module: foo_error
Name: b_parse_machine_predicate/2	Module: bmachine
Name: format/2

Name: add_all_perrors/3	Module: foo_error
Name: debug_println/2	Module: foo_error
Name: true
Name: =/2
Name: ->/3
Name: !
Name: \=/2
Name: b_get_all_used_filenames/1	Module: bmachine

Name: fail
Name: assertz/1
Name: debug_println/2	Module: foo_error
Name: member/2
Name: get_bottom_event/2	Module: bmachine

Name: fail
Name: operation_has_valid_read_modifies_infos/1	Module: bmachine
Name: b_is_operation_name/1	dynamic predicate

Name: set_additional_filename_as_parsing_default/3	Module: bmachine
Name: b_parse_only/5	Module: bmachine

Name: type_with_errors_in_context/5	Module: bmachine
Name: type_check_definitions2/0	Module: bmachine

Name: =/2
Name: add_error/2	Module: foo_error
Name: ajoin/2	Module: foo_error
Name: true
Name: call/3
Name: ->/3

Name: auto_precompile/0	Module: bmachine
Name: other_spec_precompile/0	Module: bmachine

Name: fail
Name: add_internal_error/2	Module: foo_error
Name: assertz/1
Name: !
Name: =/2
Name: nonvar/1

Name: execute_custom_operations/6	Module: eclipse_interface
Name: prob2_execute_custom_operation_with_predicate_aux/5	Module: prob2_interface
Name: assert_temp_predicate_with_prob_def_set_elements/1	Module: tcltk_interface

Name: debug_println/2	Module: foo_error
Name: assert_bmachine_is_precompiled/0	Module: bmachine
Name: fail
Name: assertz/1
Name: true
Name: call/1
Name: ->/3
Name: auto_precompile2/3	Module: bmachine
Name: precompiled_predicate/1	Module: bmachine

Name: call/1
Name: retractall/1
Name: unify_args/3	Module: bmachine
Name: functor/3
Name: atom_concat/3

Name: auto_precompile_phase2/0	Module: bmachine
Name: auto_precompile/0	Module: bmachine

Name: extended_static_check_visb_file/2	Module: visb_visualiser
Name: load_visb_file/1	Module: visb_visualiser

Name: b_get_machine_setscope_calc/2	Module: bmachine
Name: b_get_machine_animation_expression_calc/2	Module: bmachine
Name: b_get_set_pref_definition/4	Module: pref_definitions
Name: print_seq_chart_transition/2	Module: uml_generator
Name: b_get_machine_operation_max_calc/2	Module: bmachine
Name: get_operation_read_projection_infos/6	Module: b_operation_cache
Name: get_ltl_formula_string/2	Module: ltl

Name: fail
Name: add_error/4	Module: foo_error
Name: add_warning/4	Module: foo_error
Name: ajoin/2	Module: foo_error
Name: pretty_type/2	Module: translate
Name: b_is_constant/2	dynamic predicate
Name: ->/3
Name: add_message/4	Module: foo_error
Name: lookup_global_constant/2	Module: b_global_sets
Name: b_get_constant_represented_inside_global_set/2	dynamic predicate
Name: true
Name: b_get_machine_set/1	Module: bmachine
Name: b_extract_values_clause_assignment/3	dynamic predicate
Name: assertz/1
Name: debug_mode/1	Module: foo_error
Name: safe_create_texpr/4	Module: bsyntaxtree
Name: =/2
Name: member/2
Name: unify_types_strict/2	Module: btypechecker
Name: debug_println/2	Module: foo_error
Name: get_texpr_type/2	Module: bsyntaxtree
Name: get_texpr_id/2	Module: bsyntaxtree
Name: get_section_from_current_machine/2	Module: bmachine

Name: =/2
Name: get_texpr_expr/2	Module: foo_error
Name: b_get_machine_operation/6	dynamic predicate

Name: complete_discharged_info2/0	Module: bmachine
Name: complete_discharged_info3/3	Module: bmachine

Name: get_filename/2	Module: error_manager
Name: add_additional_filename/2	Module: bmachine
Name: add_all_perrors_in_context_of_used_filenames/2	Module: bmachine
Name: b_machine_statistics_calc/2	Module: bmachine
Name: cli_print_machine_info/1	Module: prob_cli

Name: sort/2
Name: findall/3
Name: member/2
Name: full_b_machine/1	Module: bmachine

Name: zmq_start_master/2	Module: prob_cli
Name: b_get_assertion_count/3	Module: bmachine
Name: source_code_for_identifier/6	Module: bmachine
Name: we_need_only_static_assertions/1	Module: prob_cli

Name: get_texpr_description/2	Module: foo_error
Name: member/2
Name: get_texpr_id/2	Module: bsyntaxtree
Name: b_get_machine_variables/1	dynamic predicate
Name: b_get_machine_constants/1	dynamic predicate

Name: dot_def_trans/5	Module: visualize_graph
Name: source_code_for_identifier/6	Module: bmachine
Name: dot_def_node/6	Module: visualize_graph
Name: b_get_definition_string_from_machine_calc/3	Module: bmachine
Name: b_get_typed_definition/3	Module: bmachine
Name: process_json_def_lst/2	Module: visb_visualiser
Name: print_seq_chart_transition/2	Module: uml_generator
Name: b_get_typed_predicate_definition/3	Module: bmachine
Name: dot_def_subgraph/3	Module: visualize_graph
Name: b_get_typed_expression_definition/3	Module: bmachine
Name: get_definition_with_nr_suffix/3	Module: bmachine

Name: type_check_definitions2/0	Module: bmachine
Name: b_get_click_subst_definition/4	Module: graphical_state_viewer_images
Name: b_get_definition/5	Module: bmachine
Name: portray_defs/0	Module: bmachine
Name: print_defs_as_json/0	Module: translate
Name: b_definition_prefixed/5	Module: bmachine

prob_prolog/src/bmachine.pl

Modules

Predicates of bmachine

Module Information

3228 Lines

342 Predicates

Imported Modules: lists ordsets self_check error_manager debug bsyntaxtree parsercall tools b_machine_hierarchy debug specfile state_packing

204 Exports

81 specified Imports

Predicates:

Name: =/2
Name: get_operation_type/4	Module: bmachine
Name: get_texpr_expr/2	Module: foo_error
Name: ->/3
Name: get_section_from_current_machine/2	Module: bmachine

Name: get_single_transition_predicate/2	Module: predicate_handling
Name: get_weakest_precondition_aux/3	Module: prob2_interface
Name: b_get_operation_variant/3	Module: bmachine
Name: build_up_b_operation_for_csp/3	Module: specfile
Name: preprocess_tp/2	Module: ltl_tools
Name: lookup_operation/4	Module: weakest_preconditions
Name: before_after_predicate_no_equalities_aux/3	Module: before_after_predicates
Name: cse_optimize_operation/1	Module: b_expression_sharing
Name: compute_enabling_predicate/5	Module: enabling_predicates
Name: b_get_read_may_must_write/3	Module: b_read_write_info
Name: execute_operation/4	Module: enable_graph
Name: parameter_values/2	Module: ltl_propositions
Name: typecheck_tp/3	Module: ltl_tools
Name: machine_operation_uses_parameters/2	Module: b_synthesis
Name: before_after_predicate_for_operation_no_equalities/5	Module: before_after_predicates
Name: get_line_amount/4	Module: constraints
Name: get_operation_parameters_constraint/3	Module: constraints
Name: before_after_predicate_for_operation/2	Module: before_after_predicates
Name: b_get_machine_operation_with_local_paras/3	Module: b_read_write_info
Name: get_operation_guard/3	Module: b_read_write_info

Name: =/2
Name: cse_optimize_substitution/2	Module: foo_error
Name: debug_println/2	Module: foo_error
Name: animation_minor_mode/1	Module: specfile
Name: not/1
Name: get_preference/2	Module: preferences
Name: ->/3
Name: true
Name: get_texpr_pos/2	Module: foo_error
Name: get_operation_type/4	Module: bmachine
Name: !
Name: ==/2
Name: member/2
Name: get_texpr_id/2	Module: bsyntaxtree
Name: get_texpr_expr/2	Module: foo_error
Name: get_section_from_current_machine/2	Module: bmachine
Name: is_ground/2	Module: bmachine

Name: get_operation_propositional_guards/3	Module: b_operation_guards
Name: b_compile2/8	Module: b_compiler
Name: setup_local_state_for_operation/4	Module: b_state_model_check
Name: action_dependent_to_itself/4	Module: static_analysis
Name: get_operation_enabling_condition2/4	Module: b_operation_guards
Name: get_operation_enabling_condition/7	Module: b_operation_guards
Name: get_operation/3	Module: b_read_write_info
Name: build_up_b_real_operation/2	Module: specfile

Name: get_texpr_ids/2	Module: foo_error
Name: b_get_machine_operation_typed_parameters/2	Module: bmachine
Name: RECURSIVE_CALL/2	Module: bmachine

Name: decompose_operation2/3	Module: b_intelligent_trace_replay
Name: translate_json_operation/2	Module: b_trace_checking

Name: maplist/3	Module: foo_error
Name: b_get_machine_operation_typed_parameters/2	Module: bmachine

Name: ajoin/2	Module: foo_error
Name: ajoin_with_sep/3	Module: foo_error
Name: get_texpr_ids/2	Module: foo_error
Name: =/2
Name: ->/3
Name: b_get_machine_operation_calc/6	Module: bmachine

Name: perform_custom_operation_retry/2	Module: b_trace_checking
Name: b_get_machine_operation_parameter_types/2	Module: bmachine
Name: b_get_operation_typed_paras/2	Module: b_intelligent_trace_replay
Name: illegal_json_binding_type/4	Module: b_intelligent_trace_replay
Name: b_get_machine_operation_parameter_names/2	Module: bmachine

Name: b_get_operation_typed_results/2	Module: b_intelligent_trace_replay
Name: illegal_json_binding_type/4	Module: b_intelligent_trace_replay