Dynamic Predicates: change_flag/0 change_flag_backup/0 pref_backup/2 preference/2 temp_pref/3 nr_of_recent_documents/1 recent_documents/1 add_recent_documents_active/0 searched_patterns/1 replaced_patterns/1 eval_history_elements/1 eval_csp_history_elements/1 checked_ltl_formulas/1 prob_application_type/1

2965 Lines

108 Predicates

Imported Modules: error_manager lists file_systems

62 Exports

22 specified Imports

Imports	Exports
Name: print_message/1 Module: tools Name: get_modulename_filename/2 Module: tools Name: safe_on_exception/3 Module: tools_meta Name: safe_on_exception_silent/3 Module: tools_meta Name: translate_term_into_atom/2 Module: tools_meta Name: host_platform/1 Module: tools_platform Name: string_concatenate/3 Module: tools_strings Name: ajoin/2 Module: tools_strings Name: print_dynamic_pred/4 Module: tools_printing Name: print_error/1 Module: tools_printing Name: format_error_with_nl/2 Module: tools_printing Name: version_str/1 Module: version Name: revision/1 Module: version Name: lastchangeddate/1 Module: version Name: module_info/2 Module: module_information Name: file_exists/1 Module: file_systems Name: directory_exists/1 Module: file_systems Name: environ/2 Module: system Name: preference_value_requires_extension/3 Module: pathes_extensions_db Name: unavailable_extension/2 Module: pathes_lib Name: maplist/2 Module: lists Name: register_event_listener/3 Module: eventhandling	Name: init_preferences/0 Name: tcltk_get_preference/2 Name: get_computed_preference/2 Name: get_preference/2 Name: get_preferences_list/1 Name: get_preferences_list/2 Name: set_preference/2 Name: call_with_preference/3 Name: temporary_set_preference/2 Name: temporary_set_preference/3 Name: reset_temporary_preference/1 Name: reset_temporary_preference/2 Name: reset_all_temporary_preferences/0 Name: preference_category/2 Name: preference_description/2 Name: preference_val_type/2 Name: preference_default_value/2 Name: preference/2 Name: is_of_type/2 Name: pref_type_synonym/2 Name: get_ith_preference_type/2 Name: get_ith_preference_value/2 Name: set_ith_preference_value/2 Name: get_ith_preference_type/3 Name: get_ith_preference_value/3 Name: set_ith_preference_value/3 Name: virtual_preference_category/2 Name: load_preferences/1 Name: save_preferences/1 Name: backup_preferences/0 Name: revert_preferences/0 Name: reset_to_defaults/1 Name: reset_for_benchmarking/0 Name: set_preference_group/2 Name: activate_recent_documents/0 Name: deactivate_recent_documents/0 Name: print_preferences/0 Name: print_preferences/1 Name: get_preference_with_warnings/2 Name: add_recent_document/1 Name: get_recent_documents/1 Name: clear_recent_documents/0 Name: add_element_to_history/3 Name: get_history_elements_list/3 Name: eclipse_preference/2 Name: print_eclipse_prefs/0 Name: advanced_eclipse_preference/2 Name: obsolete_eclipse_preference/1 Name: obsolete_preference/1 Name: deprecated_eclipse_preference/4 Name: get_non_default_preferences/1 Name: has_default_value/1 Name: get_time_out_preference_with_factor/2 Name: add_time_outs/3 Name: time_out_preference_disabled/0 Name: get_prob_application_type/1 Name: set_prob_application_type/1 Name: try_get_program_path/2 Name: valid_rgb_color/1 Name: valid_dot_shape/1 Name: valid_dot_line_style/1 Name: valid_dot_node_style/1

Imports

Exports

Name: print_message/1

Module: tools

Name: get_modulename_filename/2

Module: tools

Name: safe_on_exception/3

Module: tools_meta

Name: safe_on_exception_silent/3

Module: tools_meta

Name: translate_term_into_atom/2

Module: tools_meta

Name: host_platform/1

Module: tools_platform

Name: string_concatenate/3

Module: tools_strings

Name: ajoin/2

Module: tools_strings

Name: print_dynamic_pred/4

Module: tools_printing

Name: print_error/1

Module: tools_printing

Name: format_error_with_nl/2

Module: tools_printing

Name: version_str/1

Module: version

Name: revision/1

Module: version

Name: lastchangeddate/1

Module: version

Name: module_info/2

Module: module_information

Name: file_exists/1

Module: file_systems

Name: directory_exists/1

Module: file_systems

Name: environ/2

Module: system

Name: preference_value_requires_extension/3

Module: pathes_extensions_db

Name: unavailable_extension/2

Module: pathes_lib

Name: maplist/2

Module: lists

Name: register_event_listener/3

Module: eventhandling

Name: init_preferences/0

Name: tcltk_get_preference/2

Name: get_computed_preference/2

Name: get_preference/2

Name: get_preferences_list/1

Name: get_preferences_list/2

Name: set_preference/2

Name: call_with_preference/3

Name: temporary_set_preference/2

Name: temporary_set_preference/3

Name: reset_temporary_preference/1

Name: reset_temporary_preference/2

Name: reset_all_temporary_preferences/0

Name: preference_category/2

Name: preference_description/2

Name: preference_val_type/2

Name: preference_default_value/2

Name: preference/2

Name: is_of_type/2

Name: pref_type_synonym/2

Name: get_ith_preference_type/2

Name: get_ith_preference_value/2

Name: set_ith_preference_value/2

Name: get_ith_preference_type/3

Name: get_ith_preference_value/3

Name: set_ith_preference_value/3

Name: virtual_preference_category/2

Name: load_preferences/1

Name: save_preferences/1

Name: backup_preferences/0

Name: revert_preferences/0

Name: reset_to_defaults/1

Name: reset_for_benchmarking/0

Name: set_preference_group/2

Name: activate_recent_documents/0

Name: deactivate_recent_documents/0

Name: print_preferences/0

Name: print_preferences/1

Name: get_preference_with_warnings/2

Name: add_recent_document/1

Name: get_recent_documents/1

Name: clear_recent_documents/0

Name: add_element_to_history/3

Name: get_history_elements_list/3

Name: eclipse_preference/2

Name: print_eclipse_prefs/0

Name: advanced_eclipse_preference/2

Name: obsolete_eclipse_preference/1

Name: obsolete_preference/1

Name: deprecated_eclipse_preference/4

Name: get_non_default_preferences/1

Name: has_default_value/1

Name: get_time_out_preference_with_factor/2

Name: add_time_outs/3

Name: time_out_preference_disabled/0

Name: get_prob_application_type/1

Name: set_prob_application_type/1

Name: try_get_program_path/2

Name: valid_rgb_color/1

Name: valid_dot_shape/1

Name: valid_dot_line_style/1

Name: valid_dot_node_style/1

Predicates

Predicates:

activate_recent_documents/0

add_element_to_history/3

add_recent_document/1

add_recent_documents_active/0

add_time_outs/3

advanced_eclipse_preference/2

alternate_preference_category/2

assert_change_flag/0

backup_preferences/0

bool_type/1

call_with_preference/3

check_directory_exists/1

clear_dynamic_preference_predicates/0

clear_recent_documents/0

convert_pref/3

cur_pref_string/2

deactivate_recent_documents/0

deprecated_eclipse_preference/4

digit/1

disabled_time_out/1

dynamic_preference_predicate/1

eclipse_preference/2

gen_preference_warnings/1

get_computed_preference/2

get_history_elements_list/3

get_ith_preference_type/2

get_ith_preference_type/3

get_ith_preference_value/2

get_ith_preference_value/3

get_non_default_preferences/1

get_predicate_term_with_single_argument/3

get_preference/2

get_preference_with_warnings/2

get_preferences_list/1

get_preferences_list/2

get_prob_application_type/1

get_recent_documents/1

get_time_out_preference_with_factor/2

has_default_value/1

hex/1

init_preferences/0

invalid_application/2

is_of_type/2

load_preferences/1

load_preferences2/2

merge_prefix_with_suffix/3

non_default_pref/1

nr_of_recent_documents/1

obsolete_eclipse_preference/1

obsolete_preference/1

possible_program/2

possible_program_aux/3

pref_type_synonym/2

preference/2

preference_category/2

preference_default_value/2

preference_description/2

preference_group_description/2

preference_group_val/4

preference_update_action/2

preference_val_type/2

print_dynamic_preferences/1

print_eclipse_prefs/0

print_preferences/0

print_preferences/1

print_preferences_for_saving/1

print_see_exception/2

prob_application_type/1

prune_time_out_preference/2

read_only_preference/1

read_preferences/1

read_preferences2/1

recompute_nr_of_recent_documents/0

reset_all_temporary_preferences/0

reset_for_benchmarking/0

reset_temporary_preference/1

reset_temporary_preference/2

set_ith_preference_value/2

set_ith_preference_value/3

set_preference/2

set_preference_direct/3

set_preference_group/2

set_prob_application_type/1

tcltk_get_preference/2

temporary_set_preference/2

temporary_set_preference/3

time_out_preference_disabled/0

tk_color/1

tk_color/3

try_get_program_path/2

type_element/2

unix/1

valid_dot_line_style/1

valid_dot_node_style/1

valid_dot_shape/1

valid_gray/1

valid_rgb_color/1

virtual_preference_category/2

volatile_preference/1

activate_recent_documents/0

add_element_to_history/3

add_recent_document/1

add_recent_documents_active/0

Dynamic: true

add_time_outs/3

advanced_eclipse_preference/2

advanced_eclipse_preference('OPTIMIZE_AST',optimize_ast).

advanced_eclipse_preference('NORMALIZE_AST',normalize_ast).

advanced_eclipse_preference('STATIC_SYMMETRY_DETECTION',use_static_symmetry_detection).

advanced_eclipse_preference('ENUMERATION_ORDER_ANALYSIS',perform_enumeration_order_analysis). % should probably not be disabled in Rodin

advanced_eclipse_preference('DETECT_LAMBDAS',detect_lambdas).

advanced_eclipse_preference('DATA_VALIDATION',data_validation_mode).

advanced_eclipse_preference('RAISE_ABORT_IMMEDIATELY',raise_abort_immediately).

advanced_eclipse_preference('ENUMERATE_INFINITE_TYPES',allow_enumeration_of_infinite_types).

advanced_eclipse_preference('KODKOD_ONLY_FULL',kodkod_for_components).

advanced_eclipse_preference('KODKOD_RAISE_WARNINGS',kodkod_raise_warnings).

advanced_eclipse_preference('KODKOD_MAX_NR_SOLS',kodkod_max_nr_solutions).

advanced_eclipse_preference('KODKOD_SYMMETRY',kodkod_symmetry_level).

advanced_eclipse_preference('KODKOD_SAT_SOLVER',kodkod_sat_solver).

advanced_eclipse_preference('CSE_PRED',use_common_subexpression_also_for_predicates).

advanced_eclipse_preference('CSE_WD_ONLY',use_common_subexpression_wd_only).

advanced_eclipse_preference('CSE_SUBST',use_common_subexpression_also_for_substitutions).

advanced_eclipse_preference('USELESS_CODE_ELIMINATION',useless_code_elimination).

advanced_eclipse_preference('ALLOW_INCOMPLETE_SETUP_CONSTANTS',allow_incomplete_partial_setup_constants).

advanced_eclipse_preference('PARTITION_PROPERTIES',partition_predicates).

advanced_eclipse_preference('PARTITION_PROPERTIES_INLINE',partition_predicates_inline_equalities).

advanced_eclipse_preference('SHOW_EVENTB_ANY_VALUES',show_eventb_any_arguments).

advanced_eclipse_preference('RANDOMISE_OPERATION_ORDER',randomise_operation_order).

advanced_eclipse_preference('RANDOMISED_RESTART_INIT',randomisedRestartInitalisations).

advanced_eclipse_preference('EXPAND_FORALL_UPTO',expand_forall_upto).

advanced_eclipse_preference('LIFT_EXISTS',lift_existential_quantifiers).

advanced_eclipse_preference('REMOVE_IMPLIED_CONSTRAINTS',remove_implied_constraints). % imply

advanced_eclipse_preference('MAX_DISPLAY_SET',expand_avl_upto).

advanced_eclipse_preference('SHOW_FORMULA_FUNCTOR',show_bvisual_formula_functor_from).

advanced_eclipse_preference('SHOW_FORMULA_PROOF_INFO',show_bvisual_proof_info_icons).

advanced_eclipse_preference('SHOW_FORMULA_EXPLANATIONS',show_bvisual_formula_explanations).

advanced_eclipse_preference('WARN_IF_DEFINITION_HIDES_VARIABLE',warn_if_definition_hides_variable).

advanced_eclipse_preference('TYPE_CHECK_DEFINITIONS',type_check_definitions).

advanced_eclipse_preference('TRACE_INFO',provide_trace_information).

advanced_eclipse_preference('PROFILING_INFO',prob_profiling_on).

advanced_eclipse_preference('SOURCE_PROFILING_INFO',prob_source_profiling_on).

advanced_eclipse_preference('PERFORMANCE_INFO',performance_monitoring_on).

advanced_eclipse_preference('PERFORMANCE_INFO_LIMIT',performance_monitoring_expansion_limit).

advanced_eclipse_preference('DOUBLE_EVALUATION',double_evaluation_when_analysing).

advanced_eclipse_preference('PROB_SAFE_MODE',prob_safe_mode).

advanced_eclipse_preference('IGNORE_HASH_COLLISIONS',ignore_hash_collisions).

advanced_eclipse_preference('USE_SCOPE_DEFINITION',use_scope_predicate).

advanced_eclipse_preference('FORGET_STATE_SPACE',forget_state_space).

advanced_eclipse_preference('SAFETY_MODEL_CHECK',store_only_one_incoming_transition). % is actually INVARIANT_MC

advanced_eclipse_preference('LTL_SAFETY_MODEL_CHECK',use_safety_ltl_model_checker).

advanced_eclipse_preference('JVM_PARSER_HEAP_MB',jvm_parser_heap_size_mb). % TO DO: do not show in ProB2-UI

advanced_eclipse_preference('JVM_PARSER_ARGS',jvm_parser_additional_args).

advanced_eclipse_preference('JVM_PARSER_POSITION_INFOS',jvm_parser_position_infos).

advanced_eclipse_preference('CSP_STRIP_SOURCE_LOC',cspm_strip_source_location).

advanced_eclipse_preference('INVARIANT_CHECKING',do_invariant_checking).

advanced_eclipse_preference('ASSERT_CHECKING',do_assert_checking).

advanced_eclipse_preference('ALLOW_SIMULTANEOUS_ASSIGNMENTS',allow_simultaneous_assignments).

advanced_eclipse_preference('ALLOW_REALS',allow_arith_operators_on_reals).

advanced_eclipse_preference('REAL_SOLVER',solver_for_reals).

advanced_eclipse_preference('BUGLY',bugly_pp_scrambling). % B Ugly

advanced_eclipse_preference('ATELIERB_KRT_PATH',path_to_atb_krt).

advanced_eclipse_preference('JAVA_PATH',path_to_java).

advanced_eclipse_preference('JAVA_PARSER_PATH',path_to_java_parser).

advanced_eclipse_preference('TRY_ATELIERB_PROVERS',try_atb_provers).

advanced_eclipse_preference('SMTLIB_BOOL_ARRAYS_TO_SETS',smtlib2b_arrays_as_sets).

advanced_eclipse_preference('SMTLIB_PREPROCESS',smtlib2b_cleanup_predicate).

advanced_eclipse_preference('SYMBOLIC_MC_TRY_OTHER_SOLVERS',symbolic_mc_try_other_solvers).

advanced_eclipse_preference('SMT_SUPPORTED_INTERPRETER',smt_supported_interpreter).

advanced_eclipse_preference('SAT_SUPPORTED_INTERPRETER',sat_supported_interpreter).

advanced_eclipse_preference('PP_FROZEN_INFOS',translate_print_frozen_infos).

advanced_eclipse_preference('PP_SEQUENCES',translate_print_all_sequences).

advanced_eclipse_preference('PP_CS_STYLE_SEQUENCES',translate_print_cs_style_sequences).

advanced_eclipse_preference('STRING_AS_SEQUENCE',allow_sequence_operators_on_strings).

advanced_eclipse_preference('COMPILE_WHILE',compile_while_body).

advanced_eclipse_preference('PGE',pge).

advanced_eclipse_preference('DOT_PROP',dot_print_node_properties).

advanced_eclipse_preference('DOT_IDS',dot_print_node_ids).

advanced_eclipse_preference('DOT_TRANS_IDS',dot_print_transition_ids).

advanced_eclipse_preference('DOT_INFO',dot_print_node_info).

advanced_eclipse_preference('DOT_LOOPS',dot_print_self_loops).

advanced_eclipse_preference('DOT_ARC_COLORS',dot_print_arc_colors).

advanced_eclipse_preference('DOT_FUNCTIONS',dot_print_functions).

advanced_eclipse_preference('DOT_ROOT',dot_print_root).

advanced_eclipse_preference('DOT_EDGE_LABELS',dot_print_edge_labels).

advanced_eclipse_preference('DOT_ARGUMENTS',dot_print_action_arguments).

advanced_eclipse_preference('DOT_COLOR_ARC',dot_normal_arc_colour).

advanced_eclipse_preference('DOT_COLOR_NODE',dot_normal_node_colour).

advanced_eclipse_preference('DOT_COLOR_NODE_ERROR',dot_invariant_violated_node_colour).

advanced_eclipse_preference('DOT_COLOR_NODE_OPEN',dot_open_node_colour).

advanced_eclipse_preference('DOT_COLOR_NODE_GOAL',dot_goal_node_colour).

advanced_eclipse_preference('DOT_PEN_WIDTH',dot_node_penwidth).

advanced_eclipse_preference('DOT_EDGE_PEN_WIDTH',dot_edge_penwidth).

advanced_eclipse_preference('DOT_SHOW_OP_READ_WRITES',dot_enabling_show_readwrites).

advanced_eclipse_preference('DOT',path_to_dot).

advanced_eclipse_preference('DOT_ENGINE',dot_default_engine).

advanced_eclipse_preference('DOT_DECOMPOSE_NODES',dot_state_graph_decompose).

advanced_eclipse_preference('TK_CUSTOM_STATE_VIEW_PADDING',tk_custom_state_viewer_padding).

advanced_eclipse_preference('TK_CUSTOM_STATE_VIEW_STRING_PADDING',tk_custom_state_viewer_str_padding).

advanced_eclipse_preference('TK_CUSTOM_STATE_VIEW_FONT_NAME',tk_custom_state_viewer_font_name).

advanced_eclipse_preference('TK_CUSTOM_STATE_VIEW_FONT_SIZE',tk_custom_state_viewer_font_size).

advanced_eclipse_preference('TK_CUSTOM_STATE_VIEW_VISIBLE',use_tk_custom_state_viewer).

advanced_eclipse_preference('ALLOW_UNTYPED_IDENTIFIERS',allow_untyped_identifiers).

advanced_eclipse_preference('ALLOW_LOCAL_OPERATION_CALLS',allow_local_operation_calls).

advanced_eclipse_preference('ALLOW_OPERATION_CALLS_IN_EXPRESSIONS',allow_operation_calls_in_expr).

advanced_eclipse_preference('ALLOW_COMPLEX_LETS',allow_let_to_reuse_introduced_ids).

advanced_eclipse_preference('REQUIRE_OUTPUT_ASSIGNMENT',require_operations_to_assign_all_outputs).

advanced_eclipse_preference('ALLOW_OUTPUT_READING',allow_operations_to_read_outputs).

advanced_eclipse_preference('ALLOW_OPERATION_CALLS_FOR_USES',allow_operation_calls_for_uses).

advanced_eclipse_preference('ALLOW_INITIALISATION_OVERRIDE',allow_overriding_initialisation).

advanced_eclipse_preference('REPL_UNICODE',repl_unicode).

advanced_eclipse_preference('REPL_CACHE_PARSING',repl_cache_parsing).

advanced_eclipse_preference('CACHE_OPERATIONS',cache_operations).

advanced_eclipse_preference('LATEX_ENCODING',latex_encoding).

advanced_eclipse_preference('LATEX_GREEK_IDENTIFIERS',latex_pp_greek_ids).

advanced_eclipse_preference('XML_ENCODING',xml_encoding).

advanced_eclipse_preference('BBRESULTS',view_probcli_errors_using_bbresults).

advanced_eclipse_preference('IGNORE_PRJ_TYPES',ignore_prj_types).

advanced_eclipse_preference('FILTER_UNUSED',filter_unused_constants).

advanced_eclipse_preference('DISPROVER_MODE',disprover_mode).

advanced_eclipse_preference('TRACE_UPON_ERROR',trace_upon_error).

advanced_eclipse_preference('NDJSON_ERROR_LOG_FILE',error_log_file).

advanced_eclipse_preference('STRICT_RAISE_WARNINGS',strict_raise_warnings).

advanced_eclipse_preference('STRICT_RAISE_ENUM_WARNINGS',strict_raise_enum_warnings).

advanced_eclipse_preference('STRICT_CLASH_CHECKING',clash_strict_checks).

advanced_eclipse_preference('EDITOR',path_to_text_editor_launch).

advanced_eclipse_preference('EDITOR_GUI',path_to_text_editor).

advanced_eclipse_preference('TLC_WORKERS',tlc_number_of_workers). % will be useful once we can call TLC from probcli (-mc_with_tlc)

advanced_eclipse_preference('TLC_USE_PROB_CONSTANTS',tlc_use_prob_constant_setup).

advanced_eclipse_preference('LTSMIN',path_to_ltsmin).

advanced_eclipse_preference('INTERNAL_ARGUMENT_PREFIX',prefix_internal_operation_arguments).

advanced_eclipse_preference('MINIMAL_TEST_SUITES',generate_minimal_nr_of_testcases).

advanced_eclipse_preference('ALLOW_NEW_OPERATIONS_IN_REFINEMENT',allow_new_ops_in_refinement).

advanced_eclipse_preference('ALLOY_USE_IMPLEMENTABLE_INTEGERS',alloy_use_implementable_integers).

advanced_eclipse_preference('ALLOY_SCOPELESS_TRANSLATION',alloy_scopeless_translation).

advanced_eclipse_preference('ALLOY_TRANSLATION_FOR_PROOF',alloy_translation_for_proof).

advanced_eclipse_preference('ALLOY_STRICT_INTEGERS',alloy_strict_integers).

advanced_eclipse_preference('DOT_EVENT_HIERARCHY_HORIZONTAL',dot_event_hierarchy_horizontal).

advanced_eclipse_preference('DOT_EVENT_HIERARCHY_MCH_COL',dot_event_hierarchy_machine_colour).

advanced_eclipse_preference('DOT_EVENT_HIERARCHY_REF_COL',dot_event_hierarchy_refines_colour).

advanced_eclipse_preference('DOT_EVENT_HIERARCHY_NEW_COL',dot_event_hierarchy_new_event_colour).

advanced_eclipse_preference('DOT_EVENT_HIERARCHY_RENAME_COL',dot_event_hierarchy_rename_event_colour).

