| 1 | | % (c) 2009-2025 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
| 2 | | % Heinrich Heine Universitaet Duesseldorf |
| 3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) |
| 4 | | |
| 5 | | :- module(preferences, |
| 6 | | [init_preferences/0, |
| 7 | | tcltk_get_preference/2, |
| 8 | | get_computed_preference/2, |
| 9 | | get_preference/2, get_preferences_list/1, get_preferences_list/2, |
| 10 | | set_preference/2, |
| 11 | | call_with_preference/3, |
| 12 | | temporary_set_preference/2, temporary_set_preference/3, |
| 13 | | reset_temporary_preference/1, reset_temporary_preference/2, |
| 14 | | reset_all_temporary_preferences/0, |
| 15 | | preference_category/2, preference_description/2, preference_val_type/2, preference_val_type_list/2, preference_default_value/2, |
| 16 | | preference/2, |
| 17 | | is_of_type/2, pref_type_synonym/2, |
| 18 | | get_ith_preference_type/2, get_ith_preference_value/2, set_ith_preference_value/2, |
| 19 | | get_ith_preference_type/3, get_ith_preference_value/3, set_ith_preference_value/3, |
| 20 | | virtual_preference_category/2, |
| 21 | | load_preferences/1,save_preferences/1, |
| 22 | | backup_preferences/0, revert_preferences/0, reset_to_defaults/1, reset_for_benchmarking/0, |
| 23 | | set_preference_group/2, |
| 24 | | activate_recent_documents/0,deactivate_recent_documents/0, |
| 25 | | print_preferences/0, print_preferences/1, |
| 26 | | get_preference_with_warnings/2, |
| 27 | | |
| 28 | | add_recent_document/1, /* use to add a file to recent documents list */ |
| 29 | | get_recent_documents/1, clear_recent_documents/0, |
| 30 | | add_element_to_history/3, get_history_elements_list/3, |
| 31 | | |
| 32 | | eclipse_preference/2, print_eclipse_prefs/0, |
| 33 | | advanced_eclipse_preference/2, |
| 34 | | obsolete_eclipse_preference/1, obsolete_preference/1, |
| 35 | | deprecated_eclipse_preference/4, |
| 36 | | get_non_default_preferences/1, |
| 37 | | has_default_value/1, |
| 38 | | |
| 39 | | get_time_out_preference_with_factor/2, |
| 40 | | add_time_outs/3, |
| 41 | | time_out_preference_disabled/0, |
| 42 | | |
| 43 | | get_prob_application_type/1, set_prob_application_type/1, |
| 44 | | try_get_program_path/2, |
| 45 | | |
| 46 | | valid_rgb_color/1, valid_dot_shape/1, valid_dot_line_style/1, valid_dot_node_style/1 |
| 47 | | ]). |
| 48 | | |
| 49 | | :- meta_predicate call_with_preference(0,-,-). |
| 50 | | |
| 51 | | :- use_module(tools, [print_message/1, get_modulename_filename/2]). |
| 52 | | :- use_module(tools_meta, [safe_on_exception/3, safe_on_exception_silent/3, translate_term_into_atom/2]). |
| 53 | | :- use_module(tools_platform, [host_platform/1]). |
| 54 | | :- use_module(tools_strings, [string_concatenate/3, ajoin/2]). |
| 55 | | :- use_module(tools_printing, [print_dynamic_pred/4,print_error/1,format_error_with_nl/2]). |
| 56 | | :- use_module(version, [version_str/1, revision/1, lastchangeddate/1]). |
| 57 | | |
| 58 | | :- use_module(module_information,[module_info/2]). |
| 59 | | :- module_info(group,infrastructure). |
| 60 | | :- module_info(description,'This module manages the various preferences of ProB. Preferences can be grouped, saved and restored and validated from file.'). |
| 61 | | |
| 62 | | :- load_files(library(system), [when(compile_time), imports([environ/2])]). |
| 63 | | |
| 64 | | %:- use_module(debug). % no longer required |
| 65 | | % :- use_module(self_check). % tests now in basic_tests |
| 66 | | :- use_module(error_manager). |
| 67 | | :- use_module(library(lists)). |
| 68 | | |
| 69 | | :- volatile change_flag/0. |
| 70 | | :- dynamic change_flag/0. |
| 71 | | assert_change_flag :- assertz(change_flag). |
| 72 | | |
| 73 | | % -------------- |
| 74 | | |
| 75 | | init_preferences :- retractall(change_flag), |
| 76 | | reset_to_defaults, check_preferences. |
| 77 | | |
| 78 | | check_preferences :- |
| 79 | ? | preference_default_value(P,_), %print(check(P)),nl, |
| 80 | | check_preference(P), |
| 81 | | fail. |
| 82 | | check_preferences :- |
| 83 | ? | (preference_description(P,_) ; preference_category(P,_)), |
| 84 | | \+ preference_default_value(P,_), |
| 85 | | add_internal_error('Preference has no default value:',check_preference(P)). |
| 86 | | check_preferences. % :- print_message('Preferences Checked'). |
| 87 | | |
| 88 | | check_preference(P) :- \+ preference(P,_), |
| 89 | | add_internal_error('Preference has no value:',check_preference(P)),fail. |
| 90 | | check_preference(P) :- \+ preference_val_type(P,_), |
| 91 | | add_internal_error('Preference has no value type:',check_preference(P)),fail. |
| 92 | | check_preference(P) :- \+ preference_category(P,_), |
| 93 | | add_internal_error('Preference has no category:',check_preference(P)),fail. |
| 94 | | check_preference(P) :- \+ preference_description(P,_), |
| 95 | | add_internal_error('Preference has no description:',check_preference(P)),fail. |
| 96 | | check_preference(P) :- |
| 97 | | preference(P,Val), preference_val_type(P,T), |
| 98 | ? | \+ is_of_type(Val,T), |
| 99 | | add_internal_error('Preference value of incorrect type:',is_of_type(P,Val,T)),fail. |
| 100 | | check_preference(P) :- preference_category(P,C1), preference_category(P,C2), C1 \= C2, !, |
| 101 | | add_internal_error('Multiple categories for preference:',category(P,C1,C2)). |
| 102 | | check_preference(_). |
| 103 | | |
| 104 | | % -------------- |
| 105 | | |
| 106 | | load_preferences(File) :- print_message(load_preferences(File)), |
| 107 | | safe_on_exception_silent(Exception1, |
| 108 | | open(File,read,Stream,[encoding(utf8)]), |
| 109 | | (print_see_exception(Exception1,File),fail)), |
| 110 | | !, |
| 111 | | load_preferences2(Stream,File). |
| 112 | | load_preferences(_). |
| 113 | | |
| 114 | | load_preferences2(Stream,File) :- |
| 115 | | safe_on_exception(_Exc2,read_preferences(Stream), |
| 116 | | (print_message('### corrupted preference file'),print_message(File))), |
| 117 | | !. |
| 118 | | %print(loaded_preferences(File)),nl. |
| 119 | | load_preferences2(_Stream,File) :- |
| 120 | | print_message('### error occured reading preference file'), |
| 121 | | print_message(File). |
| 122 | | |
| 123 | | print_see_exception(error(existence_error(_,_),_),File) :- !, |
| 124 | | print_message('preference file does not exist, ProB will create a fresh one'),print_message(File). |
| 125 | | print_see_exception(Exception,File) :- |
| 126 | | print_message('### cannot open preference file'),print_message(File), |
| 127 | | print_message(Exception). |
| 128 | | |
| 129 | | read_preferences(Stream) :- clear_dynamic_preference_predicates, |
| 130 | | call_cleanup(read_preferences2(Stream),close(Stream)). |
| 131 | | read_preferences2(Stream) :- |
| 132 | | read(Stream,Term), |
| 133 | | Term \= end_of_file, !, %print(pref(Term)),nl, |
| 134 | | (Term = preference(Pref,NVal) |
| 135 | | -> (volatile_preference(Pref) -> true |
| 136 | | ; retract(preference(Pref,_)) -> assertz(preference(Pref,NVal)) |
| 137 | | ; obsolete_preference(Pref) -> print_message(obsolete(Pref)) |
| 138 | | ; add_message(load_preferences,'Unknown preference in preference file: ',Pref) |
| 139 | | ) |
| 140 | | ; Term = ':-'(dynamic(_)) -> true |
| 141 | | ; dynamic_preference_predicate(Term) -> assertz(Term) |
| 142 | | ; (Term = (Head:-fail),dynamic_preference_predicate(Head)) -> true |
| 143 | | ; add_error(load_preferences,'Unrecognised:',Term) |
| 144 | | ), |
| 145 | | read_preferences2(Stream). |
| 146 | | read_preferences2(_Stream) :- retractall(change_flag), recompute_nr_of_recent_documents. |
| 147 | | %recompute_nr_of_searched_and_replaced_patterns. |
| 148 | | %recompute_nr_of_eval_history_elements. |
| 149 | | |
| 150 | | clear_dynamic_preference_predicates :- dynamic_preference_predicate(X), retractall(X),fail. |
| 151 | | clear_dynamic_preference_predicates. |
| 152 | | |
| 153 | | % declare which dynamic predicates are stored in Preference file |
| 154 | | dynamic_preference_predicate(recent_documents(_)). |
| 155 | | dynamic_preference_predicate(searched_patterns(_)). |
| 156 | | dynamic_preference_predicate(replaced_patterns(_)). |
| 157 | | dynamic_preference_predicate(eval_history_elements(_)). |
| 158 | | dynamic_preference_predicate(eval_csp_history_elements(_)). |
| 159 | | dynamic_preference_predicate(checked_ltl_formulas(_)). |
| 160 | | |
| 161 | | save_preferences(File) :- change_flag,!, |
| 162 | | % catch exception in case we cannot write preferences file |
| 163 | | catch(save_preferences2(File), Exception, ( |
| 164 | | string_concatenate('Cannot write preferences file ',File,Msg), |
| 165 | | add_error(save_preferences,Msg,Exception) |
| 166 | | )). |
| 167 | | save_preferences(File) :- print_message(preferences_unchanged(File)). |
| 168 | | |
| 169 | | save_preferences2(File) :- |
| 170 | | print_message(save_preferences(File)), |
| 171 | | open(File,write,S,[encoding(utf8)]), |
| 172 | | (print_preferences_for_saving(S) -> true ; true), |
| 173 | | close(S), |
| 174 | | retractall(change_flag). |
| 175 | | |
| 176 | | % if we have temporarily set a preference, then print the old value |
| 177 | | print_preferences_for_saving(Stream) :- |
| 178 | | preference_default_value(Pref,_), |
| 179 | | preference(Pref,CurVal), |
| 180 | | (temp_pref(Pref,OldVal,CurVal) -> V=OldVal ; V=CurVal), % temp_pref can be nested !, will not print initial value in this case |
| 181 | | write_term(Stream,preference(Pref,V),[quoted(true)]),print(Stream,'.'),nl(Stream), |
| 182 | | fail. |
| 183 | | print_preferences_for_saving(Stream) :- print_dynamic_preferences(Stream). |
| 184 | | |
| 185 | | print_preferences :- print_preferences(user_output). |
| 186 | | print_preferences(Stream) :- |
| 187 | | print_dynamic_pred(Stream,preferences,preference,2), |
| 188 | | print_dynamic_preferences(Stream). |
| 189 | | |
| 190 | | print_dynamic_preferences(Stream) :- |
| 191 | | dynamic_preference_predicate(P), functor(P,F,N), |
| 192 | | print_dynamic_pred(Stream,preferences,F,N),fail. |
| 193 | | print_dynamic_preferences(_). |
| 194 | | |
| 195 | | % now in basic_tests.pl |
| 196 | | %:- assert_must_succeed(get_non_default_preferences(_)). |
| 197 | | |
| 198 | | get_non_default_preferences(list(L)) :- |
| 199 | | findall(PS,non_default_pref(PS),L). |
| 200 | | |
| 201 | | has_default_value(Pref) :- get_preference(Pref,Val), preference_default_value(Pref,Val). |
| 202 | | |
| 203 | | non_default_pref(PrefStr) :- preference(Pref,Val), preference_default_value(Pref,DVal), |
| 204 | | DVal \= Val, |
| 205 | | (eclipse_preference(ECLPREF,Pref) -> |
| 206 | | ajoin([Pref,' (',ECLPREF,') == ',Val,' (default = ',DVal, ')'],PrefStr) |
| 207 | | ; |
| 208 | | ajoin([Pref,' == ',Val,' (default = ',DVal, ')'],PrefStr) |
| 209 | | ). |
| 210 | | |
| 211 | | :- volatile change_flag_backup/0, pref_backup/2. |
| 212 | | :- dynamic change_flag_backup/0. |
| 213 | | :- dynamic pref_backup/2. |
| 214 | | |
| 215 | | backup_preferences :- retractall(pref_backup(_,_)),retractall(change_flag_backup), |
| 216 | | preference(P,Val), assertz(pref_backup(P,Val)),fail. |
| 217 | | backup_preferences :- (change_flag -> assertz(change_flag_backup) ; true). |
| 218 | | |
| 219 | | revert_preferences :- \+(pref_backup(_,_)),!, print_error('No previously backed-up preferences in revert_preferences!'). |
| 220 | | revert_preferences :- retractall(preference(_,_)),pref_backup(P,Val), assertz(preference(P,Val)),fail. |
| 221 | | revert_preferences :- retractall(change_flag), (change_flag_backup -> assert_change_flag ; true). |
| 222 | | |
| 223 | | reset_to_defaults :- |
| 224 | | reset_to_defaults(_). |
| 225 | | |
| 226 | ? | reset_to_defaults(Category) :- preference_category(Pref,Category), |
| 227 | | preference_default_value(Pref,Val), |
| 228 | | retractall(preference(Pref,_)), |
| 229 | | assertz(preference(Pref,Val)), |
| 230 | | fail. |
| 231 | | reset_to_defaults(_) :- assert_change_flag. |
| 232 | | |
| 233 | | |
| 234 | | reset_for_benchmarking :- |
| 235 | | set_preference(maxNrOfInitialisations,3), |
| 236 | | set_preference(randomisedRestartInitalisations,false), |
| 237 | | set_preference(maxNrOfEnablingsPerOperation,10), |
| 238 | | set_preference(maxint,4), |
| 239 | | set_preference(minint,-1), |
| 240 | | set_preference(time_out,3500), |
| 241 | | set_preference(globalsets_fdrange,3), |
| 242 | | set_preference(show_initialisation_arguments,true), |
| 243 | | set_preference(provide_trace_information,false), |
| 244 | | set_preference(prob_profiling_on,false), |
| 245 | | set_preference(prob_source_profiling_on,false), |
| 246 | | set_preference(performance_monitoring_on,false), |
| 247 | | set_preference(data_validation_mode,false), |
| 248 | | set_preference(find_abort_values,false), |
| 249 | | set_preference(raise_abort_immediately,false), |
| 250 | | set_preference(expand_forall_upto,100), |
| 251 | | %set_preference(animate_skip_operations,true), |
| 252 | | set_preference(cspm_animate_all_processes_without_arguments,false), |
| 253 | | set_preference(cspm_animate_all_processes,false). |
| 254 | | % set_preference(convert_closures_into_explicit_form_for_store,true). |
| 255 | | |
| 256 | | |
| 257 | | call_with_preference(Call,Pref,Val) :- |
| 258 | | temporary_set_preference(Pref,Val,CHNG1), |
| 259 | | call_cleanup(Call, |
| 260 | | reset_temporary_preference(Pref,CHNG1)). |
| 261 | | |
| 262 | | |
| 263 | | % ------------------------ |
| 264 | | |
| 265 | | |
| 266 | | % now in basic_tests.pl |
| 267 | | %:- assert_must_succeed( \+((eclipse_preference(_EP,P), \+preference_default_value(P,_Val)))). |
| 268 | | % the order is also the order in which they appear in ProB for Rodin: |
| 269 | | eclipse_preference('DEFAULT_SETSIZE',globalsets_fdrange). |
| 270 | | eclipse_preference('MAX_INITIALISATIONS',maxNrOfInitialisations). |
| 271 | | eclipse_preference('MAX_OPERATIONS',maxNrOfEnablingsPerOperation). |
| 272 | | eclipse_preference('MAXINT',maxint). |
| 273 | | eclipse_preference('MININT',minint). |
| 274 | | %eclipse_preference('ANIMATE_SKIP_OPERATIONS',animate_skip_operations). |
| 275 | | %eclipse_preference('EXPAND_CLOSURES_FOR_STATE',convert_closures_into_explicit_form_for_store). |
| 276 | | eclipse_preference('TIME_OUT',time_out). |
| 277 | | eclipse_preference('NUMBER_OF_ANIMATED_ABSTRACTIONS',number_animated_abstractions). |
| 278 | | eclipse_preference('NUMBER_OF_SKIPPED_REFINEMENTS',number_skipped_refined_machines). |
| 279 | | eclipse_preference('USE_RECORD_CONSTRUCTION',use_record_construction). |
| 280 | | eclipse_preference('USE_IGNORE_PRAGMAS',use_ignore_pragmas). |
| 281 | | |
| 282 | | eclipse_preference('COMPRESSION',try_use_state_packing). |
| 283 | | 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 |
| 284 | | eclipse_preference('OPERATION_REUSE_FOR_INVARIANTS',try_operation_reuse_for_invariants). |
| 285 | | eclipse_preference('PROOF_INFO',use_po). |
| 286 | | |
| 287 | | eclipse_preference('RANDOMISE_ENUMERATION_ORDER',randomise_enumeration_order). |
| 288 | | eclipse_preference('TRY_FIND_ABORT',find_abort_values). % maybe rename into TRY_FIND_WD_ERROR ? |
| 289 | | eclipse_preference('CLPFD',use_clpfd_solver). |
| 290 | | eclipse_preference('CLPFD_LABELING',clpfd_solver_label_option). |
| 291 | | eclipse_preference('CHR',use_chr_solver). |
| 292 | | eclipse_preference('SMT',use_smt_mode). |
| 293 | | eclipse_preference('SOLVER_STRENGTH',solver_strength). |
| 294 | | eclipse_preference('CSE',use_common_subexpression_elimination). |
| 295 | | eclipse_preference('STATIC_ORDERING',use_static_ordering). |
| 296 | | |
| 297 | | %eclipse_preference('SYMMETRY_MARKERS',use_symmetry_marker_hash). |
| 298 | | %eclipse_preference('PERMUTATION_FLOODING',enable_permutation_reducation). |
| 299 | | eclipse_preference('SYMMETRY_MODE',symmetry_mode). |
| 300 | | %eclipse_preference('KODKOD',try_kodkod_on_load). % new preference try_solver_on_load |
| 301 | | eclipse_preference('SOLVER_FOR_PROPERTIES',use_solver_on_load). |
| 302 | | |
| 303 | | eclipse_preference('SYMBOLIC',convert_comprehension_sets_into_closures). |
| 304 | | eclipse_preference('SYMBOLIC_LIMIT',comprehension_set_symbolic_limit). |
| 305 | | eclipse_preference('MEMO',use_closure_expansion_memoization). |
| 306 | | eclipse_preference('MEMOIZE_FUNCTIONS',use_function_memoization). |
| 307 | | |
| 308 | | eclipse_preference('AUTO_DETECT_THEORY_MAPPING',auto_detect_theory_ops). |
| 309 | | eclipse_preference('PROB_VERSION_INFO',prob_version_info). |
| 310 | | eclipse_preference('PROB_REVISION_INFO',prob_revision_info). |
| 311 | | eclipse_preference('PROB_LASTCHANGED_INFO',prob_lastchangedate_info). |
| 312 | | |
| 313 | | eclipse_preference(A,B) :- advanced_eclipse_preference(A,B). |
| 314 | | |
| 315 | | % these will not be shown in ProB for Rodin for example: |
| 316 | | advanced_eclipse_preference('OPTIMIZE_AST',optimize_ast). |
| 317 | | advanced_eclipse_preference('NORMALIZE_AST',normalize_ast). |
| 318 | | advanced_eclipse_preference('STATIC_SYMMETRY_DETECTION',use_static_symmetry_detection). |
| 319 | | advanced_eclipse_preference('ENUMERATION_ORDER_ANALYSIS',perform_enumeration_order_analysis). % should probably not be disabled in Rodin |
| 320 | | advanced_eclipse_preference('DETECT_LAMBDAS',detect_lambdas). |
| 321 | | advanced_eclipse_preference('DATA_VALIDATION',data_validation_mode). |
| 322 | | advanced_eclipse_preference('RAISE_ABORT_IMMEDIATELY',raise_abort_immediately). |
| 323 | | %advanced_eclipse_preference('WARN_WHEN_EXPANDING_INFINITE_CLOSURES',warn_when_expanding_infinite_closures). |
| 324 | | advanced_eclipse_preference('ENUMERATE_INFINITE_TYPES',allow_enumeration_of_infinite_types). |
| 325 | | advanced_eclipse_preference('KODKOD_ONLY_FULL',kodkod_for_components). |
| 326 | | advanced_eclipse_preference('KODKOD_RAISE_WARNINGS',kodkod_raise_warnings). |
| 327 | | advanced_eclipse_preference('KODKOD_MAX_NR_SOLS',kodkod_max_nr_solutions). |
| 328 | | advanced_eclipse_preference('KODKOD_SYMMETRY',kodkod_symmetry_level). |
| 329 | | advanced_eclipse_preference('KODKOD_SAT_SOLVER',kodkod_sat_solver). |
| 330 | | advanced_eclipse_preference('CSE_PRED',use_common_subexpression_also_for_predicates). |
| 331 | | advanced_eclipse_preference('CSE_WD_ONLY',use_common_subexpression_wd_only). |
| 332 | | advanced_eclipse_preference('CSE_SUBST',use_common_subexpression_also_for_substitutions). |
| 333 | | advanced_eclipse_preference('USELESS_CODE_ELIMINATION',useless_code_elimination). |
| 334 | | advanced_eclipse_preference('ALLOW_INCOMPLETE_SETUP_CONSTANTS',allow_incomplete_partial_setup_constants). |
| 335 | | advanced_eclipse_preference('PARTITION_PROPERTIES',partition_predicates). |
| 336 | | advanced_eclipse_preference('PARTITION_PROPERTIES_INLINE',partition_predicates_inline_equalities). |
| 337 | | advanced_eclipse_preference('SHOW_EVENTB_ANY_VALUES',show_eventb_any_arguments). |
| 338 | | advanced_eclipse_preference('RANDOMISE_OPERATION_ORDER',randomise_operation_order). |
| 339 | | advanced_eclipse_preference('RANDOMISED_RESTART_INIT',randomisedRestartInitalisations). |
| 340 | | advanced_eclipse_preference('EXPAND_FORALL_UPTO',expand_forall_upto). |
| 341 | | advanced_eclipse_preference('LIFT_EXISTS',lift_existential_quantifiers). |
| 342 | | advanced_eclipse_preference('REMOVE_IMPLIED_CONSTRAINTS',remove_implied_constraints). % imply |
| 343 | | advanced_eclipse_preference('MAX_DISPLAY_SET',expand_avl_upto). |
| 344 | | advanced_eclipse_preference('SHOW_FORMULA_FUNCTOR',show_bvisual_formula_functor_from). |
| 345 | | advanced_eclipse_preference('SHOW_FORMULA_PROOF_INFO',show_bvisual_proof_info_icons). |
| 346 | | advanced_eclipse_preference('SHOW_FORMULA_EXPLANATIONS',show_bvisual_formula_explanations). |
| 347 | | advanced_eclipse_preference('WARN_IF_DEFINITION_HIDES_VARIABLE',warn_if_definition_hides_variable). |
| 348 | | advanced_eclipse_preference('TYPE_CHECK_DEFINITIONS',type_check_definitions). |
| 349 | | advanced_eclipse_preference('TRACE_INFO',provide_trace_information). |
| 350 | | advanced_eclipse_preference('PROFILING_INFO',prob_profiling_on). |
| 351 | | advanced_eclipse_preference('SOURCE_PROFILING_INFO',prob_source_profiling_on). |
| 352 | | advanced_eclipse_preference('STORE_DETAILED_TRANSITION_INFOS',eventtrace). % Event Trace Info |
| 353 | | advanced_eclipse_preference('PERFORMANCE_INFO',performance_monitoring_on). |
| 354 | | advanced_eclipse_preference('PERFORMANCE_INFO_LIMIT',performance_monitoring_expansion_limit). |
| 355 | | advanced_eclipse_preference('DOUBLE_EVALUATION',double_evaluation_when_analysing). |
| 356 | | advanced_eclipse_preference('PROB_SAFE_MODE',prob_safe_mode). |
| 357 | | %advanced_eclipse_preference('RECURSIVE',allow_recursive_closures). |
| 358 | | advanced_eclipse_preference('IGNORE_HASH_COLLISIONS',ignore_hash_collisions). |
| 359 | | advanced_eclipse_preference('USE_SCOPE_DEFINITION',use_scope_predicate). |
| 360 | | advanced_eclipse_preference('FORGET_STATE_SPACE',forget_state_space). |
| 361 | | advanced_eclipse_preference('SAFETY_MODEL_CHECK',store_only_one_incoming_transition). % is actually INVARIANT_MC |
| 362 | | advanced_eclipse_preference('LTL_SAFETY_MODEL_CHECK',use_safety_ltl_model_checker). |
| 363 | | %advanced_eclipse_preference('LARGE_PARSER_JVM',use_large_jvm_for_parser). |
| 364 | | advanced_eclipse_preference('JVM_PARSER_HEAP_MB',jvm_parser_heap_size_mb). % TO DO: do not show in ProB2-UI |
| 365 | | advanced_eclipse_preference('JVM_PARSER_ARGS',jvm_parser_additional_args). |
| 366 | | advanced_eclipse_preference('JVM_PARSER_POSITION_INFOS',jvm_parser_position_infos). |
| 367 | | %advanced_eclipse_preference('JVM_PARSER_FASTRW',jvm_parser_fastrw). |
| 368 | | advanced_eclipse_preference('CSP_STRIP_SOURCE_LOC',cspm_strip_source_location). |
| 369 | | advanced_eclipse_preference('INVARIANT_CHECKING',do_invariant_checking). |
| 370 | | advanced_eclipse_preference('ASSERT_CHECKING',do_assert_checking). |
| 371 | | %advanced_eclipse_preference('NEGATED_INVARIANT_CHECKING',do_neginvariant_checking). % use double_evaluation_when_analysing |
| 372 | | advanced_eclipse_preference('ALLOW_SIMULTANEOUS_ASSIGNMENTS',allow_simultaneous_assignments). |
| 373 | | advanced_eclipse_preference('ALLOW_REALS',allow_arith_operators_on_reals). |
| 374 | | advanced_eclipse_preference('REAL_SOLVER',solver_for_reals). |
| 375 | | advanced_eclipse_preference('BUGLY',bugly_pp_scrambling). % B Ugly |
| 376 | | advanced_eclipse_preference('ATELIERB_KRT_PATH',path_to_atb_krt). |
| 377 | | advanced_eclipse_preference('JAVA_PATH',path_to_java). |
| 378 | | advanced_eclipse_preference('JAVA_PARSER_PATH',path_to_java_parser). |
| 379 | | advanced_eclipse_preference('TRY_ATELIERB_PROVERS',try_atb_provers). |
| 380 | | advanced_eclipse_preference('SMTLIB_BOOL_ARRAYS_TO_SETS',smtlib2b_arrays_as_sets). |
| 381 | | advanced_eclipse_preference('SMTLIB_PREPROCESS',smtlib2b_cleanup_predicate). |
| 382 | | advanced_eclipse_preference('SYMBOLIC_MC_TRY_OTHER_SOLVERS',symbolic_mc_try_other_solvers). |
| 383 | | advanced_eclipse_preference('SMT_SUPPORTED_INTERPRETER',smt_supported_interpreter). |
| 384 | | advanced_eclipse_preference('SAT_SUPPORTED_INTERPRETER',sat_supported_interpreter). |
| 385 | | advanced_eclipse_preference('PP_FROZEN_INFOS',translate_print_frozen_infos). |
| 386 | | advanced_eclipse_preference('PP_SEQUENCES',translate_print_all_sequences). |
| 387 | | advanced_eclipse_preference('PP_CS_STYLE_SEQUENCES',translate_print_cs_style_sequences). |
| 388 | | advanced_eclipse_preference('STRING_AS_SEQUENCE',allow_sequence_operators_on_strings). |
| 389 | | advanced_eclipse_preference('COMPILE_WHILE',compile_while_body). |
| 390 | | advanced_eclipse_preference('EXPAND_BECOMES_SUCH',expand_becomes_such_into_set). |
| 391 | | %advanced_eclipse_preference('PGE',pge). |
| 392 | | |
| 393 | | |
| 394 | | advanced_eclipse_preference('DOT_PROP',dot_print_node_properties). |
| 395 | | advanced_eclipse_preference('DOT_IDS',dot_print_node_ids). |
| 396 | | advanced_eclipse_preference('DOT_TRANS_IDS',dot_print_transition_ids). |
| 397 | | advanced_eclipse_preference('DOT_INFO',dot_print_node_info). |
| 398 | | advanced_eclipse_preference('DOT_LOOPS',dot_print_self_loops). |
| 399 | | advanced_eclipse_preference('DOT_ARC_COLORS',dot_print_arc_colors). |
| 400 | | advanced_eclipse_preference('DOT_FUNCTIONS',dot_print_functions). |
| 401 | | advanced_eclipse_preference('DOT_ROOT',dot_print_root). |
| 402 | | %advanced_eclipse_preference('DOT_LEAVES',dot_print_leaves). |
| 403 | | advanced_eclipse_preference('DOT_EDGE_LABELS',dot_print_edge_labels). |
| 404 | | advanced_eclipse_preference('DOT_ARGUMENTS',dot_print_action_arguments). |
| 405 | | advanced_eclipse_preference('DOT_COLOR_ARC',dot_normal_arc_colour). |
| 406 | | advanced_eclipse_preference('DOT_COLOR_NODE',dot_normal_node_colour). |
| 407 | | advanced_eclipse_preference('DOT_COLOR_NODE_ERROR',dot_invariant_violated_node_colour). |
| 408 | | advanced_eclipse_preference('DOT_COLOR_NODE_OPEN',dot_open_node_colour). |
| 409 | | advanced_eclipse_preference('DOT_COLOR_NODE_GOAL',dot_goal_node_colour). |
| 410 | | advanced_eclipse_preference('DOT_PEN_WIDTH',dot_node_penwidth). |
| 411 | | advanced_eclipse_preference('DOT_EDGE_PEN_WIDTH',dot_edge_penwidth). |
| 412 | | advanced_eclipse_preference('DOT_SHOW_OP_READ_WRITES',dot_enabling_show_readwrites). |
| 413 | | advanced_eclipse_preference('DOT',path_to_dot). |
| 414 | | advanced_eclipse_preference('DOT_ENGINE',dot_default_engine). |
| 415 | | advanced_eclipse_preference('DOT_DECOMPOSE_NODES',dot_state_graph_decompose). |
| 416 | | |
| 417 | | advanced_eclipse_preference('SUCCESSFUL_RULE_COLOUR',successful_rule_colour). |
| 418 | | advanced_eclipse_preference('FAILED_RULE_COLOUR',failed_rule_colour). |
| 419 | | advanced_eclipse_preference('DISABLED_RULE_COLOUR',disabled_rule_colour). |
| 420 | | advanced_eclipse_preference('NOT_CHECKED_RULE_COLOUR',not_checked_rule_colour). |
| 421 | | advanced_eclipse_preference('RULE_GRAPH_SHAPE',rule_graph_shape). |
| 422 | | advanced_eclipse_preference('EXECUTED_COMPUTATION_COLOUR',executed_computation_colour). |
| 423 | | advanced_eclipse_preference('NOT_EXECUTED_COMPUTATION_COLOUR',not_executed_computation_colour). |
| 424 | | advanced_eclipse_preference('DISABLED_COMPUTATION_COLOUR',disabled_computation_colour). |
| 425 | | advanced_eclipse_preference('COMPUTATION_GRAPH_SHAPE',computation_graph_shape). |
| 426 | | advanced_eclipse_preference('SUCCEEDED_DEPENDENCY_COLOUR',succeeded_dependency_colour). |
| 427 | | advanced_eclipse_preference('FAILED_DEPENDENCY_COLOUR',failed_dependency_colour). |
| 428 | | advanced_eclipse_preference('NORMAL_DEPENDENCY_COLOUR',normal_dependency_colour). |
| 429 | | |
| 430 | | |
| 431 | | advanced_eclipse_preference('TK_CUSTOM_STATE_VIEW_PADDING',tk_custom_state_viewer_padding). |
| 432 | | advanced_eclipse_preference('TK_CUSTOM_STATE_VIEW_STRING_PADDING',tk_custom_state_viewer_str_padding). |
| 433 | | advanced_eclipse_preference('TK_CUSTOM_STATE_VIEW_FONT_NAME',tk_custom_state_viewer_font_name). |
| 434 | | advanced_eclipse_preference('TK_CUSTOM_STATE_VIEW_FONT_SIZE',tk_custom_state_viewer_font_size). |
| 435 | | advanced_eclipse_preference('TK_CUSTOM_STATE_VIEW_VISIBLE',use_tk_custom_state_viewer). |
| 436 | | |
| 437 | | %advanced_eclipse_preference('BOOL_AS_PREDICATE',bool_expression_as_predicate). % obsolete |
| 438 | | advanced_eclipse_preference('ALLOW_UNTYPED_IDENTIFIERS',allow_untyped_identifiers). |
| 439 | | advanced_eclipse_preference('ALLOW_LOCAL_OPERATION_CALLS',allow_local_operation_calls). |
| 440 | | advanced_eclipse_preference('ALLOW_OPERATION_CALLS_IN_EXPRESSIONS',allow_operation_calls_in_expr). |
| 441 | | advanced_eclipse_preference('ALLOW_COMPLEX_LETS',allow_let_to_reuse_introduced_ids). |
| 442 | | advanced_eclipse_preference('REQUIRE_OUTPUT_ASSIGNMENT',require_operations_to_assign_all_outputs). |
| 443 | | advanced_eclipse_preference('ALLOW_OUTPUT_READING',allow_operations_to_read_outputs). |
| 444 | | advanced_eclipse_preference('ALLOW_OPERATION_CALLS_FOR_USES',allow_operation_calls_for_uses). |
| 445 | | advanced_eclipse_preference('ALLOW_INITIALISATION_OVERRIDE',allow_overriding_initialisation). |
| 446 | | advanced_eclipse_preference('REPL_UNICODE',repl_unicode). |
| 447 | | advanced_eclipse_preference('REPL_CACHE_PARSING',repl_cache_parsing). |
| 448 | | advanced_eclipse_preference('CACHE_CONSTANTS',cache_constants). |
| 449 | | advanced_eclipse_preference('CACHE_OPERATIONS',cache_operations). |
| 450 | | advanced_eclipse_preference('CACHE_OPERATIONS_RUNTIME_LIMIT',cache_operations_runtime_limit). |
| 451 | | advanced_eclipse_preference('LATEX_ENCODING',latex_encoding). |
| 452 | | advanced_eclipse_preference('LATEX_GREEK_IDENTIFIERS',latex_pp_greek_ids). |
| 453 | | advanced_eclipse_preference('XML_ENCODING',xml_encoding). |
| 454 | | advanced_eclipse_preference('BBRESULTS',view_probcli_errors_using_bbresults). |
| 455 | | advanced_eclipse_preference('IGNORE_PRJ_TYPES',ignore_prj_types). |
| 456 | | advanced_eclipse_preference('FILTER_UNUSED',filter_unused_constants). |
| 457 | | advanced_eclipse_preference('DISPROVER_MODE',disprover_mode). |
| 458 | | advanced_eclipse_preference('TRACE_UPON_ERROR',trace_upon_error). |
| 459 | | advanced_eclipse_preference('NDJSON_ERROR_LOG_FILE',error_log_file). |
| 460 | | advanced_eclipse_preference('STRICT_RAISE_WARNINGS',strict_raise_warnings). |
| 461 | | advanced_eclipse_preference('STRICT_RAISE_ENUM_WARNINGS',strict_raise_enum_warnings). |
| 462 | | advanced_eclipse_preference('STRICT_CLASH_CHECKING',clash_strict_checks). |
| 463 | | %advanced_eclipse_preference('SHOW_FULL_ERROR_LOCATIONS',show_full_error_span). |
| 464 | | advanced_eclipse_preference('EDITOR',path_to_text_editor_launch). |
| 465 | | advanced_eclipse_preference('EDITOR_GUI',path_to_text_editor). |
| 466 | | advanced_eclipse_preference('TLC_WORKERS',tlc_number_of_workers). % will be useful once we can call TLC from probcli (-mc_with_tlc) |
| 467 | | advanced_eclipse_preference('TLC_USE_PROB_CONSTANTS',tlc_use_prob_constant_setup). |
| 468 | | advanced_eclipse_preference('LTSMIN',path_to_ltsmin). |
| 469 | | |
| 470 | | advanced_eclipse_preference('INTERNAL_ARGUMENT_PREFIX',prefix_internal_operation_arguments). |
| 471 | | advanced_eclipse_preference('MINIMAL_TEST_SUITES',generate_minimal_nr_of_testcases). |
| 472 | | advanced_eclipse_preference('ALLOW_NEW_OPERATIONS_IN_REFINEMENT',allow_new_ops_in_refinement). |
| 473 | | |
| 474 | | advanced_eclipse_preference('ALLOY_USE_IMPLEMENTABLE_INTEGERS',alloy_use_implementable_integers). |
| 475 | | advanced_eclipse_preference('ALLOY_SCOPELESS_TRANSLATION',alloy_scopeless_translation). |
| 476 | | advanced_eclipse_preference('ALLOY_TRANSLATION_FOR_PROOF',alloy_translation_for_proof). |
| 477 | | advanced_eclipse_preference('ALLOY_STRICT_INTEGERS',alloy_strict_integers). |
| 478 | | |
| 479 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_HORIZONTAL',dot_event_hierarchy_horizontal). |
| 480 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_MCH_COL',dot_event_hierarchy_machine_colour). |
| 481 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_REF_COL',dot_event_hierarchy_refines_colour). |
| 482 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_NEW_COL',dot_event_hierarchy_new_event_colour). |
| 483 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_RENAME_COL',dot_event_hierarchy_rename_event_colour). |
| 484 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_RENAME_UNCHG_COL',dot_event_hierarchy_rename_unchanged_event_colour). |
| 485 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_UNCHG_COL',dot_event_hierarchy_unchanged_event_colour). |
| 486 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_GRD_STRGTH_COL',dot_event_hierarchy_grd_strengthening_event_colour). |
| 487 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_GRD_KEEP_COL',dot_event_hierarchy_grd_keeping_event_colour). |
| 488 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_EDGE_COL',dot_event_hierarchy_edge_colour). |
| 489 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_EXTENDS_COL',dot_event_hierarchy_extends_colour). |
| 490 | | advanced_eclipse_preference('DOT_HIERARCHY_EXTRA_DETAIL',dot_hierarchy_show_extra_detail). |
| 491 | | advanced_eclipse_preference('DOT_USE_CONSTANTS',dot_print_use_constants). |
| 492 | | advanced_eclipse_preference('DOT_ROOT_SHAPE',dot_root_shape). |
| 493 | | advanced_eclipse_preference('DOT_NORMAL_NODE_SHAPE',dot_normal_node_shape). |
| 494 | | advanced_eclipse_preference('DOT_CURRENT_NODE_SHAPE',dot_current_node_shape). |
| 495 | | advanced_eclipse_preference('DOT_SCOPE_LIMIT_COL',dot_scope_limit_node_colour). |
| 496 | | advanced_eclipse_preference('DOT_FILL_NORMAL_NODES',dot_fill_normal_nodes). |
| 497 | | advanced_eclipse_preference('DOT_NODE_FONT_SIZE',dot_node_font_size). |
| 498 | | advanced_eclipse_preference('DOT_EDGE_FONT_SIZE',dot_edge_font_size). |
| 499 | | advanced_eclipse_preference('DOT_LIMIT_PAGE_SIZE',dot_with_page_size). |
| 500 | | advanced_eclipse_preference('DOT_HORIZONTAL_LAYOUT',dot_horizontal_layout). |
| 501 | | advanced_eclipse_preference('DOT_COLOUR_GOAL',dot_colour_goal_nodes). |
| 502 | | advanced_eclipse_preference('DOT_DEFINITIONS_USE_SUB_GRAPH',dot_definitions_use_sub_graph). |
| 503 | | advanced_eclipse_preference('DOT_DEFINITIONS_SHOW_ALL',dot_definitions_show_all). |
| 504 | | advanced_eclipse_preference('DOT_PROJECTION_NON_DET_COL',dot_projection_non_det_edge_colour). |
| 505 | | advanced_eclipse_preference('DOT_PROJECTION_DET_COL',dot_projection_det_edge_colour). |
| 506 | | advanced_eclipse_preference('DOT_PROJECTION_NON_DEF_COL',dot_projection_non_definite_edge_style). |
| 507 | | advanced_eclipse_preference('DOT_PROJECTION_DEF_COL',dot_projection_definite_edge_style). |
| 508 | | advanced_eclipse_preference('DOT_PROJECTION_LABEL_LIMIT',dot_projection_label_limit). |
| 509 | | advanced_eclipse_preference('DOT_PROJECTION_ONLY_EXPLORED_NODES',dot_projection_process_only_explored). |
| 510 | | advanced_eclipse_preference('DOT_USE_UNICODE',dot_use_unicode). |
| 511 | | advanced_eclipse_preference('DOT_PREDICATE_NODE_SHAPE',dot_predicate_node_shape). |
| 512 | | advanced_eclipse_preference('DOT_EXPRESSION_NODE_SHAPE',dot_expression_node_shape). |
| 513 | | advanced_eclipse_preference('DOT_VARIABLE_MODIFICATION_HIDE_ONLY_WRITTEN',dot_var_mod_hide_only_written). |
| 514 | | advanced_eclipse_preference('DOT_MACHINE_HIERARCHY_MAX_IDS',dot_hierarchy_max_ids). |
| 515 | | advanced_eclipse_preference('CBC_PROVIDE_EXPLANATIONS',cbc_provide_explanations). |
| 516 | | advanced_eclipse_preference('CBC_ENABLE_ANALYSIS_TIME_OUT',timeout_cbc_analysis). |
| 517 | | advanced_eclipse_preference('SYNTAX_HIGHLIGHT',do_syntax_highlighting). |
| 518 | | advanced_eclipse_preference('WD_IGNORE_EXTERNAL',wd_ignore_external_funs). |
| 519 | | advanced_eclipse_preference('WD_IGNORE_FINITE_POS',wd_skip_finite_pos). |
| 520 | | advanced_eclipse_preference('WD_ANALYSIS_FOR_ANIMATION',wd_analysis_for_animation). |
| 521 | | advanced_eclipse_preference('Z3_SOLVE_FOR_ANIMATION',z3_solve_for_animation). |
| 522 | | advanced_eclipse_preference('ADD_WD_POS_FOR_Z3',add_wd_pos_for_z3). |
| 523 | | %advanced_eclipse_preference('DO_NOT_PRINT_WD_ERRORS',do_not_print_wd_errors). |
| 524 | | advanced_eclipse_preference('TABLE_COLUMN_LIMIT',translation_limit_for_table_commands). |
| 525 | | advanced_eclipse_preference('MAX_TRACES',trace_generation_limit). |
| 526 | | advanced_eclipse_preference('TRACES_TIME_OUT',trace_generation_time_out). |
| 527 | | |
| 528 | | advanced_eclipse_preference('MC_DC_Level',mc_dc_default_level). |
| 529 | | advanced_eclipse_preference('VISB_DEBUG_INFO',visb_show_debug_infos). |
| 530 | | |
| 531 | | % obsolete |
| 532 | | obsolete_eclipse_preference('EXPAND_CLOSURES_FOR_STATE'). |
| 533 | | obsolete_eclipse_preference('BOOL_AS_PREDICATE'). |
| 534 | | obsolete_eclipse_preference('BPARSER'). |
| 535 | | obsolete_eclipse_preference('DOT_LEAVES'). |
| 536 | | obsolete_eclipse_preference('PROB2_TRACE_FILE'). |
| 537 | | obsolete_eclipse_preference('PROB2_TRACE_FILE_UNIQUE'). |
| 538 | | obsolete_eclipse_preference('SFDP'). |
| 539 | | obsolete_eclipse_preference('SHOW_FULL_ERROR_LOCATIONS'). |
| 540 | | obsolete_eclipse_preference('WARN_WHEN_EXPANDING_INFINITE_CLOSURES'). |
| 541 | | |
| 542 | | |
| 543 | | deprecated_eclipse_preference('KODKOD',bool,use_solver_on_load,[true/kodkod,false/prob]). % try_kodkod_on_load |
| 544 | | |
| 545 | | |
| 546 | | |
| 547 | | print_eclipse_prefs :- findall(X,eclipse_preference(X,_),Xs), sort(Xs,SXs), |
| 548 | | length(SXs,Len), |
| 549 | | format('VALUE and DESCRIPTION of ~w ProB PREFERENCES~n FORMAT:~n',[Len]), |
| 550 | | format(' ~w = ~w~w : ~w ==> ~w~n',['PREFERENCE','CurrentValue','(*)','Type','Description']), |
| 551 | | format(' * indicates current value does not correspond to default.~n',[]), |
| 552 | | member(X,SXs), |
| 553 | | eclipse_preference(X,P), |
| 554 | | preference_val_type(P,VT), |
| 555 | | preference_description(P,Desc), |
| 556 | | preference(P,Val), |
| 557 | | preference_default_value(P,Def), |
| 558 | | (Def=Val -> Info = '' ; Info = ' *'), |
| 559 | | format(' ~w = ~w~w : ~w ==> ~w~n',[X,Val,Info,VT,Desc]), |
| 560 | | fail. |
| 561 | | print_eclipse_prefs :- |
| 562 | | format('DESCRIPTION of ProB PREFERENCE GROUPS:~n',[]), |
| 563 | | preference_group_description(Group,Desc), |
| 564 | | findall(Setting,preference_group_val(Group,Setting,_,_),S), |
| 565 | | sort(S,Sorted), |
| 566 | | format(' * PREFERENCE GROUP ~w : SETTINGS ~w : ~w~n',[Group,Sorted,Desc]), |
| 567 | | fail. |
| 568 | | print_eclipse_prefs. |
| 569 | | |
| 570 | | |
| 571 | | :- dynamic preference/2. |
| 572 | | |
| 573 | | % add clause in case init_preferences forgotten |
| 574 | | preference(A,B) :- format(user_error,'Preferences not initalised (~w,~w)',[A,B]), |
| 575 | | init_preferences,!, preference(A,B). |
| 576 | | %add_internal_error('Preferences not initialised: ',preference(A,B)),fail. |
| 577 | | |
| 578 | | |
| 579 | | % ------------------ |
| 580 | | |
| 581 | | preference_default_value(maxint,3). % 2147483647 |
| 582 | | preference_default_value(minint,-1). %-2147483648 |
| 583 | | preference_default_value(number_animated_abstractions, 20). |
| 584 | | preference_default_value(number_skipped_refined_machines, 0). |
| 585 | | preference_default_value(globalsets_fdrange,2). |
| 586 | | preference_default_value(do_invariant_checking,true). |
| 587 | | preference_default_value(do_assert_checking,true). |
| 588 | | %preference_default_value(do_full_invariant_checking,true). |
| 589 | | %preference_default_value(use_new_kernel,false). |
| 590 | | preference_default_value(find_abort_values,false). |
| 591 | | preference_default_value(raise_abort_immediately,false). |
| 592 | | preference_default_value(treat_outermost_pre_as_select,true). |
| 593 | | preference_default_value(require_operations_to_assign_all_outputs,false). |
| 594 | | preference_default_value(allow_operations_to_read_outputs,false). |
| 595 | | preference_default_value(allow_operation_calls_for_uses,false). |
| 596 | | preference_default_value(allow_overriding_initialisation,false). |
| 597 | | preference_default_value(allow_simultaneous_assignments,false). |
| 598 | | preference_default_value(allow_arith_operators_on_reals,default). |
| 599 | | preference_default_value(solver_for_reals,precise_float_solver). |
| 600 | | preference_default_value(cspm_animate_all_processes_without_arguments,false). |
| 601 | | preference_default_value(cspm_animate_all_processes,false). |
| 602 | | %preference_default_value(cspm_display_inout,false). |
| 603 | | preference_default_value(cspm_detailed_animation,false). |
| 604 | | preference_default_value(cspm_strip_source_location,false). |
| 605 | | %preference_default_value(csp_event_visible_to_user,false). |
| 606 | | %preference_default_value(cspm_allow_incomplete_records,false). |
| 607 | | %preference_default_value(findOnlyOneSol,false). |
| 608 | | preference_default_value(maxNrOfInitialisations,4). |
| 609 | | preference_default_value(randomisedRestartInitalisations,false). |
| 610 | | preference_default_value(maxNrOfEnablingsPerOperation,10). |
| 611 | | preference_default_value(time_out,2500). |
| 612 | | preference_default_value(debug_time_out_factor,5). |
| 613 | | %preference_default_value(use_large_jvm_for_parser,false). |
| 614 | | preference_default_value(jvm_parser_heap_size_mb,0). |
| 615 | | preference_default_value(jvm_parser_additional_args,''). |
| 616 | | preference_default_value(jvm_parser_position_infos,true). |
| 617 | | preference_default_value(jvm_parser_fastrw,false). |
| 618 | | preference_default_value(jvm_parser_force_parsing,false). |
| 619 | | preference_default_value(show_initialisation_arguments,true). |
| 620 | | preference_default_value(deterministic_trace_replay,false). |
| 621 | | %preference_default_value(animate_skip_operations,true). |
| 622 | | preference_default_value(show_eventb_any_arguments,false). |
| 623 | | preference_default_value(convert_comprehension_sets_into_closures,false). /* <------------ was true */ |
| 624 | | preference_default_value(comprehension_set_symbolic_limit,20000). |
| 625 | | preference_default_value(use_clpfd_solver,true). % Default was changed from false to true on November 28 2013; commit d26b1bf1edeb29d630cf798c0773bfa1ba71219b |
| 626 | | preference_default_value(clpfd_solver_label_option,ffc). |
| 627 | | preference_default_value(use_chr_solver,false). |
| 628 | | preference_default_value(data_validation_mode,false). |
| 629 | | preference_default_value(use_smt_mode,false). |
| 630 | | preference_default_value(solver_strength,0). |
| 631 | | preference_default_value(remove_implied_constraints,false). |
| 632 | | preference_default_value(lift_existential_quantifiers,false). |
| 633 | | preference_default_value(use_common_subexpression_elimination,false). % CSE |
| 634 | | preference_default_value(use_common_subexpression_also_for_predicates,true). % CSE_PRED |
| 635 | | preference_default_value(use_common_subexpression_also_for_substitutions,false). % CSE_SUBST |
| 636 | | preference_default_value(use_common_subexpression_wd_only,false). % CSE_WD_ONLY |
| 637 | | preference_default_value(normalize_ast,false). % NORMALIZE_AST |
| 638 | | preference_default_value(normalize_ast_sort_commutative,false). |
| 639 | | preference_default_value(optimize_ast,true). % OPTIMIZE_AST |
| 640 | | %preference_default_value(optimize_enum_set_elems,false). |
| 641 | | preference_default_value(useless_code_elimination,false). % see test 1660 |
| 642 | | preference_default_value(compile_while_body,true). % COMPILE_WHILE |
| 643 | | preference_default_value(expand_becomes_such_into_set,false). % EXPAND_BECOMES_SUCH |
| 644 | | preference_default_value(detect_lambdas,true). % DETECT_LAMBDAS |
| 645 | | preference_default_value(auto_detect_theory_ops,false). % AUTO_DETECT_THEORY_MAPPING |
| 646 | | preference_default_value(ltsmin_guard_splitting,false). |
| 647 | | preference_default_value(ltsmin_do_not_evaluate_top_level_guards,false). |
| 648 | | preference_default_value(fail_if_clpfd_timeout,false). |
| 649 | | %preference_default_value(allow_recursive_closures,false). |
| 650 | | preference_default_value(use_static_ordering,false). |
| 651 | | preference_default_value(try_use_state_packing,auto). |
| 652 | | preference_default_value(use_state_packing,false). % computed |
| 653 | | preference_default_value(force_state_packing_for_closures,false). |
| 654 | | preference_default_value(provide_trace_information,false). |
| 655 | | :- if(environ(prob_profile,true)). |
| 656 | | preference_default_value(prob_profiling_on,true). |
| 657 | | :- else. |
| 658 | | preference_default_value(prob_profiling_on,false). |
| 659 | | :- endif. |
| 660 | | :- if(environ(prob_src_profile,true)). |
| 661 | | preference_default_value(prob_source_profiling_on,true). |
| 662 | | :- else. |
| 663 | | preference_default_value(prob_source_profiling_on,false). |
| 664 | | :- endif. |
| 665 | | preference_default_value(performance_monitoring_on,false). |
| 666 | | preference_default_value(performance_monitoring_expansion_limit,100). |
| 667 | | preference_default_value(partition_predicates,true). |
| 668 | | preference_default_value(partition_predicates_inline_equalities,true). |
| 669 | | preference_default_value(use_closure_expansion_memoization,false). |
| 670 | | preference_default_value(use_function_memoization,default). |
| 671 | | preference_default_value(allow_incomplete_partial_setup_constants,false). |
| 672 | | preference_default_value(re_execute_operations_with_side_effects,false). |
| 673 | | preference_default_value(warn_if_definition_hides_variable,true). |
| 674 | | preference_default_value(type_check_definitions,false). % can consume time, see test 778; and produces error messages for some tests |
| 675 | | %preference_default_value(warn_when_expanding_infinite_closures,5). |
| 676 | | preference_default_value(allow_enumeration_of_infinite_types,true). |
| 677 | | 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 |
| 678 | | preference_default_value(strict_raise_enum_warnings,false). |
| 679 | | preference_default_value(clash_strict_checks,false). |
| 680 | | preference_default_value(perform_stricter_static_checks,false). |
| 681 | | preference_default_value(ignore_prj_types,false). |
| 682 | | %preference_default_value(never_convert_closures_into_explicit_form,false). |
| 683 | | %preference_default_value(convert_types_into_closures,true). |
| 684 | | %preference_default_value(convert_closures_into_explicit_form_for_store,true). % <--- maybe remove preference |
| 685 | | %preference_default_value(allow_empty_global_sets,false). |
| 686 | | %preference_default_value(test_case_gen_stop_at_first_error,false). |
| 687 | | preference_default_value(prefix_internal_operation_arguments,'$none'). %all operations arguments are external and shown in testcases |
| 688 | | preference_default_value(generate_minimal_nr_of_testcases,true). |
| 689 | | preference_default_value(use_tk_custom_state_viewer,true). |
| 690 | | preference_default_value(tk_custom_state_viewer_font_name,''). |
| 691 | | preference_default_value(tk_custom_state_viewer_font_size,0). |
| 692 | | preference_default_value(tk_custom_state_viewer_padding,0). |
| 693 | | preference_default_value(tk_custom_state_viewer_str_padding,10). |
| 694 | | preference_default_value(use_small_window,false). |
| 695 | | preference_default_value(tk_show_source_pane,true). |
| 696 | | preference_default_value(ignore_hash_collisions,false). |
| 697 | | preference_default_value(forget_state_space,false). |
| 698 | | preference_default_value(store_only_one_incoming_transition,false). |
| 699 | | preference_default_value(mc_continue_after_error,false). |
| 700 | | %preference_default_value(enable_permutation_reducation,false). |
| 701 | | %preference_default_value(use_symmetry_marker_hash,false). |
| 702 | | %preference_default_value(enable_canonical_symmetry,false). |
| 703 | | %preference_default_value(use_nauty_symmetry_reduction,false). |
| 704 | | preference_default_value(symmetry_mode,off). |
| 705 | | preference_default_value(use_static_symmetry_detection,true). |
| 706 | | %preference_default_value(bool_expression_as_predicate,false). |
| 707 | | preference_default_value(allow_untyped_identifiers,false). |
| 708 | | preference_default_value(repl_unicode,false). |
| 709 | | preference_default_value(repl_cache_parsing,false). |
| 710 | | preference_default_value(cache_constants,true). |
| 711 | | preference_default_value(cache_operations,true). |
| 712 | | preference_default_value(cache_operations_runtime_limit,0). |
| 713 | | preference_default_value(latex_encoding,auto). |
| 714 | | preference_default_value(latex_pp_greek_ids,false). |
| 715 | | preference_default_value(xml_encoding,auto). |
| 716 | | preference_default_value(view_probcli_errors_using_bbresults,false). |
| 717 | | preference_default_value(eventtrace,false). |
| 718 | | preference_default_value(store_event_transinfo,false). |
| 719 | | preference_default_value(use_solver_on_load,prob). |
| 720 | | %preference_default_value(try_kodkod_on_load,false). |
| 721 | | preference_default_value(kodkod_for_components,true). |
| 722 | | preference_default_value(kodkod_raise_warnings,false). |
| 723 | | preference_default_value(kodkod_max_nr_solutions,22). |
| 724 | | preference_default_value(kodkod_symmetry_level,0). |
| 725 | | preference_default_value(kodkod_sat_solver,sat4j). |
| 726 | | preference_default_value(smt_supported_interpreter,false). |
| 727 | | preference_default_value(sat_supported_interpreter,false). |
| 728 | | preference_default_value(use_record_construction,true). % was false |
| 729 | | preference_default_value(seen_machines_included,false). |
| 730 | | preference_default_value(allow_sequence_operators_on_strings,true). |
| 731 | | |
| 732 | | preference_default_value(dot_print_edge_labels,true). |
| 733 | | preference_default_value(dot_print_action_arguments,true). |
| 734 | | preference_default_value(dot_print_functions,false). |
| 735 | | preference_default_value(dot_print_self_loops,true). |
| 736 | | preference_default_value(dot_print_arc_colors,true). |
| 737 | | preference_default_value(dot_print_root,true). |
| 738 | | %preference_default_value(dot_print_leaves,true). |
| 739 | | preference_default_value(dot_print_node_ids,false). |
| 740 | | preference_default_value(dot_print_transition_ids,false). |
| 741 | | preference_default_value(dot_print_use_constants,true). |
| 742 | | preference_default_value(dot_print_node_info,true). |
| 743 | | preference_default_value(dot_use_ps_viewer,PS) :- host_platform(X), |
| 744 | | (X = darwin -> PS = true % on recent macOS platforms all GraphViz Dotty viewers seem broken |
| 745 | | ; X=windows -> PS = true % GraphViz no longer seems to distribute the Dotty viewer |
| 746 | | ; PS=false). |
| 747 | | preference_default_value(path_to_dot,Path) :- try_get_program_path('dot',Path). |
| 748 | | preference_default_value(dot_default_engine,dot). |
| 749 | | preference_default_value(path_to_dotty,VIEWER) :- (possible_program(dot_viewer,E) -> VIEWER=E ; VIEWER ='dotty'). |
| 750 | | %preference_default_value(path_to_dotty,'/Applications/OmniGraffle/OmniGraffle.app/Contents/MacOS/OmniGraffle'). |
| 751 | | 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 |
| 752 | | preference_default_value(path_to_ps_viewer,VIEWER) :- |
| 753 | | (possible_program(pdf_viewer,E) -> VIEWER=E ; VIEWER ='gv'). |
| 754 | | preference_default_value(path_to_latex,Path) :- try_get_program_path('pdflatex',Path). |
| 755 | | %preference_default_value(path_to_ps_viewer,'open -a /Applications/Preview.app') :- host_platform(darwin). |
| 756 | | %preference_default_value(path_to_ps_viewer,'C:/Program Files/Ghostgum/gsview/gsview32') :- host_platform(windows). |
| 757 | | %preference_default_value(path_to_ps_viewer,'gv') :- host_platform(linux) ; host_platform(unknown). |
| 758 | | %preference_default_value(path_to_ps_viewer,'open -a /Applications/MacGhostViewX_Folder/MacGhostViewX.app'). |
| 759 | | preference_default_value(dot_root_shape,invtriangle). |
| 760 | | preference_default_value(dot_node_penwidth,2). |
| 761 | | preference_default_value(dot_edge_penwidth,1). |
| 762 | | preference_default_value(dot_normal_node_shape,box). % egg,ellipse |
| 763 | | preference_default_value(dot_current_node_shape,doubleoctagon). |
| 764 | | preference_default_value(dot_open_node_colour,'#F4E3C1'). %'#E88C59' '#C96D37' |
| 765 | | preference_default_value(dot_scope_limit_node_colour,gray). |
| 766 | | preference_default_value(dot_normal_node_colour,'#99BF38'). |
| 767 | | preference_default_value(dot_invariant_violated_node_colour,'#FF3800'). %'#FF4409' |
| 768 | | preference_default_value(dot_fill_normal_nodes,false). |
| 769 | | preference_default_value(dot_normal_arc_colour,'#006391'). |
| 770 | | preference_default_value(dot_node_font_size,12). |
| 771 | | preference_default_value(dot_edge_font_size,12). |
| 772 | | preference_default_value(dot_with_page_size,true). |
| 773 | | preference_default_value(dot_horizontal_layout,false). |
| 774 | | preference_default_value(dot_colour_goal_nodes,true). |
| 775 | | preference_default_value(dot_goal_node_colour,orange). |
| 776 | | preference_default_value(dot_print_node_properties,false). |
| 777 | | preference_default_value(dot_counterexample_node_colour,brown). |
| 778 | | preference_default_value(dot_counterexample_op_colour,brown). |
| 779 | | preference_default_value(dot_hierarchy_max_ids,0). |
| 780 | | preference_default_value(cbc_provide_explanations,false). |
| 781 | | |
| 782 | | preference_default_value(successful_rule_colour,'#4caf504d'). |
| 783 | | preference_default_value(failed_rule_colour,'#cc2f274d'). |
| 784 | | preference_default_value(disabled_rule_colour,lightgray). |
| 785 | | preference_default_value(not_checked_rule_colour,white). |
| 786 | | preference_default_value(rule_graph_shape,ellipse). |
| 787 | | preference_default_value(executed_computation_colour,'#4caf504d'). |
| 788 | | preference_default_value(not_executed_computation_colour,white). |
| 789 | | preference_default_value(disabled_computation_colour,lightgray). |
| 790 | | preference_default_value(computation_graph_shape,rectangle). |
| 791 | | preference_default_value(succeeded_dependency_colour,'#4caf50'). |
| 792 | | preference_default_value(failed_dependency_colour,'#cc2f27'). |
| 793 | | preference_default_value(normal_dependency_colour,black). |
| 794 | | |
| 795 | | preference_default_value(dot_event_hierarchy_horizontal,true). |
| 796 | | preference_default_value(dot_event_hierarchy_machine_colour,gray95). |
| 797 | | preference_default_value(dot_event_hierarchy_refines_colour,'#C0A060'). % Dark Khaki; see http://www.gpeters.com/color/color-schemes.php?search_term=Art+Nouveau |
| 798 | | preference_default_value(dot_event_hierarchy_new_event_colour,'#C06040'). % Coral '#C08040'). % Peru |
| 799 | | preference_default_value(dot_event_hierarchy_rename_event_colour,'#E0E0A0'). % Pale Goldenrod |
| 800 | | preference_default_value(dot_event_hierarchy_rename_unchanged_event_colour,'#E0F0E0'). % Honeydew |
| 801 | | preference_default_value(dot_event_hierarchy_unchanged_event_colour,gray92). |
| 802 | | preference_default_value(dot_event_hierarchy_grd_strengthening_event_colour,gray83). |
| 803 | | preference_default_value(dot_event_hierarchy_grd_keeping_event_colour,'#E0C080'). % Burlywood |
| 804 | | preference_default_value(dot_event_hierarchy_edge_colour,'#806040'). % Sienna |
| 805 | | preference_default_value(dot_event_hierarchy_extends_colour,gray50). |
| 806 | | preference_default_value(dot_hierarchy_show_extra_detail,false). |
| 807 | | |
| 808 | | preference_default_value(dot_projection_non_det_edge_colour,'#806040'). % Sienna; alternative :#A06040 Light Salmon |
| 809 | | preference_default_value(dot_projection_det_edge_colour,black). |
| 810 | | preference_default_value(dot_projection_non_definite_edge_style,dashed). |
| 811 | | preference_default_value(dot_projection_definite_edge_style,solid). |
| 812 | | preference_default_value(dot_projection_label_limit,75). |
| 813 | | preference_default_value(dot_projection_process_only_explored,false). |
| 814 | | preference_default_value(dot_use_unicode,true). |
| 815 | | preference_default_value(dot_predicate_node_shape,rect). |
| 816 | | preference_default_value(dot_expression_node_shape,record). |
| 817 | | preference_default_value(dot_var_mod_hide_only_written,false). |
| 818 | | |
| 819 | | |
| 820 | | preference_default_value(mc_dc_default_level,2). |
| 821 | | |
| 822 | | preference_default_value(dot_enabling_show_readwrites,true). |
| 823 | | |
| 824 | | preference_default_value(dot_definitions_use_sub_graph,true). |
| 825 | | preference_default_value(dot_definitions_show_all,false). |
| 826 | | preference_default_value(dot_state_graph_decompose,true). |
| 827 | | |
| 828 | | preference_default_value(font_size,'Monaco 12') :- host_platform(darwin). |
| 829 | | % Monaco looks better than Courier on Mac, Consolas |
| 830 | | % Note: ctext seems to use a non-monospaced font for TkFixedFont |
| 831 | | preference_default_value(font_size,'TkFixedFont 12') :- host_platform(X), X\==darwin. % alternative: Courier, Monaco, Consolas |
| 832 | | preference_default_value(font_name,'Monaco') :- host_platform(darwin). |
| 833 | | preference_default_value(font_name,'TkFixedFont') :- host_platform(X), X\==darwin. % alternative: Courier, Monaco |
| 834 | | preference_default_value(font_size_only,12). |
| 835 | | preference_default_value(use_font_size_for_columns,false). |
| 836 | | preference_default_value(allow_source_code_editing,true). |
| 837 | | preference_default_value(show_line_numbers,false). |
| 838 | | %preference_default_value(show_full_error_span,true). |
| 839 | | preference_default_value(highlight_brackets,true). |
| 840 | | preference_default_value(highlight_current_line,true). |
| 841 | | preference_default_value(ask_when_content_changed,false). |
| 842 | | preference_default_value(user_not_beginner,false). |
| 843 | | preference_default_value(user_is_an_expert_with_accessto_source_distribution,false). |
| 844 | | %preference_default_value(default_to_runtime_type_checking_on_startup_for_expert,false). |
| 845 | | preference_default_value(path_to_probe,'C:/probe/probe-1.30-windows/probe.exe') :- host_platform(windows). |
| 846 | | preference_default_value(path_to_probe,'more') :- host_platform(X), X\==windows. |
| 847 | | preference_default_value(path_to_spin,'xspin'). |
| 848 | | preference_default_value(path_to_cspm,'/usr/bin/cspm'). |
| 849 | | preference_default_value(path_to_text_editor,EDITOR) :- |
| 850 | | (possible_program(editor,E) -> EDITOR=E ; EDITOR =''). |
| 851 | | preference_default_value(path_to_text_editor_launch,EDITOR) :- |
| 852 | | (possible_program(editor_launch,E) -> EDITOR=E ; EDITOR ='vi'). |
| 853 | | %preference_default_value(path_to_fuzz,'fuzz'). |
| 854 | | preference_default_value(path_to_fdr,'fdr2'). |
| 855 | | preference_default_value(path_to_csp_typechecker,FDR3) :- |
| 856 | | (possible_program(fdr3,E) -> FDR3=E ; FDR3 ='refines'). |
| 857 | | preference_default_value(path_to_bcomp,'bcomp'). |
| 858 | | preference_default_value(path_to_atb_krt,Default) :- try_get_program_path('krt',Default). |
| 859 | | preference_default_value(path_to_java,Default) :- try_get_program_path('java',Default). |
| 860 | | preference_default_value(path_to_java_parser,''). % use default probcliparser.jar in lib folder |
| 861 | | preference_default_value(try_atb_provers,false). |
| 862 | | preference_default_value(smtlib2b_arrays_as_sets,false). |
| 863 | | preference_default_value(smtlib2b_cleanup_predicate,false). |
| 864 | | preference_default_value(symbolic_mc_try_other_solvers,false). |
| 865 | | preference_default_value(ltl_to_ba_tool,'lib/ltl2ba'). |
| 866 | | preference_default_value(path_to_clingo,Default) :- try_get_program_path(clingo,Default). |
| 867 | | |
| 868 | | preference_default_value(number_of_recent_documents,25). |
| 869 | | preference_default_value(number_of_searched_patterns,9). |
| 870 | | preference_default_value(number_of_replaced_patterns,9). |
| 871 | | preference_default_value(number_of_eval_history_elements,50). |
| 872 | | preference_default_value(number_of_eval_csp_history_elements,50). |
| 873 | | preference_default_value(number_of_checked_ltl_formulas,20). |
| 874 | | |
| 875 | | preference_default_value(do_syntax_highlighting,true). |
| 876 | | preference_default_value(sh_type_colour,darkred). |
| 877 | | preference_default_value(sh_logical_colour,tomato). |
| 878 | | preference_default_value(sh_assignments_colour,darkslateblue). |
| 879 | | preference_default_value(sh_operators,'#5883be'). |
| 880 | | preference_default_value(sh_top_level_keywords,blue). |
| 881 | | preference_default_value(sh_control_keywords,darkviolet). |
| 882 | | %preference_default_value(sh_includes_keywords,darkslateblue). |
| 883 | | preference_default_value(sh_comments,'#784e50'). |
| 884 | | preference_default_value(sh_pragmas,'#5b5b5b'). |
| 885 | | preference_default_value(sh_unsupported_background,yellow). |
| 886 | | |
| 887 | | preference_default_value(expand_forall_upto,100). |
| 888 | | preference_default_value(double_evaluation_when_analysing,true). |
| 889 | | :- if(environ(prob_safe_mode,true)). |
| 890 | | preference_default_value(prob_safe_mode,true). |
| 891 | | :- else. |
| 892 | | preference_default_value(prob_safe_mode,false). |
| 893 | | :- endif. |
| 894 | | preference_default_value(expand_avl_upto,100). |
| 895 | | preference_default_value(show_bvisual_formula_explanations,false). |
| 896 | | preference_default_value(show_bvisual_formula_functor_from,Val) :- |
| 897 | | (get_prob_application_type(tcltk) -> Val=0 ; Val = -1). % disable for ProB2 |
| 898 | | preference_default_value(show_bvisual_proof_info_icons,Val) :- |
| 899 | | (get_prob_application_type(tcltk) -> Val=true ; Val = false). % disable for ProB2 |
| 900 | | preference_default_value(formula_tree_minimal_timeout,1000). |
| 901 | | preference_default_value(formula_tree_maximal_timeout,30000). |
| 902 | | preference_default_value(show_function_tuples_in_property,true). |
| 903 | | preference_default_value(bugly_pp_scrambling,false). |
| 904 | | preference_default_value(pp_propositional_logic_mode,false). |
| 905 | | preference_default_value(pp_wd_infos,false). |
| 906 | | preference_default_value(pp_with_terminal_colour,false). |
| 907 | | preference_default_value(wd_ignore_external_funs,false). |
| 908 | | preference_default_value(wd_skip_finite_pos,false). |
| 909 | | preference_default_value(wd_analysis_for_animation,true). |
| 910 | | preference_default_value(z3_solve_for_animation,true). |
| 911 | | preference_default_value(add_wd_pos_for_z3,true). |
| 912 | | preference_default_value(do_not_print_wd_errors,false). |
| 913 | | |
| 914 | | preference_default_value(allow_new_ops_in_refinement,false). |
| 915 | | preference_default_value(allow_local_operation_calls,false). |
| 916 | | preference_default_value(allow_operation_calls_in_expr,false). |
| 917 | | preference_default_value(allow_let_to_reuse_introduced_ids,false). |
| 918 | | preference_default_value(use_po,true). |
| 919 | | preference_default_value(try_operation_reuse,auto). |
| 920 | | preference_default_value(try_operation_reuse_for_invariants,true). |
| 921 | | preference_default_value(operation_reuse_setting,false). |
| 922 | | preference_default_value(randomise_operation_order,false). |
| 923 | | preference_default_value(randomise_enumeration_order,false). |
| 924 | | preference_default_value(perform_enumeration_order_analysis,true). |
| 925 | | preference_default_value(set_rand,false). |
| 926 | | preference_default_value(rand_seed,2342452). |
| 927 | | |
| 928 | | preference_default_value(use_cbc_analysis,true). |
| 929 | | preference_default_value(timeout_cbc_analysis,300). |
| 930 | | |
| 931 | | preference_default_value(use_scope_predicate,true). |
| 932 | | preference_default_value(use_ignore_pragmas,false). |
| 933 | | |
| 934 | | preference_default_value(alloy_use_implementable_integers,false). |
| 935 | | preference_default_value(alloy_scopeless_translation,false). |
| 936 | | preference_default_value(alloy_translation_for_proof,false). |
| 937 | | preference_default_value(alloy_strict_integers,true). |
| 938 | | |
| 939 | | %preference_default_value(pge,off). |
| 940 | | preference_default_value(por,off). |
| 941 | | preference_default_value(por_heur,random). |
| 942 | | preference_default_value(use_safety_ltl_model_checker,true). |
| 943 | | |
| 944 | | preference_default_value(enable_graph,false). |
| 945 | | preference_default_value(enable_graph_depth,1). |
| 946 | | |
| 947 | | preference_default_value(dependency_enable_predicates,false). |
| 948 | | |
| 949 | | preference_default_value(filter_unused_constants,false). |
| 950 | | preference_default_value(translate_force_all_typing_infos,false). |
| 951 | | preference_default_value(translate_print_typing_infos,false). |
| 952 | | preference_default_value(translate_print_frozen_infos,false). |
| 953 | | preference_default_value(translate_ids_to_parseable_format,false). |
| 954 | | preference_default_value(translate_suppress_rodin_positions_flag,false). |
| 955 | | preference_default_value(translate_print_all_sequences,false). |
| 956 | | preference_default_value(translate_print_cs_style_sequences,false). |
| 957 | | preference_default_value(translation_limit_for_table_commands,100). |
| 958 | | preference_default_value(visb_allow_variables_for_objects,Res) :- |
| 959 | | (prob_application_type(tcltk) -> Res=true ; Res=false). |
| 960 | | preference_default_value(visb_show_debug_infos,false). |
| 961 | | |
| 962 | | preference_default_value(trace_generation_limit,100). |
| 963 | | preference_default_value(trace_generation_time_out,2147483646). % disabled |
| 964 | | |
| 965 | | /* Disprover mode - deactivates some optimizations only valid for animation */ |
| 966 | | preference_default_value(disprover_mode,false). |
| 967 | | preference_default_value(allow_improving_wd_mode,false). |
| 968 | | preference_default_value(trace_upon_error,false). |
| 969 | | preference_default_value(error_log_file,''). |
| 970 | | preference_default_value(tlc_number_of_workers,2). |
| 971 | | preference_default_value(tlc_use_prob_constant_setup,false). |
| 972 | | preference_default_value(unsat_core_algorithm,linear_greedy). |
| 973 | | |
| 974 | | preference_default_value(port, 6000). % on macOS Monterey 5000 and 7000 are now used by control center |
| 975 | | preference_default_value(ip, localhost). |
| 976 | | preference_default_value(max_states, 0). |
| 977 | | preference_default_value(tmpdir, '/tmp/'). |
| 978 | | preference_default_value(logdir, './distb-logs/'). |
| 979 | | preference_default_value(proxynumber, 0). |
| 980 | | preference_default_value(queue_threshold, 20). /* TODO: this is not used an implemented in the proxy (pk, 12.01.18) */ |
| 981 | | preference_default_value(hash_cycle, 25). |
| 982 | | preference_default_value(cdclt_perform_static_analysis, true). |
| 983 | | preference_default_value(cdclt_perform_symmetry_breaking, false). |
| 984 | | preference_default_value(cdclt_use_idl_theory_solver, false). |
| 985 | | preference_default_value(prob_version_info,Version) :- version_str(Version). |
| 986 | | preference_default_value(prob_revision_info,Rev) :- revision(Rev). |
| 987 | | preference_default_value(prob_lastchangedate_info,D) :- lastchangeddate(D). |
| 988 | | |
| 989 | | preference_default_value(xtl_safe_mode,false). |
| 990 | | |
| 991 | | preference_default_value(machines_path,Dir) :- |
| 992 | | catch(absolute_file_name(examples('.'),Dir),_,Dir='.'). |
| 993 | | |
| 994 | | |
| 995 | | |
| 996 | | :- use_module(library(file_systems),[file_exists/1,directory_exists/1]). |
| 997 | | try_get_program_path(Name,Path) :- |
| 998 | | (possible_program(Name,R) -> Path=R |
| 999 | | ; Path=Name). % hope in PATH |
| 1000 | ? | possible_program(Type,E) :- host_platform(P),possible_program_aux(Type,P,E), |
| 1001 | | %format('Trying program ~w for ~w on platform ~w.~n',[E,Type,P]), |
| 1002 | | (file_exists(E) -> true ; P=darwin, directory_exists(E)). |
| 1003 | | %format('Found program ~w for ~w on platform ~w.~n',[E,Type,P]). |
| 1004 | | |
| 1005 | | :-use_module(library(system),[environ/2]). |
| 1006 | | possible_program_aux(editor_launch,darwin,'/usr/local/bin/bbedit'). |
| 1007 | | possible_program_aux(editor_launch,darwin,'/usr/local/bin/edit'). % Text Wrangler |
| 1008 | | possible_program_aux(editor_launch,_,PATH) :- environ('EDITOR',PATH). |
| 1009 | | possible_program_aux(editor_launch,darwin,'/usr/local/bin/atom'). |
| 1010 | | possible_program_aux(editor_launch,linux,'/usr/local/bin/atom'). |
| 1011 | | possible_program_aux(editor_launch,linux,'/usr/bin/kwrite'). |
| 1012 | | possible_program_aux(editor_launch,linux,'/usr/bin/gedit'). |
| 1013 | | possible_program_aux(editor_launch,linux,'/usr/bin/vim'). |
| 1014 | | possible_program_aux(editor,darwin,'/Applications/BBEdit.app'). |
| 1015 | | possible_program_aux(editor,darwin,'/Applications/TextWrangler.app'). |
| 1016 | | possible_program_aux(editor,darwin,'/Applications/Atom.app'). |
| 1017 | | possible_program_aux(editor,darwin,'/Applications/Sublime Text 2.app'). |
| 1018 | | possible_program_aux(editor,darwin,'/Applications/TextMate.app'). |
| 1019 | | possible_program_aux(editor,darwin,'/Applications/TextEdit.app'). |
| 1020 | | 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 |
| 1021 | | possible_program_aux(pdf_viewer,darwin,'/Applications/Preview.app') :- prob_application_type(tcltk). % probcli cannot use open -a yet. |
| 1022 | | possible_program_aux(pdf_viewer,darwin,'/usr/bin/open'). |
| 1023 | | possible_program_aux(pdf_viewer,linux,'/usr/bin/okular'). % KDE |
| 1024 | | possible_program_aux(pdf_viewer,linux,'/usr/bin/evince'). % GNOME |
| 1025 | | possible_program_aux(pdf_viewer,windows,'C:/Program Files/Ghostgum/gsview/gsview32'). |
| 1026 | | possible_program_aux(dot_viewer,darwin,'/Applications/MacPorts/Graphviz.app') :- % only version that seems to run on mac |
| 1027 | | % sudo port install graphviz-gui (see https://ports.macports.org/port/graphviz-gui/) |
| 1028 | | prob_application_type(tcltk). |
| 1029 | | possible_program_aux(dot_viewer,darwin,'/Applications/Graphviz.app') :- prob_application_type(tcltk). % probcli cannot use open -a yet |
| 1030 | | possible_program_aux(dot_viewer,darwin,'/Applications/OmniGraffle.app') :- prob_application_type(tcltk). |
| 1031 | | possible_program_aux(dot_viewer,darwin,'/Applications/Visual Studio Code.app') :- |
| 1032 | | % using Graphviz Interactive Preview extension |
| 1033 | | prob_application_type(tcltk). |
| 1034 | | possible_program_aux(dot_viewer,darwin,'/usr/bin/open'). |
| 1035 | | possible_program_aux(dot_viewer,windows,'C:/Program Files/Graphviz2.38/bin/dotty.exe'). |
| 1036 | | possible_program_aux(dot_viewer,windows,'C:/Program Files (x86)/Graphviz2.38/bin/dotty.exe'). |
| 1037 | | possible_program_aux(krt,darwin,'/Applications/AtelierB.app/AB/bbin/macosx/krt'). |
| 1038 | | possible_program_aux(krt,darwin,'/Applications/atelierb-free-arm64-24.04.2.app/Contents/Resources/bin/krt'). |
| 1039 | | %possible_program_aux(krt,darwin,'/Applications/atelierb-full-4.6.0-rc4.app/Contents/Resources/bbin/macosx/krt'). % set DYLD_VERSIONED_LIBRARY_PATH ? |
| 1040 | | possible_program_aux(java,windows,'C:/Program Files/Java/jre7/bin/java.exe'). |
| 1041 | | possible_program_aux(java,P,'/usr/bin/java') :- unix(P). |
| 1042 | | possible_program_aux(fdr3,darwin,'/Applications/FDR3.app/Contents/MacOS/refines'). |
| 1043 | | possible_program_aux(fdr3,darwin,'/Applications/FDR4.app/Contents/MacOS/refines'). |
| 1044 | | %possible_program_aux(sfdp,P,'/usr/local/bin/sfdp') :- unix(P). |
| 1045 | | possible_program_aux(dot,P,'/usr/local/bin/dot') :- unix(P). |
| 1046 | | possible_program_aux(dot,darwin,'/opt/homebrew/bin/dot'). % location of new homebrew on M1/Arm Macs |
| 1047 | | % full location is e.g. /opt/homebrew/Cellar/graphviz/8.0.1/bin/dot |
| 1048 | | possible_program_aux(dot,P,'/opt/local/bin/dot') :- unix(P). % e.g., location of MacPorts |
| 1049 | | possible_program_aux(dot,P,'/usr/bin/dot') :- P=linux. |
| 1050 | | possible_program_aux(pdflatex,P,'/usr/local/texlive/2016/bin/x86_64-darwin/pdflatex') :- P=darwin. |
| 1051 | | possible_program_aux(pdflatex,P,'/usr/local/texlive/2019/bin/x86_64-darwin/pdflatex') :- P=darwin. |
| 1052 | | possible_program_aux(pdflatex,P,'/usr/local/bin/pdflatex') :- unix(P). |
| 1053 | | possible_program_aux(pdflatex,P,'/opt/local/bin/pdflatex') :- unix(P). |
| 1054 | | possible_program_aux(open,darwin,'/usr/bin/open'). |
| 1055 | | possible_program_aux(open,linux,'xdg-open'). |
| 1056 | | possible_program_aux(open,windows,'start'). |
| 1057 | | possible_program_aux(clingo,darwin,'/opt/homebrew/bin/clingo'). |
| 1058 | | |
| 1059 | | |
| 1060 | | unix(darwin). |
| 1061 | | unix(linux). |
| 1062 | | |
| 1063 | | /* ------------------------- */ |
| 1064 | | |
| 1065 | | % now in basic_tests.pl |
| 1066 | | %:- assert_must_succeed( \+((preference_description(P,_D),\+preference_default_value(P,_Val)))). |
| 1067 | | %:- assert_must_succeed( \+((preference_default_value(P,_D), \+preference_description(P,_Val)))). |
| 1068 | | preference_description(maxNrOfInitialisations,'Max Number of Initialisations and Constant-Setups Computed'). |
| 1069 | | 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)'). |
| 1070 | | preference_description(maxNrOfEnablingsPerOperation,'Max Number of Enablings per Operation Computed'). |
| 1071 | | 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)'). |
| 1072 | | preference_description(globalsets_fdrange,'Size of unspecified deferred sets in SETS section'). |
| 1073 | | preference_description(maxint,Desc) :- |
| 1074 | | (get_prob_application_type(rodin) |
| 1075 | | -> Desc='maximum value for unbounded integer enumerations' |
| 1076 | | ; Desc='value of MAXINT, controls enumeration of integers and used to define NAT in classical B (2147483647 for 32 bit ints)'). |
| 1077 | | preference_description(minint,Desc) :- |
| 1078 | | (get_prob_application_type(rodin) |
| 1079 | | -> Desc='minimum value for unbounded integer enumerations' |
| 1080 | | ; 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 |
| 1081 | | preference_description(number_animated_abstractions,'How many levels of refined Event-B models are animated by default'). |
| 1082 | | preference_description(number_skipped_refined_machines,'How many levels of concrete Event-B refinements are skipped for animation'). |
| 1083 | | %preference_description(findOnlyOneSol,'Find only one solution per Operation or Initialisation'). |
| 1084 | | preference_description(debug_time_out_factor,'Debug Properties: Multiplying Factor for Timeout'). |
| 1085 | | %preference_description(use_large_jvm_for_parser,'Use large Heap and Stack size for Java Parser'). |
| 1086 | | preference_description(jvm_parser_heap_size_mb,'Heap size in MB for Java parser (-Xmx JVM option, 0 means default value)'). |
| 1087 | | preference_description(jvm_parser_additional_args,'Additional arguments sent to the JVM for the Java parser (e.g., "-XX:+UseG1GC -Xss5m")'). |
| 1088 | | 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)'). |
| 1089 | | preference_description(jvm_parser_fastrw,'Use binary (fastrw) format for .prob files for faster loading'). |
| 1090 | | preference_description(jvm_parser_force_parsing,'Always parse B machines even if .prob file is up-to-date'). |
| 1091 | | preference_description(do_invariant_checking,'Check invariant while animating and model checking'). |
| 1092 | | preference_description(do_assert_checking,'Check ASSERT statements while animating and model checking'). |
| 1093 | | %preference_description(do_neginvariant_checking,'Check negation of invariant'). |
| 1094 | | %preference_description(do_full_invariant_checking,'Check types when checking invariant'). |
| 1095 | | %preference_description(use_new_kernel,'Use new Kernel (only some basic operations supported, only fore PRE and INITs)'). |
| 1096 | | 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'). |
| 1097 | | 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)'). |
| 1098 | | preference_description(cspm_animate_all_processes,'Animate all CSP-M processes (also processes with arguments)'). |
| 1099 | | preference_description(cspm_animate_all_processes_without_arguments,'Animate all CSP-M processes without arguments (not just MAIN)'). |
| 1100 | | %preference_description(cspm_display_inout,'Display unsynchronised inputs/outputs as ?/!'). |
| 1101 | | preference_description(cspm_detailed_animation,'Provide more fine-grained source-location animation for CSP (can slow model checking down)'). |
| 1102 | | preference_description(cspm_strip_source_location,'Strip CSP source-location information (for RHS of processes, except for internal choice)'). |
| 1103 | | %preference_description(csp_event_visible_to_user,'Return the CSP event as visible event to the user (option only relevant for models in \'CSP || B\' mode).'). |
| 1104 | | %preference_description(cspm_allow_incomplete_records,'Allow construction of incomplete records (e.g., for Casper files)'). |
| 1105 | | preference_description(use_clpfd_solver,'Use CLP(FD) solver for B integers (restricts range to -2^28..2^28-1 on 32 bit machines)'). |
| 1106 | | preference_description(clpfd_solver_label_option,'CLP(FD) labeling option used: ffc (default), occurence, ff, leftmost, min, max, max_regret, dom_w_deg, anti_first_fail (see SICStus manual)'). |
| 1107 | | preference_description(use_chr_solver,'Use CHR based solver. Should speed up detection of unsolvable predicates, but might slow down solving in general.'). |
| 1108 | | preference_description(data_validation_mode,'Assume everything can be computed without constraint solving.'). |
| 1109 | | preference_description(convert_comprehension_sets_into_closures,'Lazy expansion of lambdas and set comprehensions (i.e., keep them symbolic by default even if smaller than SYMBOLIC_LIMIT)'). |
| 1110 | | preference_description(comprehension_set_symbolic_limit,'Limit for expanding comprehension sets (comprehension sets known to be larger than limit will be kept symbolic)'). |
| 1111 | | 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 |
| 1112 | | preference_description(solver_strength,'Strength of certain Solver propagations (0 is default)'). |
| 1113 | | preference_description(remove_implied_constraints,'Remove unnecessary constraints implied by other constraints'). |
| 1114 | | preference_description(lift_existential_quantifiers,'Lift existential quantifiers, i.e., treat existentially quantified variables like ordinary variables'). |
| 1115 | | preference_description(use_common_subexpression_elimination,'Enable CSE (Common Subexpression Elimination)'). |
| 1116 | | preference_description(use_common_subexpression_also_for_predicates,'Apply CSE (if enabled) also to predicates'). |
| 1117 | | preference_description(use_common_subexpression_also_for_substitutions,'Apply CSE (if enabled) also to substitutions (operation/event bodies) [EXPERIMENTAL]'). |
| 1118 | | preference_description(use_common_subexpression_wd_only,'Apply CSE (if enabled) only to well-defined sub-formulas'). |
| 1119 | | preference_description(normalize_ast,'Normalize AST before passing to ProB kernel (rewrites many B predicates into simpler form)'). |
| 1120 | | preference_description(normalize_ast_sort_commutative,'Sort commutative operators (useful with NORMALIZE_AST to try detect equivalent formulas)'). |
| 1121 | | preference_description(optimize_ast,'Optimize AST (Abstract Syntax Tree) before passing to ProB kernel (rewrites many B predicates into more efficient form)'). |
| 1122 | | %preference_description(optimize_enum_set_elems,'Optimize type checking and compilation of sets containing enumerated set elements; assumes enumerated set ids are not used as quantifier ids'). % in future this preference will disappear and ProB will do safe detection automatically |
| 1123 | | preference_description(useless_code_elimination,'Useless Code Elimination: try and find useless statements which have no influence on the result of an operation.'). |
| 1124 | | preference_description(compile_while_body,'Compile bodies of WHILE loops if variant large'). |
| 1125 | | preference_description(expand_becomes_such_into_set,'Convert becomes_such x:(Pred) into x::{x|Pred} (can be more efficient within complex statements)'). |
| 1126 | | preference_description(detect_lambdas,'Detect set comprehensions which can be rewritten into lambdas.'). |
| 1127 | | preference_description(auto_detect_theory_ops,'Try and detect mappings of Rodin axiomatic theory operators based on name.'). |
| 1128 | | 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'). |
| 1129 | | 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)'). |
| 1130 | | preference_description(fail_if_clpfd_timeout,'Assume failure if posting a CLP(FD) constraint times-out'). |
| 1131 | | %preference_description(allow_recursive_closures,'Lazy expansion of *Recursive* set Comprehensions and lambdas'). |
| 1132 | | preference_description(use_static_ordering,'Use static ordering to enumerate constants which occur in most PROPERTIES first'). % sort properties |
| 1133 | | preference_description(try_use_state_packing,'Use more aggressive COMPRESSION when storing states (false: off, true: compromise between speed and memory, full: preserve more memory, auto: use heuristic)'). |
| 1134 | | preference_description(use_state_packing,'Computed actual value of COMPRESSION preference'). |
| 1135 | | preference_description(force_state_packing_for_closures,'Use more aggressive COMPRESSION when storing states with symbolic closures'). % only has influence if use_state_packing is not already full |
| 1136 | | preference_description(provide_trace_information,'Provide various tracing information on the terminal/console.'). |
| 1137 | | preference_description(prob_profiling_on,'Keep track of ProB profiling information (e.g., for time spent in operations or memoized function calls)'). |
| 1138 | | preference_description(prob_source_profiling_on,'Keep track of ProB source profiling information (e.g., which parts of the B source code is covered)'). |
| 1139 | | preference_description(performance_monitoring_on,'Provide performance monitoring information on the terminal/console.'). |
| 1140 | | preference_description(performance_monitoring_expansion_limit,'Limit in ms for printing warnings when expanding comprehension sets in performance monitoring mode.'). |
| 1141 | | preference_description(partition_predicates,'Partition predicates (PROPERTIES) into components'). |
| 1142 | | preference_description(partition_predicates_inline_equalities,'Inline equalities when partitioning into components'). |
| 1143 | | preference_description(use_closure_expansion_memoization,'MEMOize expansions of set comprehensions and lambda abstractions.'). |
| 1144 | | preference_description(use_function_memoization,'MEMOIZE function applications of all functions defined in ABSTRACT_CONSTANTS (default means only memoize functions annotated /*@desc memo */).'). |
| 1145 | | preference_description(allow_incomplete_partial_setup_constants,'Allow ProB to proceed even if only part of the CONSTANTS have been found.'). |
| 1146 | | 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).'). |
| 1147 | | preference_description(warn_if_definition_hides_variable,'Warn if a DEFINITION hides a variable with the same name'). |
| 1148 | | preference_description(type_check_definitions,'Type check all visible DEFINITIONs (not just used ones)'). |
| 1149 | | %preference_description(warn_when_expanding_infinite_closures,'Warn when expanding infinite closures if MAXINT larger than: '). |
| 1150 | | preference_description(allow_enumeration_of_infinite_types,'Allow enumeration of infinite types'). |
| 1151 | | preference_description(strict_raise_warnings,'Treat warnings as errors (Warning: can generate spurious NOT-WELL-DEFINED messages).'). |
| 1152 | | preference_description(strict_raise_enum_warnings,'Treat ENUMERATION warnings (aka VIRTUAL TIME-OUTS) as errors (Warning: can generate spurious NOT-WELL-DEFINED messages).'). |
| 1153 | | preference_description(clash_strict_checks,'Do a stricter checking for name CLASHES in B machines'). |
| 1154 | | preference_description(perform_stricter_static_checks,'Perform stricter additional static checks on formulas (automatically set by ProB).'). |
| 1155 | | preference_description(ignore_prj_types,'Ignore types of prj1 and prj2 (i.e., prj1({1},{1})(2,3) is considered well-defined'). |
| 1156 | | |
| 1157 | | %preference_description(never_convert_closures_into_explicit_form,'Never convert closures back into explicit form (only use for debugging !)'). |
| 1158 | | %preference_description(convert_types_into_closures,'Lazy expansion of type expressions (POW,-->,...)'). |
| 1159 | | %preference_description(convert_closures_into_explicit_form_for_store,'Convert lazy form back into explicit form for Variables, Constants, Operation Arguments'). |
| 1160 | | %preference_description(allow_empty_global_sets,'Allow empty global SETs'). |
| 1161 | | %preference_description(test_case_gen_stop_at_first_error,'Stop at first error in test case generation'). |
| 1162 | | preference_description(prefix_internal_operation_arguments,'Prefix of internal operation arguments (these are not included in test cases)'). |
| 1163 | | preference_description(generate_minimal_nr_of_testcases,'Generate minimal suite of mcm testcases (and not one per event)'). |
| 1164 | | preference_description(use_tk_custom_state_viewer,'Use custom Tk viewer to represent state of B Machine'). |
| 1165 | | preference_description(tk_custom_state_viewer_font_name,'Font for animation strings (if empty, the editor font will be used)'). |
| 1166 | | preference_description(tk_custom_state_viewer_font_size,'Font size for animation strings (if 0, the editor font size will be used)'). |
| 1167 | | preference_description(tk_custom_state_viewer_padding,'Padding (in pixels) between images of custom TK state viewer'). |
| 1168 | | preference_description(tk_custom_state_viewer_str_padding,'Padding (in pixels) between strings of custom TK state viewer'). |
| 1169 | | preference_description(use_small_window,'Use a small main window for ProB (useful on small screens)'). |
| 1170 | | preference_description(tk_show_source_pane,'Show the B Source Code'). |
| 1171 | | preference_description(ignore_hash_collisions,'Ignore hash collisions in state space (if true not all states may be computed!)'). |
| 1172 | | preference_description(forget_state_space,'Do not remember state space (mainly useful in conjunction with IGNORE_HASH_COLLISIONS)'). |
| 1173 | | 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 |
| 1174 | | preference_description(mc_continue_after_error,'Continue model checking even after an error or goal has been found'). |
| 1175 | | %preference_description(enable_permutation_reducation,'Enable Permutation Flooding'). |
| 1176 | | %preference_description(use_symmetry_marker_hash,'Use Symmetry Hash Marker'). |
| 1177 | | %preference_description(enable_canonical_symmetry,'Enable Symmetry Reduction by Canonical Form Computation'). |
| 1178 | | %preference_description(use_nauty_symmetry_reduction,'Use Nauty ((c) McKay) C Library for Symmetry Reduction with Canonical Form Computation'). |
| 1179 | | preference_description(symmetry_mode,'Symmetry Mode: off,flood,canon,nauty,hash'). |
| 1180 | | preference_description(use_static_symmetry_detection,'Detect symmetries in forall/exists and in PROPERTIES for deferred sets'). |
| 1181 | | %preference_description(bool_expression_as_predicate,'Extended Predicate Syntax (allow p&q as syntactic sugar for (p=TRUE) & (q=TRUE), only possible in REPL and DEPRECATED)' ). |
| 1182 | | preference_description(allow_untyped_identifiers,'Allow UNTYPED identifiers (they will be assigned new deferred sets as type)' ). |
| 1183 | | preference_description(repl_unicode,'Use UNICODE in REPL and editing window'). |
| 1184 | | preference_description(repl_cache_parsing,'Cache parsing in REPL (useful if same formula gets parsed multiple times, e.g., for Latex processing)'). |
| 1185 | | preference_description(cache_constants,'Cache constant values when -cache is activated'). % value_persistance |
| 1186 | | preference_description(cache_operations,'Cache operations/events when -cache is activated'). % ditto |
| 1187 | | preference_description(cache_operations_runtime_limit,'Minimal runtime for operations to be stored in -cache'). |
| 1188 | | preference_description(latex_encoding,'Encoding used for Latex processing with -latex (auto,ISO-8859-1,ISO-8859-2,UTF-8,UTF-16,...)'). |
| 1189 | | preference_description(latex_pp_greek_ids,'Prety-print Greek identifiers (Sigma,...) in Latex mode'). |
| 1190 | | preference_description(xml_encoding,'Encoding used for XML processing, e.g., with -logxml (auto,ISO-8859-1,ISO-8859-2,UTF-8,UTF-16,...)'). |
| 1191 | | preference_description(view_probcli_errors_using_bbresults,'Show probcli errors using the BBEdit (11.6 or newer) bbresults command'). |
| 1192 | | |
| 1193 | | preference_description(eventtrace,'Store detailed trace for each execution of a Rodin event or classical B operation (may cause large memory requirement)'). % detailed info with guards, simulation errors, ... or path(.) for classical B |
| 1194 | | preference_description(store_event_transinfo,'Store information about parameters and abstract events for each execution of a Rodin event (may cause larger memory requirement)'). % just event(Name,Parameters) trace |
| 1195 | | preference_description(use_solver_on_load,'Use this solver for PROPERTIES when loading machines'). |
| 1196 | | %preference_description(try_kodkod_on_load,'Apply translation to KODKOD on PROPERTIES when loading machines'). |
| 1197 | | preference_description(kodkod_for_components,'Translate only complete components to KODKOD (false allows partial translations)'). % and full throws enumeration warning if translation fails |
| 1198 | | preference_description(kodkod_raise_warnings,'Raise WARNING when component or predicate cannot be translated to KODKOD'). |
| 1199 | | preference_description(kodkod_max_nr_solutions,'Maximum number of solutions computed and sent by KODKOD per batch.'). |
| 1200 | | 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'). |
| 1201 | | % from Kodkod API: If a non-symmetric solver is chosen for this.solver, this value controls the maximum length of the generated lex-leader symmetry breaking predicate. In general, the higher this value, the more symmetries will be broken. But setting the value too high may have the opposite effect and slow down the solving. The default value for this property is 20. |
| 1202 | | preference_description(kodkod_sat_solver,'SAT solver used for Kodkod (sat4j, minisat, lingeling, glucose)'). |
| 1203 | | preference_description(smt_supported_interpreter,'Use Z3 / CVC4 for predicates inside the B interpreter'). |
| 1204 | | preference_description(sat_supported_interpreter,'Use Kodkod for specific predicates inside the B interpreter'). |
| 1205 | | preference_description(use_record_construction,'Records: Check if axioms/properties describe a record pattern'). |
| 1206 | | preference_description(seen_machines_included,'Seen/used machines are included (no operations available) instead of extended'). |
| 1207 | | preference_description(allow_sequence_operators_on_strings,'Allow sequence operators (^) to be applied to STRINGs'). |
| 1208 | | preference_description(show_eventb_any_arguments,'Show top-level ANY variable values of B Operations without parameters as parameters'). |
| 1209 | | 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 |
| 1210 | | %preference_description(animate_skip_operations,'Animate operations which are skip or PRE C THEN skip'). |
| 1211 | | preference_description(deterministic_trace_replay,'Replay Traces without backtracking (to reduce memory consumption)'). |
| 1212 | | preference_description(treat_outermost_pre_as_select,'Treat outermost PRE as SELECT'). |
| 1213 | | preference_description(require_operations_to_assign_all_outputs,'Require operations to assign to all outputs'). |
| 1214 | | preference_description(allow_operations_to_read_outputs,'Allow B operations to read output parameters; output values will be initialised to default value in animator.'). |
| 1215 | | 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'). |
| 1216 | | preference_description(allow_overriding_initialisation,'Allow to override INITIALISATION of included/extended machines'). % useful when using EXTENDS to create animation instances |
| 1217 | | preference_description(allow_simultaneous_assignments,'Allow B operations to assign multiple times to same variable (ASM style)'). |
| 1218 | | preference_description(allow_arith_operators_on_reals,'Allow to use the REAL datatype'). |
| 1219 | | 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)'). |
| 1220 | | %preference_description(check_prolog_b_ast,'Check the abstract syntax tree for B machines'). |
| 1221 | | preference_description(dot_print_edge_labels,'Show edge labels (operation names) in state space'). |
| 1222 | | preference_description(dot_print_action_arguments,'Show operation arguments (when edge labels shown)'). |
| 1223 | | preference_description(dot_print_functions,'Show functions (operations that return values w/o changing state) in state space'). |
| 1224 | | preference_description(dot_print_self_loops,'Show self-loops in state space and other dot graphs'). |
| 1225 | | %preference_description(dot_print_leaves,'Print Leaves'). |
| 1226 | | preference_description(dot_print_arc_colors,'Colour the arcs (disable for import in OmniGraffle)'). |
| 1227 | | preference_description(dot_print_root,'Show root node in state space'). |
| 1228 | | preference_description(dot_print_node_ids,'Show internal state ids in state space'). |
| 1229 | | preference_description(dot_print_transition_ids,'Show transition ids in state space'). |
| 1230 | | preference_description(dot_print_node_info,'Show additional state information (values of variables)'). |
| 1231 | | preference_description(dot_print_use_constants,'Use constants for deferred set values if possible'). |
| 1232 | | preference_description(dot_use_ps_viewer,'Use PDF/Postscript Viewer for .dot files'). |
| 1233 | | preference_description(path_to_dot,'Path/Command for dot program (using "/" even on Windows. Try avoiding spaces in path)'). |
| 1234 | | preference_description(dot_default_engine,'Default layout engine used for dot (dot,neato,sfdp,fdp,twopi,circo)'). |
| 1235 | | preference_description(path_to_dotty,'Path/Command for viewer of .dot files (e.g., dotty)'). |
| 1236 | | %preference_description(path_to_sfdp,'Path/Command for sfdp program for dot files (using "/" even on Windows. Try avoiding spaces in path)'). |
| 1237 | | preference_description(path_to_ltsmin,'Path to LTSmin commands, such as prob2lts-sym for symbolic model checking (not available for Windows.)'). |
| 1238 | | preference_description(path_to_ps_viewer,'Path/Command for PDF/Postscript viewer'). |
| 1239 | | preference_description(path_to_latex,'Path/Command for Latex (pdflatex)'). |
| 1240 | | preference_description(dot_root_shape,'Shape for root node (invtriangle,triangle, ellipse, box, diamond,...)'). |
| 1241 | | preference_description(dot_normal_node_shape,'Shape for normal node'). |
| 1242 | | preference_description(dot_current_node_shape,'Shape for current node'). |
| 1243 | | 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'). |
| 1244 | | preference_description(dot_scope_limit_node_colour,'Colour for open, but uninteresting nodes (red,green,blue,gray,... or rgb hex #ff00ff)'). |
| 1245 | | preference_description(dot_normal_node_colour,'Colour for normal node'). |
| 1246 | | preference_description(dot_node_penwidth,'Pen width for nodes'). |
| 1247 | | preference_description(dot_edge_penwidth,'Pen width for edges'). |
| 1248 | | preference_description(dot_invariant_violated_node_colour,'Colour for invariant violation'). |
| 1249 | | preference_description(dot_fill_normal_nodes,'Fill normal nodes with color'). |
| 1250 | | preference_description(dot_normal_arc_colour,'Colour for normal arcs'). |
| 1251 | | preference_description(dot_node_font_size,'Font Size for Node labels'). |
| 1252 | | preference_description(dot_edge_font_size,'Font Size for Edge labels'). |
| 1253 | | preference_description(dot_with_page_size,'Limit page size by default (does not affect all dot graphs)'). |
| 1254 | | preference_description(dot_horizontal_layout,'Use horizontal layout by default (does not affect all dot graphs)'). |
| 1255 | | preference_description(dot_colour_goal_nodes,'Colour the nodes that satisfy the GOAL predicate'). |
| 1256 | | preference_description(dot_goal_node_colour,'Colour for nodes satisfying the GOAL predicate'). |
| 1257 | | preference_description(dot_print_node_properties,'Show properties of statespace node (useful for CSP models)'). |
| 1258 | | preference_description(dot_counterexample_node_colour,'Colour for counterexample nodes'). |
| 1259 | | preference_description(dot_counterexample_op_colour,'Colour for counterexample transitions'). |
| 1260 | | preference_description(dot_hierarchy_max_ids,'Max. number of identifiers shown in hierarchy view (-1 to show all)'). |
| 1261 | | preference_description(cbc_provide_explanations,'Provide explanations (unsat core,...) for some CBC commands'). |
| 1262 | | |
| 1263 | | preference_description(successful_rule_colour,'Colour of successful rules nodes'). |
| 1264 | | preference_description(failed_rule_colour,'Colour of failed rule nodes'). |
| 1265 | | preference_description(disabled_rule_colour,'Colour of disabled rule nodes'). |
| 1266 | | preference_description(not_checked_rule_colour,'Colour of not checked rule nodes'). |
| 1267 | | preference_description(rule_graph_shape,'Shape of rule nodes'). |
| 1268 | | preference_description(executed_computation_colour,'Colour of executed computation nodes'). |
| 1269 | | preference_description(not_executed_computation_colour,'Colour of not executed computation nodes'). |
| 1270 | | preference_description(disabled_computation_colour,'Colour of disabled computation nodes'). |
| 1271 | | preference_description(computation_graph_shape,'Shape of computation nodes'). |
| 1272 | | preference_description(succeeded_dependency_colour,'Colour of edges to succeeded dependencies'). |
| 1273 | | preference_description(failed_dependency_colour,'Colour of edges to failed dependencies'). |
| 1274 | | preference_description(normal_dependency_colour,'Colour of edges to executed dependencies'). |
| 1275 | | |
| 1276 | | preference_description(dot_event_hierarchy_horizontal,'Organize refinements horizontally'). |
| 1277 | | preference_description(dot_event_hierarchy_machine_colour,'Colour for machine event cluster'). |
| 1278 | | preference_description(dot_event_hierarchy_refines_colour,'Colour for events refining themselves (i.e., not renamed and modifying guard or action)'). |
| 1279 | | preference_description(dot_event_hierarchy_new_event_colour,'Colour for new events (not refining any event) or variables'). |
| 1280 | | preference_description(dot_event_hierarchy_rename_event_colour,'Colour for renamed events (with change in guard or action)'). |
| 1281 | | preference_description(dot_event_hierarchy_rename_unchanged_event_colour,'Colour for renamed unchanged events'). |
| 1282 | | preference_description(dot_event_hierarchy_unchanged_event_colour,'Colour for unchanged events (not renamed, no guards or actions added) or variables'). |
| 1283 | | preference_description(dot_event_hierarchy_grd_strengthening_event_colour,'Colour for events just adding a guard (not renamed, no actions added)'). |
| 1284 | | preference_description(dot_event_hierarchy_grd_keeping_event_colour,'Colour for events just changing an action (not renamed, keeping guard unchanged)'). |
| 1285 | | preference_description(dot_event_hierarchy_edge_colour,'Edge colour for refine relation'). |
| 1286 | | preference_description(dot_event_hierarchy_extends_colour,'Edge colour for extends relation'). |
| 1287 | | preference_description(dot_hierarchy_show_extra_detail,'Provide more details in hierarchy diagram (e.g., constants)'). |
| 1288 | | |
| 1289 | | preference_description(dot_projection_non_det_edge_colour,'Edge colour for deterministic edges'). |
| 1290 | | preference_description(dot_projection_det_edge_colour,'Edge colour for non-deterministic edges'). |
| 1291 | | preference_description(dot_projection_non_definite_edge_style,'Style for non-definite edges (solid,dashed,dotted,bold,invis)'). |
| 1292 | | preference_description(dot_projection_definite_edge_style,'Style for definite edges (solid,dashed,dotted,bold,invis)'). |
| 1293 | | preference_description(dot_projection_label_limit,'Max. nr of characters for node labels'). |
| 1294 | | preference_description(dot_projection_process_only_explored,'Project only on the explored nodes'). |
| 1295 | | preference_description(dot_use_unicode,'Use Unicode symbols for values and formulas'). |
| 1296 | | preference_description(dot_predicate_node_shape,'Shape for predicate nodes in formula trees'). |
| 1297 | | preference_description(dot_expression_node_shape,'Shape for expression nodes in formula trees'). |
| 1298 | | preference_description(dot_var_mod_hide_only_written,'Hide variables which are only written and not read in any guard'). |
| 1299 | | |
| 1300 | | |
| 1301 | | preference_description(mc_dc_default_level,'Default Predicate Expansion Level for MC/DC Coverage Analyses (0=no expansion, 1=only top level connective expanded,...)'). |
| 1302 | | |
| 1303 | | preference_description(dot_enabling_show_readwrites,'Show read/write info for enabling diagrams'). |
| 1304 | | |
| 1305 | | preference_description(dot_definitions_use_sub_graph,'Show expression-, predicate-, substitution-DEFINITIONS as sub-graphs'). |
| 1306 | | preference_description(dot_definitions_show_all,'Show all DEFINITIONS'). |
| 1307 | | preference_description(dot_state_graph_decompose,'Decompose sets and complex pairs into individual vertices'). |
| 1308 | | |
| 1309 | | preference_description(font_size,'Font size in main window'). |
| 1310 | | preference_description(font_name,'Font name in text editor'). |
| 1311 | | preference_description(font_size_only,'Font size in text editor'). |
| 1312 | | preference_description(use_font_size_for_columns,'Use font size also for columns (you need to reselect font size + Courier will be used)'). |
| 1313 | | preference_description(allow_source_code_editing,'Allow editing and saving of main B machine file'). |
| 1314 | | preference_description(show_line_numbers,'Show line numbers in main window'). |
| 1315 | | %preference_description(show_full_error_span,'Show also the end line and column in error messages'). |
| 1316 | | preference_description(highlight_brackets,'Highlights brackets'). |
| 1317 | | preference_description(highlight_current_line,'Highlights current line'). |
| 1318 | | preference_description(ask_when_content_changed,'Asking when file content changed from external program'). |
| 1319 | | preference_description(user_not_beginner,'User is not a beginner'). |
| 1320 | | preference_description(user_is_an_expert_with_accessto_source_distribution,'User is expert with access to source distribution of ProB'). |
| 1321 | | %preference_description(default_to_runtime_type_checking_on_startup_for_expert,'When starting up (in expert mode) turn runtime type checking on'). |
| 1322 | | preference_description(path_to_probe,'Path to Probe or other tool to view .csp files'). |
| 1323 | | preference_description(path_to_spin,'Path to Spin or other tool to view .prom files'). |
| 1324 | | preference_description(path_to_cspm,'Path to cspm to view and analyze .csp files.'). |
| 1325 | | preference_description(path_to_text_editor,'Path to external GUI text editor'). |
| 1326 | | 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 ??! |
| 1327 | | %preference_description(path_to_fuzz,'Path to the fuzz tool for ProZ'). |
| 1328 | | preference_description(path_to_fdr,'Path to the FDR2 tool'). |
| 1329 | | preference_description(path_to_csp_typechecker,'Path to a CSP type checking tool, such as refines from FDR3 (taking --typecheck as argument)'). |
| 1330 | | preference_description(path_to_bcomp,'Path to a bcomp (Atelier B Parser and type checker )'). |
| 1331 | | preference_description(path_to_java,'Path to the "java" command (in case java is not found on the PATH)'). |
| 1332 | | 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)'). |
| 1333 | | preference_description(path_to_atb_krt,'Path to Atelier B Provers krt tool'). |
| 1334 | | preference_description(try_atb_provers,'Try Atelier B Provers for unknown SMTLIB specifications'). |
| 1335 | | preference_description(smtlib2b_arrays_as_sets,'Translate SMTLib boolean Arrays to B Sets (when processing .smt2 files)'). |
| 1336 | | preference_description(smtlib2b_cleanup_predicate,'Preprocess before solving SMTLib formulas (when processing .smt2 files)'). |
| 1337 | | preference_description(symbolic_mc_try_other_solvers,'Symbolic Model Checking: Try different solver / settings combinations'). |
| 1338 | | preference_description(number_of_recent_documents,'Number of recently opened file names memorised'). |
| 1339 | | preference_description(number_of_searched_patterns,'Number of recently searched patterns in text'). |
| 1340 | | preference_description(number_of_replaced_patterns,'Number of recently replaced patterns in text'). |
| 1341 | | preference_description(number_of_eval_history_elements,'Number of recently runs of commands in the eval window'). |
| 1342 | | preference_description(number_of_eval_csp_history_elements,'Number of recently runs of commands in the eval window'). |
| 1343 | | preference_description(number_of_checked_ltl_formulas,'Number of recently checked LTL formulas'). |
| 1344 | | preference_description(ltl_to_ba_tool,'Tool in lib/ directory for generating a Buechi automaton from LTL.'). |
| 1345 | | preference_description(path_to_clingo,'Path to clingo binary (for alternate constraint solving backend)'). |
| 1346 | | |
| 1347 | | preference_description(do_syntax_highlighting,'Enable Syntax Colour Highlighting'). |
| 1348 | | preference_description(sh_type_colour,'Colour of typing constructs: NAT,POW,... (red,green,... or rgb hex #ff00ff)'). |
| 1349 | | preference_description(sh_logical_colour,'Colour of logical operators: &,or,...'). |
| 1350 | | preference_description(sh_assignments_colour,'Colour of assignments: :=, <-- and strings'). |
| 1351 | | preference_description(sh_operators,'Colour of normal operators ran,dom,...'). |
| 1352 | | preference_description(sh_top_level_keywords,'Colour of top level keywords: MACHINE, INVARIANT,...'). |
| 1353 | | preference_description(sh_control_keywords,'Colour of control keywords: IF, CASE,...'). |
| 1354 | | %preference_description(sh_includes_keywords,'Colour of inclusion related keywords: USES,...'). |
| 1355 | | preference_description(sh_comments,'Colour of comments /* ... */'). |
| 1356 | | preference_description(sh_pragmas,'Colour of pragmas /*@ ... */'). |
| 1357 | | preference_description(sh_unsupported_background,'Background colour for unsupported features (closure,...)'). |
| 1358 | | |
| 1359 | | preference_description(expand_forall_upto,'When analysing predicates: max. domain size for expansion of forall'). |
| 1360 | | preference_description(double_evaluation_when_analysing,'Evaluate PREDICATES positively and negatively when analysing'). |
| 1361 | | preference_description(prob_safe_mode,'Perform additional safety checks, which can slow down ProB'). |
| 1362 | | preference_description(expand_avl_upto,'Max size for pretty-printing sets (-1 means no limit)'). |
| 1363 | | preference_description(show_bvisual_formula_functor_from,'Show prefix/infix operators in state view for formulas longer than (use -1 to disable feature):'). |
| 1364 | | preference_description(show_bvisual_proof_info_icons,'Show proof info icon in state view (currently only for Event-B):'). |
| 1365 | | preference_description(formula_tree_minimal_timeout,'Minimal time-out for formula tree visualisation to find solutions to quantified identifiers'). |
| 1366 | | preference_description(formula_tree_maximal_timeout,'Maximal time-out for formula tree visualisation to find solutions to quantified identifiers'). |
| 1367 | | preference_description(show_bvisual_formula_explanations,'Show explanation nodes in state view for certain formulas (e.g., <:, ...)'). |
| 1368 | | preference_description(show_function_tuples_in_property,'Show function tuples in state view or dot files (f(1)=2 instead of f={(1,2)})'). |
| 1369 | | preference_description(bugly_pp_scrambling,'Scramble identifiers when pretty-printing (BUGLY)'). |
| 1370 | | preference_description(pp_propositional_logic_mode,'Try and pretty-print formulas using propositional variables (A=TRUE will be printed as A)'). |
| 1371 | | preference_description(pp_wd_infos,'Pretty-print well-definedness information for formulas'). |
| 1372 | | preference_description(pp_with_terminal_colour,'Pretty-print values and formulas with terminal colour escape codes'). |
| 1373 | | preference_description(wd_ignore_external_funs,'Do not create (unprovable) WD PO for external functions with WD condition'). |
| 1374 | | preference_description(wd_skip_finite_pos,'Do not generate finite WD POs'). |
| 1375 | | preference_description(wd_analysis_for_animation,'Perform the WD analysis in the context of ProB animation (e.g., deferred sets considered finite)'). |
| 1376 | | preference_description(z3_solve_for_animation,'Perform SMT solving with Z3 in the context of ProB animation (e.g., deferred sets considered finite)'). |
| 1377 | | preference_description(add_wd_pos_for_z3,'Add well-definedness POs to constraints before translating to SMT-LIB'). |
| 1378 | | preference_description(do_not_print_wd_errors,'Do not print well-definedness (WD) errors on the console.'). |
| 1379 | | |
| 1380 | | |
| 1381 | | preference_description(allow_new_ops_in_refinement,'Allow introduction of new operations in refinements (automatically set to TRUE for SYSTEM machines)'). |
| 1382 | | preference_description(allow_local_operation_calls,'Allow to call operations in OPERATIONS section of same machine (operations in LOCAL_OPERATIONS of same machine can always be called)'). |
| 1383 | | preference_description(allow_operation_calls_in_expr,'Allow to call query operations in (some) expressions'). |
| 1384 | | 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 ...)'). |
| 1385 | | |
| 1386 | | |
| 1387 | | preference_description(use_po,'Use PROOF information to restrict invariant checking to affected clauses.'). |
| 1388 | | %preference_description(use_po,'Restrict invariant checking to affected clauses. Also remove clauses that are proven (EventB)'). |
| 1389 | | 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 |
| 1390 | | preference_description(try_operation_reuse_for_invariants,'Apply OPERATION_REUSE also to invariants (cache projected state space per invariant check)'). |
| 1391 | | preference_description(operation_reuse_setting,'real setting computed from OPERATION_REUSE'). |
| 1392 | | preference_description(randomise_operation_order,'Randomise order of operations when computing successor states.'). |
| 1393 | | % currently only alternates between normal and reverse order |
| 1394 | | preference_description(randomise_enumeration_order,'Randomise enumeration of variables.'). |
| 1395 | | preference_description(perform_enumeration_order_analysis,'Perform enumeration order analysis within quantifiers, e.g., to detect identifiers that should not be enumerated'). |
| 1396 | | preference_description(set_rand,'Use a fix seed for random number generator. Allows to reproduce results.'). |
| 1397 | | preference_description(rand_seed,'Seed for Random Number Generator'). |
| 1398 | | |
| 1399 | | preference_description(machines_path,'Last open directory'). |
| 1400 | | |
| 1401 | | % Options for enabling/disabling the POR and PGE optimisations for Model Checking of B and Event-B models |
| 1402 | | 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).'). |
| 1403 | | preference_description(timeout_cbc_analysis,'Time out for computing independence and enable relations between operations.'). |
| 1404 | | |
| 1405 | | preference_description(alloy_use_implementable_integers,'Use INT (minint..maxint) for the translation from Alloy to B.'). |
| 1406 | | preference_description(alloy_scopeless_translation,'Do not set any scopes when translating an Alloy model to B (useful for proof assistants).'). |
| 1407 | | 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.'). |
| 1408 | | 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.'). |
| 1409 | | |
| 1410 | | preference_description(use_scope_predicate, |
| 1411 | | 'Use SCOPE predicate (if defined) to restrict state space exploration for model checking and animation.'). |
| 1412 | | 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 |
| 1413 | | |
| 1414 | | preference_description(por,'Type of Partial Order Reduction Technique (ample_sets, ample_sets2).'). |
| 1415 | | preference_description(por_heur,'Type of heuritic for choosing a valid ample set.'). |
| 1416 | | %preference_description(use_por_for_ltl,'Use Partial Order Reduction for LTL.'). |
| 1417 | | 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 |
| 1418 | | |
| 1419 | | preference_description(enable_graph,'Option for using the enable graph module for partial order reduction.'). |
| 1420 | | preference_description(enable_graph_depth,'The depth of evaluating the weakest-preconditions along a path in an enable graph.'). |
| 1421 | | |
| 1422 | | preference_description(dependency_enable_predicates,'Compute in each state whether two events can disable each other.'). |
| 1423 | | |
| 1424 | | preference_description(filter_unused_constants,'Filter out unused constants (can interfere with VisB or other visualisations)'). |
| 1425 | | preference_description(translate_force_all_typing_infos,'Print all typing infos when pretty-printing'). |
| 1426 | | preference_description(translate_print_typing_infos,'Print needed typing infos when pretty-printing'). |
| 1427 | | preference_description(translate_print_frozen_infos,'Print Prolog frozen goal infos for unbound variables'). |
| 1428 | | preference_description(translate_ids_to_parseable_format,'Print Identifiers in a format that can be parsed again'). |
| 1429 | | preference_description(translate_suppress_rodin_positions_flag,'Suppres Rodin position information when pretty-printing'). |
| 1430 | | preference_description(translate_print_all_sequences,'Print B relations as sequences when possible during pretty-printing.'). |
| 1431 | | preference_description(translate_print_cs_style_sequences,'Print B sequences in theoretical CS style without separators.'). |
| 1432 | | % Note: also influenced by expand_avl_upto preference |
| 1433 | | preference_description(translation_limit_for_table_commands,'Translation/pretty print limit for columns used by some table (CSV) commands'). |
| 1434 | | 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 |
| 1435 | | preference_description(visb_show_debug_infos,'Show VisB debug information in title hovers'). |
| 1436 | | |
| 1437 | | preference_description(trace_generation_limit,'Max. number of traces generated'). |
| 1438 | | preference_description(trace_generation_time_out,'Timeout for trace generation'). |
| 1439 | | |
| 1440 | | preference_description(disprover_mode,'Assume that well-definedness is guaranteed or checked by other means (for Rodin DISPROVER Plugin)'). |
| 1441 | | 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 |
| 1442 | | preference_description(trace_upon_error,'Trace upon error (requires running from source)'). |
| 1443 | | preference_description(error_log_file, 'File were all errors and warnings are logged (NDJSON format). Can be set to stderr or stdout.'). |
| 1444 | | preference_description(tlc_number_of_workers,'Number of parallel workers for external tool TLC (for -workers option)'). |
| 1445 | | preference_description(tlc_use_prob_constant_setup,'Use constants found by ProB for TLC model checking (for -constantssetup option)'). |
| 1446 | | 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)'). |
| 1447 | | |
| 1448 | | |
| 1449 | | preference_description(port, 'First number to be used by parB/distb/ZMQ. Default: 5000'). |
| 1450 | | 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.'). |
| 1451 | | 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'). |
| 1452 | | preference_description(tmpdir, 'The directory where temporary files should be stored. Default: /tmp/.'). |
| 1453 | | preference_description(logdir, 'The directory where log files should be stored. Default: ./distb-logs/'). |
| 1454 | | 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'). |
| 1455 | | preference_description(queue_threshold, 'The amount of states that may be kept in a ZMQ queue before it is allowed to share. Default: 20'). |
| 1456 | | preference_description(hash_cycle, 'Minimum amount of milliseconds that has to pass between hash code updates from the ZMQ master. Default: 25'). |
| 1457 | | preference_description(cdclt_perform_static_analysis, 'CDCL(T) Solver: Perform static analysis to infer implied constraints'). |
| 1458 | | preference_description(cdclt_perform_symmetry_breaking, 'CDCL(T) Solver: Perform symmetry breaking using BLISS (if installed)'). |
| 1459 | | preference_description(cdclt_use_idl_theory_solver, 'CDCL(T) Solver: Use additional IDL (Integer-Difference-Logic) solver'). |
| 1460 | | preference_description(prob_version_info,'Version of ProB (read-only preference)'). % mainly so that in ProB for Rodin we can see the version number |
| 1461 | | preference_description(prob_revision_info,'Git revision of ProB (read-only preference)'). |
| 1462 | | preference_description(prob_lastchangedate_info,'Last change date of ProB source (read-only preference)'). |
| 1463 | | |
| 1464 | | preference_description(xtl_safe_mode,'Use runtime checking to make sure the predicates in XTL models are implemented correctly, the tradeoff is performance.'). |
| 1465 | | |
| 1466 | | /* ------------------------- */ |
| 1467 | | |
| 1468 | | :- use_module(pathes_extensions_db, [preference_value_requires_extension/3]). |
| 1469 | | :- use_module(pathes_lib, [unavailable_extension/2]). |
| 1470 | | |
| 1471 | | %preference_update_action(do_full_invariant_checking,_) :- !, b_types_precompile. |
| 1472 | | %preference_change_requires_reload(enable_canonical_symmetry,true) :- !, . |
| 1473 | | %preference_update_action(use_nauty_symmetry_reduction,true) :- !, graph_iso_nauty:nauty_init. |
| 1474 | | %:- use_module(probsrc(bmachine),[bmachine_is_precompiled/0]). |
| 1475 | | %:- use_module(probsrc(graph_iso_nauty),[nauty_init/0]). |
| 1476 | | preference_update_action(Pref,Val) :- |
| 1477 | ? | preference_value_requires_extension(Pref,Val,Extension), |
| 1478 | | unavailable_extension(Extension,Reason), |
| 1479 | | ajoin(['Value ', Val,' for preference ',Pref, |
| 1480 | | ' may lead to errors because extension not available (',Reason,'): '],Msg), |
| 1481 | | add_warning(preferences,Msg,Extension), |
| 1482 | | fail. |
| 1483 | | preference_update_action(symmetry_mode,nauty) :- !, |
| 1484 | | (bmachine:bmachine_is_precompiled -> graph_iso_nauty:nauty_init ; true). |
| 1485 | | preference_update_action(_,_). |
| 1486 | | % TODO: jvm_parser_position_infos : release_console_parser |
| 1487 | | |
| 1488 | | /* ------------------------- */ |
| 1489 | | |
| 1490 | | % now in basic_tests.pl |
| 1491 | | %:- assert_must_succeed( \+((preference_val_type(P,_D),\+preference_default_value(P,_Val)))). |
| 1492 | | %:- assert_must_succeed( \+((preference_default_value(P,_D), \+preference_val_type(P,_Val)))). |
| 1493 | | preference_val_type(maxint,nat1). |
| 1494 | | preference_val_type(minint,neg). |
| 1495 | | preference_val_type(number_animated_abstractions,nat). |
| 1496 | | preference_val_type(number_skipped_refined_machines,nat). |
| 1497 | | preference_val_type(globalsets_fdrange,nat). |
| 1498 | | preference_val_type(do_invariant_checking,bool). |
| 1499 | | preference_val_type(do_assert_checking,bool). |
| 1500 | | preference_val_type(find_abort_values,xbool). |
| 1501 | | preference_val_type(raise_abort_immediately,xbool). |
| 1502 | | preference_val_type(treat_outermost_pre_as_select,bool). |
| 1503 | | preference_val_type(require_operations_to_assign_all_outputs,bool). |
| 1504 | | preference_val_type(allow_operations_to_read_outputs,bool). |
| 1505 | | preference_val_type(allow_operation_calls_for_uses,bool). |
| 1506 | | preference_val_type(allow_overriding_initialisation,bool). |
| 1507 | | preference_val_type(allow_simultaneous_assignments,bool). |
| 1508 | | preference_val_type(allow_arith_operators_on_reals,dbool). |
| 1509 | | preference_val_type(solver_for_reals,[aggressive_float_solver,float_solver,none,precise_float_solver]). |
| 1510 | | preference_val_type(cspm_animate_all_processes_without_arguments,bool). |
| 1511 | | preference_val_type(cspm_animate_all_processes,bool). |
| 1512 | | preference_val_type(cspm_detailed_animation,bool). |
| 1513 | | preference_val_type(cspm_strip_source_location,bool). |
| 1514 | | %preference_val_type(csp_event_visible_to_user,bool). |
| 1515 | | preference_val_type(show_initialisation_arguments,bool). |
| 1516 | | preference_val_type(deterministic_trace_replay,bool). |
| 1517 | | preference_val_type(show_eventb_any_arguments,bool). |
| 1518 | | preference_val_type(maxNrOfInitialisations,nat). |
| 1519 | | preference_val_type(randomisedRestartInitalisations,bool). |
| 1520 | | preference_val_type(maxNrOfEnablingsPerOperation,nat). |
| 1521 | | preference_val_type(time_out,nat1). |
| 1522 | | preference_val_type(debug_time_out_factor,nat1). |
| 1523 | | %preference_val_type(use_large_jvm_for_parser,bool). |
| 1524 | | preference_val_type(jvm_parser_heap_size_mb,nat). |
| 1525 | | preference_val_type(jvm_parser_additional_args,string). |
| 1526 | | preference_val_type(jvm_parser_position_infos,bool). |
| 1527 | | preference_val_type(jvm_parser_fastrw,bool). |
| 1528 | | preference_val_type(jvm_parser_force_parsing,bool). |
| 1529 | | preference_val_type(convert_comprehension_sets_into_closures,bool). |
| 1530 | | preference_val_type(comprehension_set_symbolic_limit,nat). |
| 1531 | | preference_val_type(use_clpfd_solver,bool). |
| 1532 | | preference_val_type(clpfd_solver_label_option,labeling_option). |
| 1533 | | preference_val_type(use_chr_solver,bool). |
| 1534 | | preference_val_type(data_validation_mode,bool). |
| 1535 | | preference_val_type(use_smt_mode,bool). |
| 1536 | | preference_val_type(solver_strength,nat). |
| 1537 | | preference_val_type(use_common_subexpression_elimination,bool). |
| 1538 | | preference_val_type(remove_implied_constraints,bool). |
| 1539 | | preference_val_type(lift_existential_quantifiers,bool). |
| 1540 | | preference_val_type(use_common_subexpression_also_for_predicates,bool). |
| 1541 | | preference_val_type(use_common_subexpression_also_for_substitutions,bool). |
| 1542 | | preference_val_type(use_common_subexpression_wd_only,bool). |
| 1543 | | preference_val_type(normalize_ast,bool). |
| 1544 | | preference_val_type(normalize_ast_sort_commutative,bool). |
| 1545 | | preference_val_type(optimize_ast,bool). |
| 1546 | | %preference_val_type(optimize_enum_set_elems,bool). |
| 1547 | | preference_val_type(useless_code_elimination,bool). |
| 1548 | | preference_val_type(compile_while_body,bool). |
| 1549 | | preference_val_type(expand_becomes_such_into_set,bool). |
| 1550 | | preference_val_type(detect_lambdas,bool). |
| 1551 | | preference_val_type(auto_detect_theory_ops,bool). |
| 1552 | | preference_val_type(ltsmin_guard_splitting,bool). |
| 1553 | | preference_val_type(ltsmin_do_not_evaluate_top_level_guards,xbool). |
| 1554 | | preference_val_type(fail_if_clpfd_timeout,bool). |
| 1555 | | %preference_val_type(allow_recursive_closures,bool). |
| 1556 | | preference_val_type(use_static_ordering,bool). |
| 1557 | | preference_val_type(try_use_state_packing,axbool). |
| 1558 | | preference_val_type(use_state_packing,xbool). |
| 1559 | | preference_val_type(force_state_packing_for_closures,bool). |
| 1560 | | preference_val_type(provide_trace_information,bool). |
| 1561 | | preference_val_type(prob_profiling_on,bool). |
| 1562 | | preference_val_type(prob_source_profiling_on,bool). |
| 1563 | | preference_val_type(performance_monitoring_on,bool). |
| 1564 | | preference_val_type(performance_monitoring_expansion_limit,int). |
| 1565 | | preference_val_type(partition_predicates,bool). |
| 1566 | | preference_val_type(partition_predicates_inline_equalities,bool). |
| 1567 | | preference_val_type(use_closure_expansion_memoization,bool). |
| 1568 | | preference_val_type(use_function_memoization,dbool). |
| 1569 | | preference_val_type(allow_incomplete_partial_setup_constants,bool). |
| 1570 | | preference_val_type(re_execute_operations_with_side_effects,bool). |
| 1571 | | preference_val_type(warn_if_definition_hides_variable,bool). |
| 1572 | | preference_val_type(type_check_definitions,bool). |
| 1573 | | %preference_val_type(warn_when_expanding_infinite_closures,int). |
| 1574 | | preference_val_type(allow_enumeration_of_infinite_types,bool). |
| 1575 | | preference_val_type(strict_raise_warnings,bool). |
| 1576 | | preference_val_type(strict_raise_enum_warnings,bool). |
| 1577 | | preference_val_type(clash_strict_checks,bool). |
| 1578 | | preference_val_type(perform_stricter_static_checks,bool). |
| 1579 | | preference_val_type(ignore_prj_types,bool). |
| 1580 | | preference_val_type(prefix_internal_operation_arguments,string). |
| 1581 | | preference_val_type(generate_minimal_nr_of_testcases,bool). |
| 1582 | | preference_val_type(use_tk_custom_state_viewer,bool). |
| 1583 | | preference_val_type(tk_custom_state_viewer_font_name,string). |
| 1584 | | preference_val_type(tk_custom_state_viewer_font_size,nat). |
| 1585 | | preference_val_type(tk_custom_state_viewer_padding,nat). |
| 1586 | | preference_val_type(tk_custom_state_viewer_str_padding,nat). |
| 1587 | | preference_val_type(use_small_window,bool). |
| 1588 | | preference_val_type(tk_show_source_pane,bool). |
| 1589 | | preference_val_type(ignore_hash_collisions,bool). |
| 1590 | | preference_val_type(forget_state_space,bool). |
| 1591 | | preference_val_type(store_only_one_incoming_transition,bool). |
| 1592 | | preference_val_type(mc_continue_after_error,bool). |
| 1593 | | preference_val_type(symmetry_mode,[off,flood,nauty,hash]). |
| 1594 | | preference_val_type(use_static_symmetry_detection,bool). |
| 1595 | | %preference_val_type(bool_expression_as_predicate,bool). |
| 1596 | | preference_val_type(allow_untyped_identifiers,[true,false,true_with_string_type]). |
| 1597 | | preference_val_type(repl_unicode,bool). |
| 1598 | | preference_val_type(repl_cache_parsing,bool). |
| 1599 | | preference_val_type(cache_constants,bool). |
| 1600 | | preference_val_type(cache_operations,bool). |
| 1601 | | preference_val_type(cache_operations_runtime_limit,nat). |
| 1602 | | preference_val_type(latex_encoding,text_encoding). |
| 1603 | | preference_val_type(latex_pp_greek_ids,bool). |
| 1604 | | preference_val_type(xml_encoding,text_encoding). |
| 1605 | | preference_val_type(view_probcli_errors_using_bbresults,bool). |
| 1606 | | preference_val_type(eventtrace,bool). |
| 1607 | | preference_val_type(store_event_transinfo,bool). |
| 1608 | | preference_val_type(use_solver_on_load,solver_name). |
| 1609 | | %preference_val_type(try_kodkod_on_load,bool). |
| 1610 | | preference_val_type(kodkod_for_components,xbool). |
| 1611 | | preference_val_type(kodkod_raise_warnings,bool). |
| 1612 | | preference_val_type(kodkod_max_nr_solutions,nat1). |
| 1613 | | preference_val_type(kodkod_symmetry_level,nat). |
| 1614 | | preference_val_type(kodkod_sat_solver,[sat4j,minisat,lingeling,glucose]). |
| 1615 | | preference_val_type(smt_supported_interpreter,bool). |
| 1616 | | preference_val_type(sat_supported_interpreter,bool). |
| 1617 | | preference_val_type(use_record_construction,bool). |
| 1618 | | preference_val_type(seen_machines_included,bool). |
| 1619 | | preference_val_type(allow_sequence_operators_on_strings,bool). |
| 1620 | | |
| 1621 | | preference_val_type(dot_print_node_ids,bool). |
| 1622 | | preference_val_type(dot_print_transition_ids,bool). |
| 1623 | | preference_val_type(dot_print_use_constants,bool). |
| 1624 | | preference_val_type(dot_print_node_info,bool). |
| 1625 | | preference_val_type(dot_print_edge_labels,bool). |
| 1626 | | preference_val_type(dot_print_action_arguments,bool). |
| 1627 | | preference_val_type(dot_print_functions,bool). |
| 1628 | | preference_val_type(dot_print_self_loops,bool). |
| 1629 | | preference_val_type(dot_print_root,bool). |
| 1630 | | %preference_val_type(dot_print_leaves,bool). |
| 1631 | | preference_val_type(dot_print_arc_colors,bool). |
| 1632 | | preference_val_type(dot_use_ps_viewer,bool). |
| 1633 | | preference_val_type(path_to_dot,path). |
| 1634 | | preference_val_type(dot_default_engine,[dot,neato,sfdp,fdp,twopi,circo,patchwork,osage,nop,nop2]). |
| 1635 | | preference_val_type(path_to_dotty,path). |
| 1636 | | preference_val_type(path_to_ltsmin,path). |
| 1637 | | preference_val_type(path_to_ps_viewer,path). |
| 1638 | | preference_val_type(path_to_latex,path). |
| 1639 | | preference_val_type(dot_root_shape,dot_shape). |
| 1640 | | preference_val_type(dot_node_penwidth,nat). |
| 1641 | | preference_val_type(dot_edge_penwidth,nat). |
| 1642 | | preference_val_type(dot_normal_node_shape,dot_shape). |
| 1643 | | preference_val_type(dot_current_node_shape,dot_shape). |
| 1644 | | preference_val_type(dot_open_node_colour,rgb_color). |
| 1645 | | preference_val_type(dot_scope_limit_node_colour,rgb_color). |
| 1646 | | preference_val_type(dot_normal_node_colour,rgb_color). |
| 1647 | | preference_val_type(dot_invariant_violated_node_colour,rgb_color). |
| 1648 | | preference_val_type(dot_fill_normal_nodes,bool). |
| 1649 | | preference_val_type(dot_normal_arc_colour,rgb_color). |
| 1650 | | preference_val_type(dot_node_font_size,nat1). |
| 1651 | | preference_val_type(dot_edge_font_size,nat1). |
| 1652 | | preference_val_type(dot_with_page_size,bool). |
| 1653 | | preference_val_type(dot_horizontal_layout,bool). |
| 1654 | | preference_val_type(dot_colour_goal_nodes,bool). |
| 1655 | | preference_val_type(dot_goal_node_colour,rgb_color). |
| 1656 | | preference_val_type(dot_print_node_properties,bool). |
| 1657 | | preference_val_type(dot_counterexample_node_colour,rgb_color). |
| 1658 | | preference_val_type(dot_counterexample_op_colour,rgb_color). |
| 1659 | | preference_val_type(dot_hierarchy_max_ids,int). |
| 1660 | | preference_val_type(cbc_provide_explanations,bool). |
| 1661 | | |
| 1662 | | preference_val_type(successful_rule_colour,rgb_color). |
| 1663 | | preference_val_type(failed_rule_colour,rgb_color). |
| 1664 | | preference_val_type(disabled_rule_colour,rgb_color). |
| 1665 | | preference_val_type(not_checked_rule_colour,rgb_color). |
| 1666 | | preference_val_type(rule_graph_shape,dot_shape). |
| 1667 | | preference_val_type(executed_computation_colour,rgb_color). |
| 1668 | | preference_val_type(not_executed_computation_colour,rgb_color). |
| 1669 | | preference_val_type(disabled_computation_colour,rgb_color). |
| 1670 | | preference_val_type(computation_graph_shape,dot_shape). |
| 1671 | | preference_val_type(succeeded_dependency_colour,rgb_color). |
| 1672 | | preference_val_type(failed_dependency_colour,rgb_color). |
| 1673 | | preference_val_type(normal_dependency_colour,rgb_color). |
| 1674 | | |
| 1675 | | preference_val_type(dot_event_hierarchy_horizontal,bool). |
| 1676 | | preference_val_type(dot_event_hierarchy_machine_colour,rgb_color). |
| 1677 | | preference_val_type(dot_event_hierarchy_refines_colour,rgb_color). |
| 1678 | | preference_val_type(dot_event_hierarchy_new_event_colour,rgb_color). |
| 1679 | | preference_val_type(dot_event_hierarchy_rename_event_colour,rgb_color). |
| 1680 | | preference_val_type(dot_event_hierarchy_rename_unchanged_event_colour,rgb_color). |
| 1681 | | preference_val_type(dot_event_hierarchy_unchanged_event_colour,rgb_color). |
| 1682 | | preference_val_type(dot_event_hierarchy_grd_strengthening_event_colour,rgb_color). |
| 1683 | | preference_val_type(dot_event_hierarchy_grd_keeping_event_colour,rgb_color). |
| 1684 | | preference_val_type(dot_event_hierarchy_edge_colour,rgb_color). |
| 1685 | | preference_val_type(dot_event_hierarchy_extends_colour,rgb_color). |
| 1686 | | preference_val_type(dot_hierarchy_show_extra_detail,bool). |
| 1687 | | |
| 1688 | | preference_val_type(dot_projection_non_det_edge_colour,rgb_color). |
| 1689 | | preference_val_type(dot_projection_det_edge_colour,rgb_color). |
| 1690 | | preference_val_type(dot_projection_non_definite_edge_style,dot_line_style). |
| 1691 | | preference_val_type(dot_projection_definite_edge_style,dot_line_style). |
| 1692 | | preference_val_type(dot_projection_label_limit,nat). |
| 1693 | | preference_val_type(dot_projection_process_only_explored,bool). |
| 1694 | | preference_val_type(dot_use_unicode,bool). |
| 1695 | | preference_val_type(dot_predicate_node_shape,dot_shape). |
| 1696 | | preference_val_type(dot_expression_node_shape,dot_shape). |
| 1697 | | preference_val_type(dot_var_mod_hide_only_written,bool). |
| 1698 | | |
| 1699 | | preference_val_type(mc_dc_default_level,nat). |
| 1700 | | |
| 1701 | | preference_val_type(dot_enabling_show_readwrites,bool). |
| 1702 | | |
| 1703 | | preference_val_type(dot_definitions_use_sub_graph,bool). |
| 1704 | | preference_val_type(dot_definitions_show_all,bool). |
| 1705 | | preference_val_type(dot_state_graph_decompose,bool). |
| 1706 | | |
| 1707 | | preference_val_type(font_name,string). |
| 1708 | | preference_val_type(font_size_only,nat1). |
| 1709 | | preference_val_type(font_size,string). |
| 1710 | | preference_val_type(use_font_size_for_columns,bool). |
| 1711 | | preference_val_type(allow_source_code_editing,bool). |
| 1712 | | preference_val_type(show_line_numbers,bool). |
| 1713 | | %preference_val_type(show_full_error_span,bool). |
| 1714 | | preference_val_type(highlight_brackets,bool). |
| 1715 | | preference_val_type(highlight_current_line,bool). |
| 1716 | | preference_val_type(ask_when_content_changed,bool). |
| 1717 | | |
| 1718 | | preference_val_type(user_not_beginner,bool). |
| 1719 | | preference_val_type(user_is_an_expert_with_accessto_source_distribution,bool). |
| 1720 | | %preference_val_type(default_to_runtime_type_checking_on_startup_for_expert,bool). |
| 1721 | | preference_val_type(path_to_probe,path). |
| 1722 | | %preference_val_type(path_to_fuzz,path). |
| 1723 | | preference_val_type(path_to_fdr,path). |
| 1724 | | preference_val_type(path_to_csp_typechecker,path). |
| 1725 | | preference_val_type(path_to_bcomp,path). % Atelier B parser & type checker |
| 1726 | | preference_val_type(path_to_java,path). % Path to Java |
| 1727 | | preference_val_type(path_to_java_parser,path). % Path to probcliparser.java or cliparser, default '' |
| 1728 | | preference_val_type(path_to_atb_krt,path). |
| 1729 | | preference_val_type(try_atb_provers,bool). |
| 1730 | | preference_val_type(smtlib2b_arrays_as_sets,bool). |
| 1731 | | preference_val_type(smtlib2b_cleanup_predicate,bool). |
| 1732 | | preference_val_type(symbolic_mc_try_other_solvers,bool). |
| 1733 | | preference_val_type(path_to_spin,path). |
| 1734 | | preference_val_type(path_to_cspm,path). |
| 1735 | | preference_val_type(path_to_text_editor,path). |
| 1736 | | preference_val_type(path_to_text_editor_launch,path). |
| 1737 | | preference_val_type(number_of_recent_documents,nat). |
| 1738 | | preference_val_type(number_of_searched_patterns,nat). |
| 1739 | | preference_val_type(number_of_replaced_patterns,nat). |
| 1740 | | preference_val_type(number_of_eval_history_elements,nat). |
| 1741 | | preference_val_type(number_of_eval_csp_history_elements,nat). |
| 1742 | | preference_val_type(number_of_checked_ltl_formulas,nat). |
| 1743 | | preference_val_type(ltl_to_ba_tool,path). |
| 1744 | | preference_val_type(path_to_clingo,path). |
| 1745 | | |
| 1746 | | preference_val_type(do_syntax_highlighting,bool). |
| 1747 | | preference_val_type(sh_type_colour,rgb_color). |
| 1748 | | preference_val_type(sh_logical_colour,rgb_color). |
| 1749 | | preference_val_type(sh_assignments_colour,rgb_color). |
| 1750 | | preference_val_type(sh_operators,rgb_color). |
| 1751 | | preference_val_type(sh_top_level_keywords,rgb_color). |
| 1752 | | preference_val_type(sh_control_keywords,rgb_color). |
| 1753 | | %preference_val_type(sh_includes_keywords,rgb_color). |
| 1754 | | preference_val_type(sh_comments,rgb_color). |
| 1755 | | preference_val_type(sh_pragmas,rgb_color). |
| 1756 | | preference_val_type(sh_unsupported_background,rgb_color). |
| 1757 | | |
| 1758 | | preference_val_type(expand_forall_upto,nat). |
| 1759 | | preference_val_type(double_evaluation_when_analysing,bool). |
| 1760 | | preference_val_type(prob_safe_mode,bool). |
| 1761 | | preference_val_type(expand_avl_upto,int). |
| 1762 | | preference_val_type(show_bvisual_formula_functor_from,int). |
| 1763 | | preference_val_type(show_bvisual_proof_info_icons,bool). |
| 1764 | | preference_val_type(show_bvisual_formula_explanations,bool). |
| 1765 | | preference_val_type(formula_tree_minimal_timeout,nat). |
| 1766 | | preference_val_type(formula_tree_maximal_timeout,nat). |
| 1767 | | preference_val_type(show_function_tuples_in_property,bool). |
| 1768 | | preference_val_type(bugly_pp_scrambling,bool). |
| 1769 | | preference_val_type(pp_propositional_logic_mode,bool). |
| 1770 | | preference_val_type(pp_wd_infos,bool). |
| 1771 | | preference_val_type(pp_with_terminal_colour,bool). |
| 1772 | | preference_val_type(wd_ignore_external_funs,bool). |
| 1773 | | preference_val_type(wd_skip_finite_pos,bool). |
| 1774 | | preference_val_type(wd_analysis_for_animation,bool). |
| 1775 | | preference_val_type(z3_solve_for_animation,bool). |
| 1776 | | preference_val_type(add_wd_pos_for_z3,bool). |
| 1777 | | preference_val_type(do_not_print_wd_errors,bool). |
| 1778 | | |
| 1779 | | preference_val_type(allow_new_ops_in_refinement,bool). |
| 1780 | | preference_val_type(allow_local_operation_calls,bool). |
| 1781 | | preference_val_type(allow_operation_calls_in_expr,bool). |
| 1782 | | preference_val_type(allow_let_to_reuse_introduced_ids,bool). |
| 1783 | | preference_val_type(use_po,bool). |
| 1784 | | preference_val_type(try_operation_reuse,axbool). % false,true,full,auto |
| 1785 | | preference_val_type(try_operation_reuse_for_invariants,bool). |
| 1786 | | preference_val_type(operation_reuse_setting,xbool). |
| 1787 | | preference_val_type(randomise_operation_order,bool). |
| 1788 | | preference_val_type(randomise_enumeration_order,bool). |
| 1789 | | preference_val_type(perform_enumeration_order_analysis,bool). |
| 1790 | | |
| 1791 | | preference_val_type(set_rand,bool). |
| 1792 | | preference_val_type(rand_seed,nat). |
| 1793 | | |
| 1794 | | preference_val_type(alloy_use_implementable_integers,bool). |
| 1795 | | preference_val_type(alloy_scopeless_translation,bool). |
| 1796 | | preference_val_type(alloy_translation_for_proof,bool). |
| 1797 | | preference_val_type(alloy_strict_integers,bool). |
| 1798 | | |
| 1799 | | preference_val_type(use_scope_predicate,bool). |
| 1800 | | preference_val_type(use_ignore_pragmas,bool). |
| 1801 | | %% Options' meaning |
| 1802 | | % disabled: skipping guard evaluation of actions known to be disabled at state |
| 1803 | | % enabled: skipping guard evaluation of actions known to be enabled at state |
| 1804 | | % full: skipping guard evaluations of actions known to be enabled or disabled at state |
| 1805 | | % disabled2, enabled2, full2: same for these, but another (more precise) way for computing the sets of enabled and disabled actions is used |
| 1806 | | %preference_val_type(pge,[off,disabled,enabled,full,disabled2,enabled2,full2]). |
| 1807 | | |
| 1808 | | preference_val_type(use_cbc_analysis,bool). |
| 1809 | | preference_val_type(timeout_cbc_analysis,nat1). |
| 1810 | | |
| 1811 | | preference_val_type(por,[off,ample_sets,ample_sets2]). |
| 1812 | | preference_val_type(por_heur,[first,random,minimal]). |
| 1813 | | preference_val_type(use_safety_ltl_model_checker,bool). |
| 1814 | | |
| 1815 | | preference_val_type(enable_graph,bool). |
| 1816 | | preference_val_type(enable_graph_depth,int). |
| 1817 | | |
| 1818 | | preference_val_type(dependency_enable_predicates,bool). |
| 1819 | | |
| 1820 | | preference_val_type(filter_unused_constants,bool). |
| 1821 | | preference_val_type(translate_force_all_typing_infos,bool). |
| 1822 | | preference_val_type(translate_print_typing_infos,bool). |
| 1823 | | preference_val_type(translate_print_frozen_infos,bool). |
| 1824 | | preference_val_type(translate_ids_to_parseable_format,bool). |
| 1825 | | preference_val_type(translate_suppress_rodin_positions_flag,bool). |
| 1826 | | preference_val_type(translate_print_all_sequences,bool). |
| 1827 | | preference_val_type(translate_print_cs_style_sequences,bool). |
| 1828 | | preference_val_type(translation_limit_for_table_commands,int). |
| 1829 | | preference_val_type(visb_allow_variables_for_objects,bool). |
| 1830 | | preference_val_type(visb_show_debug_infos,bool). |
| 1831 | | preference_val_type(trace_generation_limit,nat). |
| 1832 | | preference_val_type(trace_generation_time_out,nat). |
| 1833 | | |
| 1834 | | |
| 1835 | | preference_val_type(disprover_mode,bool). |
| 1836 | | preference_val_type(allow_improving_wd_mode,bool). |
| 1837 | | preference_val_type(trace_upon_error,bool). |
| 1838 | | preference_val_type(tlc_number_of_workers,nat1). |
| 1839 | | preference_val_type(tlc_use_prob_constant_setup,bool). |
| 1840 | | preference_val_type(error_log_file,path). |
| 1841 | | |
| 1842 | | preference_val_type(unsat_core_algorithm,[divide_and_conquer,linear,linear_greedy,linear_greedy_decompose]). |
| 1843 | | |
| 1844 | | preference_val_type(port, nat1). |
| 1845 | | preference_val_type(ip, string). |
| 1846 | | preference_val_type(max_states, nat). |
| 1847 | | preference_val_type(tmpdir, path). |
| 1848 | | preference_val_type(logdir, path). |
| 1849 | | preference_val_type(proxynumber, nat). |
| 1850 | | preference_val_type(queue_threshold, nat1). |
| 1851 | | preference_val_type(hash_cycle, nat). |
| 1852 | | preference_val_type(cdclt_perform_static_analysis,bool). |
| 1853 | | preference_val_type(cdclt_perform_symmetry_breaking,bool). |
| 1854 | | preference_val_type(cdclt_use_idl_theory_solver,bool). |
| 1855 | | preference_val_type(prob_version_info, string). |
| 1856 | | preference_val_type(prob_revision_info, string). |
| 1857 | | preference_val_type(prob_lastchangedate_info, string). |
| 1858 | | |
| 1859 | | preference_val_type(xtl_safe_mode, bool). |
| 1860 | | |
| 1861 | | preference_val_type(machines_path,path). %directory_path). % preference not so critical; default value may not exist |
| 1862 | | |
| 1863 | | |
| 1864 | | % obtain list of all valid values, e.g. for ProB2-UI |
| 1865 | | preference_val_type_list(Pref,ValList) :- |
| 1866 | | preference_val_type(Pref,Type), |
| 1867 | | val_list_for_type(Type,ValList). |
| 1868 | | |
| 1869 | | val_list_for_type(Type,List) :- is_list(Type), !, Type=List. |
| 1870 | | val_list_for_type(Type,List) :- list_valid_type_vals(Type,List), !. |
| 1871 | | val_list_for_type(Type,List) :- pref_type_synonym(Type,List), !. |
| 1872 | | val_list_for_type(Type,Type). % no enumeration of valid values possible - provide type name |
| 1873 | | |
| 1874 | | list_valid_type_vals(axbool,[false,true,full,auto]). |
| 1875 | | list_valid_type_vals(xbool,[false,true,full]). |
| 1876 | | list_valid_type_vals(dbool,[default,false,true]). % maybe put these in pref_type_synonym |
| 1877 | | list_valid_type_vals(dot_shape,Opt) :- findall(X,valid_dot_shape(X),Opt). |
| 1878 | | list_valid_type_vals(dot_node_style,Opt) :- findall(X,valid_dot_node_style(X),Opt). |
| 1879 | | list_valid_type_vals(dot_line_style,Opt) :- findall(X,valid_dot_line_style(X),Opt). |
| 1880 | | list_valid_type_vals(labeling_option,[anti_first_fail,dom_w_deg, |
| 1881 | | ff, % first_fail |
| 1882 | | ffc, % most_constrained |
| 1883 | | impact,leftmost,min,max,max_regret,occurrence]). |
| 1884 | | /* ------------------------- */ |
| 1885 | | |
| 1886 | | |
| 1887 | | % now in basic_tests.pl |
| 1888 | | %:- assert_must_succeed( \+((preference_category(P,_D),\+preference_default_value(P,_Val)))). |
| 1889 | | %:- assert_must_succeed( \+((preference_default_value(P,_D), \+preference_category(P,_Val)))). |
| 1890 | | preference_category(unsat_core_algorithm,advanced). |
| 1891 | | preference_category(maxint,animation). |
| 1892 | | preference_category(minint,animation). |
| 1893 | | preference_category(globalsets_fdrange,animation). |
| 1894 | | preference_category(do_invariant_checking,advanced). |
| 1895 | | preference_category(do_assert_checking,advanced). |
| 1896 | | %preference_category(do_full_invariant_checking,animation). |
| 1897 | | %preference_category(use_new_kernel,advanced). |
| 1898 | | preference_category(find_abort_values,animation). |
| 1899 | | preference_category(raise_abort_immediately,advanced). |
| 1900 | | preference_category(treat_outermost_pre_as_select,animation). |
| 1901 | | preference_category(require_operations_to_assign_all_outputs,animation). |
| 1902 | | preference_category(allow_operations_to_read_outputs,advanced). |
| 1903 | | preference_category(allow_operation_calls_for_uses,advanced). |
| 1904 | | preference_category(allow_overriding_initialisation,advanced). |
| 1905 | | preference_category(allow_simultaneous_assignments,hidden). % only useful for loading and inspecting AST |
| 1906 | | preference_category(allow_arith_operators_on_reals,advanced). |
| 1907 | | preference_category(solver_for_reals,advanced). |
| 1908 | | preference_category(cspm_animate_all_processes_without_arguments,csp_prefs). |
| 1909 | | preference_category(cspm_animate_all_processes,csp_prefs). |
| 1910 | | %preference_category(cspm_display_inout,csp_prefs). |
| 1911 | | preference_category(cspm_detailed_animation,csp_prefs). |
| 1912 | | preference_category(cspm_strip_source_location,csp_prefs). |
| 1913 | | %preference_category(csp_event_visible_to_user,csp_prefs). |
| 1914 | | %preference_category(cspm_allow_incomplete_records,csp_prefs). |
| 1915 | | %preference_category(findOnlyOneSol,advanced). |
| 1916 | | preference_category(show_eventb_any_arguments,animation). |
| 1917 | | preference_category(maxNrOfInitialisations,animation). |
| 1918 | | preference_category(randomisedRestartInitalisations,advanced). |
| 1919 | | preference_category(maxNrOfEnablingsPerOperation,animation). |
| 1920 | | preference_category(time_out,animation). |
| 1921 | | preference_category(number_animated_abstractions,animation). |
| 1922 | | preference_category(number_skipped_refined_machines,animation). |
| 1923 | | preference_category(show_initialisation_arguments,animation). |
| 1924 | | preference_category(deterministic_trace_replay,hidden). |
| 1925 | | %preference_category(animate_skip_operations,animation). |
| 1926 | | preference_category(debug_time_out_factor,advanced). |
| 1927 | | %preference_category(use_large_jvm_for_parser,advanced). |
| 1928 | | preference_category(jvm_parser_heap_size_mb,advanced). |
| 1929 | | preference_category(jvm_parser_additional_args,advanced). |
| 1930 | | preference_category(jvm_parser_position_infos,advanced). |
| 1931 | | preference_category(jvm_parser_fastrw,hidden). |
| 1932 | | preference_category(jvm_parser_force_parsing,bool). |
| 1933 | | preference_category(convert_comprehension_sets_into_closures,animation). |
| 1934 | | preference_category(comprehension_set_symbolic_limit,animation). |
| 1935 | | preference_category(use_clpfd_solver,animation). |
| 1936 | | preference_category(clpfd_solver_label_option,advanced). |
| 1937 | | preference_category(use_chr_solver,animation). |
| 1938 | | preference_category(data_validation_mode,advanced). |
| 1939 | | preference_category(use_smt_mode,advanced). |
| 1940 | | preference_category(solver_strength,advanced). |
| 1941 | | preference_category(use_common_subexpression_elimination,advanced). |
| 1942 | | preference_category(remove_implied_constraints,advanced). |
| 1943 | | preference_category(lift_existential_quantifiers,advanced). |
| 1944 | | preference_category(use_common_subexpression_also_for_predicates,advanced). |
| 1945 | | preference_category(use_common_subexpression_also_for_substitutions,advanced). |
| 1946 | | preference_category(use_common_subexpression_wd_only,advanced). |
| 1947 | | preference_category(normalize_ast,hidden). |
| 1948 | | preference_category(normalize_ast_sort_commutative,hidden). |
| 1949 | | preference_category(optimize_ast,advanced). |
| 1950 | | %preference_category(optimize_enum_set_elems,hidden). |
| 1951 | | preference_category(useless_code_elimination,advanced). |
| 1952 | | preference_category(compile_while_body,advanced). |
| 1953 | | preference_category(expand_becomes_such_into_set,advanced). |
| 1954 | | preference_category(detect_lambdas,advanced). |
| 1955 | | preference_category(auto_detect_theory_ops,advanced). |
| 1956 | | preference_category(ltsmin_guard_splitting,hidden). |
| 1957 | | preference_category(ltsmin_do_not_evaluate_top_level_guards,hidden). |
| 1958 | | preference_category(fail_if_clpfd_timeout,advanced). |
| 1959 | | %preference_category(allow_recursive_closures,hidden). |
| 1960 | | preference_category(use_static_ordering,advanced). |
| 1961 | | preference_category(try_use_state_packing,advanced). |
| 1962 | | preference_category(use_state_packing,hidden). % derived from try_use_state_packing |
| 1963 | | preference_category(force_state_packing_for_closures,hidden). |
| 1964 | | preference_category(provide_trace_information,advanced). |
| 1965 | | preference_category(prob_profiling_on,advanced). |
| 1966 | | preference_category(prob_source_profiling_on,advanced). |
| 1967 | | preference_category(performance_monitoring_on,advanced). |
| 1968 | | preference_category(performance_monitoring_expansion_limit,advanced). |
| 1969 | | preference_category(partition_predicates,advanced). |
| 1970 | | preference_category(partition_predicates_inline_equalities,advanced). |
| 1971 | | preference_category(use_closure_expansion_memoization,advanced). |
| 1972 | | preference_category(use_function_memoization,advanced). |
| 1973 | | preference_category(allow_incomplete_partial_setup_constants,advanced). |
| 1974 | | preference_category(re_execute_operations_with_side_effects,advanced). |
| 1975 | | preference_category(warn_if_definition_hides_variable,advanced). |
| 1976 | | preference_category(type_check_definitions,advanced). |
| 1977 | | %preference_category(warn_when_expanding_infinite_closures,advanced). |
| 1978 | | preference_category(allow_enumeration_of_infinite_types,advanced). |
| 1979 | | preference_category(strict_raise_warnings,advanced). |
| 1980 | | preference_category(strict_raise_enum_warnings,hidden). % only for testing |
| 1981 | | preference_category(clash_strict_checks,advanced). |
| 1982 | | preference_category(perform_stricter_static_checks,hidden). % set by prob |
| 1983 | | preference_category(ignore_prj_types,advanced). |
| 1984 | | %preference_category(never_convert_closures_into_explicit_form,hidden). |
| 1985 | | %preference_category(convert_types_into_closures,animation). |
| 1986 | | %preference_category(convert_closures_into_explicit_form_for_store,animation). |
| 1987 | | %preference_category(allow_empty_global_sets,advanced). |
| 1988 | | preference_category(ignore_hash_collisions,advanced). |
| 1989 | | preference_category(forget_state_space,advanced). |
| 1990 | | preference_category(store_only_one_incoming_transition,advanced). |
| 1991 | | preference_category(mc_continue_after_error,hidden). |
| 1992 | | %preference_category(enable_permutation_reducation,advanced). |
| 1993 | | %preference_category(use_symmetry_marker_hash,advanced). |
| 1994 | | %preference_category(enable_canonical_symmetry,advanced). |
| 1995 | | %preference_category(use_nauty_symmetry_reduction,advanced). |
| 1996 | | preference_category(symmetry_mode,hidden). |
| 1997 | | preference_category(use_static_symmetry_detection,advanced). |
| 1998 | | %preference_category(bool_expression_as_predicate,hidden). |
| 1999 | | preference_category(allow_untyped_identifiers,hidden). |
| 2000 | | preference_category(repl_unicode,syntax_highlighting). |
| 2001 | | preference_category(repl_cache_parsing,hidden). |
| 2002 | | preference_category(cache_constants,hidden). |
| 2003 | | preference_category(cache_operations,hidden). |
| 2004 | | preference_category(cache_operations_runtime_limit,hidden). |
| 2005 | | preference_category(latex_encoding,latex). |
| 2006 | | preference_category(latex_pp_greek_ids,latex). |
| 2007 | | preference_category(xml_encoding,hidden). |
| 2008 | | preference_category(view_probcli_errors_using_bbresults,hidden). |
| 2009 | | preference_category(eventtrace,animation). |
| 2010 | | preference_category(store_event_transinfo,hidden). % automatically set by probcli |
| 2011 | | preference_category(use_solver_on_load,hidden). % hidden for the moment |
| 2012 | | %preference_category(try_kodkod_on_load,hidden). |
| 2013 | | preference_category(kodkod_for_components,advanced). |
| 2014 | | preference_category(kodkod_raise_warnings,advanced). |
| 2015 | | preference_category(kodkod_max_nr_solutions,advanced). |
| 2016 | | preference_category(kodkod_symmetry_level,advanced). |
| 2017 | | preference_category(kodkod_sat_solver,advanced). |
| 2018 | | preference_category(smt_supported_interpreter,advanced). |
| 2019 | | preference_category(sat_supported_interpreter,advanced). |
| 2020 | | preference_category(use_record_construction,advanced). |
| 2021 | | preference_category(seen_machines_included,animation). |
| 2022 | | preference_category(allow_sequence_operators_on_strings,animation). |
| 2023 | | |
| 2024 | | %preference_category(test_case_gen_stop_at_first_error,advanced). |
| 2025 | | preference_category(prefix_internal_operation_arguments,advanced). |
| 2026 | | preference_category(generate_minimal_nr_of_testcases,advanced). |
| 2027 | | preference_category(use_tk_custom_state_viewer,hidden). % actually : if user wants to turn it off; simply do not define ANIMATION_FUNCTION |
| 2028 | | preference_category(tk_custom_state_viewer_font_name,hidden). |
| 2029 | | preference_category(tk_custom_state_viewer_font_size,hidden). |
| 2030 | | preference_category(tk_custom_state_viewer_padding,animation). |
| 2031 | | preference_category(tk_custom_state_viewer_str_padding,animation). |
| 2032 | | preference_category(use_small_window,animation). |
| 2033 | | preference_category(tk_show_source_pane,animation). |
| 2034 | | |
| 2035 | | preference_category(path_to_ltsmin,advanced). |
| 2036 | | |
| 2037 | | |
| 2038 | | preference_category(dot_print_node_ids,dot). |
| 2039 | | preference_category(dot_print_transition_ids,dot). |
| 2040 | | preference_category(dot_print_use_constants,dot). |
| 2041 | | preference_category(dot_print_node_info,dot). |
| 2042 | | preference_category(dot_print_edge_labels,dot). |
| 2043 | | preference_category(dot_print_action_arguments,dot). |
| 2044 | | preference_category(dot_print_functions,dot). |
| 2045 | | preference_category(dot_print_self_loops,dot). |
| 2046 | | preference_category(dot_print_root,dot). |
| 2047 | | %preference_category(dot_print_leaves,dot). |
| 2048 | | preference_category(dot_print_arc_colors,dot). |
| 2049 | | preference_category(dot_use_ps_viewer,hidden). |
| 2050 | | preference_category(path_to_dotty,dot). |
| 2051 | | preference_category(path_to_dot,dot). |
| 2052 | | preference_category(dot_default_engine,dot). |
| 2053 | | preference_category(path_to_ps_viewer,dot). |
| 2054 | | preference_category(dot_root_shape,dot). |
| 2055 | | preference_category(dot_node_penwidth,dot). |
| 2056 | | preference_category(dot_edge_penwidth,dot). |
| 2057 | | preference_category(dot_normal_node_shape,dot). |
| 2058 | | preference_category(dot_current_node_shape,dot). |
| 2059 | | preference_category(dot_open_node_colour,dot). |
| 2060 | | preference_category(dot_scope_limit_node_colour,dot). |
| 2061 | | preference_category(dot_normal_node_colour,dot). |
| 2062 | | preference_category(dot_invariant_violated_node_colour,dot). |
| 2063 | | preference_category(dot_fill_normal_nodes,dot). |
| 2064 | | preference_category(dot_normal_arc_colour,dot). |
| 2065 | | |
| 2066 | | %preference_category(dot_font_size,hidden). |
| 2067 | | preference_category(dot_node_font_size,dot). |
| 2068 | | preference_category(dot_edge_font_size,dot). |
| 2069 | | preference_category(dot_with_page_size,dot). |
| 2070 | | preference_category(dot_horizontal_layout,dot). |
| 2071 | | preference_category(dot_colour_goal_nodes,dot). |
| 2072 | | preference_category(dot_goal_node_colour,dot). |
| 2073 | | preference_category(dot_print_node_properties,dot). |
| 2074 | | preference_category(dot_counterexample_node_colour,dot). |
| 2075 | | preference_category(dot_counterexample_op_colour,dot). |
| 2076 | | |
| 2077 | | % preferences used by rule_validation.pl for rule dependency graph: |
| 2078 | | preference_category(successful_rule_colour,rule_dependency_graph). |
| 2079 | | preference_category(failed_rule_colour,rule_dependency_graph). |
| 2080 | | preference_category(disabled_rule_colour,rule_dependency_graph). |
| 2081 | | preference_category(not_checked_rule_colour,rule_dependency_graph). |
| 2082 | | preference_category(rule_graph_shape,rule_dependency_graph). |
| 2083 | | preference_category(executed_computation_colour,rule_dependency_graph). |
| 2084 | | preference_category(not_executed_computation_colour,rule_dependency_graph). |
| 2085 | | preference_category(disabled_computation_colour,rule_dependency_graph). |
| 2086 | | preference_category(computation_graph_shape,rule_dependency_graph). |
| 2087 | | preference_category(succeeded_dependency_colour,rule_dependency_graph). |
| 2088 | | preference_category(failed_dependency_colour,rule_dependency_graph). |
| 2089 | | preference_category(normal_dependency_colour,rule_dependency_graph). |
| 2090 | | |
| 2091 | | preference_category(dot_event_hierarchy_horizontal,dot_event_hierarchy). |
| 2092 | | preference_category(dot_event_hierarchy_machine_colour,dot_event_hierarchy). |
| 2093 | | preference_category(dot_event_hierarchy_refines_colour,dot_event_hierarchy). |
| 2094 | | preference_category(dot_event_hierarchy_new_event_colour,dot_event_hierarchy). |
| 2095 | | preference_category(dot_event_hierarchy_rename_event_colour,dot_event_hierarchy). |
| 2096 | | preference_category(dot_event_hierarchy_unchanged_event_colour,dot_event_hierarchy). |
| 2097 | | preference_category(dot_event_hierarchy_rename_unchanged_event_colour,dot_event_hierarchy). |
| 2098 | | preference_category(dot_event_hierarchy_grd_strengthening_event_colour,dot_event_hierarchy). |
| 2099 | | preference_category(dot_event_hierarchy_grd_keeping_event_colour,dot_event_hierarchy). |
| 2100 | | preference_category(dot_event_hierarchy_edge_colour,dot_event_hierarchy). |
| 2101 | | preference_category(dot_event_hierarchy_extends_colour,dot_event_hierarchy). |
| 2102 | | preference_category(dot_hierarchy_show_extra_detail,dot_event_hierarchy). |
| 2103 | | |
| 2104 | | |
| 2105 | | preference_category(dot_projection_non_det_edge_colour,dot_projection). |
| 2106 | | preference_category(dot_projection_det_edge_colour,dot_projection). |
| 2107 | | preference_category(dot_projection_non_definite_edge_style,dot_projection). |
| 2108 | | preference_category(dot_projection_definite_edge_style,dot_projection). |
| 2109 | | preference_category(dot_projection_label_limit,dot_projection). |
| 2110 | | preference_category(dot_projection_process_only_explored,dot_projection). |
| 2111 | | preference_category(dot_use_unicode,dot_projection). |
| 2112 | | |
| 2113 | | preference_category(dot_predicate_node_shape,dot_formula_tree). |
| 2114 | | preference_category(dot_expression_node_shape,dot_formula_tree). |
| 2115 | | preference_category(dot_var_mod_hide_only_written,dot_variable_modification). |
| 2116 | | |
| 2117 | | preference_category(mc_dc_default_level,mc_dc_commands). |
| 2118 | | |
| 2119 | | preference_category(dot_enabling_show_readwrites,dot). |
| 2120 | | |
| 2121 | | preference_category(dot_definitions_use_sub_graph,dot_definitions). |
| 2122 | | preference_category(dot_definitions_show_all,dot_definitions). |
| 2123 | | |
| 2124 | | preference_category(dot_state_graph_decompose,dot_state_graph). |
| 2125 | | |
| 2126 | | preference_category(dot_hierarchy_max_ids,dot_machine_hierarchy). |
| 2127 | | preference_category(cbc_provide_explanations,cbc_commands). |
| 2128 | | |
| 2129 | | preference_category(font_size,gui_prefs). |
| 2130 | | preference_category(font_name,gui_prefs). |
| 2131 | | preference_category(font_size_only,gui_prefs). |
| 2132 | | preference_category(use_font_size_for_columns,advanced). |
| 2133 | | preference_category(allow_source_code_editing,gui_prefs). |
| 2134 | | preference_category(show_line_numbers,gui_prefs). |
| 2135 | | preference_category(highlight_brackets,gui_prefs). |
| 2136 | | preference_category(highlight_current_line,gui_prefs). |
| 2137 | | preference_category(ask_when_content_changed,gui_prefs). |
| 2138 | | preference_category(user_not_beginner,gui_prefs). |
| 2139 | | |
| 2140 | | preference_category(user_is_an_expert_with_accessto_source_distribution,hidden). |
| 2141 | | %preference_category(default_to_runtime_type_checking_on_startup_for_expert,hidden). |
| 2142 | | preference_category(path_to_probe,csp_prefs). |
| 2143 | | %preference_category(path_to_fuzz,advanced). |
| 2144 | | preference_category(path_to_fdr,csp_prefs). |
| 2145 | | preference_category(path_to_csp_typechecker,csp_prefs). |
| 2146 | | preference_category(path_to_bcomp,advanced). |
| 2147 | | preference_category(path_to_java,advanced). |
| 2148 | | preference_category(path_to_java_parser,hidden). |
| 2149 | | preference_category(path_to_atb_krt,advanced). % not yet used from within ProB Tcl/Tk, ... |
| 2150 | | preference_category(try_atb_provers,advanced). |
| 2151 | | preference_category(smtlib2b_arrays_as_sets,smtlib2b). |
| 2152 | | preference_category(smtlib2b_cleanup_predicate,smtlib2b). |
| 2153 | | preference_category(symbolic_mc_try_other_solvers,advanced). |
| 2154 | | preference_category(path_to_spin,advanced). |
| 2155 | | preference_category(path_to_cspm,advanced). |
| 2156 | | preference_category(path_to_text_editor,advanced). |
| 2157 | | preference_category(path_to_text_editor_launch,hidden). |
| 2158 | | preference_category(number_of_recent_documents,advanced). |
| 2159 | | preference_category(number_of_searched_patterns,advanced). |
| 2160 | | preference_category(number_of_replaced_patterns,advanced). |
| 2161 | | preference_category(number_of_eval_history_elements,advanced). |
| 2162 | | preference_category(number_of_eval_csp_history_elements,advanced). |
| 2163 | | preference_category(number_of_checked_ltl_formulas,advanced). |
| 2164 | | preference_category(allow_new_ops_in_refinement,advanced). |
| 2165 | | preference_category(allow_local_operation_calls,advanced). |
| 2166 | | preference_category(allow_operation_calls_in_expr,advanced). |
| 2167 | | preference_category(allow_let_to_reuse_introduced_ids,advanced). |
| 2168 | | preference_category(use_po,advanced). |
| 2169 | | preference_category(try_operation_reuse,advanced). |
| 2170 | | preference_category(try_operation_reuse_for_invariants,advanced). |
| 2171 | | preference_category(operation_reuse_setting,hidden). |
| 2172 | | preference_category(randomise_operation_order,advanced). |
| 2173 | | preference_category(randomise_enumeration_order,advanced). |
| 2174 | | preference_category(perform_enumeration_order_analysis,advanced). |
| 2175 | | preference_category(set_rand,advanced). |
| 2176 | | preference_category(rand_seed,advanced). |
| 2177 | | preference_category(ltl_to_ba_tool,advanced). |
| 2178 | | preference_category(path_to_clingo,advanced). |
| 2179 | | |
| 2180 | | preference_category(do_syntax_highlighting,syntax_highlighting). |
| 2181 | | preference_category(sh_type_colour,syntax_highlighting). |
| 2182 | | preference_category(sh_logical_colour,syntax_highlighting). |
| 2183 | | preference_category(sh_assignments_colour,syntax_highlighting). |
| 2184 | | preference_category(sh_operators,syntax_highlighting). |
| 2185 | | preference_category(sh_top_level_keywords,syntax_highlighting). |
| 2186 | | preference_category(sh_control_keywords,syntax_highlighting). |
| 2187 | | %preference_category(sh_includes_keywords,syntax_highlighting). |
| 2188 | | preference_category(sh_comments,syntax_highlighting). |
| 2189 | | preference_category(sh_pragmas,syntax_highlighting). |
| 2190 | | preference_category(sh_unsupported_background,syntax_highlighting). |
| 2191 | | |
| 2192 | | preference_category(expand_forall_upto,advanced). |
| 2193 | | preference_category(double_evaluation_when_analysing,advanced). |
| 2194 | | preference_category(prob_safe_mode,advanced). |
| 2195 | | preference_category(expand_avl_upto,advanced). |
| 2196 | | preference_category(show_bvisual_formula_functor_from,advanced). |
| 2197 | | preference_category(show_bvisual_proof_info_icons,advanced). |
| 2198 | | preference_category(show_bvisual_formula_explanations,advanced). |
| 2199 | | preference_category(formula_tree_minimal_timeout,dot_formula_tree). |
| 2200 | | preference_category(formula_tree_maximal_timeout,dot_formula_tree). |
| 2201 | | preference_category(show_function_tuples_in_property,animation). |
| 2202 | | preference_category(bugly_pp_scrambling,advanced). |
| 2203 | | preference_category(pp_propositional_logic_mode,hidden). |
| 2204 | | preference_category(pp_wd_infos,hidden). |
| 2205 | | preference_category(pp_with_terminal_colour,hidden). |
| 2206 | | preference_category(wd_ignore_external_funs,wd_analyser). |
| 2207 | | preference_category(wd_skip_finite_pos,wd_analyser). |
| 2208 | | preference_category(wd_analysis_for_animation,wd_analyser). |
| 2209 | | preference_category(z3_solve_for_animation,advanced). |
| 2210 | | preference_category(add_wd_pos_for_z3,advanced). |
| 2211 | | preference_category(do_not_print_wd_errors,hidden). % set by unsat core or by solver_interface |
| 2212 | | %preference_category(show_full_error_span,hidden). |
| 2213 | | |
| 2214 | | preference_category(machines_path,hidden). |
| 2215 | | |
| 2216 | | preference_category(alloy_use_implementable_integers,alloy2b). |
| 2217 | | preference_category(alloy_scopeless_translation,alloy2b). |
| 2218 | | preference_category(alloy_translation_for_proof,alloy2b). |
| 2219 | | preference_category(alloy_strict_integers,alloy2b). |
| 2220 | | |
| 2221 | | /* Partial techniques for optimising the Model Checker */ |
| 2222 | | |
| 2223 | | preference_category(use_scope_predicate,advanced). |
| 2224 | | preference_category(use_ignore_pragmas,advanced). |
| 2225 | | %preference_category(pge,model_checker). |
| 2226 | | |
| 2227 | | preference_category(use_cbc_analysis,advanced). % for por |
| 2228 | | preference_category(timeout_cbc_analysis,advanced). |
| 2229 | | preference_category(por,model_checker). |
| 2230 | | preference_category(por_heur,model_checker). |
| 2231 | | preference_category(use_safety_ltl_model_checker,model_checker). |
| 2232 | | preference_category(enable_graph,model_checker). |
| 2233 | | preference_category(enable_graph_depth,model_checker). |
| 2234 | | preference_category(dependency_enable_predicates,model_checker). |
| 2235 | | |
| 2236 | | preference_category(path_to_latex,latex). |
| 2237 | | |
| 2238 | | %------------------------------------ |
| 2239 | | |
| 2240 | | preference_category(filter_unused_constants,advanced). |
| 2241 | | preference_category(translate_force_all_typing_infos,hidden). |
| 2242 | | preference_category(translate_print_typing_infos,hidden). |
| 2243 | | preference_category(translate_print_frozen_infos,hidden). |
| 2244 | | preference_category(translate_ids_to_parseable_format,hidden). |
| 2245 | | preference_category(translate_suppress_rodin_positions_flag,hidden). |
| 2246 | | preference_category(translate_print_all_sequences,hidden). |
| 2247 | | preference_category(translate_print_cs_style_sequences,hidden). |
| 2248 | | |
| 2249 | | preference_category(translation_limit_for_table_commands,wd_commands). |
| 2250 | | preference_category(visb_allow_variables_for_objects,visb). |
| 2251 | | preference_category(visb_show_debug_infos,visb). |
| 2252 | | |
| 2253 | | preference_category(trace_generation_limit,trace_generator). |
| 2254 | | preference_category(trace_generation_time_out,trace_generator). |
| 2255 | | |
| 2256 | | preference_category(disprover_mode,advanced). |
| 2257 | | preference_category(allow_improving_wd_mode,hidden). |
| 2258 | | preference_category(trace_upon_error,hidden). |
| 2259 | | preference_category(error_log_file,advanced). |
| 2260 | | preference_category(tlc_number_of_workers,hidden). |
| 2261 | | preference_category(tlc_use_prob_constant_setup,hidden). |
| 2262 | | |
| 2263 | | preference_category(port, distb). |
| 2264 | | preference_category(ip, distb). |
| 2265 | | preference_category(max_states, distb). |
| 2266 | | preference_category(tmpdir, distb). |
| 2267 | | preference_category(logdir, distb). |
| 2268 | | preference_category(proxynumber, distb). |
| 2269 | | preference_category(queue_threshold, distb). |
| 2270 | | preference_category(hash_cycle, distb). |
| 2271 | | |
| 2272 | | preference_category(cdclt_perform_static_analysis, cdclt). |
| 2273 | | preference_category(cdclt_perform_symmetry_breaking, cdclt). |
| 2274 | | preference_category(cdclt_use_idl_theory_solver,cdclt). |
| 2275 | | |
| 2276 | | preference_category(prob_version_info,hidden). |
| 2277 | | preference_category(prob_revision_info, hidden). |
| 2278 | | preference_category(prob_lastchangedate_info, hidden). |
| 2279 | | |
| 2280 | | preference_category(xtl_safe_mode,hidden). |
| 2281 | | |
| 2282 | | /* ------------------------- */ |
| 2283 | | |
| 2284 | | % secondary, alternate additional categories: |
| 2285 | | alternate_preference_category(dot_print_node_ids,dot_state_space). |
| 2286 | | alternate_preference_category(dot_print_transition_ids,dot_state_space). |
| 2287 | | alternate_preference_category(dot_print_use_constants,dot_state_space). %? |
| 2288 | | alternate_preference_category(dot_print_node_info,dot_state_space). |
| 2289 | | alternate_preference_category(dot_print_edge_labels,dot_state_space). |
| 2290 | | alternate_preference_category(dot_print_action_arguments,dot_state_space). |
| 2291 | | alternate_preference_category(dot_print_functions,dot_state_space). |
| 2292 | | alternate_preference_category(dot_print_self_loops,dot_state_space). |
| 2293 | | alternate_preference_category(dot_print_root,dot_state_space). |
| 2294 | | alternate_preference_category(dot_print_arc_colors,dot_state_space). |
| 2295 | | alternate_preference_category(dot_root_shape,dot_state_space). |
| 2296 | | alternate_preference_category(dot_node_penwidth,dot_state_space). |
| 2297 | | alternate_preference_category(dot_edge_penwidth,dot_state_space). |
| 2298 | | alternate_preference_category(dot_normal_node_shape,dot_state_space). |
| 2299 | | alternate_preference_category(dot_current_node_shape,dot_state_space). |
| 2300 | | alternate_preference_category(dot_open_node_colour,dot_state_space). |
| 2301 | | alternate_preference_category(dot_scope_limit_node_colour,dot_state_space). |
| 2302 | | alternate_preference_category(dot_normal_node_colour,dot_state_space). |
| 2303 | | alternate_preference_category(dot_invariant_violated_node_colour,dot_state_space). |
| 2304 | | alternate_preference_category(dot_fill_normal_nodes,dot_state_space). |
| 2305 | | alternate_preference_category(dot_normal_arc_colour,dot_state_space). |
| 2306 | | alternate_preference_category(dot_node_font_size,dot_state_space). |
| 2307 | | alternate_preference_category(dot_edge_font_size,dot_state_space). |
| 2308 | | alternate_preference_category(dot_colour_goal_nodes,dot_state_space). |
| 2309 | | alternate_preference_category(dot_goal_node_colour,dot_state_space). |
| 2310 | | alternate_preference_category(dot_print_node_properties,dot_state_space). |
| 2311 | | alternate_preference_category(dot_horizontal_layout,dot_state_space). |
| 2312 | | |
| 2313 | | alternate_preference_category(dot_use_unicode,dot_formula_tree). |
| 2314 | | |
| 2315 | | alternate_preference_category(dot_event_hierarchy_unchanged_event_colour,dot_variable_hierarchy). |
| 2316 | | alternate_preference_category(dot_event_hierarchy_new_event_colour,dot_variable_hierarchy). |
| 2317 | | alternate_preference_category(dot_event_hierarchy_edge_colour,dot_variable_hierarchy). |
| 2318 | | alternate_preference_category(dot_hierarchy_show_extra_detail,dot_variable_hierarchy). |
| 2319 | | |
| 2320 | | % these commands for the graph_canon / state_as_dot_graph state_graph: |
| 2321 | | alternate_preference_category(dot_normal_node_shape,state_as_graph). |
| 2322 | | alternate_preference_category(dot_state_graph_decompose,state_as_graph). |
| 2323 | | %alternate_preference_category(dot_with_page_size,state_as_graph). |
| 2324 | | alternate_preference_category(dot_horizontal_layout,state_as_graph). |
| 2325 | | |
| 2326 | | % these commands use the dot_graph_generator: |
| 2327 | | alternate_preference_category(X,dot_variable_modification) :- alternate_preference_category(X,dot_graph_generator). |
| 2328 | | alternate_preference_category(X,dot_event_hierarchy) :- alternate_preference_category(X,dot_graph_generator). |
| 2329 | | alternate_preference_category(X,dot_variable_hierarchy) :- alternate_preference_category(X,dot_graph_generator). |
| 2330 | | alternate_preference_category(X,dot_projection) :- alternate_preference_category(X,dot_graph_generator). |
| 2331 | | alternate_preference_category(dot_print_self_loops,dot_projection). |
| 2332 | | alternate_preference_category(X,dot_definitions) :- alternate_preference_category(X,dot_graph_generator). |
| 2333 | | alternate_preference_category(timeout_cbc_analysis,dot_enable_graph). |
| 2334 | | alternate_preference_category(X,dot_enable_graph) :- alternate_preference_category(X,dot_graph_generator). |
| 2335 | | |
| 2336 | | % preferences used by dot_graph_generator.pl: |
| 2337 | | alternate_preference_category(dot_print_self_loops,dot_graph_generator). |
| 2338 | | alternate_preference_category(dot_print_arc_colors,dot_graph_generator). |
| 2339 | | alternate_preference_category(dot_node_font_size,dot_graph_generator). |
| 2340 | | alternate_preference_category(dot_edge_font_size,dot_graph_generator). |
| 2341 | | alternate_preference_category(dot_edge_penwidth,dot_graph_generator). |
| 2342 | | alternate_preference_category(dot_with_page_size,dot_graph_generator). |
| 2343 | | alternate_preference_category(dot_horizontal_layout,dot_graph_generator). |
| 2344 | | alternate_preference_category(dot_default_engine,dot_graph_generator). |
| 2345 | | alternate_preference_category(path_to_dot,dot_graph_generator). |
| 2346 | | |
| 2347 | | alternate_preference_category(translation_limit_for_table_commands,cbc_commands). |
| 2348 | | alternate_preference_category(translation_limit_for_table_commands,table_commands). |
| 2349 | | |
| 2350 | | /* ------------------------- */ |
| 2351 | | % now in basic_tests.pl |
| 2352 | | %:- assert_must_succeed( \+((preferences:obsolete_preference(P),preference_default_value(P,_Val)))). |
| 2353 | | obsolete_preference(optimize_enum_set_elems). |
| 2354 | | obsolete_preference(warn_when_expanding_infinite_closures). |
| 2355 | | obsolete_preference(do_neginvariant_checking). % use double_evaluation_when_analysing |
| 2356 | | obsolete_preference(check_prolog_b_ast). |
| 2357 | | obsolete_preference(use_large_jvm_for_parser). |
| 2358 | | obsolete_preference(default_to_runtime_type_checking_on_startup_for_expert). |
| 2359 | | obsolete_preference(animate_skip_operations). |
| 2360 | | obsolete_preference(debug_try_minimise). |
| 2361 | | obsolete_preference(convert_types_into_closures). |
| 2362 | | obsolete_preference(use_avl_trees_for_sets). |
| 2363 | | obsolete_preference(dot_font_size). |
| 2364 | | obsolete_preference(only_label_base_types). |
| 2365 | | obsolete_preference(use_new_kernel). |
| 2366 | | obsolete_preference(findOnlyOneSol). |
| 2367 | | obsolete_preference(enable_permutation_reducation). |
| 2368 | | obsolete_preference(use_symmetry_marker_hash). |
| 2369 | | obsolete_preference(enable_canonical_symmetry). |
| 2370 | | obsolete_preference(use_nauty_symmetry_reduction). |
| 2371 | | obsolete_preference(do_full_invariant_checking). |
| 2372 | | obsolete_preference(test_case_gen_stop_at_first_error). |
| 2373 | | obsolete_preference(use_failure_refinement). |
| 2374 | | obsolete_preference(do_on_the_fly_refinement). |
| 2375 | | obsolete_preference(never_convert_closures_into_explicit_form). |
| 2376 | | obsolete_preference(allow_empty_global_sets). |
| 2377 | | obsolete_preference(multilevel_animation). |
| 2378 | | obsolete_preference(remove_multilevel_prefix). |
| 2379 | | obsolete_preference(cspm_allow_incomplete_records). |
| 2380 | | obsolete_preference(cspm_display_inout). |
| 2381 | | obsolete_preference(allow_recursive_closures). |
| 2382 | | obsolete_preference(absint_abstract_domain_module). |
| 2383 | | obsolete_preference(absint_use_widening). |
| 2384 | | obsolete_preference(absint_soft_widening). |
| 2385 | | obsolete_preference(absint_extrapolation_threshold). |
| 2386 | | obsolete_preference(convert_closures_into_explicit_form_for_store). |
| 2387 | | obsolete_preference(use_por). |
| 2388 | | obsolete_preference(use_pge). |
| 2389 | | obsolete_preference(pge_dis). |
| 2390 | | obsolete_preference(pge_ind). |
| 2391 | | obsolete_preference(pge_keep). |
| 2392 | | obsolete_preference(pge). |
| 2393 | | obsolete_preference(use_pge_keep). |
| 2394 | | obsolete_preference(use_pge_dis). |
| 2395 | | obsolete_preference(use_pge_ind). |
| 2396 | | obsolete_preference(selected_bparser). |
| 2397 | | obsolete_preference(dot_print_leaves). |
| 2398 | | obsolete_preference(csp_event_visible_to_user). |
| 2399 | | obsolete_preference(path_to_fuzz). |
| 2400 | | obsolete_preference(use_optimistic_por). |
| 2401 | | obsolete_preference(show_full_error_span). |
| 2402 | | obsolete_preference(path_to_sfdp). |
| 2403 | | obsolete_preference(dot_use_alterate_dot_viewer). |
| 2404 | | obsolete_preference(path_to_dotty2). |
| 2405 | | obsolete_preference(prob2_trace_file). |
| 2406 | | obsolete_preference(prob2_trace_file_gen_unique_name). |
| 2407 | | obsolete_preference(try_kodkod_on_load). |
| 2408 | | |
| 2409 | | % might be re-included later |
| 2410 | | obsolete_preference(plugin(absint,use_widening)). |
| 2411 | | obsolete_preference(plugin(absint,soft_widening)). |
| 2412 | | obsolete_preference(plugin(absint,extrapolation_threshold)). |
| 2413 | | obsolete_preference(plugin(absint,retract_widening_related_states)). |
| 2414 | | |
| 2415 | | obsolete_preference(use_por_for_ltl). |
| 2416 | | |
| 2417 | | % replaced by api calls |
| 2418 | | obsolete_preference(path_to_smt_solver). |
| 2419 | | |
| 2420 | | % has been renamed |
| 2421 | | obsolete_preference(try_atb_provers_for_smtlib). |
| 2422 | | |
| 2423 | | obsolete_preference(bool_expression_as_predicate). % BOOL_AS_PREDICATE |
| 2424 | | |
| 2425 | | |
| 2426 | | % VOLATILE |
| 2427 | | % not necessary to store in file; value will not be changed when loading pref file |
| 2428 | | % dangerous preferences: user should explicitly reset it every time or put it explicitly into file |
| 2429 | | volatile_preference(store_event_transinfo). |
| 2430 | | volatile_preference(fail_if_clpfd_timeout). |
| 2431 | | volatile_preference(ignore_hash_collisions). |
| 2432 | | volatile_preference(forget_state_space). |
| 2433 | | volatile_preference(store_only_one_incoming_transition). |
| 2434 | | volatile_preference(mc_continue_after_error). |
| 2435 | | volatile_preference(filter_unused_constants). |
| 2436 | | volatile_preference(disprover_mode). |
| 2437 | | volatile_preference(allow_improving_wd_mode). |
| 2438 | | volatile_preference(trace_upon_error). |
| 2439 | | volatile_preference(performance_monitoring_on). |
| 2440 | | volatile_preference(translate_force_all_typing_infos). |
| 2441 | | volatile_preference(translate_print_typing_infos). |
| 2442 | | volatile_preference(translate_ids_to_parseable_format). |
| 2443 | | volatile_preference(translate_suppress_rodin_positions_flag). |
| 2444 | | volatile_preference(deterministic_trace_replay). |
| 2445 | | %volatile_preference(bool_expression_as_predicate). % Deprecated |
| 2446 | | volatile_preference(prob_version_info). |
| 2447 | | volatile_preference(prob_revision_info). |
| 2448 | | volatile_preference(prob_lastchangedate_info). |
| 2449 | | volatile_preference(path_to_java_parser). |
| 2450 | | volatile_preference(do_not_print_wd_errors). % set by unsat core |
| 2451 | | volatile_preference(operation_reuse_setting). % computed |
| 2452 | | volatile_preference(use_state_packing). % computed |
| 2453 | | |
| 2454 | | read_only_preference(prob_version_info). |
| 2455 | | read_only_preference(prob_revision_info). |
| 2456 | | read_only_preference(prob_lastchangedate_info). |
| 2457 | | |
| 2458 | | /* ------------------------- */ |
| 2459 | ? | is_of_type(El,Type) :- type_element(Type,El). |
| 2460 | | |
| 2461 | | type_element(bool,X) :- !, (X=true -> true ; X=false). |
| 2462 | | type_element(directory_path,X) :- !, atomic(X),check_directory_exists(X). |
| 2463 | | type_element(int,X) :- !, integer(X). |
| 2464 | | type_element(neg,X) :- !, integer(X), X=<0. |
| 2465 | | type_element(nat,X) :- !, integer(X), X>=0. |
| 2466 | | type_element(nat1,X) :- !, integer(X), X>0. |
| 2467 | | type_element(range(Low,Up),X) :- !, number(X), X>=Low, X=<Up. |
| 2468 | | type_element(string,X) :- !, atomic(X). |
| 2469 | | type_element(path,X) :- !, atomic(X). % some paths are files, some directorys (.app) and some aliases |
| 2470 | | type_element(file_path,X) :- !, atomic(X),check_file_exists(X). |
| 2471 | | type_element(term,X) :- !, nonvar(X). |
| 2472 | | type_element(dot_shape,X) :- !, valid_dot_shape(X). |
| 2473 | | type_element(dot_node_style,X) :- !, valid_dot_node_style(X). |
| 2474 | | type_element(dot_line_style,X) :- !, valid_dot_line_style(X). |
| 2475 | ? | type_element(rgb_color,X) :- !, valid_rgb_color(X). |
| 2476 | ? | type_element(ListOfCsts,X) :- ListOfCsts=[_|_], !, member(X,ListOfCsts). |
| 2477 | ? | type_element(Type,X) :- list_valid_type_vals(Type,List),!, member(X,List). |
| 2478 | | type_element(Type,X) :- pref_type_synonym(Type,List),!, |
| 2479 | ? | is_of_type(X,List). % cvc4 not working |
| 2480 | | |
| 2481 | | pref_type_synonym(por,[off,ample_sets,ample_sets2]). |
| 2482 | | pref_type_synonym(solver_name,[cdclt,clingo,kodkod,prob,sat,'sat-z3',z3,z3cns,z3axm]). |
| 2483 | | pref_type_synonym(text_encoding,[auto, 'ASCII', % ascii not directly listed in manual page, but is on web page below |
| 2484 | | 'ISO-8859-1','ISO-8859-2', |
| 2485 | | 'ISO-8859-15', |
| 2486 | | 'UTF-8','UTF-16','UTF-16LE','UTF-16BE','UTF-32','UTF-32LE','UTF-32BE', |
| 2487 | | 'ANSI_X3.4-1968', 'windows 1252']). |
| 2488 | | % a few more names seem to be allowed (section 4.6.7.5 of SICStus handbook) |
| 2489 | | % few from https://www.iana.org/assignments/character-sets/character-sets.xhtml |
| 2490 | | % using illegal names leads to SPIO_E_CHARSET_NOT_FOUND exception |
| 2491 | | |
| 2492 | | valid_dot_node_style(bold). |
| 2493 | | valid_dot_node_style(dashed). |
| 2494 | | valid_dot_node_style(diagonals). |
| 2495 | | valid_dot_node_style(dotted). |
| 2496 | | valid_dot_node_style(filled). |
| 2497 | | valid_dot_node_style(invisible). |
| 2498 | | valid_dot_node_style(rounded). |
| 2499 | | valid_dot_node_style(solid). |
| 2500 | | valid_dot_node_style(striped). |
| 2501 | | valid_dot_node_style(wedged). |
| 2502 | | valid_dot_node_style(''). % revert to default |
| 2503 | | |
| 2504 | | valid_dot_line_style(bold). |
| 2505 | | valid_dot_line_style(dashed). |
| 2506 | | valid_dot_line_style(dotted). |
| 2507 | | valid_dot_line_style(invis). |
| 2508 | | valid_dot_line_style(solid). |
| 2509 | | valid_dot_line_style(''). |
| 2510 | | |
| 2511 | | valid_dot_shape('Mcircle'). |
| 2512 | | valid_dot_shape('Mdiamond'). |
| 2513 | | valid_dot_shape('Msquare'). |
| 2514 | | valid_dot_shape(box). |
| 2515 | | valid_dot_shape(box3d). % requires newer version of graphviz |
| 2516 | | valid_dot_shape(cds). % requires newer version of graphviz |
| 2517 | | valid_dot_shape(circle). |
| 2518 | | valid_dot_shape(component). % requires newer version of graphviz |
| 2519 | | valid_dot_shape(cylinder). % requires newer version of graphviz |
| 2520 | | valid_dot_shape(diamond). |
| 2521 | | valid_dot_shape(doublecircle). |
| 2522 | | valid_dot_shape(doubleoctagon). |
| 2523 | | valid_dot_shape(egg). |
| 2524 | | valid_dot_shape(ellipse). |
| 2525 | | valid_dot_shape(folder). % requires newer version of graphviz |
| 2526 | | valid_dot_shape(hexagon). |
| 2527 | | valid_dot_shape(house). |
| 2528 | | valid_dot_shape(invhouse). |
| 2529 | | valid_dot_shape(invtrapez). |
| 2530 | | valid_dot_shape(invtrapezium). |
| 2531 | | valid_dot_shape(invtriangle). |
| 2532 | | valid_dot_shape(larrow). % requires newer version of graphviz |
| 2533 | | valid_dot_shape(lpromoter). % requires newer version of graphviz |
| 2534 | | valid_dot_shape(none). |
| 2535 | | valid_dot_shape(note). % requires newer version of graphviz |
| 2536 | | valid_dot_shape(octagon). |
| 2537 | | valid_dot_shape(oval). |
| 2538 | | valid_dot_shape(parallelogram). |
| 2539 | | valid_dot_shape(pentagon). |
| 2540 | | valid_dot_shape(plain). |
| 2541 | | valid_dot_shape(plaintext). |
| 2542 | | valid_dot_shape(point). |
| 2543 | | valid_dot_shape(promoter). % requires newer version of graphviz |
| 2544 | | valid_dot_shape(record). |
| 2545 | | valid_dot_shape(rarrow). % requires newer version of graphviz |
| 2546 | | valid_dot_shape(rect). |
| 2547 | | valid_dot_shape(rectangle). |
| 2548 | | valid_dot_shape(rpromoter). % requires newer version of graphviz |
| 2549 | | valid_dot_shape(septagon). |
| 2550 | | valid_dot_shape(square). |
| 2551 | | valid_dot_shape(star). % requires newer version of graphviz |
| 2552 | | valid_dot_shape(tab). % requires newer version of graphviz |
| 2553 | | valid_dot_shape(trapezium). |
| 2554 | | valid_dot_shape(triangle). |
| 2555 | | valid_dot_shape(tripleoctagon). |
| 2556 | | |
| 2557 | | :- use_module(library(lists),[maplist/2]). |
| 2558 | | valid_rgb_color(X) :- tk_color(X). |
| 2559 | | valid_rgb_color(X) :- % check for composed colors like chocolate3 |
| 2560 | | atom_codes(X,Codes), append(Prefix,[Digit],Codes), |
| 2561 | | Digit >= 48, Digit =< 57, Nr is Digit - 48, atom_codes(ColorName,Prefix), |
| 2562 | | tk_color(ColorName,Low,Up), |
| 2563 | | Nr >= Low, Nr =< Up. |
| 2564 | | valid_rgb_color(X) :- valid_gray(X). |
| 2565 | | valid_rgb_color(X) :- atom(X),atom_codes(X,[35|HexCodes]), |
| 2566 | | length(HexCodes,Len), |
| 2567 | | (Len=6 ; Len=8), % with Alpha codes |
| 2568 | ? | maplist(hex,HexCodes). % should be of the form #ff00ff, optionally with alpha value |
| 2569 | | |
| 2570 | | % colors which also accept numbers at end: |
| 2571 | | tk_color(aquamarine,1,4). |
| 2572 | | tk_color(azure,1,4). |
| 2573 | | tk_color(bisque,1,4). |
| 2574 | | tk_color(blue,1,4). |
| 2575 | | tk_color(brown,1,4). |
| 2576 | | tk_color(burlywood,1,4). |
| 2577 | | tk_color('CadetBlue',1,4). |
| 2578 | | tk_color(chartreuse,1,4). |
| 2579 | | tk_color(chocolate,1,4). |
| 2580 | | tk_color(coral,1,4). |
| 2581 | | tk_color(cornsilk,1,4). |
| 2582 | | tk_color(cyan,1,4). |
| 2583 | | tk_color(deepskyblue,1,4). |
| 2584 | | tk_color('DarkGoldenrod',1,4). |
| 2585 | | tk_color('DarkOliveGreen',1,4). |
| 2586 | | tk_color('DarkOrange',1,4). |
| 2587 | | tk_color('DarkSeaGreen',1,4). |
| 2588 | | tk_color('DarkSlateGray',1,4). |
| 2589 | | tk_color('DeepPink',1,4). |
| 2590 | | tk_color('DeepSkyBlue',1,4). |
| 2591 | | tk_color('DodgerBlue',1,4). |
| 2592 | | tk_color(firebrick,1,4). |
| 2593 | | tk_color(gold,1,4). |
| 2594 | | tk_color(goldenrod,1,4). |
| 2595 | | tk_color(gray,0,99). |
| 2596 | | tk_color(green,1,4). |
| 2597 | | tk_color(grey,0,99). |
| 2598 | | tk_color(honeydew,1,4). |
| 2599 | | tk_color('HotPink',1,4). |
| 2600 | | tk_color(indianred,1,4). |
| 2601 | | tk_color('IndianRed',1,4). |
| 2602 | | tk_color(ivory,1,4). |
| 2603 | | tk_color(khaki,1,4). |
| 2604 | | tk_color('LavenderBlush',1,4). |
| 2605 | | tk_color('LemonChiffon',1,4). |
| 2606 | | tk_color('LightBlue',1,4). |
| 2607 | | tk_color('LightCyan',1,4). |
| 2608 | | tk_color('LightGoldenrod',1,4). |
| 2609 | | tk_color('LightPink',1,4). |
| 2610 | | tk_color('LightSalmon',1,4). |
| 2611 | | tk_color('LightSkyBlue',1,4). |
| 2612 | | tk_color('LightSteelBlue',1,4). |
| 2613 | | tk_color('LightYellow',1,4). |
| 2614 | | tk_color(magenta,1,4). |
| 2615 | | tk_color(maroon,1,4). |
| 2616 | | tk_color('MediumOrchid',1,4). |
| 2617 | | tk_color('MediumPurple',1,4). |
| 2618 | | tk_color('MistyRose',1,4). |
| 2619 | | tk_color('NavajoWhite',1,4). |
| 2620 | | tk_color(orchid,1,4). |
| 2621 | | tk_color(orange,1,4). |
| 2622 | | tk_color(olivedrab,1,4). |
| 2623 | | tk_color('OliveDrab',1,4). |
| 2624 | | tk_color('OrangeRed',1,4). |
| 2625 | | tk_color(mistyrose,1,4). |
| 2626 | | tk_color(peachpuff,1,4). |
| 2627 | | tk_color(pink,1,4). |
| 2628 | | tk_color(plum,1,4). |
| 2629 | | tk_color(purple,1,4). |
| 2630 | | tk_color('PaleGreen',1,4). |
| 2631 | | tk_color('PaleTurquoise',1,4). |
| 2632 | | tk_color('PaleVioletRed',1,4). |
| 2633 | | tk_color('PeachPuff',1,4). |
| 2634 | | tk_color(red,1,4). |
| 2635 | | tk_color(royalblue,1,4). |
| 2636 | | tk_color('RosyBrown',1,4). |
| 2637 | | tk_color('RoyalBlue',1,4). |
| 2638 | | tk_color(salmon,1,4). |
| 2639 | | tk_color(seagreen,1,4). |
| 2640 | | tk_color(seashell,1,4). |
| 2641 | | tk_color(sienna,1,4). |
| 2642 | | tk_color(skyblue,1,4). |
| 2643 | | tk_color(snow,1,4). |
| 2644 | | tk_color(springgreen,1,4). |
| 2645 | | tk_color(steelblue,1,4). |
| 2646 | | tk_color('SeaGreen',1,4). |
| 2647 | | tk_color('SkyBlue',1,4). |
| 2648 | | tk_color('SlateBlue',1,4). |
| 2649 | | tk_color('SlateGray',1,4). |
| 2650 | | tk_color('SpringGreen',1,4). |
| 2651 | | tk_color('SteelBlue',1,4). |
| 2652 | | tk_color(tan,1,4). |
| 2653 | | tk_color(thistle,1,4). |
| 2654 | | tk_color(tomato,1,4). |
| 2655 | | tk_color(turquoise,1,4). |
| 2656 | | tk_color('VioletRed',1,4). |
| 2657 | | tk_color(wheat,1,4). |
| 2658 | | tk_color(yellow,1,4). |
| 2659 | | |
| 2660 | | |
| 2661 | | tk_color(X) :- tk_color(X,_,_). |
| 2662 | | tk_color('AliceBlue'). |
| 2663 | | tk_color(beige). |
| 2664 | | tk_color(black). |
| 2665 | | tk_color('BlanchedAlmond'). |
| 2666 | | tk_color('BlueViolet'). |
| 2667 | | tk_color(darkblue). |
| 2668 | | tk_color(darkgray). % this is not a valid X11 color; but it is recognised by Tk (but not by sfdp) |
| 2669 | | tk_color(darkgreen). |
| 2670 | | tk_color(darkorange). |
| 2671 | | tk_color(darkorchid). |
| 2672 | | tk_color(darkred). |
| 2673 | | tk_color(darkslateblue). |
| 2674 | | tk_color(darkviolet). |
| 2675 | | tk_color('DarkBlue'). |
| 2676 | | tk_color('DarkCyan'). |
| 2677 | | tk_color('DarkGray'). |
| 2678 | | tk_color('DarkGreen'). |
| 2679 | | tk_color('DarkGrey'). |
| 2680 | | tk_color('DarkKhaki'). |
| 2681 | | tk_color('DarkMagenta'). |
| 2682 | | tk_color('DarkRed'). |
| 2683 | | tk_color('DarkSalmon'). |
| 2684 | | tk_color('DarkSlateBlue'). |
| 2685 | | tk_color('DarkTurquoise'). |
| 2686 | | tk_color('DarkViolet'). |
| 2687 | | tk_color('DimGray'). |
| 2688 | | tk_color('DimGrey'). |
| 2689 | | tk_color('FloralWhite'). |
| 2690 | | tk_color('ForestGreen'). |
| 2691 | | tk_color(lightblue). |
| 2692 | | tk_color(lightgray). |
| 2693 | | tk_color('LawnGreen'). |
| 2694 | | tk_color('LightCoral'). |
| 2695 | | tk_color('LightGray'). |
| 2696 | | tk_color('LightGreen'). |
| 2697 | | tk_color('LightGrey'). |
| 2698 | | tk_color('LightSeaGreen'). |
| 2699 | | tk_color('LimeGreen'). |
| 2700 | | tk_color(moccasin). |
| 2701 | | tk_color('MediumAquamarine'). |
| 2702 | | tk_color('MediumBlue'). |
| 2703 | | tk_color('MediumSeaGreen'). |
| 2704 | | tk_color('MediumSlateBlue'). |
| 2705 | | tk_color('MediumSpringGreen'). |
| 2706 | | tk_color('MediumTurquoise'). |
| 2707 | | tk_color('MediumVioletRed'). |
| 2708 | | tk_color('MidnightBlue'). |
| 2709 | | tk_color('MintCream'). |
| 2710 | | tk_color(navy). |
| 2711 | | tk_color('NavyBlue'). |
| 2712 | | tk_color('OldLace'). |
| 2713 | | tk_color('PapayaWhip'). |
| 2714 | | tk_color('PowderBlue'). |
| 2715 | | tk_color(slateblue). |
| 2716 | | tk_color(steelblue). |
| 2717 | | tk_color('SaddleBrown'). |
| 2718 | | tk_color('SandyBrown'). |
| 2719 | | tk_color(violet). |
| 2720 | | tk_color(white). |
| 2721 | | tk_color('WhiteSmoke'). |
| 2722 | | tk_color('YellowGreen'). |
| 2723 | | |
| 2724 | | valid_gray(G) :- atom(G), atom_concat('gray',NAtom,G), atom_codes(NAtom,[N1|T]), digit(N1), |
| 2725 | | (T=[] -> true ; T=[N2],digit(N2)). |
| 2726 | | digit(N) :- N >47, N<58. |
| 2727 | | |
| 2728 | | |
| 2729 | | hex(X) :- atomic(X), number(X), ((X<103,X>96) ; (X<71,X>64) ; (X>47,X<58)). |
| 2730 | | |
| 2731 | | :- use_module(library(file_systems)). |
| 2732 | | check_file_exists(X) :- file_exists(X) -> true ; add_message(preferences,'Warning file for preference does not exist: ',X). |
| 2733 | | check_directory_exists(X) :- |
| 2734 | | directory_exists(X) -> true ; add_message(preferences,'Warning directory for preference does not exist: ',X). |
| 2735 | | :- public check_path_exists/1. |
| 2736 | | check_path_exists(X) :- (file_exists(X) -> true |
| 2737 | | ; directory_exists(X) -> true |
| 2738 | | ; add_message(preferences,'Warning path for preference does not exist: ',X)). |
| 2739 | | |
| 2740 | | :- dynamic temp_pref/3. |
| 2741 | | % use to temporarily set preferences; |
| 2742 | | % changes can be undone with reset_temporary_preference |
| 2743 | | % change will not be saved if reset_temporary_preference not called (e.g., due to bug/timeout/Ctrl-C) |
| 2744 | | temporary_set_preference(Pref,Val) :- temporary_set_preference(Pref,Val,_). |
| 2745 | | temporary_set_preference(Pref,Val,ChangeOccured) :- get_preference(Pref,OldVal),!, |
| 2746 | | (OldVal=Val -> ChangeOccured=false |
| 2747 | | ; set_preference_direct(Pref,Val,_), ChangeOccured = true, |
| 2748 | | asserta(temp_pref(Pref,OldVal,Val)) |
| 2749 | | %,debug:debug_println(9,temp_set_pref(Pref,Val)) |
| 2750 | | ). |
| 2751 | | % Note: assertz(p(1)), assertz(p(2)), retract(p(X)), retract(p(Y)) -> X=1, Y=2 |
| 2752 | | % Note: asserta(p(1)), asserta(p(2)), retract(p(X)), retract(p(Y)) -> X=2, Y=1 |
| 2753 | | |
| 2754 | | reset_temporary_preference(P) :- reset_temporary_preference(P,_). |
| 2755 | | reset_temporary_preference(_,ChangeOccured) :- ChangeOccured==false,!. % nothing to do |
| 2756 | | reset_temporary_preference(Pref,_) :- |
| 2757 | | (retract(temp_pref(Pref,OldVal,_NewVal)) |
| 2758 | | -> set_preference_direct(Pref,OldVal,_) |
| 2759 | | ; true). |
| 2760 | | |
| 2761 | ? | reset_all_temporary_preferences :- retract(temp_pref(Pref,OldVal,_)),set_preference(Pref,OldVal),fail. |
| 2762 | | reset_all_temporary_preferences. |
| 2763 | | |
| 2764 | | % this set_preference does not update change flag and performs no preference_update_action |
| 2765 | | set_preference_direct(Pref,Val,_) :- var(Pref),!, |
| 2766 | | print_error('Variable as preference not allowed'), |
| 2767 | | print_error(set_preference(Pref,Val)), |
| 2768 | | fail. |
| 2769 | | set_preference_direct(Pref,Val,OldVal) :- read_only_preference(Pref),!, |
| 2770 | | print_error('Preference is read-only'), |
| 2771 | | print_error(set_preference(Pref,Val)), |
| 2772 | | % do not fail, the Rodin plugin calls this when switching workspaces |
| 2773 | | preference(Pref,OldVal). |
| 2774 | | set_preference_direct(Pref,Val,OldVal) :- |
| 2775 | | % format(user_output,'~nset_preference ~w to ~w (~w)~n~n',[Pref,Val,OldVal]), |
| 2776 | | (preference_val_type(Pref,Type) |
| 2777 | ? | -> (is_of_type(Val,Type) |
| 2778 | | -> NewVal=Val |
| 2779 | | ; convert_pref(Val,Type,NewVal), is_of_type(NewVal,Type) |
| 2780 | | -> true |
| 2781 | | ; format_error_with_nl('New preference value for ~w of incorrect type (expected ~w): ~w',[Pref,Type,Val]), |
| 2782 | | %Val =.. L, print_error(val(L)), |
| 2783 | | print_error('No changes performed!'), |
| 2784 | | fail |
| 2785 | | ) |
| 2786 | | ; obsolete_preference(Pref) -> print_error('Obsolete preference'), print_error(Pref) |
| 2787 | | ; print_error('Do not know type of preference'), print_error(Pref) |
| 2788 | | ), |
| 2789 | | (retract(preference(Pref,OLD)) -> OldVal=OLD ; OldVal = '$none'), |
| 2790 | | assertz(preference(Pref,NewVal)), |
| 2791 | | (OldVal=NewVal -> true |
| 2792 | | ; preference_update_action(Pref,NewVal) -> true). |
| 2793 | | |
| 2794 | | % in case the preferences are set by user using upper-case TRUE and FALSE |
| 2795 | | convert_pref('TRUE',T,true) :- bool_type(T). |
| 2796 | | convert_pref('FALSE',T,false) :- bool_type(T). |
| 2797 | | convert_pref('FULL',T,full) :- xbool_type(T). |
| 2798 | | convert_pref('DEFAULT',dbool,default). |
| 2799 | | bool_type(bool). |
| 2800 | | bool_type(dbool). |
| 2801 | | bool_type(T) :- xbool_type(T). |
| 2802 | | xbool_type(xbool). |
| 2803 | | xbool_type(axbool). |
| 2804 | | |
| 2805 | | set_preference(Pref,Val) :- |
| 2806 | | set_preference_direct(Pref,Val,OldVal), |
| 2807 | | retractall(temp_pref(Pref,_,_)), % user has overriden temporary choice |
| 2808 | | (OldVal=Val -> true ; assert_change_flag). |
| 2809 | | |
| 2810 | | |
| 2811 | | |
| 2812 | | tcltk_get_preference(Pref,Val) :- /* same as get_preference, but convert non-atomic into atoms */ |
| 2813 | | get_preference(Pref,V), |
| 2814 | | (atomic(V) -> Val=V |
| 2815 | | ; translate_term_into_atom(V,Val) |
| 2816 | | ). |
| 2817 | | |
| 2818 | | get_preference(Pref,Val) :- |
| 2819 | | (preference(Pref,V) |
| 2820 | | -> Val=V |
| 2821 | | ; (preference_default_value(Pref,V) |
| 2822 | | -> Val=V |
| 2823 | | ; (obsolete_preference(Pref) |
| 2824 | | -> print_error('Obsolete preference in get_preference:') |
| 2825 | | ; print_error('Invalid preference in get_preference:') |
| 2826 | | ), |
| 2827 | | print_error(Pref), |
| 2828 | | Val = 0 |
| 2829 | | ) |
| 2830 | | ). |
| 2831 | | |
| 2832 | | % -------------- |
| 2833 | | |
| 2834 | | % rules for computed/derived preferences: |
| 2835 | | get_computed_preference(debug_time_out,Res) :- |
| 2836 | | preference(debug_time_out_factor,TFactor), !, |
| 2837 | | get_time_out_preference_with_factor(TFactor,Res). |
| 2838 | | get_computed_preference(convert_closures_into_explicit_form_for_store,Value) :- |
| 2839 | | preference(convert_comprehension_sets_into_closures,SymbolicV),!, |
| 2840 | | (SymbolicV=true -> Value=false ; Value=true). |
| 2841 | | get_computed_preference(X,_) :- print_error('Invalid Preference in get_computed_preference:'), |
| 2842 | | print_error(X). |
| 2843 | | |
| 2844 | | |
| 2845 | | |
| 2846 | | % -------------- |
| 2847 | | |
| 2848 | | get_time_out_preference_with_factor(TFactor,Res) :- |
| 2849 | | preference(time_out,CurTO), |
| 2850 | | (disabled_time_out(CurTO) |
| 2851 | | -> disabled_time_out(Res) % keep disabled_time_out value |
| 2852 | | ; DTimeOut is round(CurTO * TFactor), |
| 2853 | | prune_time_out_preference(DTimeOut,Res)). |
| 2854 | | add_time_outs(TO1,TO2,ResTO) :- |
| 2855 | | (disabled_time_out(TO1) -> ResTO=TO1 |
| 2856 | | ; disabled_time_out(TO2) -> ResTO=TO2 |
| 2857 | | ; ResTO is integer(TO1)+integer(TO2) |
| 2858 | | ). |
| 2859 | | |
| 2860 | | % value of 2147483646 means time-out was disabled, 600 hours; should we move to 64 bits ? |
| 2861 | | disabled_time_out(2147483646). % cf no_time_out_value in tools_meta |
| 2862 | | prune_time_out_preference(X,Res) :- (X>= 2147483646 -> disabled_time_out(Res) ; Res=X). |
| 2863 | | |
| 2864 | | time_out_preference_disabled :- preference(time_out,2147483646). |
| 2865 | | |
| 2866 | | cur_pref_string(Pref,String) :- |
| 2867 | | preference_description(Pref,Desc), |
| 2868 | | (eclipse_preference(ECLPREF,Pref) -> ajoin([ECLPREF,': ',Desc],String) |
| 2869 | | ; String=Desc). %string_concatenate(Desc,';',String)). |
| 2870 | | /* preference(Pref,Val), |
| 2871 | | string_concatenate(Val,';',V1), |
| 2872 | | string_concatenate(' = ',V1,V2), |
| 2873 | | string_concatenate(Desc,V2,String). */ |
| 2874 | | |
| 2875 | | /* useful predicates for Tcl/Tk listbox interaction: */ |
| 2876 | | get_preferences_list(List) :- |
| 2877 | | findall(S,cur_pref_string(_,S),List). |
| 2878 | | get_preferences_list(Category,list(List)) :- |
| 2879 | | findall(S,(virtual_preference_category(Pref,Category),cur_pref_string(Pref,S)),List). |
| 2880 | | |
| 2881 | | % add some virtual categories like eclipse |
| 2882 | | virtual_preference_category(Pref,Category) :- Category==eclipse,!, |
| 2883 | | findall(e(E,P),(eclipse_preference(E,P), \+ preference_category(P,hidden)),List), |
| 2884 | | sort(List,SList), |
| 2885 | | member(e(_,Pref),SList). |
| 2886 | | virtual_preference_category(Pref,Category) :- preference_description(Pref,_Desc), preference_category(Pref,Category). |
| 2887 | | virtual_preference_category(Pref,Category) :- preference_description(Pref,_Desc), |
| 2888 | | alternate_preference_category(Pref,Category). |
| 2889 | | |
| 2890 | | |
| 2891 | | get_ith_preference_type(Pos,Type) :- get_ith_preference_type(_,Pos,Type). |
| 2892 | | get_ith_preference_type(Category,Pos,Type) :- |
| 2893 | | findall(S, (virtual_preference_category(Pref,Category), |
| 2894 | | preference_val_type(Pref,S)), List), |
| 2895 | | (nth1(Pos,List,FType) -> Type=FType |
| 2896 | | ; (add_error(get_ith_preference_type,'Could not find preference: ',nth1(Pos,List)),fail)). |
| 2897 | | |
| 2898 | | get_ith_preference_value(Pos,Val) :- get_ith_preference_value(_,Pos,Val). |
| 2899 | | get_ith_preference_value(Category,Pos,Val) :- |
| 2900 | | findall(S, (virtual_preference_category(Pref,Category), |
| 2901 | | tcltk_get_preference(Pref,S)), List), |
| 2902 | | (nth1(Pos,List,FVal) -> Val=FVal |
| 2903 | | ; (add_error(get_ith_preference_value,'Could not find preference: ',nth1(Pos,List)),fail)). |
| 2904 | | |
| 2905 | | set_ith_preference_value(Pos,Val) :- set_ith_preference_value(_,Pos,Val). |
| 2906 | | set_ith_preference_value(Category,Pos,Val) :- |
| 2907 | | findall(S, virtual_preference_category(S,Category), List), |
| 2908 | | (nth1(Pos,List,Pref) -> set_preference(Pref,Val) |
| 2909 | | ; add_error(set_ith_preference_value,'Could not find preference: ',nth1(Pos,List)),fail). |
| 2910 | | |
| 2911 | | |
| 2912 | | % a version of get_preference that will also generate warnings |
| 2913 | | get_preference_with_warnings(Pref,Value) :- gen_preference_warnings(Pref), |
| 2914 | | get_preference(Pref,Value). |
| 2915 | | |
| 2916 | | % get detailed warnings about a preference value |
| 2917 | | gen_preference_warnings(Pref) :- |
| 2918 | | preference(Pref,Value), |
| 2919 | | preference_val_type(Pref,T), |
| 2920 | | \+ is_of_type(Value,T), |
| 2921 | | ajoin(['The value of the preference ',Pref,' does not have the correct type:'],Msg), |
| 2922 | | add_warning(preferences,Msg,T), |
| 2923 | | fail. |
| 2924 | | gen_preference_warnings(Pref) :- |
| 2925 | | preference_val_type(Pref,path), |
| 2926 | | preference(Pref,Value), |
| 2927 | | get_modulename_filename(Value,Module), |
| 2928 | | invalid_application(Pref,Module), |
| 2929 | | ajoin(['The path chosen for preference ',Pref,' seems to point to a wrong program:'],Msg), |
| 2930 | | add_warning(preferences,Msg,Module), |
| 2931 | | fail. |
| 2932 | | gen_preference_warnings(_). |
| 2933 | | % TODO: check e.g. that OPERATION_REUSE is not used in XTL mode,... |
| 2934 | | |
| 2935 | | invalid_application(path_to_dotty,dot). |
| 2936 | | invalid_application(path_to_dot,dotty). |
| 2937 | | |
| 2938 | | /* ------------------------- */ |
| 2939 | | |
| 2940 | | :- dynamic nr_of_recent_documents/1. |
| 2941 | | :- dynamic recent_documents/1. |
| 2942 | | nr_of_recent_documents(0). |
| 2943 | | |
| 2944 | | recompute_nr_of_recent_documents :- |
| 2945 | | retractall(nr_of_recent_documents(_)), |
| 2946 | | findall(X,recent_documents(X),List), |
| 2947 | | length(List,Nr), |
| 2948 | | assertz(nr_of_recent_documents(Nr)). |
| 2949 | | |
| 2950 | | |
| 2951 | | :- dynamic add_recent_documents_active/0. |
| 2952 | | add_recent_documents_active. |
| 2953 | | |
| 2954 | | activate_recent_documents :- (add_recent_documents_active -> true ; assertz(add_recent_documents_active)). |
| 2955 | | |
| 2956 | | deactivate_recent_documents :- retractall(add_recent_documents_active). |
| 2957 | | |
| 2958 | | /* use to add a file to recent documents list */ |
| 2959 | | add_recent_document(_) :- \+ add_recent_documents_active, !. |
| 2960 | | add_recent_document(Document) :- |
| 2961 | | (retract(nr_of_recent_documents(Nr)) -> true ; Nr=0), |
| 2962 | | (retract(recent_documents(Document)) |
| 2963 | | -> N1 =Nr ; N1 is Nr+1 |
| 2964 | | ), |
| 2965 | | (preference(number_of_recent_documents,Max) -> true ; Max=25), |
| 2966 | | (N1>Max -> (retract(recent_documents(_)),assertz(nr_of_recent_documents(Nr))) |
| 2967 | | ; assertz(nr_of_recent_documents(N1))), |
| 2968 | | assertz(recent_documents(Document)), |
| 2969 | | assert_change_flag. |
| 2970 | | |
| 2971 | | get_recent_documents(list(Res)) :- |
| 2972 | | findall(X,recent_documents(X),List), |
| 2973 | | reverse(List,Res). |
| 2974 | | |
| 2975 | | clear_recent_documents :- |
| 2976 | | retractall(recent_documents(_)), |
| 2977 | | retractall(nr_of_recent_documents(_)), |
| 2978 | | assertz(nr_of_recent_documents(0)). |
| 2979 | | |
| 2980 | | |
| 2981 | | /* use to add a string to the searched patterns list */ |
| 2982 | | :- dynamic searched_patterns/1. |
| 2983 | | :- dynamic replaced_patterns/1. |
| 2984 | | :- dynamic eval_history_elements/1. |
| 2985 | | :- dynamic eval_csp_history_elements/1. |
| 2986 | | :- dynamic checked_ltl_formulas/1. |
| 2987 | | |
| 2988 | | |
| 2989 | | add_element_to_history(Predicate,Pattern,MaxNumb) :- |
| 2990 | | merge_prefix_with_suffix(number_of_,Predicate,Name), |
| 2991 | | get_predicate_term_with_single_argument(Name,Nr,TermNum), |
| 2992 | | (retract(TermNum) -> true ; Nr=0), |
| 2993 | | get_predicate_term_with_single_argument(Predicate,Pattern,Term), |
| 2994 | | (retract(Term) -> N1=Nr ; N1 is Nr+1), |
| 2995 | | (preference(TermNum,Max) -> true ; Max=MaxNumb), |
| 2996 | | get_predicate_term_with_single_argument(Predicate,_,Term1), |
| 2997 | | (N1>Max -> (retract(Term1),assertz(TermNum)) |
| 2998 | | ; get_predicate_term_with_single_argument(Name,N1,TermNum1), |
| 2999 | | assertz(TermNum1)),assertz(Term), |
| 3000 | | assert_change_flag. |
| 3001 | | |
| 3002 | | % this will be used with checked_ltl_formulas, ... from tcltk_gui.tcl |
| 3003 | | :- public searched_patterns/1, replaced_patterns/1, eval_history_elements/1, eval_csp_history_elements/1, checked_ltl_formulas/1. |
| 3004 | | get_history_elements_list(Predicate,Reversed,list(Res)) :- |
| 3005 | | get_predicate_term_with_single_argument(Predicate,X,Term), |
| 3006 | | findall(X,Term,List), |
| 3007 | | (Reversed=true -> reverse(List,Res); Res=List). |
| 3008 | | |
| 3009 | | |
| 3010 | | |
| 3011 | | /* not used |
| 3012 | | :- dynamic number_of_checked_ltl_formulas/1. |
| 3013 | | number_of_checked_ltl_formulas(0). |
| 3014 | | recompute_nr_of_checked_ltl_formulas :- |
| 3015 | | retractall(number_of_checked_ltl_formulas(_)), |
| 3016 | | findall(F,checked_ltl_formulas(F),List), |
| 3017 | | length(List,Nr),assertz(number_of_checked_ltl_formulas(Nr)). */ |
| 3018 | | |
| 3019 | | merge_prefix_with_suffix(Prefix,Ending,Name) :- |
| 3020 | | atom_codes(Prefix,Pr),atom_codes(Ending,End), |
| 3021 | | append(Pr,End,CodeName),atom_codes(Name,CodeName). |
| 3022 | | |
| 3023 | | get_predicate_term_with_single_argument(Name,Arg,Term) :- |
| 3024 | | functor(Term,Name,1),arg(1,Term,Arg). |
| 3025 | | |
| 3026 | | |
| 3027 | | /* ------------------------- */ |
| 3028 | | |
| 3029 | | :- dynamic prob_application_type/1. |
| 3030 | | prob_application_type(unknown). |
| 3031 | | |
| 3032 | | get_prob_application_type(X) :- prob_application_type(X). |
| 3033 | | set_prob_application_type(X) :- retractall(prob_application_type(_)), assertz(prob_application_type(X)). |
| 3034 | | % can be tcltk, probcli, prob2, rodin, ... |
| 3035 | | % TODO: call set_prob_application_type(prob2) via some flag when starting from ProB2/ProB2-UI |
| 3036 | | |
| 3037 | | /* ------------------------- */ |
| 3038 | | |
| 3039 | | % used by -pref_group Group procli command |
| 3040 | | set_preference_group(Group,_) :- \+ preference_group_description(Group,_),!, |
| 3041 | | add_error(set_preference_mode,'Preference mode does not exist: ',Group). |
| 3042 | | set_preference_group(Group,default) :- |
| 3043 | | preference_group_val(Group,Scheme,_,_),!, % pick one scheme and reset all values of that scheme to default |
| 3044 | | ( preference_group_val(Group,Scheme,Pref,_),preference_default_value(Pref,Val), |
| 3045 | | set_preference(Pref,Val),fail |
| 3046 | | ; true). |
| 3047 | | set_preference_group(Group,Scheme) :- \+ preference_group_val(Group,Scheme,_,_),!, |
| 3048 | | add_error(set_preference_mode,'Preference scheme does not exist: ',Group:Scheme). |
| 3049 | | set_preference_group(Group,Scheme) :- preference_group_val(Group,Scheme,Pref,Val), |
| 3050 | | set_preference(Pref,Val),fail. |
| 3051 | | set_preference_group(_,_). |
| 3052 | | |
| 3053 | | |
| 3054 | | preference_group_description(integer,'Values for MAXINT and MININT'). |
| 3055 | | preference_group_description(time_out,'To disable TIME_OUT'). |
| 3056 | | preference_group_description(model_check,'Model Checking Limits'). |
| 3057 | | preference_group_description(dot_colors,'Colours for Dot graphs'). |
| 3058 | | preference_group_description(sh_colors,'Colours for Syntax Highlighting'). |
| 3059 | | |
| 3060 | | preference_group_val(integer,int64,maxint, 9223372036854775807). % 2**63-1 |
| 3061 | | preference_group_val(integer,int64,minint,-9223372036854775808). %-2**63 |
| 3062 | | preference_group_val(integer,int32,maxint,2147483647). % 2**31-1 |
| 3063 | | preference_group_val(integer,int32,minint,-2147483648). %-2**31 |
| 3064 | | preference_group_val(integer,int8,maxint,127). |
| 3065 | | preference_group_val(integer,int8,minint,-128). |
| 3066 | | |
| 3067 | | 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 |
| 3068 | | |
| 3069 | | preference_group_val(model_check,unlimited,time_out,TO) :- disabled_time_out(TO). % this value turns time_out off |
| 3070 | | preference_group_val(model_check,unlimited,maxNrOfInitialisations,Max) :- current_prolog_flag(max_tagged_integer,Max). |
| 3071 | | preference_group_val(model_check,unlimited,maxNrOfEnablingsPerOperation,Max) :- current_prolog_flag(max_tagged_integer,Max). |
| 3072 | | preference_group_val(model_check,disable_max,maxNrOfInitialisations,Max) :- current_prolog_flag(max_tagged_integer,Max). |
| 3073 | | preference_group_val(model_check,disable_max,maxNrOfEnablingsPerOperation,Max) :- current_prolog_flag(max_tagged_integer,Max). |
| 3074 | | |
| 3075 | | preference_group_val(dot_colors,classic,dot_normal_node_colour, olivedrab2). |
| 3076 | | preference_group_val(dot_colors,classic,dot_normal_arc_colour,steelblue). |
| 3077 | | preference_group_val(dot_colors,classic,dot_open_node_colour,red). |
| 3078 | | preference_group_val(dot_colors,classic,dot_goal_node_colour,orange). |
| 3079 | | preference_group_val(dot_colors,classic,dot_invariant_violated_node_colour,maroon2). |
| 3080 | | preference_group_val(dot_colors,classic,dot_counterexample_node_colour,brown). |
| 3081 | | preference_group_val(dot_colors,classic,dot_counterexample_op_colour,brown). |
| 3082 | | |
| 3083 | | preference_group_val(dot_colors,winter,dot_normal_node_colour, '#425955'). |
| 3084 | | preference_group_val(dot_colors,winter,dot_normal_arc_colour,'#1B1D26'). |
| 3085 | | preference_group_val(dot_colors,winter,dot_open_node_colour,'#BFBD9F'). |
| 3086 | | preference_group_val(dot_colors,winter,dot_goal_node_colour,'#CC8604'). |
| 3087 | | preference_group_val(dot_colors,winter,dot_invariant_violated_node_colour,'#9C080C'). |
| 3088 | | |
| 3089 | | preference_group_val(dot_colors,dreams,dot_normal_node_colour, '#5D7359'). |
| 3090 | | preference_group_val(dot_colors,dreams,dot_invariant_violated_node_colour,'#661C0E'). |
| 3091 | | preference_group_val(dot_colors,dreams,dot_normal_arc_colour,'#8C5430'). |
| 3092 | | preference_group_val(dot_colors,dreams,dot_open_node_colour,'#D6AA5C'). |
| 3093 | | preference_group_val(dot_colors,dreams,dot_goal_node_colour,'#FFC800'). |
| 3094 | | |
| 3095 | | preference_group_val(dot_colors,solarized,dot_normal_node_colour, '#859900'). |
| 3096 | | preference_group_val(dot_colors,solarized,dot_normal_arc_colour,'#268bd2'). |
| 3097 | | preference_group_val(dot_colors,solarized,dot_open_node_colour,'#dc322f'). |
| 3098 | | preference_group_val(dot_colors,solarized,dot_goal_node_colour,'#cb4b16'). |
| 3099 | | preference_group_val(dot_colors,solarized,dot_invariant_violated_node_colour,'#dc322f'). |
| 3100 | | preference_group_val(dot_colors,solarized,dot_counterexample_node_colour,'#dc322f'). |
| 3101 | | preference_group_val(dot_colors,solarized,dot_counterexample_op_colour,'#d33682'). |
| 3102 | | |
| 3103 | | |
| 3104 | | preference_group_val(sh_colors,solarized,sh_type_colour,'#dc322f'). % $red |
| 3105 | | preference_group_val(sh_colors,solarized,sh_logical_colour,'#cb4b16'). % $orange |
| 3106 | | preference_group_val(sh_colors,solarized,sh_assignments_colour,'#268bd2'). % $blue |
| 3107 | | preference_group_val(sh_colors,solarized,sh_operators,'#2aa198'). % $cyan |
| 3108 | | preference_group_val(sh_colors,solarized,sh_top_level_keywords,'#6c71c4'). % $violet |
| 3109 | | preference_group_val(sh_colors,solarized,sh_control_keywords,'#d33682'). % $magenta |
| 3110 | | preference_group_val(sh_colors,solarized,sh_comments,'#93a1a1'). % $base1 |
| 3111 | | preference_group_val(sh_colors,solarized,sh_pragmas,'#859900'). % $green |
| 3112 | | preference_group_val(sh_colors,solarized,sh_unsupported_background,'#b58900'). % $yellow |
| 3113 | | |
| 3114 | | :- use_module(eventhandling,[register_event_listener/3]). |
| 3115 | | :- register_event_listener(startup_prob,init_preferences, |
| 3116 | | 'Initialise Preferences'). |
| 3117 | | :- register_event_listener(clear_specification,reset_all_temporary_preferences, |
| 3118 | | 'Reset Temporary Preferences.'). |
| 3119 | | :- register_event_listener(start_unit_tests,(backup_preferences, |
| 3120 | | set_preference(minint,-1), |
| 3121 | | set_preference(maxint,3), |
| 3122 | | set_preference(translate_print_all_sequences,false), |
| 3123 | | set_preference(translate_print_cs_style_sequences,false) |
| 3124 | | ), |
| 3125 | | 'Setting up Preferences for Unit Tests'). |
| 3126 | | :- register_event_listener(stop_unit_tests, revert_preferences, 'Reverting Preferences'). |
| 3127 | | :- register_event_listener(reset_prob,(reset_all_temporary_preferences, reset_to_defaults), |
| 3128 | | 'Reset Preferences just like after starup_prob'). |