bmachine

prob_prolog/src/bmachine.pl

Modules

  • ProB_Preferences_maxx.pl
  • TestPrefs.pl
  • alloy2b
  • alloy2b_benchmarks
  • ample_sets
  • any.pl
  • assert_profiler
  • ast_cleanup_for_smt
  • ast_inspector
  • ast_optimizer_for_smt
  • ast_to_difference_logic
  • atelierb_provers_interface
  • atom.pl
  • avl_custom
  • avl_tools
  • avl_tree.pl
  • avl_ugraphs
  • avlp
  • b2sat
  • b2setlog
  • b_arithmetic_expressions.pl
  • b_ast_cleanup
  • b_ast_cleanup_rewrite_rules
  • b_cogen
  • b_compiler
  • b_enumerate
  • b_enumeration_order_analysis
  • b_expression_sharing
  • b_global_sets
  • b_intelligent_trace_replay
  • b_interpreter
  • b_interpreter_components
  • b_interpreter_eventb
  • b_machine_identifier_normalization
  • b_operation_cache
  • b_operation_guards
  • b_read_write_info
  • b_show_history
  • b_simplifier
  • b_state_model_check
  • b_synthesis
  • b_to_cnf
  • b_trace_checking
  • banditfuzz
  • basic_unit_tests
  • before_after_predicates
  • benchmark.pl
  • benchmark_analyser.pl
  • between.pl
  • bf_env
  • bliss_interface
  • block_checker.pl
  • bmachine
  • bmachine_construction
  • bmachine_static_checks
  • bmachine_structure
  • bmc
  • bool_pred
  • bool_pred_test.pl
  • boolean.pl
  • bsyntaxtree
  • bsyntaxtree_quantifiers
  • bvisual
  • bvisual_any_maxsolver
  • cbc_ba
  • cbc_path_solver
  • cbc_refinement_checks
  • cdclt_pred_to_sat
  • cdclt_preprocessing
  • cdclt_sat_solver
  • cdclt_settings
  • cdclt_solver
  • cdclt_stats
  • ce_replay
  • chr_set_membership
  • closures
  • clpfd_interface
  • clpfd_lists
  • clpfd_off_interface
  • clpfd_tables
  • code2vec
  • code2vec_tests
  • codespeed_versions
  • compile_time_flags
  • consistencycheck
  • constraints
  • counter
  • coverage_statistics
  • coverage_term_expander.pl
  • coverage_tools
  • coverage_tools_annotations
  • csp_basic
  • csp_sequences
  • csp_sets
  • csp_tuples
  • ctigar
  • ctl
  • custom_explicit_sets
  • cvc4interface
  • debug
  • debugging_calls
  • debugging_calls_te.pl
  • delay
  • dependence
  • dev.pl
  • difference_logic_solver
  • disprover
  • disprover_test_runner
  • disprover_test_runner_cli.pl
  • domain
  • domain_test.pl
  • dot_graphs_static_analysis
  • eclipse_interface
  • enable_graph
  • enabling_analysis
  • enabling_predicates
  • error_manager
  • eval_interface
  • eval_let_store
  • eval_strings
  • eventhandling
  • example.pl
  • experiment.pl
  • external_function_declarations
  • external_functions
  • external_functions_reals
  • external_functions_svg
  • fastio_inspector.pl
  • fd_utils_clpfd
  • fdr_csp_generator
  • fibonacci_heap
  • find_whens.pl
  • fixed_value.pl
  • float.pl
  • fuzzer
  • fuzzer_runner.pl
  • fuzzfile
  • fuzzing
  • gensym
  • grammar
  • graph_iso_nauty
  • graphical_state_viewer_images
  • graphiso
  • graphiso_test
  • ground_truth
  • gui_tcltk.pl
  • hashing
  • haskell_csp
  • haskell_csp_analyzer
  • heuristic_grouping.pl
  • hit_profiler
  • ic3
  • inf_arith
  • input_syntax_tree
  • integer.pl
  • interval_calc
  • json_parser
  • junit_tests
  • kernel_card_arithmetic
  • kernel_cardinality_attr
  • kernel_dif
  • kernel_equality
  • kernel_freetypes
  • kernel_frozen_info
  • kernel_lists
  • kernel_mappings
  • kernel_mappings_dispatch
  • kernel_non_empty_attr
  • kernel_objects
  • kernel_ordering
  • kernel_propagation
  • kernel_reals
  • kernel_records
  • kernel_strings
  • kernel_sym_break_order
  • kernel_tools
  • kernel_waitflags
  • kernel_z
  • kinduction
  • kodkod
  • kodkod2
  • kodkod_annotator
  • kodkod_integer_recalc
  • kodkod_printer
  • kodkod_process
  • kodkod_rewrite
  • kodkod_test
  • kodkod_tools
  • kodkod_translate
  • kodkod_typing
  • latex_processor
  • library_setup
  • list.pl
  • location_vars_to_program
  • logger
  • logging
  • ltl
  • ltl2ba
  • ltl_fairness
  • ltl_propositions
  • ltl_safety
  • ltl_tools
  • ltl_translate
  • ltl_verification
  • ltlc
  • ltsmin
  • ltsmin_c_interface
  • ltsmin_trace
  • master
  • maxsolver
  • mcdc_coverage
  • member_of.pl
  • memoization
  • meta_interface
  • mic_generation
  • model_checker
  • model_translation
  • module_information
  • msg_interop
  • mutate_expressions
  • mutation.pl
  • mutation_prob_ast_int_expr.pl
  • mutation_prob_ast_pred.pl
  • mutation_prob_ast_seq_expr.pl
  • mutation_prob_ast_set_expr.pl
  • mutations
  • myheap
  • number.pl
  • operation_data_generator
  • optimizing_solver
  • ordsetsp
  • parsercall
  • partition_detection
  • pathes
  • pathes_extensions_db
  • pathes_lib
  • performance_messages
  • pge_algo
  • plspec
  • plspec_core
  • plspec_logger
  • plspec_test
  • pltables
  • pltables_export
  • pltables_export_csv
  • pltables_export_html
  • pltables_export_latex
  • pltables_export_tools
  • pltables_export_xml
  • plunit_test_runner
  • pragmas
  • predicate_abstraction
  • predicate_analysis
  • predicate_data_generator
  • predicate_debugger
  • predicate_evaluator
  • predicate_handling
  • pref_definitions
  • preferences
  • preprofiler
  • preserve_behaviour_test.pl
  • prettyprinter
  • prob2_interface
  • prob_ast_any.pl
  • prob_ast_boolean.pl
  • prob_ast_couple.pl
  • prob_ast_eval_int_expr.pl
  • prob_ast_eval_pred.pl
  • prob_ast_eval_seq_expr.pl
  • prob_ast_eval_set_expr.pl
  • prob_ast_expr.pl
  • prob_ast_identifier.pl
  • prob_ast_int_expr.pl
  • prob_ast_integer.pl
  • prob_ast_minimize_int_expr.pl
  • prob_ast_minimize_pred.pl
  • prob_ast_minimize_seq_expr.pl
  • prob_ast_minimize_set_expr.pl
  • prob_ast_pred.pl
  • prob_ast_record.pl
  • prob_ast_sat.pl
  • prob_ast_seq.pl
  • prob_ast_seq_expr.pl
  • prob_ast_set.pl
  • prob_ast_set_expr.pl
  • prob_ast_string.pl
  • prob_cli
  • prob_cov.pl
  • prob_cov_runner.pl
  • prob_profiling_cli.pl
  • prob_rule_compiler
  • prob_socketserver
  • prob_startup
  • prob_state_predicates
  • prob_tcltk.pl
  • prob_type.pl
  • prob_value_any.pl
  • prob_value_boolean.pl
  • prob_value_integer.pl
  • prob_value_record.pl
  • prob_value_seq.pl
  • prob_value_set.pl
  • prob_value_string.pl
  • probhash
  • probsocket_proxy.pl
  • profiler
  • profiler_gui
  • profiler_te
  • prologTasks
  • prothon
  • proz
  • ptest.pl
  • quantifier_instantiation
  • random_permutations
  • rational.pl
  • record_detection
  • reduce_graph_state_space
  • refinement_checker
  • regexp
  • rewrite_rules_db
  • runtime_profiler
  • safety_mc
  • sap
  • sat_symmetry_breaking
  • satsolver
  • schemaexpansion
  • schemavars
  • self_check
  • self_check_off.pl
  • seq_rewriter
  • set_rewriter
  • smt_common_predicates
  • smt_solver_benchmarks
  • smt_solvers_interface
  • smt_symmetry_breaking
  • smtlib2_cli
  • smtlib2_environment
  • smtlib2_interpreter
  • smtlib2_parser
  • smtlib2_parser_tests
  • smtlib2_translation
  • snippets.pl
  • softfloat
  • solver_dispatcher
  • solver_handling
  • solver_interface
  • solvercalls
  • source_profiler
  • specfile
  • state_as_dot_graph
  • state_custom_dot_graph
  • state_graph_canon
  • state_packing
  • state_permuter
  • state_space
  • state_space_dijkstra
  • state_space_exploration_modes
  • state_space_explorer
  • state_space_open_nodes
  • state_space_open_nodes_c
  • state_space_reduction
  • static_analysis
  • static_enabling_analysis
  • static_ordering
  • store
  • subexpressions
  • succeed_max
  • symmetry_marker
  • symmetry_reduction
  • synthesis_tests
  • synthesis_util
  • system_call
  • table_tools
  • tcltk_interface
  • tcltk_tree_inspector
  • test
  • test2
  • test_fibonacci_heap
  • test_nodestore.pl
  • test_paths
  • test_regexp
  • test_regexp_unicode
  • test_runner
  • test_runner_cov.pl
  • test_typechecker
  • testcases
  • testdining
  • testltlc
  • tests.pl
  • testsignal.pl
  • timer
  • tools
  • tools_commands
  • tools_fastread
  • tools_files
  • tools_io
  • tools_lists
  • tools_matching
  • tools_meta
  • tools_portability
  • tools_positions
  • tools_printing
  • tools_strings
  • tools_timeout
  • trace_generator
  • translate
  • translate_keywords
  • tree.pl
  • typechecker
  • typing_tools
  • uml_generator
  • unbound_spec_test.pl
  • unsat_core_generalization
  • unsat_cores
  • user_interrupts
  • user_signal
  • validator
  • validator_test
  • value_persistance
  • variable.pl
  • version
  • visb_visualiser
  • visualize_graph
  • weakest_preconditions
  • well_def_analyser
  • well_def_hyps
  • well_def_prover
  • well_def_tools
  • welldef
  • whash_send
  • worker
  • xml2b
  • xml_prob
  • xtl_interface
  • z3interface
  • z_tools
  • z_typechecker
  • zenvironment
  • zmq
  • zmq_rpc
  • zparameters
  • ztransformations
  • Predicates of bmachine

  • add_additional_filename/2
  • add_additional_property/2
  • add_all_perrors_in_context_of_used_filenames/3
  • 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/4
  • 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_names/3
  • b_get_machine_operation_parameter_names_for_animation/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_parameters3/3
  • b_get_machine_operation_typed_parameters_aux/3
  • b_get_machine_operation_typed_parameters_for_animation/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_definition_with_error_list/5
  • 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_additional_definitions_file/1
  • 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
  • bottom_event/3
  • check_codes/1
  • check_is_constant/1
  • check_is_operation/1
  • check_is_var/1
  • check_read/2
  • 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/3
  • 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_precise_rodin_model_and_name/3
  • 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
  • global_set_element/2
  • has_label/2
  • id/1
  • infeasible_subst/1
  • infeasible_tsubst/1
  • initial_machine/2
  • 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
  • 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
  • simplify_desc/2
  • 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/6
  • type_without_errors/4
  • typecheck_predicates/4
  • unify_args/3
  • useful_animation_expression/1
  • weigh_properties/5
  • weigh_properties2/2
  • weigh_term/2
  • weigh_term2/2
  • Module Information

    Module Information


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

    3311 Lines

    351 Predicates

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

    209 Exports

    82 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:    raw_update_main_file_nr/3

    Module:    input_syntax_tree


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


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


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


    Name:    b_get_machine_operation_result_names/2


    Name:    b_get_machine_operation_typed_parameters/2


    Name:    b_get_machine_operation_typed_parameters_for_animation/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_definition_with_error_list/5


    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/3
  • 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/4
  • 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_names/3
  • b_get_machine_operation_parameter_names_for_animation/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_parameters3/3
  • b_get_machine_operation_typed_parameters_aux/3
  • b_get_machine_operation_typed_parameters_for_animation/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_definition_with_error_list/5
  • 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_additional_definitions_file/1
  • 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
  • bottom_event/3
  • check_codes/1
  • check_is_constant/1
  • check_is_operation/1
  • check_is_var/1
  • check_read/2
  • 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/3
  • 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_precise_rodin_model_and_name/3
  • 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
  • global_set_element/2
  • has_label/2
  • id/1
  • infeasible_subst/1
  • infeasible_tsubst/1
  • initial_machine/2
  • 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
  • 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
  • simplify_desc/2
  • 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/6
  • type_without_errors/4
  • typecheck_predicates/4
  • unify_args/3
  • useful_animation_expression/1
  • weigh_properties/5
  • weigh_properties2/2
  • weigh_term/2
  • weigh_term2/2


  • add_additional_filename/2

    add_additional_filename/2



    add_additional_property/2

    add_additional_property/2



    add_all_perrors_in_context_of_used_filenames/3

    add_all_perrors_in_context_of_used_filenames/3



    add_discharged_po_infos/2

    add_discharged_po_infos/2



    all_operations_have_valid_read_modifies_infos/0

    all_operations_have_valid_read_modifies_infos/0



    apply_machine_transformations-->/2

    apply_machine_transformations-->/2



    apply_transformation_step/4

    apply_transformation_step/4

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



    assert_bmachine_is_precompiled/0

    assert_bmachine_is_precompiled/0

    Description:
    generate_specialized_invariants/0, %% no longer exists



    assert_main_machine/1

    assert_main_machine/1



    assert_temp_typed_predicate/1

    assert_temp_typed_predicate/1

    Description:
    set a temporary predicate as additional guard



    auto_precompile/0

    auto_precompile/0



    auto_precompile2/3

    auto_precompile2/3



    auto_precompile_phase2/0

    auto_precompile_phase2/0



    b_absolute_file_name_relative_to_main_machine/2

    b_absolute_file_name_relative_to_main_machine/2



    b_definition_prefixed/5

    b_definition_prefixed/5



    b_enumerated_sets_precompiled_calc/0

    b_enumerated_sets_precompiled_calc/0



    b_extract_values_clause_assignment_calc/3

    b_extract_values_clause_assignment_calc/3



    b_find_operation/5

    b_find_operation/5



    b_get_abstract_events/3

    b_get_abstract_events/3



    b_get_all_used_filenames/1

    b_get_all_used_filenames/1

    Dynamic: true



    b_get_all_used_identifiers_calc/1

    b_get_all_used_identifiers_calc/1



    b_get_all_used_identifiers_in_section_calc/2

    b_get_all_used_identifiers_in_section_calc/2



    b_get_animated_sections/1

    b_get_animated_sections/1



    b_get_assertion_count/3

    b_get_assertion_count/3



    b_get_assertions/3

    b_get_assertions/3



    b_get_assertions_from_main_machine_calc/2

    b_get_assertions_from_main_machine_calc/2



    b_get_constant_represented_inside_global_set_calc/2

    b_get_constant_represented_inside_global_set_calc/2



    b_get_constant_variable_description_calc/2

    b_get_constant_variable_description_calc/2



    b_get_definition/5

    b_get_definition/5



    b_get_definition_string_from_machine/2

    b_get_definition_string_from_machine/2



    b_get_definition_string_from_machine_calc/3

    b_get_definition_string_from_machine_calc/3



    b_get_definition_with_pos/6

    b_get_definition_with_pos/6



    b_get_disjoint_constants_of_type_calc/3

    b_get_disjoint_constants_of_type_calc/3



    b_get_dynamic_assertions_from_machine_calc/1

    b_get_dynamic_assertions_from_machine_calc/1



    b_get_initialisation_from_machine_calc/2

    b_get_initialisation_from_machine_calc/2



    b_get_internal_prolog_representation_as_codes/1

    b_get_internal_prolog_representation_as_codes/1



    b_get_invariant_from_machine_calc/1

    b_get_invariant_from_machine_calc/1



    b_get_linking_invariant_from_machine_calc/1

    b_get_linking_invariant_from_machine_calc/1



    b_get_machine_all_constants_calc/1

    b_get_machine_all_constants_calc/1



    b_get_machine_animation_expression_calc/2

    b_get_machine_animation_expression_calc/2



    b_get_machine_animation_function_calc/2

    b_get_machine_animation_function_calc/2



    b_get_machine_constants_calc/1

    b_get_machine_constants_calc/1



    b_get_machine_custom_edges_function_calc/2

    b_get_machine_custom_edges_function_calc/2



    b_get_machine_custom_graph_function_calc/2

    b_get_machine_custom_graph_function_calc/2



    b_get_machine_custom_nodes_function_calc/2

    b_get_machine_custom_nodes_function_calc/2



    b_get_machine_goal_calc/1

    b_get_machine_goal_calc/1



    b_get_machine_header_position/2

    b_get_machine_header_position/2



    b_get_machine_heuristic_function_calc/1

    b_get_machine_heuristic_function_calc/1



    b_get_machine_operation/4

    b_get_machine_operation/4



    b_get_machine_operation_calc/6

    b_get_machine_operation_calc/6



    b_get_machine_operation_for_animation/4

    b_get_machine_operation_for_animation/4



    b_get_machine_operation_for_animation/6

    b_get_machine_operation_for_animation/6



    b_get_machine_operation_for_animation_calc/7

    b_get_machine_operation_for_animation_calc/7



    b_get_machine_operation_max_calc/2

    b_get_machine_operation_max_calc/2



    b_get_machine_operation_parameter_names/2

    b_get_machine_operation_parameter_names/2



    b_get_machine_operation_parameter_names/3

    b_get_machine_operation_parameter_names/3



    b_get_machine_operation_parameter_names_for_animation/2

    b_get_machine_operation_parameter_names_for_animation/2



    b_get_machine_operation_parameter_types/2

    b_get_machine_operation_parameter_types/2



    b_get_machine_operation_result_names/2

    b_get_machine_operation_result_names/2



    b_get_machine_operation_signature/2

    b_get_machine_operation_signature/2



    b_get_machine_operation_typed_parameters/2

    b_get_machine_operation_typed_parameters/2



    b_get_machine_operation_typed_parameters3/3

    b_get_machine_operation_typed_parameters3/3



    b_get_machine_operation_typed_parameters_aux/3

    b_get_machine_operation_typed_parameters_aux/3



    b_get_machine_operation_typed_parameters_for_animation/2

    b_get_machine_operation_typed_parameters_for_animation/2



    b_get_machine_operation_typed_results/2

    b_get_machine_operation_typed_results/2



    b_get_machine_refinement_hierarchy/1

    b_get_machine_refinement_hierarchy/1



    b_get_machine_searchscope_calc/1

    b_get_machine_searchscope_calc/1



    b_get_machine_set/1

    b_get_machine_set/1



    b_get_machine_set_calc/2

    b_get_machine_set_calc/2



    b_get_machine_setscope_calc/2

    b_get_machine_setscope_calc/2



    b_get_machine_variables_calc/1

    b_get_machine_variables_calc/1



    b_get_machine_variables_in_original_order_calc/1

    b_get_machine_variables_in_original_order_calc/1



    b_get_model_type/1

    b_get_model_type/1



    b_get_named_machine_set/2

    b_get_named_machine_set/2



    b_get_named_machine_set_calc/3

    b_get_named_machine_set_calc/3



    b_get_operation_description/2

    b_get_operation_description/2



    b_get_operation_non_det_modifies_calc/2

    b_get_operation_non_det_modifies_calc/2



    b_get_operation_normalized_read_write_info_calc/3

    b_get_operation_normalized_read_write_info_calc/3



    b_get_operation_pos/2

    b_get_operation_pos/2



    b_get_operation_unchanged_variables_calc/2

    b_get_operation_unchanged_variables_calc/2

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



    b_get_operation_variant/3

    b_get_operation_variant/3



    b_get_promoted_machine_operations_calc/1

    b_get_promoted_machine_operations_calc/1



    b_get_properties_from_machine_calc/1

    b_get_properties_from_machine_calc/1



    b_get_refined_ancestors_names/1

    b_get_refined_ancestors_names/1



    b_get_refined_machine/1

    b_get_refined_machine/1



    b_get_refined_machine_name/1

    b_get_refined_machine_name/1



    b_get_static_assertions_from_machine_calc/1

    b_get_static_assertions_from_machine_calc/1



    b_get_true_expression_definition/1

    b_get_true_expression_definition/1



    b_get_typed_definition/3

    b_get_typed_definition/3



    b_get_typed_definition_with_error_list/5

    b_get_typed_definition_with_error_list/5



    b_get_typed_expression_definition/3

    b_get_typed_expression_definition/3



    b_get_typed_predicate_definition/3

    b_get_typed_predicate_definition/3



    b_get_unproven_dynamic_assertions_from_machine_calc/1

    b_get_unproven_dynamic_assertions_from_machine_calc/1



    b_get_unproven_static_assertions_from_machine_calc/1

    b_get_unproven_static_assertions_from_machine_calc/1



    b_invariant_number_list_calc/1

    b_invariant_number_list_calc/1



    b_is_constant/1

    b_is_constant/1



    b_is_constant_calc/2

    b_is_constant_calc/2



    b_is_initialisation_name/1

    b_is_initialisation_name/1



    b_is_operation_name_calc/1

    b_is_operation_name_calc/1



    b_is_unused_constant_calc/1

    b_is_unused_constant_calc/1



    b_is_variable/1

    b_is_variable/1



    b_is_variable_calc/2

    b_is_variable_calc/2



    b_limit_abstract_level_to_zero/2

    b_limit_abstract_level_to_zero/2



    b_load_additional_definitions_file/1

    b_load_additional_definitions_file/1



    b_load_eventb_project/1

    b_load_eventb_project/1



    b_load_machine_from_file/1

    b_load_machine_from_file/1



    b_load_machine_from_file/2

    b_load_machine_from_file/2



    b_load_machine_from_list_of_facts/2

    b_load_machine_from_list_of_facts/2



    b_load_machine_from_term/2

    b_load_machine_from_term/2



    b_load_machine_probfile/1

    b_load_machine_probfile/1



    b_load_machine_probfile/2

    b_load_machine_probfile/2



    b_machine_clear/0

    b_machine_clear/0



    b_machine_has_assertions/0

    b_machine_has_assertions/0



    b_machine_has_constants/0

    b_machine_has_constants/0



    b_machine_has_constants_or_properties/0

    b_machine_has_constants_or_properties/0



    b_machine_has_dynamic_assertions_calc/0

    b_machine_has_dynamic_assertions_calc/0



    b_machine_has_operations/0

    b_machine_has_operations/0



    b_machine_has_proven_invariants/0

    b_machine_has_proven_invariants/0



    b_machine_has_static_assertions_calc/0

    b_machine_has_static_assertions_calc/0



    b_machine_has_unproven_assertions/0

    b_machine_has_unproven_assertions/0



    b_machine_has_variables/0

    b_machine_has_variables/0



    b_machine_is_loaded/0

    b_machine_is_loaded/0



    b_machine_name_calc/1

    b_machine_name_calc/1



    b_machine_precompile/0

    b_machine_precompile/0



    b_machine_reset/0

    b_machine_reset/0



    b_machine_statistics_calc/2

    b_machine_statistics_calc/2



    b_main_machine_has_no_assertions/0

    b_main_machine_has_no_assertions/0



    b_nth1_invariant_calc/3

    b_nth1_invariant_calc/3



    b_operation_cannot_modify_state_calc/1

    b_operation_cannot_modify_state_calc/1



    b_operation_preserves_full_invariant/1

    b_operation_preserves_full_invariant/1



    b_operation_preserves_invariant_calc/2

    b_operation_preserves_invariant_calc/2



    b_operation_reads_output_variables_calc/3

    b_operation_reads_output_variables_calc/3



    b_parse_machine_expression_from_codes/2

    b_parse_machine_expression_from_codes/2



    b_parse_machine_expression_from_codes/5

    b_parse_machine_expression_from_codes/5



    b_parse_machine_expression_from_codes/6

    b_parse_machine_expression_from_codes/6



    b_parse_machine_expression_from_codes4/4

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



    b_parse_machine_expression_from_codes_with_prob_ids/3

    b_parse_machine_expression_from_codes_with_prob_ids/3



    b_parse_machine_expression_from_codes_with_prob_ids/4

    b_parse_machine_expression_from_codes_with_prob_ids/4



    b_parse_machine_formula/3

    b_parse_machine_formula/3



    b_parse_machine_formula_from_codes/7

    b_parse_machine_formula_from_codes/7



    b_parse_machine_operation_pre_post_predicate/3

    b_parse_machine_operation_pre_post_predicate/3



    b_parse_machine_operation_pre_post_predicate/5

    b_parse_machine_operation_pre_post_predicate/5



    b_parse_machine_predicate/2

    b_parse_machine_predicate/2



    b_parse_machine_predicate/3

    b_parse_machine_predicate/3



    b_parse_machine_predicate_from_codes/3

    b_parse_machine_predicate_from_codes/3



    b_parse_machine_predicate_from_codes2/5

    b_parse_machine_predicate_from_codes2/5



    b_parse_machine_predicate_from_codes_open/5

    b_parse_machine_predicate_from_codes_open/5



    b_parse_machine_subsitutions_from_codes/6

    b_parse_machine_subsitutions_from_codes/6



    b_parse_only/5

    b_parse_only/5



    b_parse_optional_machine_predicate/2

    b_parse_optional_machine_predicate/2



    b_parse_predicate/3

    b_parse_predicate/3



    b_parse_wo_type_machine_predicate_from_codes_to_raw_expr/2

    b_parse_wo_type_machine_predicate_from_codes_to_raw_expr/2



    b_reset_filenames_and_numbers/0

    b_reset_filenames_and_numbers/0



    b_reset_machine_goal_from_DEFINITIONS/0

    b_reset_machine_goal_from_DEFINITIONS/0



    b_set_empty_machine/0

    b_set_empty_machine/0



    b_set_eventb_project_flat/3

    b_set_eventb_project_flat/3



    b_set_initial_machine/0

    b_set_initial_machine/0



    b_set_machine/3

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



    b_set_machine_goal/2

    b_set_machine_goal/2



    b_set_machine_searchscope/1

    b_set_machine_searchscope/1



    b_set_machine_searchscope/2

    b_set_machine_searchscope/2



    b_set_parsed_typed_machine_goal/1

    b_set_parsed_typed_machine_goal/1



    b_set_parsed_typed_machine_searchscope/1

    b_set_parsed_typed_machine_searchscope/1



    b_set_to_level_zero/2

    b_set_to_level_zero/2



    b_set_typed_machine/2

    b_set_typed_machine/2



    b_show_eventb_as_classicalb/2

    b_show_eventb_as_classicalb/2



    b_show_eventb_as_classicalb1/3

    b_show_eventb_as_classicalb1/3



    b_show_machine_representation/4

    b_show_machine_representation/4



    b_show_machine_representation_unicode/4

    b_show_machine_representation_unicode/4



    b_sorted_b_definition_prefixed/4

    b_sorted_b_definition_prefixed/4



    b_specialized_invariant_for_op_calc/2

    b_specialized_invariant_for_op_calc/2



    b_specialized_invariant_mask_for_op_calc/2

    b_specialized_invariant_mask_for_op_calc/2



    b_top_level_feasible_operation_calc/1

    b_top_level_feasible_operation_calc/1



    b_top_level_operation_calc/1

    b_top_level_operation_calc/1



    b_type_check_raw_expr/4

    b_type_check_raw_expr/4



    b_type_expression/5

    b_type_expression/5



    b_type_expression_for_full_b_machine/6

    b_type_expression_for_full_b_machine/6



    b_type_expressions_l/6

    b_type_expressions_l/6



    b_type_literal/3

    b_type_literal/3



    b_type_only/5

    b_type_only/5



    b_type_open_exists_predicate/3

    b_type_open_exists_predicate/3



    b_type_open_predicate/5

    b_type_open_predicate/5



    b_type_open_predicate_for_full_b_machine/6

    b_type_open_predicate_for_full_b_machine/6



    b_type_open_predicate_with_errors/4

    b_type_open_predicate_with_errors/4



    b_unset_machine_goal/0

    b_unset_machine_goal/0



    b_write_eventb_machine_to_classicalb_to_file/1

    b_write_eventb_machine_to_classicalb_to_file/1



    b_write_machine_representation_to_file/2

    b_write_machine_representation_to_file/2



    b_write_machine_representation_to_file/3

    b_write_machine_representation_to_file/3



    b_write_machine_representation_to_file3/3

    b_write_machine_representation_to_file3/3



    bottom_event/3

    bottom_event/3



    check_codes/1

    check_codes/1



    check_is_constant/1

    check_is_constant/1



    check_is_operation/1

    check_is_operation/1



    check_is_var/1

    check_is_var/1



    check_read/2

    check_read/2



    check_valid_machine_name/1

    check_valid_machine_name/1



    check_wd_discharged_inv_or_thm/4

    check_wd_discharged_inv_or_thm/4



    check_write/2

    check_write/2



    clear_wp/0

    clear_wp/0



    comparison/3

    comparison/3



    complete_discharged_info2/0

    complete_discharged_info2/0



    complete_discharged_info3/3

    complete_discharged_info3/3



    complete_discharged_info_calc/0

    complete_discharged_info_calc/0



    constant_variable_marked_as_expand/1

    constant_variable_marked_as_expand/1



    constant_variable_marked_as_memo/1

    constant_variable_marked_as_memo/1



    determine_type_of_formula/2

    determine_type_of_formula/2



    determine_type_of_formula/3

    determine_type_of_formula/3



    determine_type_of_formula2/2

    determine_type_of_formula2/2



    discharged_info_exists/0

    discharged_info_exists/0



    discharged_invariant/3

    discharged_invariant/3



    do_machine_consistency_check/0

    do_machine_consistency_check/0



    empty/1

    empty/1



    empty_machine/2

    empty_machine/2



    eventb_load_command/5

    eventb_load_command/5



    extension_kind/2

    extension_kind/2



    extract_id_and_pp_type/2

    extract_id_and_pp_type/2



    filter_out_proven_assertions/2

    filter_out_proven_assertions/2



    filter_syntactically_relevant_invariants/4

    filter_syntactically_relevant_invariants/4



    filter_syntactically_relevant_invariants2/4

    filter_syntactically_relevant_invariants2/4



    find_constants_of_type/4

    find_constants_of_type/4



    find_id_uses_for_maplist/2

    find_id_uses_for_maplist/2



    find_main_file_name/3

    find_main_file_name/3



    find_used_identifier_in_machine_section/3

    find_used_identifier_in_machine_section/3



    flexible_atom_codes/2

    flexible_atom_codes/2



    full_b_machine/1

    full_b_machine/1



    gen_couple_from_list/2

    gen_couple_from_list/2



    generate_no_parse_errors/1

    generate_no_parse_errors/1



    generate_parse_errors_for/3

    generate_parse_errors_for/3



    get_all_assertions_from_machine/1

    get_all_assertions_from_machine/1



    get_animation_image/2

    get_animation_image/2



    get_animation_image_source_file/2

    get_animation_image_source_file/2



    get_assertions_from_machine/2

    get_assertions_from_machine/2



    get_bottom_event/2

    get_bottom_event/2



    get_constant_definition/2

    get_constant_definition/2



    get_constant_predicate/2

    get_constant_predicate/2



    get_constant_span/2

    get_constant_span/2



    get_constant_type_and_origin/4

    get_constant_type_and_origin/4



    get_definition_with_nr_suffix/3

    get_definition_with_nr_suffix/3



    get_full_b_machine/2

    get_full_b_machine/2



    get_full_b_machine_sha_hash/1

    get_full_b_machine_sha_hash/1



    get_goal/1

    get_goal/1



    get_invariant_list_with_proof_info/1

    get_invariant_list_with_proof_info/1



    get_invariant_list_with_used_ids/2

    get_invariant_list_with_used_ids/2



    get_invariant_with_proof_status_calc/2

    get_invariant_with_proof_status_calc/2



    get_machine_file_number/4

    get_machine_file_number/4



    get_machine_identifiers/2

    get_machine_identifiers/2

    Description:
    mode get_machine_identifiers(+Category, -ListOfIdentifiers)



    get_machine_identifiers_with_pp_type/2

    get_machine_identifiers_with_pp_type/2



    get_machine_operation_additional_identifiers/2

    get_machine_operation_additional_identifiers/2



    get_machine_operation_typing_scope/3

    get_machine_operation_typing_scope/3



    get_modifies_from_info/2

    get_modifies_from_info/2



    get_multi_sections/2

    get_multi_sections/2



    get_nr_of_machine_constants/1

    get_nr_of_machine_constants/1



    get_nr_of_machine_variables/1

    get_nr_of_machine_variables/1



    get_op_desc_template_expr_calc2/2

    get_op_desc_template_expr_calc2/2



    get_op_or_init_and_syntax_filter/5

    get_op_or_init_and_syntax_filter/5



    get_operation_description_template_expr_calc/2

    get_operation_description_template_expr_calc/2



    get_operation_info_calc/2

    get_operation_info_calc/2



    get_operation_type/4

    get_operation_type/4



    get_precise_rodin_model_and_name/3

    get_precise_rodin_model_and_name/3



    get_primed_machine_variables/1

    get_primed_machine_variables/1



    get_proven_invariant_calc/2

    get_proven_invariant_calc/2



    get_proz_animation_function/3

    get_proz_animation_function/3



    get_proz_settings/1

    get_proz_settings/1



    get_section_from_current_machine/2

    get_section_from_current_machine/2



    get_tc_scope/2

    get_tc_scope/2



    get_unproven_invariants/1

    get_unproven_invariants/1



    get_variable_type_and_origin/4

    get_variable_type_and_origin/4



    global_set_element/2

    global_set_element/2



    has_label/2

    has_label/2



    id/1

    id/1



    infeasible_subst/1

    infeasible_subst/1



    infeasible_tsubst/1

    infeasible_tsubst/1



    initial_machine/2

    initial_machine/2



    invalid_chars/1

    invalid_chars/1



    invariant_proof_status_for_event/4

    invariant_proof_status_for_event/4



    involves_id/2

    involves_id/2



    involves_id_aux/2

    involves_id_aux/2



    is_abstract_event_in_list/3

    is_abstract_event_in_list/3



    is_discharged_assertion/1

    is_discharged_assertion/1



    is_empty_string/1

    is_empty_string/1



    is_empty_string2/1

    is_empty_string2/1



    is_ground/2

    is_ground/2



    is_initialisation_op/1

    is_initialisation_op/1



    is_not_main_assertion/1

    is_not_main_assertion/1



    is_precompiled_predicate/1

    is_precompiled_predicate/1



    is_proven_invariant/2

    is_proven_invariant/2

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



    is_proven_invariant_for_model/3

    is_proven_invariant_for_model/3



    is_syntactically_relevant_inv/3

    is_syntactically_relevant_inv/3



    is_syntactically_relevant_invariant_for_event/2

    is_syntactically_relevant_invariant_for_event/2



    known_identifier/1

    known_identifier/1



    l_weigh_term/2

    l_weigh_term/2



    load_additional_information/1

    load_additional_information/1



    load_additional_information_fact/1

    load_additional_information_fact/1



    minor_mode_to_check/0

    minor_mode_to_check/0



    operation_has_valid_read_modifies_infos/1

    operation_has_valid_read_modifies_infos/1



    operation_has_valid_read_modifies_infos2/1

    operation_has_valid_read_modifies_infos2/1



    other_spec_precompile/0

    other_spec_precompile/0



    parse_expression_raw_or_atom3/3

    parse_expression_raw_or_atom3/3



    parse_expression_raw_or_atom_with_prob_ids/2

    parse_expression_raw_or_atom_with_prob_ids/2



    portray_defs/0

    portray_defs/0



    portray_filenumbers/0

    portray_filenumbers/0



    precompile_operation_names_in_reverse_order/0

    precompile_operation_names_in_reverse_order/0



    precompiled_predicate/1

    precompiled_predicate/1



    precompiled_predicate_no_error_when_not_precompiled/1

    precompiled_predicate_no_error_when_not_precompiled/1



    precompiled_predicate_phase2/1

    precompiled_predicate_phase2/1



    predicate_uses_variables/1

    predicate_uses_variables/1



    prime_variable/2

    prime_variable/2



    process_eventb_project_term/4

    process_eventb_project_term/4



    proof_status_for_inv2/4

    proof_status_for_inv2/4



    read_eventb_project_from_file/6

    read_eventb_project_from_file/6



    read_eventb_project_from_stream/4

    read_eventb_project_from_stream/4



    remove_weights/2

    remove_weights/2



    replace_prob_set_elements_in_scope/2

    replace_prob_set_elements_in_scope/2



    reset_filename_parsing_default/2

    reset_filename_parsing_default/2



    reset_temp_predicate/0

    reset_temp_predicate/0



    rewrite_complete_machine/3

    rewrite_complete_machine/3



    safe_read/3

    safe_read/3



    select_proven_invariants/4

    select_proven_invariants/4



    set_additional_filename_as_parsing_default/3

    set_additional_filename_as_parsing_default/3



    set_all_used_filenames/1

    set_all_used_filenames/1



    set_stored_prefs/1

    set_stored_prefs/1



    simplify_desc/2

    simplify_desc/2



    sort_properties/2

    sort_properties/2



    sorted_list_of_defs/3

    sorted_list_of_defs/3



    source_code_for_definition/5

    source_code_for_definition/5



    source_code_for_identifier/6

    source_code_for_identifier/6



    startup_precompiled/0

    startup_precompiled/0



    store_filenumbers/1

    store_filenumbers/1



    store_filenumbers/2

    store_filenumbers/2



    tcltk_get_proven_invariant_for_op/2

    tcltk_get_proven_invariant_for_op/2



    tcltk_get_specialized_invariant_for_op/2

    tcltk_get_specialized_invariant_for_op/2



    tcltk_get_specialized_invariant_for_op_single/3

    tcltk_get_specialized_invariant_for_op_single/3



    tcltk_get_specialized_invariants_for_ops/1

    tcltk_get_specialized_invariants_for_ops/1



    translate_any_into_parameters/3

    translate_any_into_parameters/3



    translate_any_into_parameters_aux/5

    translate_any_into_parameters_aux/5



    translate_machine_to_classicalb/3

    translate_machine_to_classicalb/3



    try_kodkod/0

    try_kodkod/0



    type_check_definitions/0

    type_check_definitions/0



    type_check_definitions2/0

    type_check_definitions2/0



    type_with_errors/4

    type_with_errors/4



    type_with_errors_in_context/6

    type_with_errors_in_context/6



    type_without_errors/4

    type_without_errors/4



    typecheck_predicates/4

    typecheck_predicates/4



    unify_args/3

    unify_args/3



    useful_animation_expression/1

    useful_animation_expression/1



    weigh_properties/5

    weigh_properties/5



    weigh_properties2/2

    weigh_properties2/2



    weigh_term/2

    weigh_term/2



    weigh_term2/2

    weigh_term2/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),_82219,[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'),_51377,[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),_44423,[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),_42759,[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),_46037,[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 extrasrc(json_parser) does not exist
    ! goal: absolute_file_name(extrasrc(json_parser),_45749,[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),_154341,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_waitflags.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),_154341,[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),_156485,[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),_162605,[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),_162747,[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'),_168015,[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),_167251,[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),_167251,[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),_168547,[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),_167873,[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),_168867,[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),_162605,[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_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),_185633,[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),_179939,[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 argument 1 of absolute_file_name/3
    ! file probsrc(avl_tools) does not exist
    ! goal: absolute_file_name(probsrc(avl_tools),_163027,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bsets_clp.pl')])
    ! Existence error in user:environ/2
    ! procedure user:environ/2 does not exist
    ! goal: user:environ(prob_use_timer,true)
    ! Existence error in argument 1 of absolute_file_name/3
    ! file extension('counter/counter') does not exist
    ! goal: absolute_file_name(extension('counter/counter'),_175541,[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),_175395,[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'),_178675,[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'),_175541,[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),_175683,[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),_163315,[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'),_163027,[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),_156485,[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),_154341,[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),_154341,[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),_129055,[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('random_permutations/random_permutations') does not exist
    ! goal: absolute_file_name(extension('random_permutations/random_permutations'),_122509,[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),_120507,[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'),_84273,[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),_78579,[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),_75015,[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),_45749,[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(tools_strings) does not exist
    ! goal: absolute_file_name(probsrc(tools_strings),_46037,[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),_45895,[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),_45895,[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),_38497,[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),_38497,[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),_40303,[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),_38497,[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),_38617,[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')])