advanced_eclipse_preference('DOT_EVENT_HIERARCHY_RENAME_UNCHG_COL',dot_event_hierarchy_rename_unchanged_event_colour).

advanced_eclipse_preference('DOT_EVENT_HIERARCHY_UNCHG_COL',dot_event_hierarchy_unchanged_event_colour).

advanced_eclipse_preference('DOT_EVENT_HIERARCHY_GRD_STRGTH_COL',dot_event_hierarchy_grd_strengthening_event_colour).

advanced_eclipse_preference('DOT_EVENT_HIERARCHY_GRD_KEEP_COL',dot_event_hierarchy_grd_keeping_event_colour).

advanced_eclipse_preference('DOT_EVENT_HIERARCHY_EDGE_COL',dot_event_hierarchy_edge_colour).

advanced_eclipse_preference('DOT_EVENT_HIERARCHY_EXTENDS_COL',dot_event_hierarchy_extends_colour).

advanced_eclipse_preference('DOT_HIERARCHY_EXTRA_DETAIL',dot_hierarchy_show_extra_detail).

advanced_eclipse_preference('DOT_USE_CONSTANTS',dot_print_use_constants).

advanced_eclipse_preference('DOT_ROOT_SHAPE',dot_root_shape).

advanced_eclipse_preference('DOT_NORMAL_NODE_SHAPE',dot_normal_node_shape).

advanced_eclipse_preference('DOT_CURRENT_NODE_SHAPE',dot_current_node_shape).

advanced_eclipse_preference('DOT_SCOPE_LIMIT_COL',dot_scope_limit_node_colour).

advanced_eclipse_preference('DOT_FILL_NORMAL_NODES',dot_fill_normal_nodes).

advanced_eclipse_preference('DOT_NODE_FONT_SIZE',dot_node_font_size).

advanced_eclipse_preference('DOT_EDGE_FONT_SIZE',dot_edge_font_size).

advanced_eclipse_preference('DOT_LIMIT_PAGE_SIZE',dot_with_page_size).

advanced_eclipse_preference('DOT_HORIZONTAL_LAYOUT',dot_horizontal_layout).

advanced_eclipse_preference('DOT_COLOUR_GOAL',dot_colour_goal_nodes).

advanced_eclipse_preference('DOT_DEFINITIONS_USE_SUB_GRAPH',dot_definitions_use_sub_graph).

advanced_eclipse_preference('DOT_DEFINITIONS_SHOW_ALL',dot_definitions_show_all).

advanced_eclipse_preference('DOT_PROJECTION_NON_DET_COL',dot_projection_non_det_edge_colour).

advanced_eclipse_preference('DOT_PROJECTION_DET_COL',dot_projection_det_edge_colour).

advanced_eclipse_preference('DOT_PROJECTION_NON_DEF_COL',dot_projection_non_definite_edge_style).

advanced_eclipse_preference('DOT_PROJECTION_DEF_COL',dot_projection_definite_edge_style).

advanced_eclipse_preference('DOT_PROJECTION_LABEL_LIMIT',dot_projection_label_limit).

advanced_eclipse_preference('DOT_PROJECTION_ONLY_EXPLORED_NODES',dot_projection_process_only_explored).

advanced_eclipse_preference('DOT_USE_UNICODE',dot_use_unicode).

advanced_eclipse_preference('DOT_PREDICATE_NODE_SHAPE',dot_predicate_node_shape).

advanced_eclipse_preference('DOT_EXPRESSION_NODE_SHAPE',dot_expression_node_shape).

advanced_eclipse_preference('DOT_VARIABLE_MODIFICATION_HIDE_ONLY_WRITTEN',dot_var_mod_hide_only_written).

advanced_eclipse_preference('DOT_MACHINE_HIERARCHY_MAX_IDS',dot_hierarchy_max_ids).

advanced_eclipse_preference('CBC_PROVIDE_EXPLANATIONS',cbc_provide_explanations).

advanced_eclipse_preference('CBC_ENABLE_ANALYSIS_TIME_OUT',timeout_cbc_analysis).

advanced_eclipse_preference('SYNTAX_HIGHLIGHT',do_syntax_highlighting).

advanced_eclipse_preference('WD_IGNORE_EXTERNAL',wd_ignore_external_funs).

advanced_eclipse_preference('WD_IGNORE_FINITE_POS',wd_skip_finite_pos).

advanced_eclipse_preference('WD_ANALYSIS_FOR_ANIMATION',wd_analysis_for_animation).

advanced_eclipse_preference('Z3_SOLVE_FOR_ANIMATION',z3_solve_for_animation).

advanced_eclipse_preference('ADD_WD_POS_FOR_Z3',add_wd_pos_for_z3).

advanced_eclipse_preference('TABLE_COLUMN_LIMIT',translation_limit_for_table_commands).

advanced_eclipse_preference('MAX_TRACES',trace_generation_limit).

advanced_eclipse_preference('TRACES_TIME_OUT',trace_generation_time_out).

advanced_eclipse_preference('MC_DC_Level',mc_dc_default_level).

alternate_preference_category/2

alternate_preference_category(dot_print_node_ids,dot_state_space).

alternate_preference_category(dot_print_transition_ids,dot_state_space).

alternate_preference_category(dot_print_use_constants,dot_state_space). %?

alternate_preference_category(dot_print_node_info,dot_state_space).

alternate_preference_category(dot_print_edge_labels,dot_state_space).

alternate_preference_category(dot_print_action_arguments,dot_state_space).

alternate_preference_category(dot_print_functions,dot_state_space).

alternate_preference_category(dot_print_self_loops,dot_state_space).

alternate_preference_category(dot_print_root,dot_state_space).

alternate_preference_category(dot_print_arc_colors,dot_state_space).

alternate_preference_category(dot_root_shape,dot_state_space).

alternate_preference_category(dot_node_penwidth,dot_state_space).

alternate_preference_category(dot_edge_penwidth,dot_state_space).

alternate_preference_category(dot_normal_node_shape,dot_state_space).

alternate_preference_category(dot_current_node_shape,dot_state_space).

alternate_preference_category(dot_open_node_colour,dot_state_space).

alternate_preference_category(dot_scope_limit_node_colour,dot_state_space).

alternate_preference_category(dot_normal_node_colour,dot_state_space).

alternate_preference_category(dot_invariant_violated_node_colour,dot_state_space).

alternate_preference_category(dot_fill_normal_nodes,dot_state_space).

alternate_preference_category(dot_normal_arc_colour,dot_state_space).

alternate_preference_category(dot_node_font_size,dot_state_space).

alternate_preference_category(dot_edge_font_size,dot_state_space).

alternate_preference_category(dot_colour_goal_nodes,dot_state_space).

alternate_preference_category(dot_goal_node_colour,dot_state_space).

alternate_preference_category(dot_print_node_properties,dot_state_space).

alternate_preference_category(dot_use_unicode,dot_formula_tree).

alternate_preference_category(dot_event_hierarchy_unchanged_event_colour,dot_variable_hierarchy).

alternate_preference_category(dot_event_hierarchy_new_event_colour,dot_variable_hierarchy).

alternate_preference_category(dot_event_hierarchy_edge_colour,dot_variable_hierarchy).

alternate_preference_category(dot_hierarchy_show_extra_detail,dot_variable_hierarchy).

alternate_preference_category(dot_normal_node_shape,state_as_graph).

alternate_preference_category(dot_state_graph_decompose,state_as_graph).

alternate_preference_category(dot_horizontal_layout,state_as_graph).

alternate_preference_category(X,dot_variable_modification) :- alternate_preference_category(X,dot_graph_generator).

alternate_preference_category(X,dot_event_hierarchy) :- alternate_preference_category(X,dot_graph_generator).

alternate_preference_category(X,dot_variable_hierarchy) :- alternate_preference_category(X,dot_graph_generator).

alternate_preference_category(X,dot_projection) :- alternate_preference_category(X,dot_graph_generator).

alternate_preference_category(dot_print_self_loops,dot_projection).

alternate_preference_category(X,dot_definitions) :- alternate_preference_category(X,dot_graph_generator).

alternate_preference_category(timeout_cbc_analysis,dot_enable_graph).

alternate_preference_category(X,dot_enable_graph) :- alternate_preference_category(X,dot_graph_generator).

alternate_preference_category(dot_print_self_loops,dot_graph_generator).

alternate_preference_category(dot_print_arc_colors,dot_graph_generator).

alternate_preference_category(dot_node_font_size,dot_graph_generator).

alternate_preference_category(dot_edge_font_size,dot_graph_generator).

alternate_preference_category(dot_edge_penwidth,dot_graph_generator).

alternate_preference_category(dot_with_page_size,dot_graph_generator).

alternate_preference_category(dot_horizontal_layout,dot_graph_generator).

alternate_preference_category(dot_default_engine,dot_graph_generator).

alternate_preference_category(path_to_dot,dot_graph_generator).

alternate_preference_category(translation_limit_for_table_commands,cbc_commands).

alternate_preference_category(translation_limit_for_table_commands,table_commands).

assert_change_flag/0

backup_preferences/0

bool_type/1

call_with_preference/3

Meta: call_with_preference(0,-,-)

check_directory_exists/1

clear_dynamic_preference_predicates/0

clear_recent_documents/0

convert_pref/3

cur_pref_string/2

deactivate_recent_documents/0

deprecated_eclipse_preference/4

digit/1

disabled_time_out/1

dynamic_preference_predicate/1

eclipse_preference/2

eclipse_preference('DEFAULT_SETSIZE',globalsets_fdrange).

eclipse_preference('MAX_INITIALISATIONS',maxNrOfInitialisations).

eclipse_preference('MAX_OPERATIONS',maxNrOfEnablingsPerOperation).

eclipse_preference('MAXINT',maxint).

eclipse_preference('MININT',minint).

eclipse_preference('TIME_OUT',time_out).

eclipse_preference('NUMBER_OF_ANIMATED_ABSTRACTIONS',number_animated_abstractions).

eclipse_preference('NUMBER_OF_SKIPPED_REFINEMENTS',number_skipped_refined_machines).

eclipse_preference('USE_RECORD_CONSTRUCTION',use_record_construction).

eclipse_preference('USE_IGNORE_PRAGMAS',use_ignore_pragmas).

eclipse_preference('COMPRESSION',use_state_packing).

eclipse_preference('OPERATION_REUSE',try_operation_reuse). % was initially not available for Event-B; see eg. prob_examples/examples/EventBPrologPackages/Advance_WP2/v6_Sep2014/ex_mch.eventb -animate 300 which generated deadlock

eclipse_preference('PROOF_INFO',use_po).

eclipse_preference('RANDOMISE_ENUMERATION_ORDER',randomise_enumeration_order).

eclipse_preference('TRY_FIND_ABORT',find_abort_values). % maybe rename into TRY_FIND_WD_ERROR ?

eclipse_preference('CLPFD',use_clpfd_solver).

eclipse_preference('CHR',use_chr_solver).

eclipse_preference('SMT',use_smt_mode).

eclipse_preference('SOLVER_STRENGTH',solver_strength).

eclipse_preference('CSE',use_common_subexpression_elimination).

eclipse_preference('STATIC_ORDERING',use_static_ordering).

eclipse_preference('SYMMETRY_MODE',symmetry_mode).

eclipse_preference('SOLVER_FOR_PROPERTIES',use_solver_on_load).

eclipse_preference('SYMBOLIC',convert_comprehension_sets_into_closures).

eclipse_preference('MEMO',use_closure_expansion_memoization).

eclipse_preference('MEMOIZE_FUNCTIONS',use_function_memoization).

eclipse_preference('AUTO_DETECT_THEORY_MAPPING',auto_detect_theory_ops).

eclipse_preference('PROB_VERSION_INFO',prob_version_info).

eclipse_preference('PROB_REVISION_INFO',prob_revision_info).

eclipse_preference('PROB_LASTCHANGED_INFO',prob_lastchangedate_info).

eclipse_preference(A,B) :- advanced_eclipse_preference(A,B).

gen_preference_warnings/1

get_computed_preference/2

get_history_elements_list/3

get_ith_preference_type/2

get_ith_preference_type/3

get_ith_preference_value/2

get_ith_preference_value/3

get_non_default_preferences/1

get_predicate_term_with_single_argument/3

get_preference/2

get_preference_with_warnings/2

get_preferences_list/1

get_preferences_list/2

get_prob_application_type/1

get_recent_documents/1

get_time_out_preference_with_factor/2

has_default_value/1

hex/1

init_preferences/0

invalid_application/2

is_of_type/2

load_preferences/1

load_preferences2/2

merge_prefix_with_suffix/3

non_default_pref/1

nr_of_recent_documents/1

Dynamic: true

obsolete_eclipse_preference/1

obsolete_preference/1

obsolete_preference(optimize_enum_set_elems).

obsolete_preference(warn_when_expanding_infinite_closures).

obsolete_preference(do_neginvariant_checking). % use double_evaluation_when_analysing

obsolete_preference(check_prolog_b_ast).

obsolete_preference(use_large_jvm_for_parser).

obsolete_preference(default_to_runtime_type_checking_on_startup_for_expert).

obsolete_preference(animate_skip_operations).

obsolete_preference(debug_try_minimise).

obsolete_preference(convert_types_into_closures).

obsolete_preference(use_avl_trees_for_sets).

obsolete_preference(dot_font_size).

obsolete_preference(only_label_base_types).

obsolete_preference(use_new_kernel).

obsolete_preference(findOnlyOneSol).

obsolete_preference(enable_permutation_reducation).

obsolete_preference(use_symmetry_marker_hash).

obsolete_preference(enable_canonical_symmetry).

obsolete_preference(use_nauty_symmetry_reduction).

obsolete_preference(do_full_invariant_checking).

obsolete_preference(test_case_gen_stop_at_first_error).

obsolete_preference(use_failure_refinement).

obsolete_preference(do_on_the_fly_refinement).

obsolete_preference(never_convert_closures_into_explicit_form).

obsolete_preference(allow_empty_global_sets).

obsolete_preference(multilevel_animation).

obsolete_preference(remove_multilevel_prefix).

obsolete_preference(cspm_allow_incomplete_records).

obsolete_preference(cspm_display_inout).

obsolete_preference(allow_recursive_closures).

obsolete_preference(absint_abstract_domain_module).

obsolete_preference(absint_use_widening).

obsolete_preference(absint_soft_widening).

obsolete_preference(absint_extrapolation_threshold).

obsolete_preference(convert_closures_into_explicit_form_for_store).

obsolete_preference(use_por).

obsolete_preference(use_pge).

obsolete_preference(pge_dis).

obsolete_preference(pge_ind).

obsolete_preference(pge_keep).

obsolete_preference(use_pge_keep).

obsolete_preference(use_pge_dis).

obsolete_preference(use_pge_ind).

obsolete_preference(selected_bparser).

obsolete_preference(dot_print_leaves).

obsolete_preference(csp_event_visible_to_user).

obsolete_preference(path_to_fuzz).

obsolete_preference(use_optimistic_por).

obsolete_preference(show_full_error_span).

obsolete_preference(path_to_sfdp).

obsolete_preference(dot_use_alterate_dot_viewer).

obsolete_preference(path_to_dotty2).

obsolete_preference(prob2_trace_file).

obsolete_preference(prob2_trace_file_gen_unique_name).

obsolete_preference(try_kodkod_on_load).

obsolete_preference(plugin(absint,use_widening)).

obsolete_preference(plugin(absint,soft_widening)).

obsolete_preference(plugin(absint,extrapolation_threshold)).

obsolete_preference(plugin(absint,retract_widening_related_states)).

obsolete_preference(use_por_for_ltl).

obsolete_preference(path_to_smt_solver).

obsolete_preference(try_atb_provers_for_smtlib).

obsolete_preference(bool_expression_as_predicate). % BOOL_AS_PREDICATE

possible_program/2

possible_program_aux/3

possible_program_aux(editor_launch,darwin,'/usr/local/bin/bbedit').

possible_program_aux(editor_launch,darwin,'/usr/local/bin/edit'). % Text Wrangler

possible_program_aux(editor_launch,_,PATH) :- environ('EDITOR',PATH).

possible_program_aux(editor_launch,darwin,'/usr/local/bin/atom').

possible_program_aux(editor_launch,linux,'/usr/local/bin/atom').

possible_program_aux(editor_launch,linux,'/usr/bin/kwrite').

possible_program_aux(editor_launch,linux,'/usr/bin/gedit').

possible_program_aux(editor_launch,linux,'/usr/bin/vim').

possible_program_aux(editor,darwin,'/Applications/BBEdit.app').

possible_program_aux(editor,darwin,'/Applications/TextWrangler.app').

possible_program_aux(editor,darwin,'/Applications/Atom.app').

possible_program_aux(editor,darwin,'/Applications/Sublime Text 2.app').

possible_program_aux(editor,darwin,'/Applications/TextMate.app').

possible_program_aux(editor,darwin,'/Applications/TextEdit.app').

possible_program_aux(editor,_,PATH) :- environ('EDITOR',PATH). % this is the Path in the Terminal; maybe the user wants other programs for the Tcl/Tk GUI; hence this is the last lookup

possible_program_aux(pdf_viewer,darwin,'/Applications/Preview.app') :- prob_application_type(tcltk). % probcli cannot use open -a yet.

possible_program_aux(pdf_viewer,darwin,'/usr/bin/open').

possible_program_aux(pdf_viewer,linux,'/usr/bin/okular'). % KDE

possible_program_aux(pdf_viewer,linux,'/usr/bin/evince'). % GNOME

possible_program_aux(pdf_viewer,windows,'C:/Program Files/Ghostgum/gsview/gsview32').

possible_program_aux(dot_viewer,darwin,'/Applications/MacPorts/Graphviz.app') :- % only version that seems to run on mac
    % sudo port install graphviz-gui (see https://ports.macports.org/port/graphviz-gui/)
    prob_application_type(tcltk).

possible_program_aux(dot_viewer,darwin,'/Applications/Graphviz.app') :- prob_application_type(tcltk). % probcli cannot use open -a yet

possible_program_aux(dot_viewer,darwin,'/Applications/OmniGraffle.app') :- prob_application_type(tcltk).

possible_program_aux(dot_viewer,darwin,'/Applications/Visual Studio Code.app') :-
    % using Graphviz Interactive Preview extension
    prob_application_type(tcltk).

possible_program_aux(dot_viewer,darwin,'/usr/bin/open').

possible_program_aux(dot_viewer,windows,'C:/Program Files/Graphviz2.38/bin/dotty.exe').

possible_program_aux(dot_viewer,windows,'C:/Program Files (x86)/Graphviz2.38/bin/dotty.exe').

possible_program_aux(krt,darwin,'/Applications/AtelierB.app/AB/bbin/macosx/krt').

possible_program_aux(java,windows,'C:/Program Files/Java/jre7/bin/java.exe').

possible_program_aux(java,P,'/usr/bin/java') :- unix(P).

possible_program_aux(fdr3,darwin,'/Applications/FDR3.app/Contents/MacOS/refines').

possible_program_aux(fdr3,darwin,'/Applications/FDR4.app/Contents/MacOS/refines').

possible_program_aux(dot,P,'/usr/local/bin/dot') :- unix(P).

possible_program_aux(dot,darwin,'/opt/homebrew/bin/dot'). % location of new homebrew on M1/Arm Macs

possible_program_aux(dot,P,'/opt/local/bin/dot') :- unix(P). % e.g., location of MacPorts

possible_program_aux(dot,P,'/usr/bin/dot') :- P=linux.

possible_program_aux(pdflatex,P,'/usr/local/texlive/2016/bin/x86_64-darwin/pdflatex') :- P=darwin.

possible_program_aux(pdflatex,P,'/usr/local/texlive/2019/bin/x86_64-darwin/pdflatex') :- P=darwin.

possible_program_aux(pdflatex,P,'/usr/local/bin/pdflatex') :- unix(P).

possible_program_aux(pdflatex,P,'/opt/local/bin/pdflatex') :- unix(P).

possible_program_aux(open,darwin,'/usr/bin/open').

possible_program_aux(open,linux,'xdg-open').

possible_program_aux(open,widnows,'start').

pref_type_synonym/2

preference/2

Dynamic: true

preference_category/2

preference_category(unsat_core_algorithm,advanced).

preference_category(maxint,animation).

preference_category(minint,animation).

preference_category(globalsets_fdrange,animation).

preference_category(do_invariant_checking,advanced).

preference_category(do_assert_checking,advanced).

preference_category(find_abort_values,animation).

preference_category(raise_abort_immediately,advanced).

preference_category(treat_outermost_pre_as_select,animation).

preference_category(require_operations_to_assign_all_outputs,animation).

preference_category(allow_operations_to_read_outputs,advanced).

preference_category(allow_operation_calls_for_uses,advanced).

preference_category(allow_overriding_initialisation,advanced).

preference_category(allow_simultaneous_assignments,hidden). % only useful for loading and inspecting AST

preference_category(allow_arith_operators_on_reals,advanced).

preference_category(solver_for_reals,advanced).

preference_category(cspm_animate_all_processes_without_arguments,csp_prefs).

preference_category(cspm_animate_all_processes,csp_prefs).

preference_category(cspm_detailed_animation,csp_prefs).

preference_category(cspm_strip_source_location,csp_prefs).

preference_category(show_eventb_any_arguments,animation).

preference_category(maxNrOfInitialisations,animation).

preference_category(randomisedRestartInitalisations,advanced).

preference_category(maxNrOfEnablingsPerOperation,animation).

preference_category(time_out,animation).

preference_category(number_animated_abstractions,animation).

preference_category(number_skipped_refined_machines,animation).

preference_category(show_initialisation_arguments,animation).

preference_category(deterministic_trace_replay,hidden).

preference_category(debug_time_out_factor,advanced).

preference_category(jvm_parser_heap_size_mb,advanced).

preference_category(jvm_parser_additional_args,advanced).

preference_category(jvm_parser_position_infos,advanced).

preference_category(jvm_parser_fastrw,hidden).

preference_category(jvm_parser_force_parsing,bool).

preference_category(convert_comprehension_sets_into_closures,animation).

preference_category(use_clpfd_solver,animation).

preference_category(use_chr_solver,animation).

preference_category(data_validation_mode,advanced).

preference_category(use_smt_mode,advanced).

preference_category(solver_strength,advanced).

preference_category(use_common_subexpression_elimination,advanced).

preference_category(remove_implied_constraints,advanced).

preference_category(lift_existential_quantifiers,advanced).

preference_category(use_common_subexpression_also_for_predicates,advanced).

preference_category(use_common_subexpression_also_for_substitutions,advanced).

preference_category(use_common_subexpression_wd_only,advanced).

preference_category(normalize_ast,hidden).

preference_category(normalize_ast_sort_commutative,hidden).

preference_category(optimize_ast,advanced).

preference_category(useless_code_elimination,advanced).

preference_category(compile_while_body,advanced).

preference_category(detect_lambdas,advanced).

preference_category(auto_detect_theory_ops,advanced).

preference_category(ltsmin_guard_splitting,hidden).

preference_category(ltsmin_do_not_evaluate_top_level_guards,hidden).

preference_category(fail_if_clpfd_timeout,advanced).

preference_category(use_static_ordering,advanced).

preference_category(use_state_packing,advanced).

preference_category(force_state_packing_for_closures,hidden).

preference_category(provide_trace_information,advanced).

preference_category(prob_profiling_on,advanced).

preference_category(prob_source_profiling_on,advanced).

preference_category(performance_monitoring_on,advanced).

preference_category(performance_monitoring_expansion_limit,advanced).

preference_category(partition_predicates,advanced).

preference_category(partition_predicates_inline_equalities,advanced).

preference_category(use_closure_expansion_memoization,advanced).

preference_category(use_function_memoization,advanced).

preference_category(allow_incomplete_partial_setup_constants,advanced).

preference_category(re_execute_operations_with_side_effects,advanced).

preference_category(warn_if_definition_hides_variable,advanced).

preference_category(type_check_definitions,advanced).

preference_category(allow_enumeration_of_infinite_types,advanced).

preference_category(strict_raise_warnings,advanced).

preference_category(strict_raise_enum_warnings,hidden). % only for testing

preference_category(clash_strict_checks,advanced).

preference_category(perform_stricter_static_checks,hidden). % set by prob

preference_category(ignore_prj_types,advanced).

preference_category(ignore_hash_collisions,advanced).

preference_category(forget_state_space,advanced).

preference_category(store_only_one_incoming_transition,advanced).

preference_category(mc_continue_after_error,hidden).

preference_category(symmetry_mode,hidden).

preference_category(use_static_symmetry_detection,advanced).

preference_category(allow_untyped_identifiers,hidden).

preference_category(repl_unicode,syntax_highlighting).

preference_category(repl_cache_parsing,hidden).

preference_category(cache_operations,hidden).

preference_category(latex_encoding,latex).

preference_category(latex_pp_greek_ids,latex).

preference_category(xml_encoding,hidden).

preference_category(view_probcli_errors_using_bbresults,hidden).

preference_category(eventtrace,animation).

preference_category(store_event_transinfo,hidden). % automatically set by probcli

preference_category(use_solver_on_load,hidden). % hidden for the moment

preference_category(kodkod_for_components,advanced).

preference_category(kodkod_raise_warnings,advanced).

preference_category(kodkod_max_nr_solutions,advanced).

preference_category(kodkod_symmetry_level,advanced).

preference_category(kodkod_sat_solver,advanced).

preference_category(smt_supported_interpreter,advanced).

preference_category(sat_supported_interpreter,advanced).

preference_category(use_record_construction,advanced).

preference_category(seen_machines_included,animation).

preference_category(allow_sequence_operators_on_strings,animation).

preference_category(prefix_internal_operation_arguments,advanced).

preference_category(generate_minimal_nr_of_testcases,advanced).

preference_category(use_tk_custom_state_viewer,hidden). % actually : if user wants to turn it off; simply do not define ANIMATION_FUNCTION

preference_category(tk_custom_state_viewer_font_name,hidden).

preference_category(tk_custom_state_viewer_font_size,hidden).

preference_category(tk_custom_state_viewer_padding,animation).

preference_category(tk_custom_state_viewer_str_padding,animation).

preference_category(use_small_window,animation).

preference_category(tk_show_source_pane,animation).

preference_category(path_to_ltsmin,advanced).

preference_category(dot_print_node_ids,dot).

preference_category(dot_print_transition_ids,dot).

preference_category(dot_print_use_constants,dot).

preference_category(dot_print_node_info,dot).

preference_category(dot_print_edge_labels,dot).

preference_category(dot_print_action_arguments,dot).

preference_category(dot_print_functions,dot).

preference_category(dot_print_self_loops,dot).

preference_category(dot_print_root,dot).

preference_category(dot_print_arc_colors,dot).

preference_category(dot_use_ps_viewer,hidden).

preference_category(path_to_dotty,dot).

preference_category(path_to_dot,dot).

preference_category(dot_default_engine,dot).

preference_category(path_to_ps_viewer,dot).

preference_category(dot_root_shape,dot).

preference_category(dot_node_penwidth,dot).

preference_category(dot_edge_penwidth,dot).

preference_category(dot_normal_node_shape,dot).

preference_category(dot_current_node_shape,dot).

preference_category(dot_open_node_colour,dot).

preference_category(dot_scope_limit_node_colour,dot).

preference_category(dot_normal_node_colour,dot).

preference_category(dot_invariant_violated_node_colour,dot).

preference_category(dot_fill_normal_nodes,dot).

preference_category(dot_normal_arc_colour,dot).

preference_category(dot_node_font_size,dot).

preference_category(dot_edge_font_size,dot).

preference_category(dot_with_page_size,dot).

preference_category(dot_horizontal_layout,dot).

preference_category(dot_colour_goal_nodes,dot).

preference_category(dot_goal_node_colour,dot).

preference_category(dot_print_node_properties,dot).

preference_category(dot_counterexample_node_colour,dot).

preference_category(dot_counterexample_op_colour,dot).

preference_category(dot_event_hierarchy_horizontal,dot_event_hierarchy).

preference_category(dot_event_hierarchy_machine_colour,dot_event_hierarchy).

preference_category(dot_event_hierarchy_refines_colour,dot_event_hierarchy).

preference_category(dot_event_hierarchy_new_event_colour,dot_event_hierarchy).

preference_category(dot_event_hierarchy_rename_event_colour,dot_event_hierarchy).

preference_category(dot_event_hierarchy_unchanged_event_colour,dot_event_hierarchy).

preference_category(dot_event_hierarchy_rename_unchanged_event_colour,dot_event_hierarchy).

preference_category(dot_event_hierarchy_grd_strengthening_event_colour,dot_event_hierarchy).

preference_category(dot_event_hierarchy_grd_keeping_event_colour,dot_event_hierarchy).

preference_category(dot_event_hierarchy_edge_colour,dot_event_hierarchy).

preference_category(dot_event_hierarchy_extends_colour,dot_event_hierarchy).

preference_category(dot_hierarchy_show_extra_detail,dot_event_hierarchy).

preference_category(dot_projection_non_det_edge_colour,dot_projection).

preference_category(dot_projection_det_edge_colour,dot_projection).

preference_category(dot_projection_non_definite_edge_style,dot_projection).

preference_category(dot_projection_definite_edge_style,dot_projection).

preference_category(dot_projection_label_limit,dot_projection).

preference_category(dot_projection_process_only_explored,dot_projection).

preference_category(dot_use_unicode,dot_projection).

preference_category(dot_predicate_node_shape,dot_formula_tree).

preference_category(dot_expression_node_shape,dot_formula_tree).

preference_category(dot_var_mod_hide_only_written,dot_variable_modification).

preference_category(mc_dc_default_level,mc_dc_commands).

preference_category(dot_enabling_show_readwrites,dot).

preference_category(dot_definitions_use_sub_graph,dot_definitions).

preference_category(dot_definitions_show_all,dot_definitions).

preference_category(dot_state_graph_decompose,dot_state_graph).

preference_category(dot_hierarchy_max_ids,dot_machine_hierarchy).

preference_category(cbc_provide_explanations,cbc_commands).

preference_category(font_size,gui_prefs).

preference_category(font_name,gui_prefs).

preference_category(font_size_only,gui_prefs).

preference_category(use_font_size_for_columns,advanced).

preference_category(allow_source_code_editing,gui_prefs).

preference_category(show_line_numbers,gui_prefs).

preference_category(highlight_brackets,gui_prefs).

preference_category(highlight_current_line,gui_prefs).

preference_category(ask_when_content_changed,gui_prefs).

preference_category(user_not_beginner,gui_prefs).

preference_category(user_is_an_expert_with_accessto_source_distribution,hidden).

preference_category(path_to_probe,csp_prefs).

preference_category(path_to_fdr,csp_prefs).

preference_category(path_to_csp_typechecker,csp_prefs).

preference_category(path_to_bcomp,advanced).

preference_category(path_to_java,advanced).

preference_category(path_to_java_parser,hidden).

preference_category(path_to_atb_krt,advanced). % not yet used from within ProB Tcl/Tk, ...

preference_category(try_atb_provers,advanced).

preference_category(smtlib2b_arrays_as_sets,smtlib2b).

preference_category(smtlib2b_cleanup_predicate,smtlib2b).

preference_category(symbolic_mc_try_other_solvers,advanced).

preference_category(path_to_spin,advanced).

preference_category(path_to_cspm,advanced).

preference_category(path_to_text_editor,advanced).

preference_category(path_to_text_editor_launch,hidden).

preference_category(number_of_recent_documents,advanced).

preference_category(number_of_searched_patterns,advanced).

preference_category(number_of_replaced_patterns,advanced).

preference_category(number_of_eval_history_elements,advanced).

preference_category(number_of_eval_csp_history_elements,advanced).

preference_category(number_of_checked_ltl_formulas,advanced).

preference_category(allow_new_ops_in_refinement,advanced).

preference_category(allow_local_operation_calls,advanced).

preference_category(allow_operation_calls_in_expr,advanced).

preference_category(allow_let_to_reuse_introduced_ids,advanced).

preference_category(use_po,advanced).

preference_category(try_operation_reuse,advanced).

preference_category(randomise_operation_order,advanced).

preference_category(randomise_enumeration_order,advanced).

preference_category(perform_enumeration_order_analysis,advanced).

preference_category(set_rand,advanced).

preference_category(rand_seed,advanced).

preference_category(ltl_to_ba_tool,advanced).

preference_category(do_syntax_highlighting,syntax_highlighting).

preference_category(sh_type_colour,syntax_highlighting).

preference_category(sh_logical_colour,syntax_highlighting).

preference_category(sh_assignments_colour,syntax_highlighting).

preference_category(sh_operators,syntax_highlighting).

preference_category(sh_top_level_keywords,syntax_highlighting).

preference_category(sh_control_keywords,syntax_highlighting).

preference_category(sh_comments,syntax_highlighting).

preference_category(sh_pragmas,syntax_highlighting).

preference_category(sh_unsupported_background,syntax_highlighting).

preference_category(expand_forall_upto,advanced).

preference_category(double_evaluation_when_analysing,advanced).

preference_category(prob_safe_mode,advanced).

preference_category(expand_avl_upto,advanced).

preference_category(show_bvisual_formula_functor_from,advanced).

preference_category(show_bvisual_proof_info_icons,advanced).

preference_category(show_bvisual_formula_explanations,advanced).

preference_category(formula_tree_minimal_timeout,dot_formula_tree).

preference_category(formula_tree_maximal_timeout,dot_formula_tree).

preference_category(show_function_tuples_in_property,animation).

preference_category(bugly_pp_scrambling,advanced).

preference_category(pp_propositional_logic_mode,hidden).

preference_category(pp_wd_infos,hidden).

preference_category(pp_with_terminal_colour,hidden).

preference_category(wd_ignore_external_funs,wd_analyser).

preference_category(wd_skip_finite_pos,wd_analyser).

preference_category(wd_analysis_for_animation,wd_analyser).

preference_category(z3_solve_for_animation,advanced).

preference_category(add_wd_pos_for_z3,advanced).

preference_category(machines_path,hidden).

preference_category(alloy_use_implementable_integers,alloy2b).

preference_category(alloy_scopeless_translation,alloy2b).

preference_category(alloy_translation_for_proof,alloy2b).

preference_category(alloy_strict_integers,alloy2b).

preference_category(use_scope_predicate,advanced).

preference_category(use_ignore_pragmas,advanced).

preference_category(pge,model_checker).

preference_category(use_cbc_analysis,advanced). % for por

preference_category(timeout_cbc_analysis,advanced).

preference_category(por,model_checker).

preference_category(por_heur,model_checker).

preference_category(use_safety_ltl_model_checker,model_checker).

preference_category(enable_graph,model_checker).

preference_category(enable_graph_depth,model_checker).

preference_category(dependency_enable_predicates,model_checker).

preference_category(path_to_latex,latex).

preference_category(filter_unused_constants,advanced).

preference_category(translate_force_all_typing_infos,hidden).

preference_category(translate_print_typing_infos,hidden).

preference_category(translate_print_frozen_infos,hidden).

preference_category(translate_ids_to_parseable_format,hidden).

preference_category(translate_suppress_rodin_positions_flag,hidden).

preference_category(translate_print_all_sequences,hidden).

preference_category(translate_print_cs_style_sequences,hidden).

preference_category(translation_limit_for_table_commands,wd_commands).

preference_category(visb_allow_variables_for_objects,visb).

preference_category(trace_generation_limit,trace_generator).

preference_category(trace_generation_time_out,trace_generator).

preference_category(disprover_mode,advanced).

preference_category(allow_improving_wd_mode,hidden).

preference_category(trace_upon_error,hidden).

preference_category(error_log_file,advanced).

preference_category(tlc_number_of_workers,hidden).

preference_category(tlc_use_prob_constant_setup,hidden).

preference_category(port, distb).

preference_category(ip, distb).

preference_category(max_states, distb).

preference_category(tmpdir, distb).

preference_category(logdir, distb).

preference_category(proxynumber, distb).

preference_category(queue_threshold, distb).

preference_category(hash_cycle, distb).

preference_category(cdclt_perform_static_analysis, cdclt).

preference_category(cdclt_perform_symmetry_breaking, cdclt).

preference_category(cdclt_use_idl_theory_solver,cdclt).

preference_category(prob_version_info,hidden).

preference_category(prob_revision_info, hidden).

preference_category(prob_lastchangedate_info, hidden).

preference_default_value/2

preference_default_value(maxint,3). % 2147483647

preference_default_value(minint,-1). %-2147483648

preference_default_value(number_animated_abstractions, 20).

preference_default_value(number_skipped_refined_machines, 0).

preference_default_value(globalsets_fdrange,2).

preference_default_value(do_invariant_checking,true).

preference_default_value(do_assert_checking,true).

preference_default_value(find_abort_values,false).

preference_default_value(raise_abort_immediately,false).

preference_default_value(treat_outermost_pre_as_select,true).

preference_default_value(require_operations_to_assign_all_outputs,false).

preference_default_value(allow_operations_to_read_outputs,false).

preference_default_value(allow_operation_calls_for_uses,false).

preference_default_value(allow_overriding_initialisation,false).

preference_default_value(allow_simultaneous_assignments,false).

preference_default_value(allow_arith_operators_on_reals,default).

preference_default_value(solver_for_reals,precise_float_solver).

preference_default_value(cspm_animate_all_processes_without_arguments,false).

preference_default_value(cspm_animate_all_processes,false).

preference_default_value(cspm_detailed_animation,false).

preference_default_value(cspm_strip_source_location,false).

preference_default_value(maxNrOfInitialisations,4).

preference_default_value(randomisedRestartInitalisations,false).

preference_default_value(maxNrOfEnablingsPerOperation,10).

preference_default_value(time_out,2500).

preference_default_value(debug_time_out_factor,5).

preference_default_value(jvm_parser_heap_size_mb,0).

preference_default_value(jvm_parser_additional_args,'').

preference_default_value(jvm_parser_position_infos,true).

preference_default_value(jvm_parser_fastrw,false).

preference_default_value(jvm_parser_force_parsing,false).

preference_default_value(show_initialisation_arguments,true).

preference_default_value(deterministic_trace_replay,false).

preference_default_value(show_eventb_any_arguments,false).

preference_default_value(convert_comprehension_sets_into_closures,false). /* <------------ was true */

preference_default_value(use_clpfd_solver,true). % Default was changed from false to true on November 28 2013; commit d26b1bf1edeb29d630cf798c0773bfa1ba71219b

preference_default_value(use_chr_solver,false).

preference_default_value(data_validation_mode,false).

preference_default_value(use_smt_mode,false).

preference_default_value(solver_strength,0).

preference_default_value(remove_implied_constraints,false).

preference_default_value(lift_existential_quantifiers,false).

preference_default_value(use_common_subexpression_elimination,false). % CSE

preference_default_value(use_common_subexpression_also_for_predicates,true). % CSE_PRED

preference_default_value(use_common_subexpression_also_for_substitutions,false). % CSE_SUBST

preference_default_value(use_common_subexpression_wd_only,false). % CSE_WD_ONLY

preference_default_value(normalize_ast,false). % NORMALIZE_AST

preference_default_value(normalize_ast_sort_commutative,false).

preference_default_value(optimize_ast,true). % OPTIMIZE_AST

preference_default_value(useless_code_elimination,false). % see test 1660

preference_default_value(compile_while_body,true). % COMPILE_WHILE

preference_default_value(detect_lambdas,true). % DETECT_LAMBDAS

preference_default_value(auto_detect_theory_ops,false). % DETECT_LAMBDAS

preference_default_value(ltsmin_guard_splitting,false).

preference_default_value(ltsmin_do_not_evaluate_top_level_guards,false).

preference_default_value(fail_if_clpfd_timeout,false).

preference_default_value(use_static_ordering,false).

preference_default_value(use_state_packing,false).

preference_default_value(force_state_packing_for_closures,false).

preference_default_value(provide_trace_information,false).

preference_default_value(prob_profiling_on,false).

preference_default_value(prob_source_profiling_on,false).

preference_default_value(performance_monitoring_on,false).

preference_default_value(performance_monitoring_expansion_limit,100).

preference_default_value(partition_predicates,true).

preference_default_value(partition_predicates_inline_equalities,true).

preference_default_value(use_closure_expansion_memoization,false).

preference_default_value(use_function_memoization,false).

preference_default_value(allow_incomplete_partial_setup_constants,false).

preference_default_value(re_execute_operations_with_side_effects,false).

preference_default_value(warn_if_definition_hides_variable,true).

preference_default_value(type_check_definitions,false). % can consume time, see test 778; and produces error messages for some tests

preference_default_value(allow_enumeration_of_infinite_types,true).

preference_default_value(strict_raise_warnings,false). % Default false as add_closure_warning otherwise will e.g. then be raised as errors; this can confuse predicate_evaluator into returning a not-well-defined result or everybody else relying ErrOcc arg of exit_error_scope

preference_default_value(strict_raise_enum_warnings,false).

preference_default_value(clash_strict_checks,false).

preference_default_value(perform_stricter_static_checks,false).

preference_default_value(ignore_prj_types,false).

preference_default_value(prefix_internal_operation_arguments,'$none'). %all operations arguments are external and shown in testcases

preference_default_value(generate_minimal_nr_of_testcases,true).

preference_default_value(use_tk_custom_state_viewer,true).

preference_default_value(tk_custom_state_viewer_font_name,'').

preference_default_value(tk_custom_state_viewer_font_size,0).

preference_default_value(tk_custom_state_viewer_padding,0).

preference_default_value(tk_custom_state_viewer_str_padding,10).

preference_default_value(use_small_window,false).

preference_default_value(tk_show_source_pane,true).

preference_default_value(ignore_hash_collisions,false).

preference_default_value(forget_state_space,false).

preference_default_value(store_only_one_incoming_transition,false).

preference_default_value(mc_continue_after_error,false).

preference_default_value(symmetry_mode,off).

preference_default_value(use_static_symmetry_detection,true).

preference_default_value(allow_untyped_identifiers,false).

preference_default_value(repl_unicode,false).

preference_default_value(repl_cache_parsing,false).

preference_default_value(cache_operations,true).

preference_default_value(latex_encoding,auto).

preference_default_value(latex_pp_greek_ids,false).

preference_default_value(xml_encoding,auto).

preference_default_value(view_probcli_errors_using_bbresults,false).

preference_default_value(eventtrace,false).

preference_default_value(store_event_transinfo,false).

preference_default_value(use_solver_on_load,prob).

preference_default_value(kodkod_for_components,true).

preference_default_value(kodkod_raise_warnings,false).

preference_default_value(kodkod_max_nr_solutions,22).

preference_default_value(kodkod_symmetry_level,0).

preference_default_value(kodkod_sat_solver,sat4j).

preference_default_value(smt_supported_interpreter,false).

preference_default_value(sat_supported_interpreter,false).

preference_default_value(use_record_construction,true). % was false

preference_default_value(seen_machines_included,false).

preference_default_value(allow_sequence_operators_on_strings,true).

preference_default_value(dot_print_edge_labels,true).

preference_default_value(dot_print_action_arguments,true).

preference_default_value(dot_print_functions,false).

preference_default_value(dot_print_self_loops,true).

preference_default_value(dot_print_arc_colors,true).

preference_default_value(dot_print_root,true).

preference_default_value(dot_print_node_ids,false).

preference_default_value(dot_print_transition_ids,false).

preference_default_value(dot_print_use_constants,true).

preference_default_value(dot_print_node_info,true).

preference_default_value(dot_use_ps_viewer,PS) :- host_platform(X),
    (X = darwin -> PS = true % on recent macOS platforms all GraphViz Dotty viewers seem broken
    ; X=windows -> PS = true % GraphViz no longer seems to distribute the Dotty viewer
    ; PS=false).

preference_default_value(path_to_dot,Path) :- try_get_program_path('dot',Path).

preference_default_value(dot_default_engine,dot).

preference_default_value(path_to_dotty,VIEWER) :- (possible_program(dot_viewer,E) -> VIEWER=E ; VIEWER ='dotty').

preference_default_value(path_to_ltsmin,'./lib/'). % Path to where we can find prob2lts min commands like prob2lts-sym; default means we look in lib

preference_default_value(path_to_ps_viewer,VIEWER) :-
    (possible_program(pdf_viewer,E) -> VIEWER=E ; VIEWER ='gv').

preference_default_value(path_to_latex,Path) :- try_get_program_path('pdflatex',Path).

preference_default_value(dot_root_shape,invtriangle).

preference_default_value(dot_node_penwidth,2).

preference_default_value(dot_edge_penwidth,1).

preference_default_value(dot_normal_node_shape,box). % egg,ellipse

preference_default_value(dot_current_node_shape,doubleoctagon).

preference_default_value(dot_open_node_colour,'#F4E3C1'). %'#E88C59' '#C96D37'

preference_default_value(dot_scope_limit_node_colour,gray).

preference_default_value(dot_normal_node_colour,'#99BF38').

preference_default_value(dot_invariant_violated_node_colour,'#FF3800'). %'#FF4409'

preference_default_value(dot_fill_normal_nodes,false).

preference_default_value(dot_normal_arc_colour,'#006391').

preference_default_value(dot_node_font_size,12).

preference_default_value(dot_edge_font_size,12).

preference_default_value(dot_with_page_size,true).

preference_default_value(dot_horizontal_layout,false).

preference_default_value(dot_colour_goal_nodes,true).

preference_default_value(dot_goal_node_colour,orange).

preference_default_value(dot_print_node_properties,false).

preference_default_value(dot_counterexample_node_colour,brown).

preference_default_value(dot_counterexample_op_colour,brown).

preference_default_value(dot_hierarchy_max_ids,0).

preference_default_value(cbc_provide_explanations,false).

preference_default_value(dot_event_hierarchy_horizontal,true).

preference_default_value(dot_event_hierarchy_machine_colour,gray95).

preference_default_value(dot_event_hierarchy_refines_colour,'#C0A060'). % Dark Khaki; see http://www.gpeters.com/color/color-schemes.php?search_term=Art+Nouveau

preference_default_value(dot_event_hierarchy_new_event_colour,'#C06040'). % Coral '#C08040'). % Peru

preference_default_value(dot_event_hierarchy_rename_event_colour,'#E0E0A0'). % Pale Goldenrod

preference_default_value(dot_event_hierarchy_rename_unchanged_event_colour,'#E0F0E0'). % Honeydew

preference_default_value(dot_event_hierarchy_unchanged_event_colour,gray92).

preference_default_value(dot_event_hierarchy_grd_strengthening_event_colour,gray83).

preference_default_value(dot_event_hierarchy_grd_keeping_event_colour,'#E0C080'). % Burlywood

preference_default_value(dot_event_hierarchy_edge_colour,'#806040'). % Sienna

preference_default_value(dot_event_hierarchy_extends_colour,gray50).

preference_default_value(dot_hierarchy_show_extra_detail,false).

preference_default_value(dot_projection_non_det_edge_colour,'#806040'). % Sienna; alternative :#A06040 Light Salmon

preference_default_value(dot_projection_det_edge_colour,black).

preference_default_value(dot_projection_non_definite_edge_style,dashed).

preference_default_value(dot_projection_definite_edge_style,solid).

preference_default_value(dot_projection_label_limit,75).

preference_default_value(dot_projection_process_only_explored,false).

preference_default_value(dot_use_unicode,true).

preference_default_value(dot_predicate_node_shape,rect).

preference_default_value(dot_expression_node_shape,record).

preference_default_value(dot_var_mod_hide_only_written,false).

preference_default_value(mc_dc_default_level,2).

preference_default_value(dot_enabling_show_readwrites,true).

preference_default_value(dot_definitions_use_sub_graph,true).

preference_default_value(dot_definitions_show_all,false).

preference_default_value(dot_state_graph_decompose,true).

preference_default_value(font_size,'Monaco 12') :- host_platform(darwin).

preference_default_value(font_size,'TkFixedFont 12') :- host_platform(X), X\==darwin. % alternative: Courier, Monaco, Consolas

preference_default_value(font_name,'Monaco') :- host_platform(darwin).

preference_default_value(font_name,'TkFixedFont') :- host_platform(X), X\==darwin. % alternative: Courier, Monaco

preference_default_value(font_size_only,12).

preference_default_value(use_font_size_for_columns,false).

preference_default_value(allow_source_code_editing,true).

preference_default_value(show_line_numbers,false).

preference_default_value(highlight_brackets,true).

preference_default_value(highlight_current_line,true).

preference_default_value(ask_when_content_changed,false).

preference_default_value(user_not_beginner,false).

preference_default_value(user_is_an_expert_with_accessto_source_distribution,false).

preference_default_value(path_to_probe,'C:/probe/probe-1.30-windows/probe.exe') :- host_platform(windows).

preference_default_value(path_to_probe,'more') :- host_platform(X), X\==windows.

preference_default_value(path_to_spin,'xspin').

preference_default_value(path_to_cspm,'/usr/bin/cspm').

preference_default_value(path_to_text_editor,EDITOR) :-
    (possible_program(editor,E) -> EDITOR=E ; EDITOR ='').

preference_default_value(path_to_text_editor_launch,EDITOR) :-
    (possible_program(editor_launch,E) -> EDITOR=E ; EDITOR ='vi').

preference_default_value(path_to_fdr,'fdr2').

preference_default_value(path_to_csp_typechecker,FDR3) :-
    (possible_program(fdr3,E) -> FDR3=E ; FDR3 ='refines').

preference_default_value(path_to_bcomp,'bcomp').

preference_default_value(path_to_atb_krt,Default) :- try_get_program_path('krt',Default).

preference_default_value(path_to_java,Default) :- try_get_program_path('java',Default).

preference_default_value(path_to_java_parser,''). % use default probcliparser.jar in lib folder

preference_default_value(try_atb_provers,false).

preference_default_value(smtlib2b_arrays_as_sets,false).

preference_default_value(smtlib2b_cleanup_predicate,false).

preference_default_value(symbolic_mc_try_other_solvers,false).

preference_default_value(ltl_to_ba_tool,'lib/ltl2ba').

preference_default_value(number_of_recent_documents,25).

preference_default_value(number_of_searched_patterns,9).

preference_default_value(number_of_replaced_patterns,9).

preference_default_value(number_of_eval_history_elements,50).

preference_default_value(number_of_eval_csp_history_elements,50).

preference_default_value(number_of_checked_ltl_formulas,20).

preference_default_value(do_syntax_highlighting,true).

preference_default_value(sh_type_colour,darkred).

preference_default_value(sh_logical_colour,tomato).

preference_default_value(sh_assignments_colour,darkslateblue).

preference_default_value(sh_operators,'#5883be').

preference_default_value(sh_top_level_keywords,blue).

preference_default_value(sh_control_keywords,darkviolet).

preference_default_value(sh_comments,'#784e50').

preference_default_value(sh_pragmas,'#5b5b5b').

preference_default_value(sh_unsupported_background,yellow).

preference_default_value(expand_forall_upto,100).

preference_default_value(double_evaluation_when_analysing,true).

preference_default_value(prob_safe_mode,false).

preference_default_value(expand_avl_upto,100).

preference_default_value(show_bvisual_formula_explanations,false).

preference_default_value(show_bvisual_formula_functor_from,Val) :-
    (get_prob_application_type(tcltk) -> Val=0 ; Val = -1). % disable for ProB2

preference_default_value(show_bvisual_proof_info_icons,Val) :-
    (get_prob_application_type(tcltk) -> Val=true ; Val = false). % disable for ProB2

preference_default_value(formula_tree_minimal_timeout,1000).

preference_default_value(formula_tree_maximal_timeout,30000).

preference_default_value(show_function_tuples_in_property,true).

preference_default_value(bugly_pp_scrambling,false).

preference_default_value(pp_propositional_logic_mode,false).

preference_default_value(pp_wd_infos,false).

preference_default_value(pp_with_terminal_colour,false).

preference_default_value(wd_ignore_external_funs,false).

preference_default_value(wd_skip_finite_pos,false).

preference_default_value(wd_analysis_for_animation,true).

preference_default_value(z3_solve_for_animation,true).

preference_default_value(add_wd_pos_for_z3,true).

preference_default_value(allow_new_ops_in_refinement,false).

preference_default_value(allow_local_operation_calls,false).

preference_default_value(allow_operation_calls_in_expr,false).

preference_default_value(allow_let_to_reuse_introduced_ids,false).

preference_default_value(use_po,true).

preference_default_value(try_operation_reuse,false).

preference_default_value(randomise_operation_order,false).

preference_default_value(randomise_enumeration_order,false).

preference_default_value(perform_enumeration_order_analysis,true).

preference_default_value(set_rand,false).

preference_default_value(rand_seed,2342452).

preference_default_value(use_cbc_analysis,true).

preference_default_value(timeout_cbc_analysis,300).

preference_default_value(use_scope_predicate,true).

preference_default_value(use_ignore_pragmas,false).

preference_default_value(alloy_use_implementable_integers,false).

preference_default_value(alloy_scopeless_translation,false).

preference_default_value(alloy_translation_for_proof,false).

preference_default_value(alloy_strict_integers,true).

preference_default_value(pge,off).

preference_default_value(por,off).

preference_default_value(por_heur,random).

preference_default_value(use_safety_ltl_model_checker,true).

preference_default_value(enable_graph,false).

preference_default_value(enable_graph_depth,1).

preference_default_value(dependency_enable_predicates,false).

preference_default_value(filter_unused_constants,false).

preference_default_value(translate_force_all_typing_infos,false).

preference_default_value(translate_print_typing_infos,false).

preference_default_value(translate_print_frozen_infos,false).

preference_default_value(translate_ids_to_parseable_format,false).

preference_default_value(translate_suppress_rodin_positions_flag,false).

preference_default_value(translate_print_all_sequences,false).

preference_default_value(translate_print_cs_style_sequences,false).

preference_default_value(translation_limit_for_table_commands,100).

preference_default_value(visb_allow_variables_for_objects,Res) :-
    (prob_application_type(tcltk) -> Res=true ; Res=false).

preference_default_value(trace_generation_limit,100).

preference_default_value(trace_generation_time_out,2147483646). % disabled

preference_default_value(disprover_mode,false).

preference_default_value(allow_improving_wd_mode,false).

preference_default_value(trace_upon_error,false).

preference_default_value(error_log_file,'').

preference_default_value(tlc_number_of_workers,2).

preference_default_value(tlc_use_prob_constant_setup,false).

preference_default_value(unsat_core_algorithm,linear_greedy).

preference_default_value(port, 6000). % on macOS Monterey 5000 and 7000 are now used by control center

preference_default_value(ip, localhost).

preference_default_value(max_states, 0).

preference_default_value(tmpdir, '/tmp/').

preference_default_value(logdir, './distb-logs/').

preference_default_value(proxynumber, 0).

preference_default_value(queue_threshold, 20). /* TODO: this is not used an implemented in the proxy (pk, 12.01.18) */

preference_default_value(hash_cycle, 25).

preference_default_value(cdclt_perform_static_analysis, true).

preference_default_value(cdclt_perform_symmetry_breaking, false).

preference_default_value(cdclt_use_idl_theory_solver, false).

preference_default_value(prob_version_info,Version) :- version_str(Version).

preference_default_value(prob_revision_info,Rev) :- revision(Rev).

preference_default_value(prob_lastchangedate_info,D) :- lastchangeddate(D).

preference_default_value(machines_path,Dir) :-
    catch(absolute_file_name(examples('.'),Dir),_,Dir='.').

preference_description/2

preference_description(maxNrOfInitialisations,'Max Number of Initialisations and Constant-Setups Computed').

preference_description(randomisedRestartInitalisations,'Use Randomised Restart for Initialisation and Constant Setup (only makes sense if RANDOMISE_ENUMERATION_ORDER is set; for an operation OP use MAX_OPERATIONS_OP == -Nr)').

preference_description(maxNrOfEnablingsPerOperation,'Max Number of Enablings per Operation Computed').

preference_description(time_out,'Time out for computing enabled transitions (in ms, is multiplied by a factor for other computations, value 2147483646 turns time outs off)').

preference_description(globalsets_fdrange,'Size of unspecified deferred sets in SETS section').

preference_description(maxint,Desc) :-
    (get_prob_application_type(rodin)
    -> Desc='maximum value for unbounded integer enumerations'
    ; Desc='value of MAXINT, controls enumeration of integers and used to define NAT in classical B (2147483647 for 32 bit ints)').

preference_description(minint,Desc) :-
    (get_prob_application_type(rodin)
    -> Desc='minimum value for unbounded integer enumerations'
    ; Desc='value of MININT, controls enumeration of integers and used to define INT in classical B (-2147483648 for 32 bit ints)'). % Atelier-B uses 2147483647

preference_description(number_animated_abstractions,'How many levels of refined Event-B models are animated by default').

preference_description(number_skipped_refined_machines,'How many levels of concrete Event-B refinements are skipped for animation').

preference_description(debug_time_out_factor,'Debug Properties: Multiplying Factor for Timeout').

preference_description(jvm_parser_heap_size_mb,'Heap size in MB for Java parser (-Xmx JVM option, 0 means default value)').

preference_description(jvm_parser_additional_args,'Additional arguments sent to the JVM for the Java parser (e.g., "-XX:+UseG1GC -Xss5m")').

preference_description(jvm_parser_position_infos,'Produce detailed position information in the Java parser (turn off to reduce memory consumption for very large B machines; change requires restarting ProB)').

preference_description(jvm_parser_fastrw,'Use binary (fastrw) format for .prob files for faster loading').

preference_description(jvm_parser_force_parsing,'Always parse B machines even if .prob file is up-to-date').

preference_description(do_invariant_checking,'Check invariant while animating and model checking').

preference_description(do_assert_checking,'Check ASSERT statements while animating and model checking').

preference_description(find_abort_values,'Try more aggressively to detect not well-defined expressions (e.g. applying function outside of domain), may slow down animator; possible values false,true,full').

preference_description(raise_abort_immediately,'Raise potential well-definedness issues immediately (may lead to false spurious alarms, but can allow to better detect WD issues which lead to timeouts; possible values false,true,full)').

preference_description(cspm_animate_all_processes,'Animate all CSP-M processes (also processes with arguments)').

preference_description(cspm_animate_all_processes_without_arguments,'Animate all CSP-M processes without arguments (not just MAIN)').

preference_description(cspm_detailed_animation,'Provide more fine-grained source-location animation for CSP (can slow model checking down)').

preference_description(cspm_strip_source_location,'Strip CSP source-location information (for RHS of processes, except for internal choice)').

preference_description(use_clpfd_solver,'Use CLP(FD) solver for B integers (restricts range to -2^28..2^28-1 on 32 bit machines)').

preference_description(use_chr_solver,'Use CHR based solver. Should speed up detection of unsolvable predicates, but might slow down solving in general.').

preference_description(data_validation_mode,'Assume everything can be computed without constraint solving.').

preference_description(convert_comprehension_sets_into_closures,'Lazy expansion of lambdas and set comprehensions').

preference_description(use_smt_mode,'Enable SMT-Mode (more aggressive enumeration of case distinctions inside predicates compared to enumeration of data values)'). % will be set automatically in CBC mode; should normally not be set by user

preference_description(solver_strength,'Strength of certain Solver propagations (0 is default)').

preference_description(remove_implied_constraints,'Remove unnecessary constraints implied by other constraints').

preference_description(lift_existential_quantifiers,'Lift existential quantifiers, i.e., treat existentially quantified variables like ordinary variables').

preference_description(use_common_subexpression_elimination,'Enable CSE (Common Subexpression Elimination)').

preference_description(use_common_subexpression_also_for_predicates,'Apply CSE (if enabled) also to predicates').

preference_description(use_common_subexpression_also_for_substitutions,'Apply CSE (if enabled) also to substitutions (operation/event bodies) [EXPERIMENTAL]').

preference_description(use_common_subexpression_wd_only,'Apply CSE (if enabled) only to well-defined sub-formulas').

preference_description(normalize_ast,'Normalize AST before passing to ProB kernel (rewrites many B predicates into simpler form)').

preference_description(normalize_ast_sort_commutative,'Sort commutative operators (useful with NORMALIZE_AST to try detect equivalent formulas)').

preference_description(optimize_ast,'Optimize AST (Abstract Syntax Tree) before passing to ProB kernel (rewrites many B predicates into more efficient form)').

preference_description(useless_code_elimination,'Useless Code Elimination: try and find useless statements which have no influence on the result of an operation.').

preference_description(compile_while_body,'Compile bodies of WHILE loops if variant large').

preference_description(detect_lambdas,'Detect set comprehensions which can be rewritten into lambdas.').

preference_description(auto_detect_theory_ops,'Try and detect mappings of Rodin axiomatic theory operators based on name.').

preference_description(ltsmin_guard_splitting,'Detect GUARDS of operations which do not depend on parameters (for LTSMin); these guards will not be evaluated by the interpreter when ltsmin_do_not_evaluate_top_level_guards is true').

preference_description(ltsmin_do_not_evaluate_top_level_guards,'Do not evaluate top-level GUARDS detected when true (for guards detected by ltsmin_guard_splitting) or full (for all top-level guards for PGE)').

preference_description(fail_if_clpfd_timeout,'Assume failure if posting a CLP(FD) constraint times-out').

preference_description(use_static_ordering,'Use static ordering to enumerate constants which occur in most PROPERTIES first'). % sort properties

preference_description(use_state_packing,'Use more aggressive COMPRESSION when storing states (false: off, true: compromise between speed and memory, full: preserve more memory)').

preference_description(force_state_packing_for_closures,'Use more aggressive COMPRESSION when storing states (false: off, symbolic closures'). % only has influence if use_state_packing is not already full

preference_description(provide_trace_information,'Provide various tracing information on the terminal/console.').

preference_description(prob_profiling_on,'Keep track of ProB profiling information (e.g., for time spent in operations or memoized function calls)').

preference_description(prob_source_profiling_on,'Keep track of ProB source profiling information (e.g., which parts of the B source code is covered)').

preference_description(performance_monitoring_on,'Provide performance monitoring information on the terminal/console.').

preference_description(performance_monitoring_expansion_limit,'Limit in ms for printing warnings when expanding comprehension sets in performance monitoring mode.').

preference_description(partition_predicates,'Partition predicates (PROPERTIES) into components').

preference_description(partition_predicates_inline_equalities,'Inline equalities when partitioning into components').

preference_description(use_closure_expansion_memoization,'MEMOize expansions of set comprehensions and lambda abstractions.').

preference_description(use_function_memoization,'MEMOIZE function applications of all functions defined in ABSTRACT_CONSTANTS (even if not marked with /*@desc memo */).').

preference_description(allow_incomplete_partial_setup_constants,'Allow ProB to proceed even if only part of the CONSTANTS have been found.').

preference_description(re_execute_operations_with_side_effects,'Re-execute operations with side-effects in the animator (only works for the forward button at the moment).').

preference_description(warn_if_definition_hides_variable,'Warn if a DEFINITION hides a variable with the same name').

preference_description(type_check_definitions,'Type check all visible DEFINITIONs (not just used ones)').

preference_description(allow_enumeration_of_infinite_types,'Allow enumeration of infinite types').

preference_description(strict_raise_warnings,'Treat warnings as errors (Warning: can generate spurious NOT-WELL-DEFINED messages).').

preference_description(strict_raise_enum_warnings,'Treat ENUMERATION warnings (aka VIRTUAL TIME-OUTS) as errors (Warning: can generate spurious NOT-WELL-DEFINED messages).').

preference_description(clash_strict_checks,'Do a stricter checking for name CLASHES in B machines').

preference_description(perform_stricter_static_checks,'Perform stricter additional static checks on formulas (automatically set by ProB).').

preference_description(ignore_prj_types,'Ignore types of prj1 and prj2 (i.e., prj1({1},{1})(2,3) is considered well-defined').

preference_description(prefix_internal_operation_arguments,'Prefix of internal operation arguments (these are not included in test cases)').

preference_description(generate_minimal_nr_of_testcases,'Generate minimal suite of mcm testcases (and not one per event)').

preference_description(use_tk_custom_state_viewer,'Use custom Tk viewer to represent state of B Machine').

preference_description(tk_custom_state_viewer_font_name,'Font for animation strings (if empty, the editor font will be used)').

preference_description(tk_custom_state_viewer_font_size,'Font size for animation strings (if 0, the editor font size will be used)').

preference_description(tk_custom_state_viewer_padding,'Padding (in pixels) between images of custom TK state viewer').

preference_description(tk_custom_state_viewer_str_padding,'Padding (in pixels) between strings of custom TK state viewer').

preference_description(use_small_window,'Use a small main window for ProB (useful on small screens)').

preference_description(tk_show_source_pane,'Show the B Source Code').

preference_description(ignore_hash_collisions,'Ignore hash collisions in state space (if true not all states may be computed!)').

preference_description(forget_state_space,'Do not remember state space (mainly useful in conjunction with IGNORE_HASH_COLLISIONS)').

preference_description(store_only_one_incoming_transition,'Only store one incoming transition/operation per reached state. Can be used when model checking of safety properties (invariants, goal, assertions). Do not use for LTL model checking, deadlock checking or animation.'). % TO DO: check config

preference_description(mc_continue_after_error,'Continue model checking even after an error or goal has been found').

preference_description(symmetry_mode,'Symmetry Mode: off,flood,canon,nauty,hash').

preference_description(use_static_symmetry_detection,'Detect symmetries in forall/exists and in PROPERTIES for deferred sets').

preference_description(allow_untyped_identifiers,'Allow UNTYPED identifiers (they will be assigned new deferred sets as type)' ).

preference_description(repl_unicode,'Use UNICODE in REPL and editing window').

preference_description(repl_cache_parsing,'Cache parsing in REPL (useful if same formula gets parsed multiple times, e.g., for Latex processing)').

preference_description(cache_operations,'Cache operations/events when -cache is activated'). %value_persistance

preference_description(latex_encoding,'Encoding used for Latex processing with -latex (auto,ISO-8859-1,ISO-8859-2,UTF-8,UTF-16,...)').

preference_description(latex_pp_greek_ids,'Prety-print Greek identifiers (Sigma,...) in Latex mode').

preference_description(xml_encoding,'Encoding used for XML processing, e.g., with -logxml (auto,ISO-8859-1,ISO-8859-2,UTF-8,UTF-16,...)').

preference_description(view_probcli_errors_using_bbresults,'Show probcli errors using the BBEdit (11.6 or newer) bbresults command').

preference_description(eventtrace,'Store trace for each event (may cause large memory requirement)').

preference_description(store_event_transinfo,'Store Event-B Event-Info for each event (may cause larger memory requirement)').

preference_description(use_solver_on_load,'Use this solver for PROPERTIES when loading machines').

preference_description(kodkod_for_components,'Translate only complete components to KODKOD (false allows partial translations)'). % and full throws enumeration warning if translation fails

preference_description(kodkod_raise_warnings,'Raise WARNING when component or predicate cannot be translated to KODKOD').

preference_description(kodkod_max_nr_solutions,'Maximum number of solutions computed and sent by KODKOD per batch.').

preference_description(kodkod_symmetry_level,'Symmetry level for Kodkod (0=off, 20=on), the higher this value, the more symmetries will be broken, you should probably only turn this on when MAX_INITIALISATIONS is set to 1').

preference_description(kodkod_sat_solver,'SAT solver used for Kodkod (sat4j, minisat, lingeling, glucose)').

preference_description(smt_supported_interpreter,'Use Z3 / CVC4 for predicates inside the B interpreter').

preference_description(sat_supported_interpreter,'Use Kodkod for specific predicates inside the B interpreter').

preference_description(use_record_construction,'Records: Check if axioms/properties describe a record pattern').

preference_description(seen_machines_included,'Seen/used machines are included (no operations available) instead of extended').

preference_description(allow_sequence_operators_on_strings,'Allow sequence operators (^) to be applied to STRINGs').

preference_description(show_eventb_any_arguments,'Show top-level ANY variable values of B Operations without parameters as parameters').

preference_description(show_initialisation_arguments,'Show effect of initialisation and setup constants in operation name'). % in case of non-deterministic assignments for INIT: only those are shown

preference_description(deterministic_trace_replay,'Replay Traces without backtracking (to reduce memory consumption)').

preference_description(treat_outermost_pre_as_select,'Treat outermost PRE as SELECT').

preference_description(require_operations_to_assign_all_outputs,'Require operations to assign to all outputs').

preference_description(allow_operations_to_read_outputs,'Allow B operations to read output parameters; output values will be initialised to default value in animator.').

preference_description(allow_operation_calls_for_uses,'Allow to call B read-only operations of used machines (via USES clauses); permitted by BToolkit but not Atelier-B').

preference_description(allow_overriding_initialisation,'Allow to override INITIALISATION of included/extended machines'). % useful when using EXTENDS to create animation instances

preference_description(allow_simultaneous_assignments,'Allow B operations to assign multiple times to same variable (ASM style)').

preference_description(allow_arith_operators_on_reals,'Allow to use the REAL datatype').

preference_description(solver_for_reals,'Solver to be used for REAL/FLOAT datatype (none, float_solver: simple det. propagation, precise_float_solver, aggressive_float_solver)').

preference_description(dot_print_edge_labels,'Show edge labels (operation names) in state space').

preference_description(dot_print_action_arguments,'Show operation arguments (when edge labels shown)').

preference_description(dot_print_functions,'Show functions (operations that return values w/o changing state) in state space').

preference_description(dot_print_self_loops,'Show self-loops in state space and other dot graphs').

preference_description(dot_print_arc_colors,'Colour the arcs (disable for import in OmniGraffle)').

preference_description(dot_print_root,'Show root node in state space').

preference_description(dot_print_node_ids,'Show internal state ids in state space').

preference_description(dot_print_transition_ids,'Show transition ids in state space').

preference_description(dot_print_node_info,'Show additional state information (values of variables)').

preference_description(dot_print_use_constants,'Use constants for deferred set values if possible').

preference_description(dot_use_ps_viewer,'Use PDF/Postscript Viewer for .dot files').

preference_description(path_to_dot,'Path/Command for dot program (using "/" even on Windows. Try avoiding spaces in path)').

preference_description(dot_default_engine,'Default layout engine used for dot (dot,neato,sfdp,fdp,twopi,circo)').

preference_description(path_to_dotty,'Path/Command for viewer of .dot files (e.g., dotty)').

preference_description(path_to_ltsmin,'Path to LTSmin commands, such as prob2lts-sym for symbolic model checking (not available for Windows.)').

preference_description(path_to_ps_viewer,'Path/Command for PDF/Postscript viewer').

preference_description(path_to_latex,'Path/Command for Latex (pdflatex)').

preference_description(dot_root_shape,'Shape for root node (invtriangle,triangle, ellipse, box, diamond,...)').

preference_description(dot_normal_node_shape,'Shape for normal node').

preference_description(dot_current_node_shape,'Shape for current node').

preference_description(dot_open_node_colour,'Colour for open node (red,green,blue,gray,... or rgb hex #ff00ff) or adjacent to an open node if print leaves is off').

preference_description(dot_scope_limit_node_colour,'Colour for open, but uninteresting nodes (red,green,blue,gray,... or rgb hex #ff00ff)').

preference_description(dot_normal_node_colour,'Colour for normal node').

preference_description(dot_node_penwidth,'Pen width for nodes').

preference_description(dot_edge_penwidth,'Pen width for edges').

preference_description(dot_invariant_violated_node_colour,'Colour for invariant violation').

preference_description(dot_fill_normal_nodes,'Fill normal nodes with color').

preference_description(dot_normal_arc_colour,'Colour for normal arcs').

preference_description(dot_node_font_size,'Font Size for Node labels').

preference_description(dot_edge_font_size,'Font Size for Edge labels').

preference_description(dot_with_page_size,'Limit page size by default (does not affect all dot graphs)').

preference_description(dot_horizontal_layout,'Use horizontal layout by default (does not affect all dot graphs)').

preference_description(dot_colour_goal_nodes,'Colour the nodes that satisfy the GOAL predicate').

preference_description(dot_goal_node_colour,'Colour for nodes satisfying the GOAL predicate').

preference_description(dot_print_node_properties,'Show properties of statespace node (useful for CSP models)').

preference_description(dot_counterexample_node_colour,'Colour for counterexample nodes').

preference_description(dot_counterexample_op_colour,'Colour for counterexample transitions').

preference_description(dot_hierarchy_max_ids,'Max. number of identifiers shown in hierarchy view (-1 to show all)').

preference_description(cbc_provide_explanations,'Provide explanations (unsat core,...) for some CBC commands').

preference_description(dot_event_hierarchy_horizontal,'Organize refinements horizontally').

preference_description(dot_event_hierarchy_machine_colour,'Colour for machine event cluster').

preference_description(dot_event_hierarchy_refines_colour,'Colour for events refining themselves (i.e., not renamed and modifying guard or action)').

preference_description(dot_event_hierarchy_new_event_colour,'Colour for new events (not refining any event) or variables').

preference_description(dot_event_hierarchy_rename_event_colour,'Colour for renamed events (with change in guard or action)').

preference_description(dot_event_hierarchy_rename_unchanged_event_colour,'Colour for renamed unchanged events').

preference_description(dot_event_hierarchy_unchanged_event_colour,'Colour for unchanged events (not renamed, no guards or actions added) or variables').

preference_description(dot_event_hierarchy_grd_strengthening_event_colour,'Colour for events just adding a guard (not renamed, no actions added)').

preference_description(dot_event_hierarchy_grd_keeping_event_colour,'Colour for events just changing an action (not renamed, keeping guard unchanged)').

preference_description(dot_event_hierarchy_edge_colour,'Edge colour for refine relation').

preference_description(dot_event_hierarchy_extends_colour,'Edge colour for extends relation').

preference_description(dot_hierarchy_show_extra_detail,'Provide more details in hierarchy diagram (e.g., constants)').

preference_description(dot_projection_non_det_edge_colour,'Edge colour for deterministic edges').

preference_description(dot_projection_det_edge_colour,'Edge colour for non-deterministic edges').

preference_description(dot_projection_non_definite_edge_style,'Style for non-definite edges (solid,dashed,dotted,bold,invis)').

preference_description(dot_projection_definite_edge_style,'Style for definite edges (solid,dashed,dotted,bold,invis)').

preference_description(dot_projection_label_limit,'Max. nr of characters for node labels').

preference_description(dot_projection_process_only_explored,'Project only on the explored nodes').

preference_description(dot_use_unicode,'Use Unicode symbols for values and formulas').

preference_description(dot_predicate_node_shape,'Shape for predicate nodes in formula trees').

preference_description(dot_expression_node_shape,'Shape for expression nodes in formula trees').

preference_description(dot_var_mod_hide_only_written,'Hide variables which are only written and not read in any guard').

preference_description(mc_dc_default_level,'Default Predicate Expansion Level for MC/DC Coverage Analyses (0=no expansion, 1=only top level connective expanded,...)').

preference_description(dot_enabling_show_readwrites,'Show read/write info for enabling diagrams').

preference_description(dot_definitions_use_sub_graph,'Show expression-, predicate-, substitution-DEFINITIONS as sub-graphs').

preference_description(dot_definitions_show_all,'Show all DEFINITIONS').

preference_description(dot_state_graph_decompose,'Decompose sets and complex pairs into individual vertices').

preference_description(font_size,'Font size in main window').

preference_description(font_name,'Font name in text editor').

preference_description(font_size_only,'Font size in text editor').

preference_description(use_font_size_for_columns,'Use font size also for columns (you need to reselect font size + Courier will be used)').

preference_description(allow_source_code_editing,'Allow editing and saving of main B machine file').

preference_description(show_line_numbers,'Show line numbers in main window').

preference_description(highlight_brackets,'Highlights brackets').

preference_description(highlight_current_line,'Highlights current line').

preference_description(ask_when_content_changed,'Asking when file content changed from external program').

preference_description(user_not_beginner,'User is not a beginner').

preference_description(user_is_an_expert_with_accessto_source_distribution,'User is expert with access to source distribution of ProB').

preference_description(path_to_probe,'Path to Probe or other tool to view .csp files').

preference_description(path_to_spin,'Path to Spin or other tool to view .prom files').

preference_description(path_to_cspm,'Path to cspm to view and analyze .csp files.').

preference_description(path_to_text_editor,'Path to external GUI text editor').

preference_description(path_to_text_editor_launch,'Path to external text editor for probcli (uses EDITOR environment variable by default)'). % different to path_to_text_editor, as from SICStus we cannot launch .app ??!

preference_description(path_to_fdr,'Path to the FDR2 tool').

preference_description(path_to_csp_typechecker,'Path to a CSP type checking tool, such as refines from FDR3 (taking --typecheck as argument)').

preference_description(path_to_bcomp,'Path to a bcomp (Atelier B Parser and type checker )').

preference_description(path_to_java,'Path to the "java" command (in case java is not found on the PATH)').

preference_description(path_to_java_parser,'Provide alternate path to the "probcliparser.jar" JAR file or "cliparser" Graal VM binary (by default ProB will use parser in lib folder)').

preference_description(path_to_atb_krt,'Path to Atelier B Provers krt tool').

preference_description(try_atb_provers,'Try Atelier B Provers for unknown SMTLIB specifications').

preference_description(smtlib2b_arrays_as_sets,'Translate SMTLib boolean Arrays to B Sets (when processing .smt2 files)').

preference_description(smtlib2b_cleanup_predicate,'Preprocess before solving SMTLib formulas (when processing .smt2 files)').

preference_description(symbolic_mc_try_other_solvers,'Symbolic Model Checking: Try different solver / settings combinations').

preference_description(number_of_recent_documents,'Number of recently opened file names memorised').

preference_description(number_of_searched_patterns,'Number of recently searched patterns in text').

preference_description(number_of_replaced_patterns,'Number of recently replaced patterns in text').

preference_description(number_of_eval_history_elements,'Number of recently runs of commands in the eval window').

preference_description(number_of_eval_csp_history_elements,'Number of recently runs of commands in the eval window').

preference_description(number_of_checked_ltl_formulas,'Number of recently checked LTL formulas').

preference_description(ltl_to_ba_tool,'Tool in lib/ directory for generatin a Buechi automaton from LTL.').

preference_description(do_syntax_highlighting,'Enable Syntax Colour Highlighting').

preference_description(sh_type_colour,'Colour of typing constructs: NAT,POW,... (red,green,... or rgb hex #ff00ff)').

preference_description(sh_logical_colour,'Colour of logical operators: &,or,...').

preference_description(sh_assignments_colour,'Colour of assignments: :=, <-- and strings').

preference_description(sh_operators,'Colour of normal operators ran,dom,...').

preference_description(sh_top_level_keywords,'Colour of top level keywords: MACHINE, INVARIANT,...').

preference_description(sh_control_keywords,'Colour of control keywords: IF, CASE,...').

preference_description(sh_comments,'Colour of comments /* ... */').

preference_description(sh_pragmas,'Colour of pragmas /*@ ... */').

preference_description(sh_unsupported_background,'Background colour for unsupported features (closure,...)').

preference_description(expand_forall_upto,'When analysing predicates: max. domain size for expansion of forall').

preference_description(double_evaluation_when_analysing,'Evaluate PREDICATES positively and negatively when analysing').

preference_description(prob_safe_mode,'Perform additional safety checks, which can slow down ProB').

preference_description(expand_avl_upto,'Max size for pretty-printing sets (-1 means no limit)').

preference_description(show_bvisual_formula_functor_from,'Show prefix/infix operators in state view for formulas longer than (use -1 to disable feature):').

preference_description(show_bvisual_proof_info_icons,'Show proof info icon in state view (currently only for Event-B):').

preference_description(formula_tree_minimal_timeout,'Minimal time-out for formula tree visualisation to find solutions to quantified identifiers').

preference_description(formula_tree_maximal_timeout,'Maximal time-out for formula tree visualisation to find solutions to quantified identifiers').

preference_description(show_bvisual_formula_explanations,'Show explanation nodes in state view for certain formulas (e.g., <:, ...)').

preference_description(show_function_tuples_in_property,'Show function tuples in state view or dot files (f(1)=2 instead of f={(1,2)})').

preference_description(bugly_pp_scrambling,'Scramble identifiers when pretty-printing (BUGLY)').

preference_description(pp_propositional_logic_mode,'Try and pretty-print formulas using propositional variables (A=TRUE will be printed as A)').

preference_description(pp_wd_infos,'Pretty-print well-definedness information for formulas').

preference_description(pp_with_terminal_colour,'Pretty-print values and formulas with terminal colour escape codes').

preference_description(wd_ignore_external_funs,'Do not create (unprovable) WD PO for external functions with WD condition').

preference_description(wd_skip_finite_pos,'Do not generate finite WD POs').

preference_description(wd_analysis_for_animation,'Perform the WD analysis in the context of ProB animation (e.g., deferred sets considered finite)').

preference_description(z3_solve_for_animation,'Perform SMT solving with Z3 in the context of ProB animation (e.g., deferred sets considered finite)').

preference_description(add_wd_pos_for_z3,'Add well-definedness POs to constraints before translating to SMT-LIB').

preference_description(allow_new_ops_in_refinement,'Allow introduction of new operations in refinements (automatically set to TRUE for SYSTEM machines)').

preference_description(allow_local_operation_calls,'Allow to call (local) operations in same machine').

preference_description(allow_operation_calls_in_expr,'Allow to call query operations in (some) expressions').

preference_description(allow_let_to_reuse_introduced_ids,'Allow LET substitutions to directly use introduced identifiers (e.g., LET x,y BE x=4 & y=x*x IN ...)').

preference_description(use_po,'Use PROOF information to restrict invariant checking to affected clauses.').

preference_description(try_operation_reuse,'Reuse previously computed operation effects in B/Event-B (cache projected state space per operation)'). % we used to have two values: true/full; true: performed local propagation to successor states for statically computed operation pairs, full: caches a projected state space per eligible operation in LTSmin style

preference_description(randomise_operation_order,'Randomise order of operations when computing successor states.').

preference_description(randomise_enumeration_order,'Randomise enumeration of variables.').

preference_description(perform_enumeration_order_analysis,'Perform enumeration order analysis within quantifiers, e.g., to detect identifiers that should not be enumerated').

preference_description(set_rand,'Use a fix seed for random number generator. Allows to reproduce results.').

preference_description(rand_seed,'Seed for Random Number Generator').

preference_description(machines_path,'Last open directory').

preference_description(use_cbc_analysis,'Use the constraint solver for more refined analysis of the action relations (in case of enabling/dependency determination for POR).').

preference_description(timeout_cbc_analysis,'Time out for computing independence and enable relations between operations.').

preference_description(alloy_use_implementable_integers,'Use INT (minint..maxint) for the translation from Alloy to B.').

preference_description(alloy_scopeless_translation,'Do not set any scopes when translating an Alloy model to B (useful for proof assistants).').

preference_description(alloy_translation_for_proof, 'Translate only a single command of an Alloy model to the B machine assertions section to enable generation of proof obligations in AtelierB.').

preference_description(alloy_strict_integers, 'Only accept integers (i.e, singleton sets in Alloy) as arguments to integer operations. Otherwise, a well-definedness error is thrown.').

preference_description(use_scope_predicate,
    'Use SCOPE predicate (if defined) to restrict state space exploration for model checking and animation.').

preference_description(use_ignore_pragmas, 'Ignore predicates with prob-ignore labels or /*@desc prob-ignore */ pragmas when checking PROPERTIES/axioms'). % later we may extend this to INVARIANTS and other contexts

preference_description(pge,
    'Use the Partial Guard Evaluation optimisation for the state space exploration of B models (off, full, ...).').

preference_description(por,'Type of Partial Order Reduction Technique (ample_sets, ample_sets2).').

preference_description(por_heur,'Type of heuritic for choosing a valid ample set.').

preference_description(use_safety_ltl_model_checker,'Recognise safety properties and check these using the safety property model checker (requires ltl2ba for more complex properties)'). % will currently ignore ltllimit set in probcli

preference_description(enable_graph,'Option for using the enable graph module for partial order reduction.').

preference_description(enable_graph_depth,'The depth of evaluating the weakest-preconditions along a path in an enable graph.').

preference_description(dependency_enable_predicates,'Compute in each state whether two events can disable each other.').

preference_description(filter_unused_constants,'Filter out unused constants (can interfere with VisB or other visualisations)').

preference_description(translate_force_all_typing_infos,'Print all typing infos when pretty-printing').

preference_description(translate_print_typing_infos,'Print needed typing infos when pretty-printing').

preference_description(translate_print_frozen_infos,'Print Prolog frozen goal infos for unbound variables').

preference_description(translate_ids_to_parseable_format,'Print Identifiers in a format that can be parsed again').

preference_description(translate_suppress_rodin_positions_flag,'Suppres Rodin position information when pretty-printing').

preference_description(translate_print_all_sequences,'Print B relations as sequences when possible during pretty-printing.').

preference_description(translate_print_cs_style_sequences,'Print B sequences in theoretical CS style without separators.').

preference_description(translation_limit_for_table_commands,'Translation/pretty print limit for columns used by some table (CSV) commands').

preference_description(visb_allow_variables_for_objects,'Allow variables to be used within VISB_SVG_OBJECTS and VISB_SVG_HOVERS expressions'). % for ProB2-UI this could cause problems

preference_description(trace_generation_limit,'Max. number of traces generated').

preference_description(trace_generation_time_out,'Timeout for trace generation').

preference_description(disprover_mode,'Assume that well-definedness is guaranteed or checked by other means (for Rodin DISPROVER Plugin)').

preference_description(allow_improving_wd_mode,'Allow transformations that improve well-definedness (e.g., transforming x=1/0 & bfalse to bfalse or replacing #x.(x=E) by btrue)'). % first example still respecting the commutative D system for well-definedness, second example not; used in clean_up

preference_description(trace_upon_error,'Trace upon error (requires running from source)').

preference_description(error_log_file, 'File were all errors and warnings are logged (NDJSON format). Can be set to stderr or stdout.').

preference_description(tlc_number_of_workers,'Number of parallel workers for external tool TLC (for -workers option)').

preference_description(tlc_use_prob_constant_setup,'Use constants found by ProB for TLC model checking (for -constantssetup option)').

preference_description(unsat_core_algorithm,'Algorithm to compute the unsat core of predicates. (divide_and_conquer or linear or linear_greedy or linear_greedy_decompose)').

preference_description(port, 'First number to be used by parB/distb/ZMQ. Default: 5000').

preference_description(ip, 'The IP addess or hostname of the current machine that should be used by parB/distb/ZMQ. Default: localhost. Must be overriden in a distributed setting.').

preference_description(max_states, 'The amount of states that shall be checked by parB/distb/ZMQ worker. Zero means explore entire state space. Default: 0').

preference_description(tmpdir, 'The directory where temporary files should be stored. Default: /tmp/.').

preference_description(logdir, 'The directory where log files should be stored. Default: ./distb-logs/').

preference_description(proxynumber, 'The number of the proxy the ZMQ component should connect to. Relevant if multiple proxies run on the same machine. Default: 0').

preference_description(queue_threshold, 'The amount of states that may be kept in a ZMQ queue before it is allowed to share. Default: 20').

preference_description(hash_cycle, 'Minimum amount of milliseconds that has to pass between hash code updates from the ZMQ master. Default: 25').

preference_description(cdclt_perform_static_analysis, 'CDCL(T) Solver: Perform static analysis to infer implied constraints').

preference_description(cdclt_perform_symmetry_breaking, 'CDCL(T) Solver: Perform symmetry breaking using BLISS (if installed)').

preference_description(cdclt_use_idl_theory_solver, 'CDCL(T) Solver: Use additional IDL (Integer-Difference-Logic) solver').

preference_description(prob_version_info,'Version of ProB (read-only preference)'). % mainly so that in ProB for Rodin we can see the version number

preference_description(prob_revision_info,'Git revision of ProB (read-only preference)').

preference_description(prob_lastchangedate_info,'Last change date of ProB source (read-only preference)').

preference_group_description/2

preference_group_val/4

preference_group_val(integer,int32,maxint,2147483647). % 2147483647

preference_group_val(integer,int32,minint,-2147483648). %-2147483648

preference_group_val(integer,int8,maxint,127).

preference_group_val(integer,int8,minint,-128).

preference_group_val(time_out,disable_time_out,time_out,TO) :- disabled_time_out(TO). % this value turns time_out off, e.g., in safe_time_out

preference_group_val(model_check,unlimited,time_out,TO) :- disabled_time_out(TO). % this value turns time_out off

preference_group_val(model_check,unlimited,maxNrOfInitialisations,Max) :- current_prolog_flag(max_tagged_integer,Max).

preference_group_val(model_check,unlimited,maxNrOfEnablingsPerOperation,Max) :- current_prolog_flag(max_tagged_integer,Max).

preference_group_val(model_check,disable_max,maxNrOfInitialisations,Max) :- current_prolog_flag(max_tagged_integer,Max).

preference_group_val(model_check,disable_max,maxNrOfEnablingsPerOperation,Max) :- current_prolog_flag(max_tagged_integer,Max).

preference_group_val(dot_colors,classic,dot_normal_node_colour, olivedrab2).

preference_group_val(dot_colors,classic,dot_normal_arc_colour,steelblue).

preference_group_val(dot_colors,classic,dot_open_node_colour,red).

preference_group_val(dot_colors,classic,dot_goal_node_colour,orange).

preference_group_val(dot_colors,classic,dot_invariant_violated_node_colour,maroon2).

preference_group_val(dot_colors,classic,dot_counterexample_node_colour,brown).

preference_group_val(dot_colors,classic,dot_counterexample_op_colour,brown).

preference_group_val(dot_colors,winter,dot_normal_node_colour, '#425955').

preference_group_val(dot_colors,winter,dot_normal_arc_colour,'#1B1D26').

preference_group_val(dot_colors,winter,dot_open_node_colour,'#BFBD9F').

preference_group_val(dot_colors,winter,dot_goal_node_colour,'#CC8604').

preference_group_val(dot_colors,winter,dot_invariant_violated_node_colour,'#9C080C').

preference_group_val(dot_colors,dreams,dot_normal_node_colour, '#5D7359').

preference_group_val(dot_colors,dreams,dot_invariant_violated_node_colour,'#661C0E').

preference_group_val(dot_colors,dreams,dot_normal_arc_colour,'#8C5430').

preference_group_val(dot_colors,dreams,dot_open_node_colour,'#D6AA5C').

preference_group_val(dot_colors,dreams,dot_goal_node_colour,'#FFC800').

preference_group_val(dot_colors,solarized,dot_normal_node_colour, '#859900').

preference_group_val(dot_colors,solarized,dot_normal_arc_colour,'#268bd2').

preference_group_val(dot_colors,solarized,dot_open_node_colour,'#dc322f').

preference_group_val(dot_colors,solarized,dot_goal_node_colour,'#cb4b16').

preference_group_val(dot_colors,solarized,dot_invariant_violated_node_colour,'#dc322f').

preference_group_val(dot_colors,solarized,dot_counterexample_node_colour,'#dc322f').

preference_group_val(dot_colors,solarized,dot_counterexample_op_colour,'#d33682').

preference_group_val(sh_colors,solarized,sh_type_colour,'#dc322f'). % $red

preference_group_val(sh_colors,solarized,sh_logical_colour,'#cb4b16'). % $orange

preference_group_val(sh_colors,solarized,sh_assignments_colour,'#268bd2'). % $blue

preference_group_val(sh_colors,solarized,sh_operators,'#2aa198'). % $cyan

preference_group_val(sh_colors,solarized,sh_top_level_keywords,'#6c71c4'). % $violet

preference_group_val(sh_colors,solarized,sh_control_keywords,'#d33682'). % $magenta

preference_group_val(sh_colors,solarized,sh_comments,'#93a1a1'). % $base1

preference_group_val(sh_colors,solarized,sh_pragmas,'#859900'). % $green

preference_group_val(sh_colors,solarized,sh_unsupported_background,'#b58900'). % $yellow

preference_update_action/2

preference_val_type/2

Description:
Options' meaning

preference_val_type(maxint,nat1).

preference_val_type(minint,neg).

preference_val_type(number_animated_abstractions,nat).

preference_val_type(number_skipped_refined_machines,nat).

preference_val_type(globalsets_fdrange,nat).

preference_val_type(do_invariant_checking,bool).

preference_val_type(do_assert_checking,bool).

preference_val_type(find_abort_values,xbool).

preference_val_type(raise_abort_immediately,xbool).

preference_val_type(treat_outermost_pre_as_select,bool).

preference_val_type(require_operations_to_assign_all_outputs,bool).

preference_val_type(allow_operations_to_read_outputs,bool).

preference_val_type(allow_operation_calls_for_uses,bool).

preference_val_type(allow_overriding_initialisation,bool).

preference_val_type(allow_simultaneous_assignments,bool).

preference_val_type(allow_arith_operators_on_reals,dbool).

preference_val_type(solver_for_reals,[aggressive_float_solver,float_solver,none,precise_float_solver]).

preference_val_type(cspm_animate_all_processes_without_arguments,bool).

preference_val_type(cspm_animate_all_processes,bool).

preference_val_type(cspm_detailed_animation,bool).

preference_val_type(cspm_strip_source_location,bool).

preference_val_type(show_initialisation_arguments,bool).

preference_val_type(deterministic_trace_replay,bool).

preference_val_type(show_eventb_any_arguments,bool).

preference_val_type(maxNrOfInitialisations,nat).

preference_val_type(randomisedRestartInitalisations,bool).

preference_val_type(maxNrOfEnablingsPerOperation,nat).

preference_val_type(time_out,nat1).

preference_val_type(debug_time_out_factor,nat1).

preference_val_type(jvm_parser_heap_size_mb,nat).

preference_val_type(jvm_parser_additional_args,string).

preference_val_type(jvm_parser_position_infos,bool).

preference_val_type(jvm_parser_fastrw,bool).

preference_val_type(jvm_parser_force_parsing,bool).

preference_val_type(convert_comprehension_sets_into_closures,bool).

preference_val_type(use_clpfd_solver,bool).

preference_val_type(use_chr_solver,bool).

preference_val_type(data_validation_mode,bool).

preference_val_type(use_smt_mode,bool).

preference_val_type(solver_strength,nat).

preference_val_type(use_common_subexpression_elimination,bool).

preference_val_type(remove_implied_constraints,bool).

preference_val_type(lift_existential_quantifiers,bool).

preference_val_type(use_common_subexpression_also_for_predicates,bool).

preference_val_type(use_common_subexpression_also_for_substitutions,bool).

preference_val_type(use_common_subexpression_wd_only,bool).

preference_val_type(normalize_ast,bool).

preference_val_type(normalize_ast_sort_commutative,bool).

preference_val_type(optimize_ast,bool).

preference_val_type(useless_code_elimination,bool).

preference_val_type(compile_while_body,bool).

preference_val_type(detect_lambdas,bool).

preference_val_type(auto_detect_theory_ops,bool).

preference_val_type(ltsmin_guard_splitting,bool).

preference_val_type(ltsmin_do_not_evaluate_top_level_guards,xbool).

preference_val_type(fail_if_clpfd_timeout,bool).

preference_val_type(use_static_ordering,bool).

preference_val_type(use_state_packing,xbool).

preference_val_type(force_state_packing_for_closures,bool).

preference_val_type(provide_trace_information,bool).

preference_val_type(prob_profiling_on,bool).

preference_val_type(prob_source_profiling_on,bool).

preference_val_type(performance_monitoring_on,bool).

preference_val_type(performance_monitoring_expansion_limit,int).

preference_val_type(partition_predicates,bool).

preference_val_type(partition_predicates_inline_equalities,bool).

preference_val_type(use_closure_expansion_memoization,bool).

preference_val_type(use_function_memoization,bool).

preference_val_type(allow_incomplete_partial_setup_constants,bool).

preference_val_type(re_execute_operations_with_side_effects,bool).

preference_val_type(warn_if_definition_hides_variable,bool).

preference_val_type(type_check_definitions,bool).

preference_val_type(allow_enumeration_of_infinite_types,bool).

preference_val_type(strict_raise_warnings,bool).

preference_val_type(strict_raise_enum_warnings,bool).

preference_val_type(clash_strict_checks,bool).

preference_val_type(perform_stricter_static_checks,bool).

preference_val_type(ignore_prj_types,bool).

preference_val_type(prefix_internal_operation_arguments,string).

preference_val_type(generate_minimal_nr_of_testcases,bool).

preference_val_type(use_tk_custom_state_viewer,bool).

preference_val_type(tk_custom_state_viewer_font_name,string).

preference_val_type(tk_custom_state_viewer_font_size,nat).

preference_val_type(tk_custom_state_viewer_padding,nat).

preference_val_type(tk_custom_state_viewer_str_padding,nat).

preference_val_type(use_small_window,bool).

preference_val_type(tk_show_source_pane,bool).

preference_val_type(ignore_hash_collisions,bool).

preference_val_type(forget_state_space,bool).

preference_val_type(store_only_one_incoming_transition,bool).

preference_val_type(mc_continue_after_error,bool).

preference_val_type(symmetry_mode,[off,flood,nauty,hash]).

preference_val_type(use_static_symmetry_detection,bool).

preference_val_type(allow_untyped_identifiers,[true,false,true_with_string_type]).

preference_val_type(repl_unicode,bool).

preference_val_type(repl_cache_parsing,bool).

preference_val_type(cache_operations,bool).

preference_val_type(latex_encoding,text_encoding).

preference_val_type(latex_pp_greek_ids,bool).

preference_val_type(xml_encoding,text_encoding).

preference_val_type(view_probcli_errors_using_bbresults,bool).

preference_val_type(eventtrace,bool).

preference_val_type(store_event_transinfo,bool).

preference_val_type(use_solver_on_load,solver_name).

preference_val_type(kodkod_for_components,xbool).

preference_val_type(kodkod_raise_warnings,bool).

preference_val_type(kodkod_max_nr_solutions,nat1).

preference_val_type(kodkod_symmetry_level,nat).

preference_val_type(kodkod_sat_solver,[sat4j,minisat,lingeling,glucose]).

preference_val_type(smt_supported_interpreter,bool).

preference_val_type(sat_supported_interpreter,bool).

preference_val_type(use_record_construction,bool).

preference_val_type(seen_machines_included,bool).

preference_val_type(allow_sequence_operators_on_strings,bool).

preference_val_type(dot_print_node_ids,bool).

preference_val_type(dot_print_transition_ids,bool).

preference_val_type(dot_print_use_constants,bool).

preference_val_type(dot_print_node_info,bool).

preference_val_type(dot_print_edge_labels,bool).

preference_val_type(dot_print_action_arguments,bool).

preference_val_type(dot_print_functions,bool).

preference_val_type(dot_print_self_loops,bool).

preference_val_type(dot_print_root,bool).

preference_val_type(dot_print_arc_colors,bool).

preference_val_type(dot_use_ps_viewer,bool).

preference_val_type(path_to_dot,path).

preference_val_type(dot_default_engine,[dot,neato,sfdp,fdp,twopi,circo,patchwork,osage,nop,nop2]).

preference_val_type(path_to_dotty,path).

preference_val_type(path_to_ltsmin,path).

preference_val_type(path_to_ps_viewer,path).

preference_val_type(path_to_latex,path).

preference_val_type(dot_root_shape,dot_shape).

preference_val_type(dot_node_penwidth,nat).

preference_val_type(dot_edge_penwidth,nat).

preference_val_type(dot_normal_node_shape,dot_shape).

preference_val_type(dot_current_node_shape,dot_shape).

preference_val_type(dot_open_node_colour,rgb_color).

preference_val_type(dot_scope_limit_node_colour,rgb_color).

preference_val_type(dot_normal_node_colour,rgb_color).

preference_val_type(dot_invariant_violated_node_colour,rgb_color).

preference_val_type(dot_fill_normal_nodes,bool).

preference_val_type(dot_normal_arc_colour,rgb_color).

preference_val_type(dot_node_font_size,nat1).

preference_val_type(dot_edge_font_size,nat1).

preference_val_type(dot_with_page_size,bool).

preference_val_type(dot_horizontal_layout,bool).

preference_val_type(dot_colour_goal_nodes,bool).

preference_val_type(dot_goal_node_colour,rgb_color).

preference_val_type(dot_print_node_properties,bool).

preference_val_type(dot_counterexample_node_colour,rgb_color).

preference_val_type(dot_counterexample_op_colour,rgb_color).

preference_val_type(dot_hierarchy_max_ids,int).

preference_val_type(cbc_provide_explanations,bool).

preference_val_type(dot_event_hierarchy_horizontal,bool).

preference_val_type(dot_event_hierarchy_machine_colour,rgb_color).

preference_val_type(dot_event_hierarchy_refines_colour,rgb_color).

preference_val_type(dot_event_hierarchy_new_event_colour,rgb_color).

preference_val_type(dot_event_hierarchy_rename_event_colour,rgb_color).

preference_val_type(dot_event_hierarchy_rename_unchanged_event_colour,rgb_color).

preference_val_type(dot_event_hierarchy_unchanged_event_colour,rgb_color).

preference_val_type(dot_event_hierarchy_grd_strengthening_event_colour,rgb_color).

preference_val_type(dot_event_hierarchy_grd_keeping_event_colour,rgb_color).

preference_val_type(dot_event_hierarchy_edge_colour,rgb_color).

preference_val_type(dot_event_hierarchy_extends_colour,rgb_color).

preference_val_type(dot_hierarchy_show_extra_detail,bool).

preference_val_type(dot_projection_non_det_edge_colour,rgb_color).

preference_val_type(dot_projection_det_edge_colour,rgb_color).

preference_val_type(dot_projection_non_definite_edge_style,dot_line_style).

preference_val_type(dot_projection_definite_edge_style,dot_line_style).

preference_val_type(dot_projection_label_limit,nat).

preference_val_type(dot_projection_process_only_explored,bool).

preference_val_type(dot_use_unicode,bool).

preference_val_type(dot_predicate_node_shape,dot_shape).

preference_val_type(dot_expression_node_shape,dot_shape).

preference_val_type(dot_var_mod_hide_only_written,bool).

preference_val_type(mc_dc_default_level,nat).

preference_val_type(dot_enabling_show_readwrites,bool).

preference_val_type(dot_definitions_use_sub_graph,bool).

preference_val_type(dot_definitions_show_all,bool).

preference_val_type(dot_state_graph_decompose,bool).

preference_val_type(font_name,string).

preference_val_type(font_size_only,nat1).

preference_val_type(font_size,string).

preference_val_type(use_font_size_for_columns,bool).

preference_val_type(allow_source_code_editing,bool).

preference_val_type(show_line_numbers,bool).

preference_val_type(highlight_brackets,bool).

preference_val_type(highlight_current_line,bool).

preference_val_type(ask_when_content_changed,bool).

preference_val_type(user_not_beginner,bool).

preference_val_type(user_is_an_expert_with_accessto_source_distribution,bool).

preference_val_type(path_to_probe,path).

preference_val_type(path_to_fdr,path).

preference_val_type(path_to_csp_typechecker,path).

preference_val_type(path_to_bcomp,path). % Atelier B parser & type checker

preference_val_type(path_to_java,path). % Path to Java

preference_val_type(path_to_java_parser,path). % Path to probcliparser.java or cliparser, default ''

preference_val_type(path_to_atb_krt,path).

preference_val_type(try_atb_provers,bool).

preference_val_type(smtlib2b_arrays_as_sets,bool).

preference_val_type(smtlib2b_cleanup_predicate,bool).

preference_val_type(symbolic_mc_try_other_solvers,bool).

preference_val_type(path_to_spin,path).

preference_val_type(path_to_cspm,path).

preference_val_type(path_to_text_editor,path).

preference_val_type(path_to_text_editor_launch,path).

preference_val_type(number_of_recent_documents,nat).

preference_val_type(number_of_searched_patterns,nat).

preference_val_type(number_of_replaced_patterns,nat).

preference_val_type(number_of_eval_history_elements,nat).

preference_val_type(number_of_eval_csp_history_elements,nat).

preference_val_type(number_of_checked_ltl_formulas,nat).

preference_val_type(ltl_to_ba_tool,path).

preference_val_type(do_syntax_highlighting,bool).

preference_val_type(sh_type_colour,rgb_color).

preference_val_type(sh_logical_colour,rgb_color).

preference_val_type(sh_assignments_colour,rgb_color).

preference_val_type(sh_operators,rgb_color).

preference_val_type(sh_top_level_keywords,rgb_color).

preference_val_type(sh_control_keywords,rgb_color).

preference_val_type(sh_comments,rgb_color).

preference_val_type(sh_pragmas,rgb_color).

preference_val_type(sh_unsupported_background,rgb_color).

preference_val_type(expand_forall_upto,nat).

preference_val_type(double_evaluation_when_analysing,bool).

preference_val_type(prob_safe_mode,bool).

preference_val_type(expand_avl_upto,int).

preference_val_type(show_bvisual_formula_functor_from,int).

preference_val_type(show_bvisual_proof_info_icons,bool).

preference_val_type(show_bvisual_formula_explanations,bool).

preference_val_type(formula_tree_minimal_timeout,nat).

preference_val_type(formula_tree_maximal_timeout,nat).

preference_val_type(show_function_tuples_in_property,bool).

preference_val_type(bugly_pp_scrambling,bool).

preference_val_type(pp_propositional_logic_mode,bool).

preference_val_type(pp_wd_infos,bool).

preference_val_type(pp_with_terminal_colour,bool).

preference_val_type(wd_ignore_external_funs,bool).

preference_val_type(wd_skip_finite_pos,bool).

preference_val_type(wd_analysis_for_animation,bool).

preference_val_type(z3_solve_for_animation,bool).

preference_val_type(add_wd_pos_for_z3,bool).

preference_val_type(allow_new_ops_in_refinement,bool).

preference_val_type(allow_local_operation_calls,bool).

preference_val_type(allow_operation_calls_in_expr,bool).

preference_val_type(allow_let_to_reuse_introduced_ids,bool).

preference_val_type(use_po,bool).

preference_val_type(try_operation_reuse,xbool). % false,true,full

preference_val_type(randomise_operation_order,bool).

preference_val_type(randomise_enumeration_order,bool).

preference_val_type(perform_enumeration_order_analysis,bool).

preference_val_type(set_rand,bool).

preference_val_type(rand_seed,nat).

preference_val_type(alloy_use_implementable_integers,bool).

preference_val_type(alloy_scopeless_translation,bool).

preference_val_type(alloy_translation_for_proof,bool).

preference_val_type(alloy_strict_integers,bool).

preference_val_type(use_scope_predicate,bool).

preference_val_type(use_ignore_pragmas,bool).

preference_val_type(pge,[off,disabled,enabled,full,disabled2,enabled2,full2]).

preference_val_type(use_cbc_analysis,bool).

preference_val_type(timeout_cbc_analysis,nat1).

preference_val_type(por,[off,ample_sets,ample_sets2]).

preference_val_type(por_heur,[first,random,minimal]).

preference_val_type(use_safety_ltl_model_checker,bool).

preference_val_type(enable_graph,bool).

preference_val_type(enable_graph_depth,int).

preference_val_type(dependency_enable_predicates,bool).

preference_val_type(filter_unused_constants,bool).

preference_val_type(translate_force_all_typing_infos,bool).

preference_val_type(translate_print_typing_infos,bool).

preference_val_type(translate_print_frozen_infos,bool).

preference_val_type(translate_ids_to_parseable_format,bool).

preference_val_type(translate_suppress_rodin_positions_flag,bool).

preference_val_type(translate_print_all_sequences,bool).

preference_val_type(translate_print_cs_style_sequences,bool).

preference_val_type(translation_limit_for_table_commands,int).

preference_val_type(visb_allow_variables_for_objects,bool).

preference_val_type(trace_generation_limit,nat).

preference_val_type(trace_generation_time_out,nat).

preference_val_type(disprover_mode,bool).

preference_val_type(allow_improving_wd_mode,bool).

preference_val_type(trace_upon_error,bool).

preference_val_type(tlc_number_of_workers,nat1).

preference_val_type(tlc_use_prob_constant_setup,bool).

preference_val_type(error_log_file,path).

preference_val_type(unsat_core_algorithm,[divide_and_conquer,linear,linear_greedy,linear_greedy_decompose]).

preference_val_type(port, nat1).

preference_val_type(ip, string).

preference_val_type(max_states, nat).

preference_val_type(tmpdir, path).

preference_val_type(logdir, path).

preference_val_type(proxynumber, nat).

preference_val_type(queue_threshold, nat1).

preference_val_type(hash_cycle, nat).

preference_val_type(cdclt_perform_static_analysis,bool).

preference_val_type(cdclt_perform_symmetry_breaking,bool).

preference_val_type(cdclt_use_idl_theory_solver,bool).

preference_val_type(prob_version_info, string).

preference_val_type(prob_revision_info, string).

preference_val_type(prob_lastchangedate_info, string).

preference_val_type(machines_path,path). %directory_path). % preference not so critical; default value may not exist

print_dynamic_preferences/1

print_eclipse_prefs/0

print_preferences/0

print_preferences/1

print_preferences_for_saving/1

print_see_exception/2

prob_application_type/1

Dynamic: true

prune_time_out_preference/2

read_only_preference/1

read_preferences/1

read_preferences2/1

recompute_nr_of_recent_documents/0

reset_all_temporary_preferences/0

reset_for_benchmarking/0

reset_temporary_preference/1

reset_temporary_preference/2

set_ith_preference_value/2

set_ith_preference_value/3

set_preference/2

set_preference_direct/3

set_preference_group/2

set_prob_application_type/1

tcltk_get_preference/2

temporary_set_preference/2

temporary_set_preference/3

time_out_preference_disabled/0

tk_color/1

tk_color/3

try_get_program_path/2

type_element/2

unix/1

valid_dot_line_style/1

valid_dot_node_style/1

valid_dot_shape/1

valid_gray/1

valid_rgb_color/1

virtual_preference_category/2

volatile_preference/1

Determinacy Checker

Determinacy Checker:

! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in argument 1 of absolute_file_name/3
! file extension('dll_path/dll_path') does not exist
! goal: absolute_file_name(extension('dll_path/dll_path'),_33867,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pathes.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_terminal_colors,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_enter_debugger_upon_error,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_use_timer,true)
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_33867,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/error_manager.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(plspec_patch_libraries,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_44071,[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),_42407,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
* Non-determinate: preferences:check_preferences/0 (clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: preferences:check_preferences/0 (clause 2)
* This clause contains a disjunction not forced to be deterministic.
! warning: predicate preferences:preference/2 is dynamic.
! Some nondeterminism may have been missed.
! Add (or move) the directive
! :- dynamic preferences:preference/2 .
! near the top of this file.
* Non-determinate: preferences:eclipse_preference/2 (clause 1)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 2)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 3)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 4)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 5)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 6)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 7)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 8)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 9)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 10)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 11)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 12)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 13)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 14)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 15)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 16)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 17)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 18)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 19)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 20)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 21)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 22)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 23)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 24)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 25)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 26)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 27)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 28)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 29)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:eclipse_preference/2 (clause 30)
* Indexing cannot distinguish this from clause 31.
! 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)
* Non-determinate: preferences:preference_default_value/2 (clause 181)
* Indexing cannot distinguish this from clause 182.
* Non-determinate: preferences:preference_default_value/2 (clause 183)
* Indexing cannot distinguish this from clause 184.
* Non-determinate: preferences:preference_default_value/2 (clause 194)
* Indexing cannot distinguish this from clause 195.
* Non-determinate: preferences:preference_default_value/2 (clause 303)
* Calls nondet predicate preferences:revision/1 .
* Non-determinate: preferences:preference_default_value/2 (clause 304)
* Calls nondet predicate preferences:lastchangeddate/1 .
* Non-determinate: preferences:possible_program_aux/3 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: preferences:possible_program_aux/3 (clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: preferences:possible_program_aux/3 (clause 3)
* Indexing cannot distinguish this from clause 4.
* Non-determinate: preferences:possible_program_aux/3 (clause 4)
* Indexing cannot distinguish this from clause 5.
* Non-determinate: preferences:possible_program_aux/3 (clause 5)
* Indexing cannot distinguish this from clause 6.
* Non-determinate: preferences:possible_program_aux/3 (clause 6)
* Indexing cannot distinguish this from clause 7.
* Non-determinate: preferences:possible_program_aux/3 (clause 7)
* Indexing cannot distinguish this from clause 8.
* Non-determinate: preferences:possible_program_aux/3 (clause 9)
* Indexing cannot distinguish this from clause 10.
* Non-determinate: preferences:possible_program_aux/3 (clause 10)
* Indexing cannot distinguish this from clause 11.
* Non-determinate: preferences:possible_program_aux/3 (clause 11)
* Indexing cannot distinguish this from clause 12.
* Non-determinate: preferences:possible_program_aux/3 (clause 12)
* Indexing cannot distinguish this from clause 13.
* Non-determinate: preferences:possible_program_aux/3 (clause 13)
* Indexing cannot distinguish this from clause 14.
* Non-determinate: preferences:possible_program_aux/3 (clause 14)
* Indexing cannot distinguish this from clause 15.
* Non-determinate: preferences:possible_program_aux/3 (clause 16)
* Indexing cannot distinguish this from clause 17.
* Non-determinate: preferences:possible_program_aux/3 (clause 17)
* Indexing cannot distinguish this from clause 18.
* Non-determinate: preferences:possible_program_aux/3 (clause 18)
* Indexing cannot distinguish this from clause 19.
* Non-determinate: preferences:possible_program_aux/3 (clause 19)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:possible_program_aux/3 (clause 21)
* Indexing cannot distinguish this from clause 22.
* Non-determinate: preferences:possible_program_aux/3 (clause 22)
* Indexing cannot distinguish this from clause 23.
* Non-determinate: preferences:possible_program_aux/3 (clause 23)
* Indexing cannot distinguish this from clause 24.
* Non-determinate: preferences:possible_program_aux/3 (clause 24)
* Indexing cannot distinguish this from clause 25.
* Non-determinate: preferences:possible_program_aux/3 (clause 25)
* Indexing cannot distinguish this from clause 26.
* Non-determinate: preferences:possible_program_aux/3 (clause 26)
* Indexing cannot distinguish this from clause 27.
* Non-determinate: preferences:possible_program_aux/3 (clause 29)
* Indexing cannot distinguish this from clause 30.
* Non-determinate: preferences:possible_program_aux/3 (clause 31)
* Indexing cannot distinguish this from clause 32.
* Non-determinate: preferences:possible_program_aux/3 (clause 33)
* Indexing cannot distinguish this from clause 34.
* Non-determinate: preferences:possible_program_aux/3 (clause 34)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:possible_program_aux/3 (clause 35)
* Indexing cannot distinguish this from clause 36.
* Non-determinate: preferences:possible_program_aux/3 (clause 37)
* Indexing cannot distinguish this from clause 38.
* Non-determinate: preferences:possible_program_aux/3 (clause 38)
* Indexing cannot distinguish this from clause 39.
* Non-determinate: preferences:possible_program_aux/3 (clause 39)
* Indexing cannot distinguish this from clause 40.
* Non-determinate: preferences:possible_program_aux/3 (clause 41)
* Indexing cannot distinguish this from clause 42.
* Non-determinate: preferences:possible_program_aux/3 (clause 42)
* Indexing cannot distinguish this from clause 43.
! 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),_365361,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pathes_lib.pl')])
* Non-determinate: preferences:alternate_preference_category/2 (clause 1)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 2)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 3)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 4)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 5)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 6)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 7)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 8)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 9)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 10)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 11)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 12)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 13)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 14)
* Indexing cannot distinguish this from clause 32.
* Non-determinate: preferences:alternate_preference_category/2 (clause 15)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 16)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 17)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 18)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 19)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 20)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 21)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 22)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 23)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 24)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 25)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 26)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 27)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 28)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 29)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 30)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 31)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 32)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 33)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 34)
* Indexing cannot distinguish this from clause 35.
* Non-determinate: preferences:alternate_preference_category/2 (clause 35)
* Indexing cannot distinguish this from clause 36.
* Non-determinate: preferences:alternate_preference_category/2 (clause 36)
* Indexing cannot distinguish this from clause 37.
* Non-determinate: preferences:alternate_preference_category/2 (clause 37)
* Indexing cannot distinguish this from clause 38.
* Non-determinate: preferences:alternate_preference_category/2 (clause 38)
* Indexing cannot distinguish this from clause 39.
* Non-determinate: preferences:alternate_preference_category/2 (clause 39)
* Indexing cannot distinguish this from clause 40.
* Non-determinate: preferences:alternate_preference_category/2 (clause 40)
* Indexing cannot distinguish this from clause 41.
* Non-determinate: preferences:alternate_preference_category/2 (clause 41)
* Indexing cannot distinguish this from clause 42.
* Non-determinate: preferences:alternate_preference_category/2 (clause 42)
* Indexing cannot distinguish this from clause 43.
* Non-determinate: preferences:alternate_preference_category/2 (clause 52)
* Indexing cannot distinguish this from clause 53.
* Non-determinate: preferences:obsolete_preference/1 (clause 55)
* Indexing cannot distinguish this from clause 56.
* Non-determinate: preferences:obsolete_preference/1 (clause 56)
* Indexing cannot distinguish this from clause 57.
* Non-determinate: preferences:obsolete_preference/1 (clause 57)
* Indexing cannot distinguish this from clause 58.
* Non-determinate: preferences:type_element/2 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: preferences:type_element/2 (clause 2)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:type_element/2 (clause 3)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:type_element/2 (clause 4)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:type_element/2 (clause 5)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:type_element/2 (clause 6)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:type_element/2 (clause 7)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:type_element/2 (clause 8)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:type_element/2 (clause 9)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:type_element/2 (clause 10)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:type_element/2 (clause 11)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:type_element/2 (clause 12)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:type_element/2 (clause 13)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:type_element/2 (clause 14)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:type_element/2 (clause 15)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:type_element/2 (clause 16)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:type_element/2 (clause 17)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:type_element/2 (clause 18)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:type_element/2 (clause 19)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:valid_rgb_color/1 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: preferences:valid_rgb_color/1 (clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: preferences:valid_rgb_color/1 (clause 3)
* Indexing cannot distinguish this from clause 4.
* Non-determinate: preferences:valid_rgb_color/1 (clause 4)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: preferences:tk_color/1 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: preferences:hex/1 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
! warning: predicate preferences:temp_pref/3 is dynamic.
! Some nondeterminism may have been missed.
! Add (or move) the directive
! :- dynamic preferences:temp_pref/3 .
! near the top of this file.
* Non-determinate: preferences:set_preference_direct/3 (clause 2)
* Calls nondet predicate preferences:preference/2 .
* Non-determinate: preferences:get_time_out_preference_with_factor/2 (clause 1)
* Calls nondet predicate preferences:preference/2 .
* Non-determinate: preferences:time_out_preference_disabled/0 (clause 1)
* Calls nondet predicate preferences:preference/2 .
* Non-determinate: preferences:virtual_preference_category/2 (clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: preferences:add_recent_document/1 (clause 2)
* Calls nondet predicate retract/1.
* Non-determinate: preferences:add_element_to_history/3 (clause 1)
* Calls nondet predicate retract/1.
! warning: predicate preferences:prob_application_type/1 is dynamic.
! Some nondeterminism may have been missed.
! Add (or move) the directive
! :- dynamic preferences:prob_application_type/1 .
! near the top of this file.
* Non-determinate: preferences:get_prob_application_type/1 (clause 1)
* Calls nondet predicate preferences:prob_application_type/1 .
* Non-determinate: preferences:preference_group_val/4 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: preferences:preference_group_val/4 (clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: preferences:preference_group_val/4 (clause 3)
* Indexing cannot distinguish this from clause 4.
* Non-determinate: preferences:preference_group_val/4 (clause 6)
* Indexing cannot distinguish this from clause 7.
* Non-determinate: preferences:preference_group_val/4 (clause 7)
* Indexing cannot distinguish this from clause 8.
* Non-determinate: preferences:preference_group_val/4 (clause 8)
* Indexing cannot distinguish this from clause 9.
* Non-determinate: preferences:preference_group_val/4 (clause 9)
* Indexing cannot distinguish this from clause 10.
* Non-determinate: preferences:preference_group_val/4 (clause 11)
* Indexing cannot distinguish this from clause 12.
* Non-determinate: preferences:preference_group_val/4 (clause 12)
* Indexing cannot distinguish this from clause 13.
* Non-determinate: preferences:preference_group_val/4 (clause 13)
* Indexing cannot distinguish this from clause 14.
* Non-determinate: preferences:preference_group_val/4 (clause 14)
* Indexing cannot distinguish this from clause 15.
* Non-determinate: preferences:preference_group_val/4 (clause 15)
* Indexing cannot distinguish this from clause 16.
* Non-determinate: preferences:preference_group_val/4 (clause 16)
* Indexing cannot distinguish this from clause 17.
* Non-determinate: preferences:preference_group_val/4 (clause 17)
* Indexing cannot distinguish this from clause 18.
* Non-determinate: preferences:preference_group_val/4 (clause 18)
* Indexing cannot distinguish this from clause 19.
* Non-determinate: preferences:preference_group_val/4 (clause 19)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: preferences:preference_group_val/4 (clause 20)
* Indexing cannot distinguish this from clause 21.
* Non-determinate: preferences:preference_group_val/4 (clause 21)
* Indexing cannot distinguish this from clause 22.
* Non-determinate: preferences:preference_group_val/4 (clause 22)
* Indexing cannot distinguish this from clause 23.
* Non-determinate: preferences:preference_group_val/4 (clause 23)
* Indexing cannot distinguish this from clause 24.
* Non-determinate: preferences:preference_group_val/4 (clause 24)
* Indexing cannot distinguish this from clause 25.
* Non-determinate: preferences:preference_group_val/4 (clause 25)
* Indexing cannot distinguish this from clause 26.
* Non-determinate: preferences:preference_group_val/4 (clause 26)
* Indexing cannot distinguish this from clause 27.
* Non-determinate: preferences:preference_group_val/4 (clause 27)
* Indexing cannot distinguish this from clause 28.
* Non-determinate: preferences:preference_group_val/4 (clause 28)
* Indexing cannot distinguish this from clause 29.
* Non-determinate: preferences:preference_group_val/4 (clause 29)
* Indexing cannot distinguish this from clause 30.
* Non-determinate: preferences:preference_group_val/4 (clause 30)
* Indexing cannot distinguish this from clause 31.
* Non-determinate: preferences:preference_group_val/4 (clause 31)
* Indexing cannot distinguish this from clause 32.
* Non-determinate: preferences:preference_group_val/4 (clause 32)
* Indexing cannot distinguish this from clause 33.
* Non-determinate: preferences:preference_group_val/4 (clause 33)
* Indexing cannot distinguish this from clause 34.
* Non-determinate: preferences:preference_group_val/4 (clause 35)
* Indexing cannot distinguish this from clause 36.
* Non-determinate: preferences:preference_group_val/4 (clause 36)
* Indexing cannot distinguish this from clause 37.
* Non-determinate: preferences:preference_group_val/4 (clause 37)
* Indexing cannot distinguish this from clause 38.
* Non-determinate: preferences:preference_group_val/4 (clause 38)
* Indexing cannot distinguish this from clause 39.
* Non-determinate: preferences:preference_group_val/4 (clause 39)
* Indexing cannot distinguish this from clause 40.
* Non-determinate: preferences:preference_group_val/4 (clause 40)
* Indexing cannot distinguish this from clause 41.
* Non-determinate: preferences:preference_group_val/4 (clause 41)
* Indexing cannot distinguish this from clause 42.
* Non-determinate: preferences:preference_group_val/4 (clause 42)
* Indexing cannot distinguish this from clause 43.

Name: assertz/1
Name: true
Name: add_recent_documents_active/0	Module: preferences
Name: ->/3

Name: assert_change_flag/0	Module: preferences
Name: assertz/1
Name: get_predicate_term_with_single_argument/3	Module: preferences
Name: call/1
Name: retract/1
Name: >/2
Name: ->/3
Name: =/2
Name: true
Name: preference/2	Module: preferences
Name: is/2
Name: merge_prefix_with_suffix/3	Module: preferences

Name: assert_change_flag/0	Module: preferences
Name: assertz/1
Name: recent_documents/1	dynamic predicate
Name: retract/1
Name: >/2
Name: ->/3
Name: =/2
Name: true
Name: preference/2	Module: preferences
Name: is/2
Name: nr_of_recent_documents/1	Module: preferences
Name: !
Name: add_recent_documents_active/0	Module: preferences
Name: not/1

Name: is/2
Name: =/2
Name: disabled_time_out/1	Module: preferences
Name: ->/3

Name: true
Name: assertz/1
Name: change_flag	dynamic predicate
Name: ->/3
Name: fail
Name: preference/2	Module: preferences
Name: retractall/1

Name: call_cleanup/2
Name: temporary_set_preference/3	Module: preferences

Name: before_after_predicate/2	Module: prob2_interface
Name: get_weakest_precondition/3	Module: prob2_interface
Name: compute_unsat_core/2	Module: disprover

Name: add_message/3	Module: foo_error
Name: true
Name: directory_exists/1	Module: file_systems
Name: ->/3

Name: add_internal_error/2	Module: foo_error
Name: !
Name: \=/2
Name: preference_category/2	Module: preferences
Name: fail
Name: is_of_type/2	Module: preferences
Name: not/1
Name: preference_val_type/2	Module: preferences
Name: preference/2	Module: preferences
Name: preference_description/2	Module: preferences

Name: fail
Name: retractall/1
Name: dynamic_preference_predicate/1	Module: preferences

Name: set_eclipse_preference/2	Module: prob2_interface
Name: set_pref_from_machine/3	Module: pref_definitions

Name: print_dynamic_preferences/1	Module: preferences
Name: clear_dynamic_preference_predicates/0	Module: preferences
Name: read_preferences2/1	Module: preferences

Name: get_eclipse_preference/2	Module: prob2_interface
Name: non_default_pref/1	Module: preferences
Name: convert_pref/2	Module: prob2_interface
Name: b_get_important_pref_mach/3	Module: pref_definitions
Name: set_eclipse_preference/2	Module: prob2_interface
Name: SET_PREF/3	Module: external_functions
Name: is_set_pref_def_name/3	Module: translate
Name: print_eclipse_prefs/0	Module: preferences
Name: set_pref_from_machine/3	Module: pref_definitions
Name: get_pref2/5	Module: external_functions
Name: cur_pref_string/2	Module: preferences
Name: auto_complete_preference/2	Module: test_runner
Name: get_eclipse_preference_infos/5	Module: prob2_interface
Name: match_preference/2	Module: test_runner

Name: fail
Name: add_warning/3	Module: foo_error
Name: ajoin/2	Module: tools_strings
Name: invalid_application/2	Module: preferences
Name: get_modulename_filename/2	Module: tools
Name: preference/2	Module: preferences
Name: preference_val_type/2	Module: preferences
Name: is_of_type/2	Module: preferences
Name: not/1

Name: check_invariant_predicate_with_time_out_res/3	Module: b_interpreter
Name: store_updates_and_normalise/3	Module: store
Name: tcltk_constraint_based_check_with_timeout/2	Module: tcltk_interface
Name: normalise_store/2	Module: store
Name: normalise_value_for_var/3	Module: store
Name: b_debug_try_remove_props/7	Module: predicate_debugger
Name: state_satisfies_assertions/3	Module: b_interpreter
Name: b_analyse_individual_conjunct/8	Module: predicate_evaluator
Name: tcltk_cbc_find_trace_aux/5	Module: tcltk_interface
Name: eval_codes_with_time_out/6	Module: eval_strings
Name: timeout_check_property/5	Module: predicate_debugger

Name: =/2
Name: reverse/2	Module: foo_error
Name: ->/3
Name: findall/3
Name: get_predicate_term_with_single_argument/3	Module: preferences

Name: fail
Name: add_error/3	Module: foo_error
Name: =/2
Name: nth1/3	Module: foo_error
Name: ->/3
Name: findall/3

Name: translate_values_for_state_table/3	Module: visb_visualiser
Name: op_hash/4	Module: b_operation_cache
Name: b_get_machine_operation_for_animation_calc/7	Module: bmachine
Name: setup_reification_for_solver/8	Module: cdclt_solver
Name: assert_warning_occured/0	Module: error_manager
Name: get_max_nr_of_solutions/1	Module: kodkod
Name: cbc_enable_trans_predicate_por/7	Module: dot_graphs_static_analysis
Name: clean_up_and_preprocess_pos_for_cdclt/2	Module: welldef
Name: get_fuzzing_timeout/1	Module: fuzzer_runner.pl
Name: try_find_and_remove_equalities/2	Module: bsyntaxtree
Name: remove_already_typed_ids/3	Module: translate
Name: smt_type_to_prob_type/3	Module: smtlib2_translation
Name: get_timeout/2	Module: predicate_debugger
Name: ppatom_opt_scramble/3	Module: translate
Name: solve3/3	Module: solver_handling
Name: do_not_to_move_let_inside/1	Module: b_ast_cleanup
Name: my_greek_latex_escape_atom/3	Module: translate
Name: propagate_idl_solution_to_bindings_bt/2	Module: cdclt_solver
Name: cbc_dependence_trans_predicate/5	Module: dot_graphs_static_analysis
Name: perform_post_static_check/1	Module: bmachine_construction
Name: add_hint_message/4	Module: b_ast_cleanup
Name: replace_expression_by_kodkod_if_enabled_aux/2	Module: eval_strings
Name: portray_instantiations/0	Module: external_functions
Name: assert_skipped_failed_conjunct/2	Module: b_interpreter_components
Name: split_predicates/2	Module: kodkod
Name: log_error_or_msg/3	Module: error_manager
Name: use_colour_codes/0	Module: translate
Name: is_top_level_function_call/1	Module: translate
Name: type_check_definitions2/0	Module: bmachine
Name: conflict_driven_clause_learning_online_grounding/6	Module: cdclt_solver
Name: current_solver_is_not_incremental/0	Module: kodkod
Name: static_syntax_analysis/1	Module: cdclt_settings
Name: get_integer_constant/2	Module: set_rewriter
Name: typecheck_tp/3	Module: ltl_tools
Name: init_smt_supported_interpreter/0	Module: smt_solvers_interface
Name: perform_one_operation_in_sequence/2	Module: b_trace_checking
Name: perform_custom_operation_retry/2	Module: b_trace_checking
Name: b_analyse_individual_conjunct/8	Module: predicate_evaluator
Name: always_defined_full_check_or_disprover_mode/1	Module: b_ast_cleanup
Name: untyped_b_ast_to_integer/2	Module: alloy2b
Name: create_top_level_wd_po/7	Module: well_def_analyser
Name: create_sorted_store/4	Module: b_intelligent_trace_replay
Name: get_cbc_assertions_sequent/4	Module: b_state_model_check
Name: check_if_op_cache_useful/0	Module: b_operation_cache
Name: disable_analysis/5	Module: static_analysis
Name: cleanup_post_function/7	Module: b_ast_cleanup
Name: extension_should_be_evaluated/1	Module: b_ast_cleanup
Name: state_value_for_expr/4	Module: state_space_reduction
Name: initialise_node_colours/0	Module: graph_iso_nauty
Name: b_get_machine_operation_calc/6	Module: bmachine
Name: add_abort_error2/8	Module: kernel_waitflags
Name: test1_aux/1	Module: fuzzer_runner.pl
Name: get_cs_limit/1	Module: translate
Name: b_compute_comprehension_set_aux/4	Module: b_interpreter
Name: time_out_call/2	Module: tools_timeout
Name: cbc_constants_det_check/6	Module: b_state_model_check
Name: perform_do_not_enumerate_analysis/5	Module: b_ast_cleanup
Name: guard_strengthening_single_event/10	Module: cbc_refinement_checks
Name: cleanup_pre/7	Module: b_ast_cleanup
Name: get_transition_predicate/1	Module: predicate_handling
Name: safety_mc_not_possible/2	Module: ltl
Name: type_infos_in_subst/3	Module: translate
Name: check_generated_info/3	Module: b_ast_cleanup
Name: smt_add_predicate_aux/3	Module: smt_solvers_interface
Name: get_expression_field_seperator/1	Module: bvisual
Name: print_op_cache_profile/0	Module: b_operation_cache
Name: pp_expr1/7	Module: translate
Name: check_is_just_type/1	Module: b_ast_cleanup
Name: hash_model_checking_imprecise/2	Module: symmetry_marker
Name: no_conflict_due_to_annotation/1	Module: fuzzer_runner.pl
Name: perform_static_analyses_if_necessary2/1	Module: ltl
Name: gen_label/2	Module: state_space_reduction
Name: unpack_constants/2	Module: value_persistance
Name: solve4/3	Module: solver_handling
Name: restart_core_linear/6	Module: unsat_cores
Name: enum_fd/3	Module: fd_utils_clpfd
Name: cspm_trans/4	Module: haskell_csp
Name: try_provers/3	Module: smtlib2_interpreter
Name: tcltk_get_visb_items/2	Module: visb_visualiser
Name: precompute_values_e/6	Module: ast_optimizer_for_smt
Name: does_not_accord_with_aux/3	Module: ltsmin
Name: clean_up_aux/4	Module: b_ast_cleanup
Name: check_unused_ids/0	Module: bmachine_static_checks
Name: tcltk_get_machine_wd_pos/4	Module: well_def_analyser
Name: cleanup_post_with_path/8	Module: b_ast_cleanup
Name: model_checking_is_incomplete/6	Module: model_checker
Name: do_not_expand/1	Module: bvisual
Name: get_unproven_assertion/1	Module: b_state_model_check
Name: observe_runtime_wf/4	Module: runtime_profiler
Name: real_sqrt_wf_aux/4	Module: kernel_reals
Name: skip_finite_pos/1	Module: well_def_analyser
Name: compute_disabled_operations/4	Module: pge_algo
Name: detect_partitions_in_predicates/2	Module: partition_detection
Name: get_typed_static_definition_with_constants_state3/8	Module: visb_visualiser
Name: translate_b_operation_call/4	Module: translate
Name: get_main_eval_scope/1	Module: prob2_interface
Name: solve_pred_with_setlog/3	Module: b2setlog
Name: disprove_double_check/8	Module: disprover
Name: boolean_shape/1	Module: bvisual
Name: mk_expr_aux/7	Module: smt_solvers_interface
Name: set_desired_preferences/4	Module: predicate_data_generator
Name: clpfd_randomised_labeling/2	Module: clpfd_interface
Name: solve2/3	Module: solver_handling
Name: pp_codes_opt_scramble/3	Module: translate
Name: write_transition_diagram_for_expr_to_dotfile/2	Module: state_space_reduction
Name: translate_bvalue_with_type_and_limit/4	Module: translate
Name: disprove_triple_check/7	Module: disprover
Name: tcltk_debug_properties_or_op/4	Module: predicate_debugger
Name: do_modelchecking/5	Module: prob2_interface
Name: not_with_enum_warning2/4	Module: delay
Name: start_ltsmin/4	Module: ltsmin
Name: startup_kodkod/0	Module: kodkod_process
Name: tcltk_get_visb_events/2	Module: visb_visualiser
Name: b2e/4	Module: b2setlog
Name: mark_operation_as_covered/1	Module: state_space
Name: assert_atelierb_mode/0	Module: alloy2b
Name: repl_parse_expression/4	Module: eval_strings
Name: assert_agent_compiled_head/4	Module: haskell_csp_analyzer
Name: write_dot_graph_to_file_aux/2	Module: bvisual
Name: initialise_specification/0	Module: prob2_interface
Name: ppstring_opt_scramble/3	Module: translate
Name: make_domain_finite/4	Module: kernel_objects
Name: cbc_enable_trans_predicate/5	Module: dot_graphs_static_analysis
Name: get_state_value_enabled_operation_status/5	Module: visb_visualiser
Name: get_constants_predicate/1	Module: prob2_interface
Name: add_value/6	Module: kernel_z
Name: repl_parse_predicate2/4	Module: eval_strings
Name: enumerate_int2/3	Module: kernel_objects
Name: size_is_in_set_limit/1	Module: translate
Name: b_analyse_conjunction_nr/9	Module: predicate_evaluator
Name: is_replace_id_by_expr_ok/4	Module: b_ast_cleanup
Name: generate_unsat_properties_warnings/0	Module: b_interpreter
Name: tcltk_compute_mcdc_operation_coverage/1	Module: mcdc_coverage
Name: element_of_global_integer_set_wf/4	Module: kernel_objects
Name: other_warning/1	Module: b_interpreter
Name: constraint_transitions/2	Module: bmc
Name: cleanup_post/7	Module: b_ast_cleanup
Name: illegal_json_binding_type/4	Module: b_intelligent_trace_replay
Name: can_be_further_decomposed_aux/5	Module: unsat_cores
Name: get_transition_style/4	Module: state_space_reduction
Name: cache_is_applicable/0	Module: value_persistance
Name: translate_event_with_src_and_target_id/5	Module: translate
Name: expression_sharing_enabled/0	Module: b_expression_sharing
Name: translate_event_with_target_id2/5	Module: translate
Name: is_set_pref_def_name/3	Module: translate
Name: solve_components_with_z3/7	Module: smt_solvers_interface
Name: is_finite_type_for_wd/2	Module: well_def_hyps
Name: minimal_timeout/1	Module: maxsolver
Name: has_default_value/1	Module: preferences
Name: get_instantiation_options/1	Module: b_to_cnf
Name: generate_transition_color_and_style/6	Module: state_space_reduction
Name: pp_expr2/5	Module: translate
Name: get_valid_inputs_for_operation/3	Module: synthesis_util
Name: cbc_gen_test_cases/5	Module: sap
Name: indent_rodin_label/3	Module: translate
Name: is_deadlocked/1	Module: model_checker
Name: mpart_typing2/4	Module: translate
Name: enable_analysis/6	Module: static_analysis
Name: get_predicate_field_seperator/1	Module: bvisual
Name: cleanup_pre_with_path/8	Module: b_ast_cleanup
Name: allow_constraint_propagation/1	Module: kernel_reals
Name: get_pp_state_limit/1	Module: translate
Name: b_operation_reads_output_variables_calc/3	Module: bmachine
Name: observe_variable/4	Module: b_interpreter_components
Name: add_error_if_result_unexpected/1	Module: smtlib2_interpreter
Name: data_validation_mode/0	Module: b_ast_cleanup
Name: generate_test_case/2	Module: sap
Name: get_solutions_around/6	Module: kernel_reals
Name: evaluate_predicate_if_necessary/5	Module: b_interpreter_eventb
Name: possible_trace/3	Module: sap
Name: b_specialized_invariant_mask_for_op_calc/2	Module: bmachine
Name: print_result/1	Module: kodkod
Name: not_element_of_global_set2/2	Module: kernel_objects
Name: observe_state/3	Module: b_interpreter_components
Name: ltl_model_check5/5	Module: ltl
Name: max_freetype_enum_depth/1	Module: kernel_freetypes
Name: cleanup_post_essential/7	Module: b_ast_cleanup
Name: translate_command_aux/6	Module: alloy2b
Name: get_proven_invariant_calc/2	Module: bmachine
Name: cleanup_pre_function/7	Module: b_ast_cleanup
Name: x_get_custom_explanation_subexpressions/5	Module: bvisual
Name: send_problem/1	Module: kodkod_process
Name: cbc_disable_trans_por/6	Module: dot_graphs_static_analysis
Name: nauty_reset/0	Module: graph_iso_nauty
Name: cbc_gen_test_cases_task_step/7	Module: sap
Name: get_target_pred/5	Module: b_state_model_check
Name: assert_integer_type_from_preference/0	Module: alloy2b
Name: get_eclipse_preference/2	Module: prob2_interface
Name: tcltk_get_preference/2	Module: preferences
Name: is_pge_opt_on/0	Module: pge_algo
Name: b_trace_test_components_wf/6	Module: b_interpreter_components
Name: replace_by_kodkod/3	Module: kodkod
Name: var_mod_pred/5	Module: b_read_write_info
Name: collision_precedence/3	Module: bmachine_construction
Name: b_type_expression_for_ltl/4	Module: ltl_tools
Name: conflict_driven_clause_learning_online/8	Module: cdclt_solver
Name: generate_traces2/4	Module: trace_generator
Name: get_guards/6	Module: b_operation_guards
Name: check_expr/3	Module: bsyntaxtree
Name: tcltk_enabling_analysis/2	Module: static_analysis
Name: typing_constraint/2	Module: smtlib2_translation
Name: translate_inner_node/3	Module: state_graph_canon
Name: fallback_to_smt_if_requested/4	Module: solver_interface
Name: open_search_check_for_error/10	Module: model_checker
Name: smt_solve_predicate/5	Module: smt_solvers_interface
Name: pp_eval_expr/1	Module: eval_strings
Name: pp_frozen_info/3	Module: translate
Name: var_op_node_predicate/6	Module: b_read_write_info
Name: temporary_set_preference/3	Module: preferences
Name: inner_predicate_level_optimizations/2	Module: b_ast_cleanup
Name: set_translation_constants/1	Module: translate
Name: b_execute_statement2/8	Module: b_interpreter
Name: register_instantiation_wf/2	Module: external_functions
Name: my_solve_predicate/2	Module: smtlib2_interpreter
Name: call_prover/3	Module: atelierb_provers_interface
Name: initialise_optimisations/5	Module: model_checker
Name: command_unavailable/2	Module: meta_interface
Name: cdclt_solve_predicate_timeout/4	Module: cdclt_solver
Name: replace_sets_by_records2/2	Module: record_detection
Name: get_binary_choice_wait_flag/3	Module: kernel_waitflags
Name: override_custom_explicit_set_aux/4	Module: custom_explicit_sets
Name: get_preference_with_warnings/2	Module: preferences
Name: cdcl_sat_solve_predicate/2	Module: cdclt_solver
Name: strengthen_loop/7	Module: ctigar
Name: try_kodkod/0	Module: bmachine
Name: b_trace_test_components2/8	Module: b_interpreter_components
Name: predicate_level_optimizations/3	Module: b_ast_cleanup
Name: ltsmin_test_path_possible/3	Module: ltsmin
Name: write_bind/3	Module: value_persistance
Name: pp_closure_value/6	Module: translate
Name: get_assertions_from_machine/2	Module: bmachine
Name: b_compute_expression2/7	Module: b_interpreter
Name: test_enabled/1	Module: eval_strings
Name: tcltk_compute_mcdc_invariant_coverage/1	Module: mcdc_coverage
Name: generate_traces/4	Module: trace_generator
Name: unsat_core_properties_table/1	Module: unsat_cores
Name: do_not_optimise_in_context/1	Module: b_ast_cleanup
Name: replay_trace/8	Module: b_intelligent_trace_replay
Name: smt_clean_up_pre/4	Module: ast_cleanup_for_smt
Name: handle_globalsets_fdrange_contradiction/2	Module: model_translation
Name: cbc_symbolic_invariant_violation_get_constraint/2	Module: cbc_ba
Name: print_json_opid/4	Module: b_trace_checking
Name: compute_enabling_predicate/5	Module: enabling_predicates
Name: x_time_out_by_size/2	Module: bvisual_any_maxsolver
Name: propagate_fd_bounds_to_idl_solver/2	Module: cdclt_solver
Name: source_profiler_enabled/0	Module: source_profiler
Name: tcltk_analyse_invariant/2	Module: predicate_evaluator
Name: x_print_dot_graph_node_style/4	Module: bvisual
Name: lib_component_full_path/4	Module: pathes_lib
Name: is_rewrite_to_idl/1	Module: cdclt_solver
Name: cleanup_comprehension_set/7	Module: b_ast_cleanup
Name: pp_external_call/7	Module: translate
Name: get_pref2/5	Module: external_functions
Name: setup_sets/3	Module: smt_solvers_interface
Name: get_ltsmin_guards/3	Module: ltsmin
Name: xml_write_parameters/3	Module: sap
Name: unsat_core_with_options_lists/4	Module: unsat_cores
Name: nested_print_sequent_as_classicalb_aux/6	Module: translate
Name: get_model_or_return_result/8	Module: smt_solvers_interface
Name: check_is_operation/1	Module: bmachine
Name: re_add_pending_aux/3	Module: kernel_waitflags
Name: get_main_repl_scope/1	Module: eval_strings
Name: check_record_construction_ok/2	Module: record_detection
Name: get_constraint/2	Module: bmc
Name: get_adapted_properties/4	Module: predicate_debugger
Name: translate_bvalue_with_limit/3	Module: translate
Name: compute_dependendency_relation_of_all_events_in_the_model/3	Module: static_analysis
Name: get_cs_avl_limit/1	Module: translate
Name: op_node_predicate/6	Module: enabling_analysis
Name: compute_operation_relations_for_pge/1	Module: pge_algo
Name: get_step_constraint/2	Module: kinduction
Name: perform_general_csp_self_check/0	Module: haskell_csp
Name: pp_value_l_with_limit/5	Module: translate
Name: smt_solve_cnf/2	Module: smt_solvers_interface
Name: perform_sequence_of_operations2/2	Module: b_trace_checking
Name: pp_any_state_with_limit/4	Module: translate
Name: compute_enabled_operations/4	Module: pge_algo
Name: check_forall_lhs_rhs/4	Module: b_ast_cleanup
Name: translate_single_alloy_model/3	Module: alloy2b
Name: consistent_deferred_set_sizes/1	Module: model_translation
Name: test2_aux/1	Module: fuzzer_runner.pl
Name: print_runtime_profile/0	Module: runtime_profiler
Name: add_optional_typing_predicates/3	Module: translate
Name: trace_if_user_wants_it/0	Module: error_manager
Name: get_alternate_prover_timeout/3	Module: disprover
Name: tcltk_disabling_analysis/1	Module: pge_algo
Name: opt_scramble_id/2	Module: translate
Name: add_special_json_definition/7	Module: visb_visualiser
Name: static_smt_symmetry_breaking/1	Module: cdclt_settings
Name: get_ample_actions/4	Module: ample_sets
Name: get_timeout_factor/2	Module: solver_handling
Name: op_name_clashes/2	Module: bmachine_static_checks
Name: get_smt_time_out/2	Module: smt_solvers_interface
Name: get_por_preferences/1	Module: ltl_propositions
Name: perform_single_operation/2	Module: b_trace_checking
Name: do_not_share_this/6	Module: b_expression_sharing
Name: find_useless_enumeration_id/2	Module: b_enumerate
Name: pp_value/4	Module: translate
Name: get_b_optimisation_options/2	Module: state_space_explorer
Name: proof_info_model_checking_incomplete/5	Module: model_checker
Name: reset_smt_supported_interpreter/0	Module: smt_solvers_interface
Name: before_after_predicate_no_equalities_top_level_aux/4	Module: before_after_predicates
Name: assert_skipped_unknown_conjunct/3	Module: b_interpreter_components
Name: get_operation_read_projection_infos/6	Module: b_operation_cache
Name: tcltk_analyse_properties/2	Module: predicate_evaluator
Name: safe_b_test_boolean_expression/7	Module: b_interpreter_components
Name: get_tree_from_expr/4	Module: bvisual
Name: strengthen_loop/5	Module: ic3
Name: find_solutions/3	Module: kodkod_test
Name: dependent_actions1/5	Module: static_analysis
Name: expand_custom_set_to_sorted_list/5	Module: custom_explicit_sets
Name: maximal_timeout/1	Module: maxsolver
Name: pp_separator_sequence/1	Module: translate
Name: get_core_str/4	Module: b_state_model_check
Name: cspm_transition/3	Module: xtl_interface

Name: get_preference/2	Module: preferences
Name: gen_preference_warnings/1	Module: preferences

Name: missing_parser_diagnostics/0	Module: parsercall
Name: parse_template_b_expression/4	Module: parsercall
Name: preference_description/2	Module: preferences
Name: perform_single_operation_retry/4	Module: b_trace_checking
Name: print_transition_list_json/3	Module: b_trace_checking
Name: preference_default_value/2	Module: preferences

Name: prune_time_out_preference/2	Module: preferences
Name: is/2
Name: disabled_time_out/1	Module: preferences
Name: ->/3
Name: preference/2	Module: preferences

Name: get_computed_preference/2	Module: preferences
Name: get_time_out_with_factor/2	Module: tools_timeout
Name: analyse_quick_time_out/1	Module: predicate_evaluator
Name: tcltk_cbc_enabling_analysis/1	Module: enabling_analysis

Name: check_preferences/0	Module: preferences
Name: reset_to_defaults/0	Module: preferences
Name: retractall/1

Name: perform_csp_self_check/0	Module: haskell_csp
Name: preference/2	Module: preferences

Name: set_preference_direct/3	Module: preferences
Name: check_preference/1	Module: preferences
Name: read_xml/4	Module: external_functions
Name: type_element/2	Module: preferences
Name: gen_preference_warnings/1	Module: preferences

prob_prolog/src/preferences.pl

Modules

Predicates of preferences

Module Information

2965 Lines

108 Predicates

Imported Modules: error_manager lists file_systems

62 Exports

22 specified Imports

Predicates:

Determinacy Checker:

Name: load_preferences2/2	Module: preferences
Name: !
Name: safe_on_exception_silent/3	Module: tools_meta
Name: print_message/1	Module: tools

Name: tcltk_load_commandline_prefs_file/0	Module: gui_tcltk.pl
Name: set_prefs/0	Module: prob_cli

Name: add_unknown_preference_error_and_fail/2	Module: prob2_interface
Name: set_eclipse_preference/2	Module: prob2_interface

Name: unix/1	Module: preferences
Name: =/2
Name: prob_application_type/1	Module: preferences
Name: environ/2	Module: system

Name: convert_pref_val/3	Module: pref_definitions
Name: type_element/2	Module: preferences

Name: RECURSIVE_CALL/2	Module: preferences
Name: !
Name: init_preferences/0	Module: preferences
Name: format/3

Name: runtime_profile_available/0	Module: runtime_profiler
Name: never_transform_or_optimise/1	Module: b_ast_cleanup
Name: must_fail_tests/0	Module: eval_strings
Name: opt_push_wait_flag_call_stack_quantifier_info/6	Module: kernel_waitflags
Name: always_well_defined_or_disprover_mode/1	Module: bsyntaxtree
Name: b_expand_compute_comprehension_set/4	Module: b_interpreter
Name: print_preferences_for_saving/1	Module: preferences
Name: equal_cons_perf_message/4	Module: kernel_objects
Name: profile_failure_driven_loop/2	Module: runtime_profiler
Name: finite_set_or_disprover_mode/1	Module: bsyntaxtree
Name: quick_propagation_element_information/4	Module: custom_explicit_sets
Name: can_translate_function_to_element_constraint/2	Module: clpfd_tables
Name: propagate_intersection/4	Module: kernel_objects
Name: lazy_fd_value_check/4	Module: clpfd_lists
Name: add_closure_warning_wf/6	Module: custom_explicit_sets
Name: opt_stop_profile/5	Module: runtime_profiler
Name: enum_unbounded/6	Module: kernel_objects
Name: b_compute_expression2/7	Module: b_interpreter
Name: avl_height_less_than_with_solver_strength/2	Module: custom_explicit_sets
Name: in_difference_set_wf/4	Module: kernel_objects
Name: clpfd_not_inrange/3	Module: clpfd_interface
Name: not_empty_set_wf/2	Module: kernel_objects
Name: enumerate_basic_type_set2/8	Module: kernel_objects
Name: post_chr_inrange/3	Module: clpfd_interface
Name: pack_closure/4	Module: state_packing
Name: compute_transitions_pge2/2	Module: pge_algo
Name: in_union_set_wf/4	Module: kernel_objects
Name: register_profiler_runtime/5	Module: runtime_profiler
Name: check_preference/1	Module: preferences
Name: add_new_transition_transid_with_infos/7	Module: tcltk_interface
Name: cleanup_post/7	Module: b_ast_cleanup
Name: constants_profiling_on/0	Module: runtime_profiler
Name: clpfd_modulo_prop/4	Module: kernel_objects
Name: reify_avl_membership/4	Module: custom_explicit_sets
Name: get_max_enablings_per_operation_aux/3	Module: specfile
Name: get_integer_set_interval/3	Module: custom_explicit_sets
Name: open_search_do_one_node/16	Module: model_checker
Name: always_well_defined_or_wd_reorderings_allowed/1	Module: bsyntaxtree
Name: get_preference/2	Module: preferences
Name: find_with_reuse/4	Module: bsyntaxtree
Name: runtime_observe_available/0	Module: runtime_profiler
Name: in_intersection_set_wf/4	Module: kernel_objects
Name: my_get_next_fdvar_to_enumerate/3	Module: kernel_waitflags
Name: observe_runtime_wf/4	Module: runtime_profiler
Name: start_profile/2	Module: runtime_profiler
Name: cleanup_post_function/7	Module: b_ast_cleanup
Name: try_post_constraint/1	Module: clpfd_interface
Name: apply_check_tuple/5	Module: custom_explicit_sets
Name: cleanup_post_with_path/8	Module: b_ast_cleanup
Name: cardval_greater_than/4	Module: b_enumerate
Name: clpfd_abs/2	Module: clpfd_interface
Name: b_execute_operation3/15	Module: b_interpreter
Name: propagate_avl_element_information/4	Module: custom_explicit_sets
Name: pack_state/2	Module: state_packing
Name: my_avl_member/2	Module: custom_explicit_sets
Name: find_typed_identifier_uses_l/3	Module: bsyntaxtree
Name: print_eclipse_prefs/0	Module: preferences
Name: will_throw_enum_warning/1	Module: kernel_objects
Name: enumerate_natural/4	Module: kernel_objects
Name: post_constraint2/2	Module: clpfd_interface
Name: create_exists_opt2/7	Module: bsyntaxtree
Name: check_invariantKO2/2	Module: tcltk_interface
Name: opt_add_source_location_hits/2	Module: source_profiler
Name: tl_normalise/2	Module: haskell_csp
Name: label_clpfd_variable/2	Module: kernel_waitflags
Name: not_in_difference_set_wf/4	Module: kernel_objects
Name: attempt_reification/0	Module: b_interpreter
Name: add_element_to_history/3	Module: preferences
Name: perform_single_operation_retry/4	Module: b_trace_checking
Name: quick_definitely_maximal_set_avl_aux/2	Module: custom_explicit_sets
Name: test_empty_closure_wf/5	Module: custom_explicit_sets
Name: propagate_apply/9	Module: custom_explicit_sets
Name: set_up_typed_localstate_for_pred/4	Module: solver_interface
Name: add_abort_error7/7	Module: kernel_waitflags
Name: b_execute_top_level_statement2/8	Module: b_interpreter
Name: floored_division/5	Module: kernel_objects
Name: b_test_atomic_not_equal_boolean_expression/6	Module: b_interpreter
Name: gen_enum_warning_wf/6	Module: kernel_objects
Name: unbound_variable_for_card/1	Module: kernel_objects
Name: post_constraint/2	Module: clpfd_interface
Name: time_out_constraint/2	Module: clpfd_interface
Name: size_of_avl_sequence/3	Module: custom_explicit_sets
Name: solve_properties/4	Module: b_interpreter
Name: add_recent_document/1	Module: preferences
Name: is_symbolic_closure_or_symbolic_mode/3	Module: custom_explicit_sets
Name: full_normalise_csp_process/3	Module: haskell_csp
Name: block_couple_element_of_avl_set_grX_wf1/7	Module: custom_explicit_sets
Name: compute_hash/3	Module: state_space_exploration_modes
Name: dom_for_specific_closure_aux/6	Module: custom_explicit_sets
Name: enumerate_bool/1	Module: kernel_objects
Name: not_in_intersection_set_wf/4	Module: kernel_objects
Name: specfile_trans_timeout/7	Module: ample_sets
Name: b_possible_trans_name/2	Module: specfile
Name: make_domain_finite/4	Module: kernel_objects
Name: force_empty_and_set_skel/4	Module: kernel_cardinality_attr
Name: apply_check_tuple_delay/9	Module: custom_explicit_sets
Name: evaluable_integer_expression/3	Module: b_global_sets
Name: non_default_pref/1	Module: preferences
Name: element_of_avl_set_wf/4	Module: custom_explicit_sets
Name: apply_to_avl_set_aux/6	Module: custom_explicit_sets
Name: int_power/5	Module: kernel_objects
Name: b_compile2/8	Module: b_compiler
Name: is_not_interesting/1	Module: worker
Name: inverse_apply_ok/4	Module: custom_explicit_sets
Name: frozen_dif/2	Module: kernel_dif
Name: enum_equality_result_smt_mode_wf/3	Module: kernel_equality
Name: b_test_closure/6	Module: custom_explicit_sets
Name: division/5	Module: kernel_objects
Name: is_deadlocked/1	Module: model_checker
Name: add_permutations/2	Module: state_space_exploration_modes
Name: set_preference_direct/3	Module: preferences
Name: get_wait_flag_if_necessary/5	Module: b_interpreter
Name: compute_all_transitions2/2	Module: tcltk_interface
Name: compute_operation_effect_max/6	Module: specfile
Name: check_element_of1/3	Module: kernel_objects
Name: gen_preference_warnings/1	Module: preferences
Name: read_preferences2/1	Module: preferences
Name: get_computed_preference/2	Module: preferences
Name: get_assign_expr_priority_wf/3	Module: b_interpreter
Name: enumerate_real_wf/3	Module: kernel_objects
Name: b_test_atomic_boolean_expression2/5	Module: b_interpreter
Name: b_trace_test_components2/8	Module: b_interpreter_components
Name: time_out_preference_disabled/0	Module: preferences
Name: expand_normal_closure_memo/7	Module: custom_explicit_sets
Name: packed_expression_already_visited/5	Module: state_space_exploration_modes
Name: b_compute_expression_function/8	Module: b_interpreter
Name: propagate_avl_not_element_information/3	Module: custom_explicit_sets
Name: print_throwing_wf/4	Module: kernel_objects
Name: is_not_interesting/1	Module: state_space_exploration_modes
Name: strict_subset_of_wf/3	Module: kernel_objects
Name: post_constraint3/3	Module: clpfd_interface
Name: get_time_out_preference_with_factor/2	Module: preferences
Name: force_equality_objects_lwf2/4	Module: kernel_equality
Name: not_strict_subset_of/2	Module: kernel_objects
Name: get_id_of_node_and_add_if_required/6	Module: state_space_exploration_modes
Name: membership_test_wf2/5	Module: kernel_equality
Name: opt_push_wait_flag_call_stack_info/3	Module: kernel_waitflags
Name: b_not_test_exists/7	Module: b_interpreter
Name: b_test_atomic_equal_boolean_expression/6	Module: b_interpreter
Name: profile_single_call/4	Module: runtime_profiler
Name: assert_id_to_marker/2	Module: state_space_exploration_modes
Name: stop_profile/4	Module: runtime_profiler
Name: expand_normal_closure2/7	Module: custom_explicit_sets
Name: unpack_state2/2	Module: state_packing
Name: observe_set/7	Module: external_functions
Name: is_lazy_extension_function_for_fun_app/1	Module: b_compiler
Name: backup_preferences/0	Module: preferences
Name: expand_forall_quantifier/6	Module: b_interpreter
Name: pack_avl_set/2	Module: state_packing
Name: clpfd_check_geq_nr/2	Module: clpfd_interface
Name: closure1_for_explicit_set/2	Module: custom_explicit_sets

Name: catch/3
Name: lastchangeddate/1	Module: version
Name: revision/1	Module: version
Name: version_str/1	Module: version
Name: =/2
Name: prob_application_type/1	Module: preferences
Name: ->/3
Name: get_prob_application_type/1	Module: preferences
Name: try_get_program_path/2	Module: preferences
Name: possible_program/2	Module: preferences
Name: \==/2
Name: host_platform/1	Module: tools_platform

Name: current_prolog_flag/2
Name: disabled_time_out/1	Module: preferences

Name: true
Name: nauty_init/0	Module: graph_iso_nauty
Name: bmachine_is_precompiled/0	Module: bmachine
Name: ->/3
Name: !
Name: fail
Name: add_warning/3	Module: foo_error
Name: ajoin/2	Module: tools_strings
Name: unavailable_extension/2	Module: pathes_lib
Name: preference_value_requires_extension/3	Module: pathes_extensions_db