| 1 | | % (c) 2009-2019 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, get_computed_preference/2, |
| 8 | | get_preference/2, get_preferences_list/1, get_preferences_list/2, |
| 9 | | set_preference/2, |
| 10 | | call_with_preference/3, |
| 11 | | temporary_set_preference/2, temporary_set_preference/3, |
| 12 | | reset_temporary_preference/1, reset_temporary_preference/2, |
| 13 | | reset_all_temporary_preferences/0, |
| 14 | | preference_category/2, preference_description/2, preference_val_type/2, preference_default_value/2, |
| 15 | | preference/2, |
| 16 | | is_of_type/2, |
| 17 | | get_ith_preference_type/2, get_ith_preference_value/2, set_ith_preference_value/2, |
| 18 | | get_ith_preference_type/3, get_ith_preference_value/3, set_ith_preference_value/3, |
| 19 | | virtual_preference_category/2, |
| 20 | | load_preferences/1,save_preferences/1, |
| 21 | | backup_preferences/0, revert_preferences/0, reset_to_defaults/1, reset_for_benchmarking/0, |
| 22 | | set_preference_group/2, |
| 23 | | activate_recent_documents/0,deactivate_recent_documents/0, |
| 24 | | print_preferences/0, |
| 25 | | |
| 26 | | add_recent_document/1, /* use to add a file to recent documents list */ |
| 27 | | get_recent_documents/1, clear_recent_documents/0, |
| 28 | | add_element_to_history/3, get_history_elements_list/3, |
| 29 | | |
| 30 | | eclipse_preference/2, print_eclipse_prefs/0, |
| 31 | | advanced_eclipse_preference/2, |
| 32 | | obsolete_eclipse_preference/1, obsolete_preference/1, |
| 33 | | get_non_default_preferences/1, |
| 34 | | |
| 35 | | get_time_out_preference_with_factor/2, |
| 36 | | add_time_outs/3, |
| 37 | | time_out_preference_disabled/0, |
| 38 | | |
| 39 | | get_prob_application_type/1, set_prob_application_type/1 |
| 40 | | ]). |
| 41 | | |
| 42 | | :- use_module(tools, [ print_message/1, host_platform/1]). |
| 43 | | :- use_module(tools_meta, [safe_on_exception/3, safe_on_exception_silent/3, translate_term_into_atom/2]). |
| 44 | | :- use_module(tools_strings, [string_concatenate/3, ajoin/2]). |
| 45 | | :- use_module(tools_printing, [print_dynamic_pred/3,print_error/1]). |
| 46 | | |
| 47 | | :- use_module(module_information,[module_info/2]). |
| 48 | | :- module_info(group,infrastructure). |
| 49 | | :- module_info(description,'This module manages the various preferences of ProB. Preferences can be grouped, saved and restored and validated from file.'). |
| 50 | | |
| 51 | | %:- use_module(debug). % no longer required |
| 52 | | % :- use_module(self_check). % tests now in basic_tests |
| 53 | | :- use_module(error_manager). |
| 54 | | :- use_module(library(lists)). |
| 55 | | |
| 56 | | :- volatile change_flag/0. |
| 57 | | :- dynamic change_flag/0. |
| 58 | | assert_change_flag :- assert(change_flag). |
| 59 | | |
| 60 | | init_preferences :- retractall(change_flag), |
| 61 | | reset_to_defaults, check_preferences. |
| 62 | | |
| 63 | | check_preferences :- |
| 64 | | %print('% '), preference_description(P,_), print(P), print(' '), |
| 65 | ? | preferences:preference_default_value(P,_), |
| 66 | ? | ( preferences:preference(P,Val), |
| 67 | | preferences:preference_val_type(P,T), |
| 68 | | preferences:preference_category(P,_) |
| 69 | ? | -> preferences:is_of_type(Val,T) |
| 70 | | ; add_internal_error('Internal error for preference: ',P) |
| 71 | | ),fail. |
| 72 | | check_preferences. % :- print_message('Preferences Checked'). |
| 73 | | |
| 74 | | |
| 75 | | |
| 76 | | load_preferences(File) :- print_message(load_preferences(File)), |
| 77 | | safe_on_exception_silent(Exception1,see(File), |
| 78 | | (print_see_exception(Exception1,File),fail)), |
| 79 | | !, |
| 80 | | load_preferences2(File). |
| 81 | | load_preferences(_). |
| 82 | | |
| 83 | | load_preferences2(File) :- |
| 84 | | safe_on_exception(_Exc2,read_preferences, |
| 85 | | (print_message('### corrupted preference file'),print_message(File))), |
| 86 | | !. |
| 87 | | %print(loaded_preferences(File)),nl. |
| 88 | | load_preferences2(File) :- print_message('### error occured reading preference file'), |
| 89 | | print_message(File). |
| 90 | | |
| 91 | | print_see_exception(error(existence_error(_,_),_),File) :- !, |
| 92 | | print_message('preference file does not exist, ProB will create a fresh one'),print_message(File). |
| 93 | | print_see_exception(Exception,File) :- |
| 94 | | print_message('### cannot open preference file'),print_message(File), |
| 95 | | print_message(Exception). |
| 96 | | |
| 97 | | read_preferences :- clear_dynamic_preference_predicates, |
| 98 | | call_cleanup(read_preferences2,seen). |
| 99 | | read_preferences2 :- |
| 100 | | read(Term), Term \= end_of_file, !, %print(pref(Term)),nl, |
| 101 | | (Term = preference(Pref,NVal) |
| 102 | | -> (volatile_preference(Pref) -> true |
| 103 | | ; retract(preference(Pref,_)) -> assert(preference(Pref,NVal)) |
| 104 | | ; obsolete_preference(Pref) -> print_message(obsolete(Pref)) |
| 105 | | ; add_message(load_preferences,'Unknown preference in preference file: ',Pref) |
| 106 | | ) |
| 107 | | ; Term = ':-'(dynamic(_)) -> true |
| 108 | | ; dynamic_preference_predicate(Term) -> assert(Term) |
| 109 | | ; (Term = (Head:-fail),dynamic_preference_predicate(Head)) -> true |
| 110 | | ; add_error(load_preferences,'Unrecognised:',Term) |
| 111 | | ), |
| 112 | | read_preferences2. |
| 113 | | read_preferences2 :- retractall(change_flag), recompute_nr_of_recent_documents. |
| 114 | | %recompute_nr_of_searched_and_replaced_patterns. |
| 115 | | %recompute_nr_of_eval_history_elements. |
| 116 | | |
| 117 | | clear_dynamic_preference_predicates :- dynamic_preference_predicate(X), retractall(X),fail. |
| 118 | | clear_dynamic_preference_predicates. |
| 119 | | |
| 120 | | % declare which dynamic predicates are stored in Preference file |
| 121 | | dynamic_preference_predicate(recent_documents(_)). |
| 122 | | dynamic_preference_predicate(searched_patterns(_)). |
| 123 | | dynamic_preference_predicate(replaced_patterns(_)). |
| 124 | | dynamic_preference_predicate(eval_history_elements(_)). |
| 125 | | dynamic_preference_predicate(eval_csp_history_elements(_)). |
| 126 | | dynamic_preference_predicate(checked_ltl_formulas(_)). |
| 127 | | |
| 128 | | save_preferences(File) :- change_flag,!, |
| 129 | | % catch exception in case we cannot write preferences file |
| 130 | | on_exception(Exception,save_preferences2(File), |
| 131 | | (string_concatenate('Cannot write preferences file ',File,Msg), |
| 132 | | add_error(save_preferences,Msg,Exception))). |
| 133 | | save_preferences(File) :- print_message(preferences_unchanged(File)). |
| 134 | | |
| 135 | | save_preferences2(File) :- |
| 136 | | print_message(save_preferences(File)), |
| 137 | | tell(File), |
| 138 | | (print_preferences_for_saving -> true ; true), |
| 139 | | told, |
| 140 | | retractall(change_flag). |
| 141 | | |
| 142 | | % if we have temporarily set a preference, then print the old value |
| 143 | | print_preferences_for_saving :- |
| 144 | | preference_default_value(Pref,_), |
| 145 | | preference(Pref,CurVal), |
| 146 | | (temp_pref(Pref,OldVal,CurVal) -> V=OldVal ; V=CurVal), % temp_pref can be nested !, will not print initial value in this case |
| 147 | | write_term(preference(Pref,V),[quoted(true)]),print('.'),nl, |
| 148 | | fail. |
| 149 | | print_preferences_for_saving :- print_dynamic_preferences. |
| 150 | | |
| 151 | | % now in basic_tests.pl |
| 152 | | %:- assert_must_succeed(print_preferences). |
| 153 | | print_preferences :- print_dynamic_pred(preferences,preference,2), |
| 154 | | print_dynamic_preferences. |
| 155 | | |
| 156 | | print_dynamic_preferences :- |
| 157 | | dynamic_preference_predicate(P), functor(P,F,N), |
| 158 | | print_dynamic_pred(preferences,F,N),fail. |
| 159 | | print_dynamic_preferences. |
| 160 | | |
| 161 | | % now in basic_tests.pl |
| 162 | | %:- assert_must_succeed(get_non_default_preferences(_)). |
| 163 | | |
| 164 | | get_non_default_preferences(list(L)) :- |
| 165 | | findall(PS,non_default_pref(PS),L). |
| 166 | | |
| 167 | | non_default_pref(PrefStr) :- preference(Pref,Val), preference_default_value(Pref,DVal), |
| 168 | | DVal \= Val, |
| 169 | | (eclipse_preference(ECLPREF,Pref) -> |
| 170 | | ajoin([Pref,' (',ECLPREF,') == ',Val,' (default = ',DVal, ')'],PrefStr) |
| 171 | | ; |
| 172 | | ajoin([Pref,' == ',Val,' (default = ',DVal, ')'],PrefStr) |
| 173 | | ). |
| 174 | | |
| 175 | | :- volatile change_flag_backup/0, pref_backup/2. |
| 176 | | :- dynamic change_flag_backup/0. |
| 177 | | :- dynamic pref_backup/2. |
| 178 | | |
| 179 | | backup_preferences :- retractall(pref_backup(_,_)),retractall(change_flag_backup), |
| 180 | | preference(P,Val), assert(pref_backup(P,Val)),fail. |
| 181 | | backup_preferences :- (change_flag -> assert(change_flag_backup) ; true). |
| 182 | | |
| 183 | | revert_preferences :- \+(pref_backup(_,_)),!, print_error('No previously backed-up preferences in revert_preferences!'). |
| 184 | | revert_preferences :- retractall(preference(_,_)),pref_backup(P,Val), assert(preference(P,Val)),fail. |
| 185 | | revert_preferences :- retractall(change_flag), (change_flag_backup -> assert_change_flag ; true). |
| 186 | | |
| 187 | | reset_to_defaults :- reset_to_defaults(_). |
| 188 | | |
| 189 | ? | reset_to_defaults(Category) :- preference_category(Pref,Category), |
| 190 | | preference_default_value(Pref,Val), |
| 191 | | retractall(preference(Pref,_)), |
| 192 | | assert(preference(Pref,Val)), |
| 193 | | fail. |
| 194 | | reset_to_defaults(_) :- assert_change_flag. |
| 195 | | |
| 196 | | |
| 197 | | reset_for_benchmarking :- |
| 198 | | set_preference(maxNrOfInitialisations,3), |
| 199 | | set_preference(randomisedRestartInitalisations,false), |
| 200 | | set_preference(maxNrOfEnablingsPerOperation,10), |
| 201 | | set_preference(maxint,4), |
| 202 | | set_preference(minint,-1), |
| 203 | | set_preference(time_out,3500), |
| 204 | | set_preference(globalsets_fdrange,3), |
| 205 | | set_preference(show_initialisation_arguments,true), |
| 206 | | set_preference(provide_trace_information,false), |
| 207 | | set_preference(performance_monitoring_on,false), |
| 208 | | set_preference(find_abort_values,false), |
| 209 | | set_preference(raise_abort_immediately,false), |
| 210 | | set_preference(expand_forall_upto,100), |
| 211 | | %set_preference(animate_skip_operations,true), |
| 212 | | set_preference(cspm_animate_all_processes_without_arguments,false), |
| 213 | | set_preference(cspm_animate_all_processes,false). |
| 214 | | % set_preference(convert_closures_into_explicit_form_for_store,true). |
| 215 | | |
| 216 | | :- meta_predicate call_with_preference(0,-,-). |
| 217 | | |
| 218 | | call_with_preference(Call,Pref,Val) :- |
| 219 | | temporary_set_preference(Pref,Val,CHNG1), |
| 220 | | call_cleanup(Call, |
| 221 | | reset_temporary_preference(Pref,CHNG1)). |
| 222 | | |
| 223 | | |
| 224 | | % ------------------------ |
| 225 | | |
| 226 | | |
| 227 | | % now in basic_tests.pl |
| 228 | | %:- assert_must_succeed( \+((eclipse_preference(_EP,P), \+preference_default_value(P,_Val)))). |
| 229 | | eclipse_preference('MAXINT',maxint). |
| 230 | | eclipse_preference('MININT',minint). |
| 231 | | eclipse_preference('DEFAULT_SETSIZE',globalsets_fdrange). |
| 232 | | eclipse_preference('MAX_INITIALISATIONS',maxNrOfInitialisations). |
| 233 | | eclipse_preference('RANDOMISED_RESTART_INIT',randomisedRestartInitalisations). |
| 234 | | eclipse_preference('MAX_OPERATIONS',maxNrOfEnablingsPerOperation). |
| 235 | | %eclipse_preference('ANIMATE_SKIP_OPERATIONS',animate_skip_operations). |
| 236 | | %eclipse_preference('EXPAND_CLOSURES_FOR_STATE',convert_closures_into_explicit_form_for_store). |
| 237 | | eclipse_preference('SYMBOLIC',convert_comprehension_sets_into_closures). |
| 238 | | eclipse_preference('CLPFD',use_clpfd_solver). |
| 239 | | eclipse_preference('CHR',use_chr_solver). |
| 240 | | eclipse_preference('SMT',use_smt_mode). |
| 241 | | eclipse_preference('SOLVER_STRENGTH',solver_strength). |
| 242 | | eclipse_preference('REMOVE_IMPLIED_CONSTRAINTS',remove_implied_constraints). |
| 243 | | eclipse_preference('LIFT_EXISTS',lift_existential_quantifiers). |
| 244 | | eclipse_preference('CSE',use_common_subexpression_elimination). |
| 245 | | eclipse_preference('STATIC_ORDERING',use_static_ordering). |
| 246 | | eclipse_preference('COMPRESSION',use_state_packing). |
| 247 | | %eclipse_preference('SYMMETRY_MARKERS',use_symmetry_marker_hash). |
| 248 | | %eclipse_preference('PERMUTATION_FLOODING',enable_permutation_reducation). |
| 249 | | eclipse_preference('SYMMETRY_MODE',symmetry_mode). |
| 250 | | eclipse_preference('STATIC_SYMMETRY_DETECTION',use_static_symmetry_detection). |
| 251 | | eclipse_preference('TIME_OUT',time_out). |
| 252 | | eclipse_preference('PROOF_INFO',use_po). |
| 253 | | eclipse_preference('TRY_FIND_ABORT',find_abort_values). % maybe rename into TRY_FIND_WD_ERROR ? |
| 254 | | eclipse_preference('RAISE_ABORT_IMMEDIATELY',raise_abort_immediately). |
| 255 | | eclipse_preference('NUMBER_OF_ANIMATED_ABSTRACTIONS',number_animated_abstractions). |
| 256 | | eclipse_preference('USE_RECORD_CONSTRUCTION',use_record_construction). |
| 257 | | eclipse_preference('KODKOD',try_kodkod_on_load). |
| 258 | | eclipse_preference('MEMO',use_closure_expansion_memoization). |
| 259 | | eclipse_preference('MEMOIZE_FUNCTIONS',use_function_memoization). |
| 260 | | eclipse_preference('RANDOMISE_ENUMERATION_ORDER',randomise_enumeration_order). |
| 261 | | eclipse_preference('PGE',pge). |
| 262 | | eclipse_preference('OPTIMIZE_AST',optimize_ast). |
| 263 | | eclipse_preference('USELESS_CODE_ELIMINATION',useless_code_elimination). |
| 264 | | eclipse_preference('COMPILE_WHILE',compile_while_body). |
| 265 | | eclipse_preference('DETECT_LAMBDAS',detect_lambdas). |
| 266 | | |
| 267 | | eclipse_preference(A,B) :- advanced_eclipse_preference(A,B). |
| 268 | | |
| 269 | | % these will not be shown in ProB for Rodin for example: |
| 270 | | advanced_eclipse_preference('OPERATION_REUSE',try_operation_reuse). % not available for Event-B this doesn't work ; see eg. prob_examples/examples/EventBPrologPackages/Advance_WP2/v6_Sep2014/ex_mch.eventb -animate 300 which generates deadlock |
| 271 | | advanced_eclipse_preference('NORMALIZE_AST',normalize_ast). |
| 272 | | advanced_eclipse_preference('DATA_VALIDATION',data_validation_mode). |
| 273 | | advanced_eclipse_preference('KODKOD_ONLY_FULL',kodkod_for_components). |
| 274 | | advanced_eclipse_preference('KODKOD_RAISE_WARNINGS',kodkod_raise_warnings). |
| 275 | | advanced_eclipse_preference('KODKOD_MAX_NR_SOLS',kodkod_max_nr_solutions). |
| 276 | | advanced_eclipse_preference('KODKOD_SYMMETRY',kodkod_symmetry_level). |
| 277 | | advanced_eclipse_preference('KODKOD_SAT_SOLVER',kodkod_sat_solver). |
| 278 | | advanced_eclipse_preference('CSE_PRED',use_common_subexpression_also_for_predicates). |
| 279 | | advanced_eclipse_preference('CSE_WD_ONLY',use_common_subexpression_wd_only). |
| 280 | | advanced_eclipse_preference('ALLOW_INCOMPLETE_SETUP_CONSTANTS',allow_incomplete_partial_setup_constants). |
| 281 | | advanced_eclipse_preference('PARTITION_PROPERTIES',partition_predicates). |
| 282 | | advanced_eclipse_preference('PARTITION_PROPERTIES_INLINE',partition_predicates_inline_equalities). |
| 283 | | advanced_eclipse_preference('SHOW_EVENTB_ANY_VALUES',show_eventb_any_arguments). |
| 284 | | advanced_eclipse_preference('RANDOMISE_OPERATION_ORDER',randomise_operation_order). |
| 285 | | advanced_eclipse_preference('EXPAND_FORALL_UPTO',expand_forall_upto). |
| 286 | | advanced_eclipse_preference('MAX_DISPLAY_SET',expand_avl_upto). |
| 287 | | %advanced_eclipse_preference('WARN_WHEN_EXPANDING_INFINITE_CLOSURES',warn_when_expanding_infinite_closures). |
| 288 | | advanced_eclipse_preference('ENUMERATE_INFINITE_TYPES',allow_enumeration_of_infinite_types). |
| 289 | | advanced_eclipse_preference('WARN_IF_DEFINITION_HIDES_VARIABLE',warn_if_definition_hides_variable). |
| 290 | | advanced_eclipse_preference('TYPE_CHECK_DEFINITIONS',type_check_definitions). |
| 291 | | advanced_eclipse_preference('TRACE_INFO',provide_trace_information). |
| 292 | | advanced_eclipse_preference('PERFORMANCE_INFO',performance_monitoring_on). |
| 293 | | advanced_eclipse_preference('DOUBLE_EVALUATION',double_evaluation_when_analysing). |
| 294 | | %advanced_eclipse_preference('RECURSIVE',allow_recursive_closures). |
| 295 | | advanced_eclipse_preference('IGNORE_HASH_COLLISIONS',ignore_hash_collisions). |
| 296 | | advanced_eclipse_preference('USE_SCOPE_DEFINITION',use_scope_predicate). |
| 297 | | advanced_eclipse_preference('USE_IGNORE_PRAGMAS',use_ignore_pragmas). |
| 298 | | advanced_eclipse_preference('FORGET_STATE_SPACE',forget_state_space). |
| 299 | | advanced_eclipse_preference('SAFETY_MODEL_CHECK',store_only_one_incoming_transition). |
| 300 | | %advanced_eclipse_preference('LARGE_PARSER_JVM',use_large_jvm_for_parser). |
| 301 | | advanced_eclipse_preference('CSP_STRIP_SOURCE_LOC',cspm_strip_source_location). |
| 302 | | advanced_eclipse_preference('INVARIANT_CHECKING',do_invariant_checking). |
| 303 | | %advanced_eclipse_preference('NEGATED_INVARIANT_CHECKING',do_neginvariant_checking). % use double_evaluation_when_analysing |
| 304 | | advanced_eclipse_preference('ALLOW_SIMULTANEOUS_ASSIGNMENTS',allow_simultaneous_assignments). |
| 305 | | advanced_eclipse_preference('BUGLY',bugly_pp_scrambling). % B Ugly |
| 306 | | advanced_eclipse_preference('ATELIERB_KRT_PATH',path_to_atb_krt). |
| 307 | | advanced_eclipse_preference('JAVA_PATH',path_to_java). |
| 308 | | advanced_eclipse_preference('TRY_ATELIERB_PROVERS',try_atb_provers). |
| 309 | | advanced_eclipse_preference('SYMBOLIC_MC_TRY_OTHER_SOLVERS',symbolic_mc_try_other_solvers). |
| 310 | | advanced_eclipse_preference('CSE_SUBST',use_common_subexpression_also_for_substitutions). |
| 311 | | advanced_eclipse_preference('SMT_SUPPORTED_INTERPRETER',smt_supported_interpreter). |
| 312 | | advanced_eclipse_preference('PP_FROZEN_INFOS',translate_print_frozen_infos). |
| 313 | | advanced_eclipse_preference('PP_SEQUENCES',translate_print_all_sequences). |
| 314 | | advanced_eclipse_preference('PP_CS_STYLE_SEQUENCES',translate_print_cs_style_sequences). |
| 315 | | advanced_eclipse_preference('STRING_AS_SEQUENCE',allow_sequence_operators_on_strings). |
| 316 | | |
| 317 | | |
| 318 | | advanced_eclipse_preference('DOT_PROP',dot_print_node_properties). |
| 319 | | advanced_eclipse_preference('DOT_IDS',dot_print_node_ids). |
| 320 | | advanced_eclipse_preference('DOT_INFO',dot_print_node_info). |
| 321 | | advanced_eclipse_preference('DOT_LOOPS',dot_print_self_loops). |
| 322 | | advanced_eclipse_preference('DOT_ARC_COLORS',dot_print_arc_colors). |
| 323 | | advanced_eclipse_preference('DOT_FUNCTIONS',dot_print_functions). |
| 324 | | advanced_eclipse_preference('DOT_ROOT',dot_print_root). |
| 325 | | %advanced_eclipse_preference('DOT_LEAVES',dot_print_leaves). |
| 326 | | advanced_eclipse_preference('DOT_EDGE_LABELS',dot_print_edge_labels). |
| 327 | | advanced_eclipse_preference('DOT_ARGUMENTS',dot_print_action_arguments). |
| 328 | | advanced_eclipse_preference('DOT_COLOR_ARC',dot_normal_arc_colour). |
| 329 | | advanced_eclipse_preference('DOT_COLOR_NODE',dot_normal_node_colour). |
| 330 | | advanced_eclipse_preference('DOT_COLOR_NODE_ERROR',dot_invariant_violated_node_colour). |
| 331 | | advanced_eclipse_preference('DOT_COLOR_NODE_OPEN',dot_open_node_colour). |
| 332 | | advanced_eclipse_preference('DOT_COLOR_NODE_GOAL',dot_goal_node_colour). |
| 333 | | advanced_eclipse_preference('DOT_PEN_WIDTH',dot_node_penwidth). |
| 334 | | advanced_eclipse_preference('DOT_SHOW_OP_READ_WRITES',dot_enabling_show_readwrites). |
| 335 | | advanced_eclipse_preference('DOT',path_to_dot). |
| 336 | | advanced_eclipse_preference('DOT_ENGINE',dot_default_engine). |
| 337 | | |
| 338 | | advanced_eclipse_preference('TK_CUSTOM_STATE_VIEW_PADDING',tk_custom_state_viewer_padding). |
| 339 | | advanced_eclipse_preference('TK_CUSTOM_STATE_VIEW_STRING_PADDING',tk_custom_state_viewer_str_padding). |
| 340 | | advanced_eclipse_preference('TK_CUSTOM_STATE_VIEW_FONT_NAME',tk_custom_state_viewer_font_name). |
| 341 | | advanced_eclipse_preference('TK_CUSTOM_STATE_VIEW_FONT_SIZE',tk_custom_state_viewer_font_size). |
| 342 | | advanced_eclipse_preference('TK_CUSTOM_STATE_VIEW_VISIBLE',use_tk_custom_state_viewer). |
| 343 | | |
| 344 | | advanced_eclipse_preference('BOOL_AS_PREDICATE',bool_expression_as_predicate). |
| 345 | | advanced_eclipse_preference('ALLOW_UNTYPED_IDENTIFIERS',allow_untyped_identifiers). |
| 346 | | advanced_eclipse_preference('ALLOW_LOCAL_OPERATION_CALLS',allow_local_operation_calls). |
| 347 | | advanced_eclipse_preference('ALLOW_OPERATION_CALLS_IN_EXPRESSIONS',allow_operation_calls_in_expr). |
| 348 | | advanced_eclipse_preference('ALLOW_COMPLEX_LETS',allow_let_to_reuse_introduced_ids). |
| 349 | | advanced_eclipse_preference('REQUIRE_OUTPUT_ASSIGNMENT',require_operations_to_assign_all_outputs). |
| 350 | | advanced_eclipse_preference('ALLOW_OUTPUT_READING',allow_operations_to_read_outputs). |
| 351 | | advanced_eclipse_preference('REPL_UNICODE',repl_unicode). |
| 352 | | advanced_eclipse_preference('REPL_CACHE_PARSING',repl_cache_parsing). |
| 353 | | advanced_eclipse_preference('LATEX_ENCODING',latex_encoding). |
| 354 | | advanced_eclipse_preference('LATEX_GREEK_IDENTIFIERS',latex_pp_greek_ids). |
| 355 | | advanced_eclipse_preference('XML_ENCODING',xml_encoding). |
| 356 | | advanced_eclipse_preference('BBRESULTS',view_probcli_errors_using_bbresults). |
| 357 | | advanced_eclipse_preference('IGNORE_PRJ_TYPES',ignore_prj_types). |
| 358 | | advanced_eclipse_preference('FILTER_UNUSED',filter_unused_constants). |
| 359 | | advanced_eclipse_preference('DISPROVER_MODE',disprover_mode). |
| 360 | | advanced_eclipse_preference('TRACE_UPON_ERROR',trace_upon_error). |
| 361 | | advanced_eclipse_preference('NDJSON_ERROR_LOG_FILE',error_log_file). |
| 362 | | advanced_eclipse_preference('STRICT_RAISE_WARNINGS',strict_raise_warnings). |
| 363 | | advanced_eclipse_preference('STRICT_RAISE_ENUM_WARNINGS',strict_raise_enum_warnings). |
| 364 | | advanced_eclipse_preference('STRICT_CLASH_CHECKING',clash_strict_checks). |
| 365 | | %advanced_eclipse_preference('SHOW_FULL_ERROR_LOCATIONS',show_full_error_span). |
| 366 | | advanced_eclipse_preference('EDITOR',path_to_text_editor_launch). |
| 367 | | advanced_eclipse_preference('EDITOR_GUI',path_to_text_editor). |
| 368 | | advanced_eclipse_preference('TLC_WORKERS',tlc_number_of_workers). % will be useful once we can call TLC from probcli |
| 369 | | advanced_eclipse_preference('LTSMIN',path_to_ltsmin). |
| 370 | | |
| 371 | | advanced_eclipse_preference('INTERNAL_ARGUMENT_PREFIX',prefix_internal_operation_arguments). |
| 372 | | advanced_eclipse_preference('MINIMAL_TEST_SUITES',generate_minimal_nr_of_testcases). |
| 373 | | advanced_eclipse_preference('ALLOW_NEW_OPERATIONS_IN_REFINEMENT',allow_new_ops_in_refinement). |
| 374 | | |
| 375 | | advanced_eclipse_preference('PROB2_TRACE_FILE',prob2_trace_file). |
| 376 | | advanced_eclipse_preference('PROB2_TRACE_FILE_UNIQUE',prob2_trace_file_gen_unique_name). |
| 377 | | |
| 378 | | |
| 379 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_HORIZONTAL',dot_event_hierarchy_horizontal). |
| 380 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_MCH_COL',dot_event_hierarchy_machine_colour). |
| 381 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_REF_COL',dot_event_hierarchy_refines_colour). |
| 382 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_NEW_COL',dot_event_hierarchy_new_event_colour). |
| 383 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_RENAME_COL',dot_event_hierarchy_rename_event_colour). |
| 384 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_RENAME_UNCHG_COL',dot_event_hierarchy_rename_unchanged_event_colour). |
| 385 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_UNCHG_COL',dot_event_hierarchy_unchanged_event_colour). |
| 386 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_GRD_STRGTH_COL',dot_event_hierarchy_grd_strengthening_event_colour). |
| 387 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_GRD_KEEP_COL',dot_event_hierarchy_grd_keeping_event_colour). |
| 388 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_EDGE_COL',dot_event_hierarchy_edge_colour). |
| 389 | | advanced_eclipse_preference('DOT_EVENT_HIERARCHY_EXTENDS_COL',dot_event_hierarchy_extends_colour). |
| 390 | | advanced_eclipse_preference('DOT_USE_CONSTANTS',dot_print_use_constants). |
| 391 | | advanced_eclipse_preference('DOT_ROOT_SHAPE',dot_root_shape). |
| 392 | | advanced_eclipse_preference('DOT_NORMAL_NODE_SHAPE',dot_normal_node_shape). |
| 393 | | advanced_eclipse_preference('DOT_CURRENT_NODE_SHAPE',dot_current_node_shape). |
| 394 | | advanced_eclipse_preference('DOT_SCOPE_LIMIT_COL',dot_scope_limit_node_colour). |
| 395 | | advanced_eclipse_preference('DOT_FILL_NORMAL_NODES',dot_fill_normal_nodes). |
| 396 | | advanced_eclipse_preference('DOT_NODE_FONT_SIZE',dot_node_font_size). |
| 397 | | advanced_eclipse_preference('DOT_EDGE_FONT_SIZE',dot_edge_font_size). |
| 398 | | advanced_eclipse_preference('DOT_COLOUR_GOAL',dot_colour_goal_nodes). |
| 399 | | advanced_eclipse_preference('DOT_DEFINITIONS_USE_SUB_GRAPH',dot_definitions_use_sub_graph). |
| 400 | | advanced_eclipse_preference('DOT_DEFINITIONS_SHOW_ALL',dot_definitions_show_all). |
| 401 | | advanced_eclipse_preference('DOT_PROJECTION_NON_DET_COL',dot_projection_non_det_edge_colour). |
| 402 | | advanced_eclipse_preference('DOT_PROJECTION_DET_COL',dot_projection_det_edge_colour). |
| 403 | | advanced_eclipse_preference('DOT_PROJECTION_NON_DEF_COL',dot_projection_non_definite_edge_style). |
| 404 | | advanced_eclipse_preference('DOT_PROJECTION_DEF_COL',dot_projection_definite_edge_style). |
| 405 | | advanced_eclipse_preference('DOT_PROJECTION_LABEL_LIMIT',dot_projection_label_limit). |
| 406 | | advanced_eclipse_preference('DOT_USE_UNICODE',dot_use_unicode). |
| 407 | | advanced_eclipse_preference('DOT_PREDICATE_NODE_SHAPE',dot_predicate_node_shape). |
| 408 | | advanced_eclipse_preference('DOT_EXPRESSION_NODE_SHAPE',dot_expression_node_shape). |
| 409 | | advanced_eclipse_preference('DOT_VARIABLE_MODIFICATION_HIDE_ONLY_WRITTEN',dot_var_mod_hide_only_written). |
| 410 | | advanced_eclipse_preference('SYNTAX_HIGHLIGHT',do_syntax_highlighting). |
| 411 | | |
| 412 | | |
| 413 | | advanced_eclipse_preference('MC_DC_Level',mc_dc_default_level). |
| 414 | | |
| 415 | | |
| 416 | | % obsolete |
| 417 | | obsolete_eclipse_preference('EXPAND_CLOSURES_FOR_STATE'). |
| 418 | | obsolete_eclipse_preference('BPARSER'). |
| 419 | | obsolete_eclipse_preference('DOT_LEAVES'). |
| 420 | | obsolete_eclipse_preference('SFDP'). |
| 421 | | obsolete_eclipse_preference('SHOW_FULL_ERROR_LOCATIONS'). |
| 422 | | obsolete_eclipse_preference('WARN_WHEN_EXPANDING_INFINITE_CLOSURES'). |
| 423 | | |
| 424 | | |
| 425 | | |
| 426 | | print_eclipse_prefs :- findall(X,eclipse_preference(X,_),Xs), sort(Xs,SXs), |
| 427 | | member(X,SXs), |
| 428 | | eclipse_preference(X,P), |
| 429 | | preference_val_type(P,VT), |
| 430 | | preference_description(P,Desc), |
| 431 | | preference(P,Val), |
| 432 | | preference_default_value(P,Def), |
| 433 | | (Def=Val -> Info = '' ; Info = ' *'), |
| 434 | | format(' ~w = ~w~w : ~w ==> ~w~n',[X,Val,Info,VT,Desc]), |
| 435 | | fail. |
| 436 | | print_eclipse_prefs :- preference_group_description(Group,Desc), |
| 437 | | findall(Setting,preference_group_val(Group,Setting,_,_),S), |
| 438 | | sort(S,Sorted), |
| 439 | | format(' * PREFERENCE GROUP ~w : SETTINGS ~w : ~w~n',[Group,Sorted,Desc]), |
| 440 | | fail. |
| 441 | | print_eclipse_prefs. |
| 442 | | |
| 443 | | |
| 444 | | :- dynamic preference/2. |
| 445 | | |
| 446 | | % add clause in case init_preferences forgotten |
| 447 | | preference(A,B) :- format(user_error,'Preferences not initalised (~w,~w)',[A,B]),trace, |
| 448 | | init_preferences,!, preference(A,B). |
| 449 | | %add_internal_error('Preferences not initialised: ',preference(A,B)),fail. |
| 450 | | |
| 451 | | |
| 452 | | % ------------------ |
| 453 | | |
| 454 | | preference_default_value(maxint,3). % 2147483647 |
| 455 | | preference_default_value(minint,-1). %-2147483648 |
| 456 | | preference_default_value(number_animated_abstractions, 20). |
| 457 | | preference_default_value(globalsets_fdrange,2). |
| 458 | | preference_default_value(do_invariant_checking,true). |
| 459 | | %preference_default_value(do_full_invariant_checking,true). |
| 460 | | %preference_default_value(use_new_kernel,false). |
| 461 | | preference_default_value(find_abort_values,false). |
| 462 | | preference_default_value(raise_abort_immediately,false). |
| 463 | | preference_default_value(treat_outermost_pre_as_select,true). |
| 464 | | preference_default_value(require_operations_to_assign_all_outputs,false). |
| 465 | | preference_default_value(allow_operations_to_read_outputs,false). |
| 466 | | preference_default_value(allow_simultaneous_assignments,false). |
| 467 | | preference_default_value(cspm_animate_all_processes_without_arguments,false). |
| 468 | | preference_default_value(cspm_animate_all_processes,false). |
| 469 | | %preference_default_value(cspm_display_inout,false). |
| 470 | | preference_default_value(cspm_detailed_animation,false). |
| 471 | | preference_default_value(cspm_strip_source_location,false). |
| 472 | | %preference_default_value(csp_event_visible_to_user,false). |
| 473 | | %preference_default_value(cspm_allow_incomplete_records,false). |
| 474 | | %preference_default_value(findOnlyOneSol,false). |
| 475 | | preference_default_value(maxNrOfInitialisations,4). |
| 476 | | preference_default_value(randomisedRestartInitalisations,false). |
| 477 | | preference_default_value(maxNrOfEnablingsPerOperation,10). |
| 478 | | preference_default_value(time_out,2500). |
| 479 | | preference_default_value(debug_time_out_factor,5). |
| 480 | | %preference_default_value(use_large_jvm_for_parser,false). |
| 481 | | preference_default_value(show_initialisation_arguments,true). |
| 482 | | preference_default_value(deterministic_trace_replay,false). |
| 483 | | %preference_default_value(animate_skip_operations,true). |
| 484 | | preference_default_value(show_eventb_any_arguments,false). |
| 485 | | preference_default_value(convert_comprehension_sets_into_closures,false). /* <------------ was true */ |
| 486 | | preference_default_value(use_clpfd_solver,true). % Default was changed from false to true on November 28 2013; commit d26b1bf1edeb29d630cf798c0773bfa1ba71219b |
| 487 | | preference_default_value(use_chr_solver,false). |
| 488 | | preference_default_value(data_validation_mode,false). |
| 489 | | preference_default_value(use_smt_mode,false). |
| 490 | | preference_default_value(solver_strength,0). |
| 491 | | preference_default_value(remove_implied_constraints,false). |
| 492 | | preference_default_value(lift_existential_quantifiers,false). |
| 493 | | preference_default_value(use_common_subexpression_elimination,false). % CSE |
| 494 | | preference_default_value(use_common_subexpression_also_for_predicates,true). % CSE_PRED |
| 495 | | preference_default_value(use_common_subexpression_also_for_substitutions,false). % CSE_SUBST |
| 496 | | preference_default_value(use_common_subexpression_wd_only,false). % CSE_WD_ONLY |
| 497 | | preference_default_value(normalize_ast,false). % NORMALIZE_AST |
| 498 | | preference_default_value(optimize_ast,true). % OPTIMIZE_AST |
| 499 | | preference_default_value(useless_code_elimination,false). % see test 1660 |
| 500 | | preference_default_value(compile_while_body,true). % COMPILE_WHILE |
| 501 | | preference_default_value(detect_lambdas,false). % DETECT_LAMBDAS |
| 502 | | preference_default_value(ltsmin_guard_splitting,false). |
| 503 | | preference_default_value(ltsmin_do_not_evaluate_top_level_guards,false). |
| 504 | | preference_default_value(fail_if_clpfd_timeout,false). |
| 505 | | %preference_default_value(allow_recursive_closures,false). |
| 506 | | preference_default_value(use_static_ordering,false). |
| 507 | | preference_default_value(use_state_packing,false). |
| 508 | | preference_default_value(provide_trace_information,false). |
| 509 | | preference_default_value(performance_monitoring_on,false). |
| 510 | | preference_default_value(partition_predicates,true). |
| 511 | | preference_default_value(partition_predicates_inline_equalities,true). |
| 512 | | preference_default_value(use_closure_expansion_memoization,false). |
| 513 | | preference_default_value(use_function_memoization,false). |
| 514 | | preference_default_value(allow_incomplete_partial_setup_constants,false). |
| 515 | | preference_default_value(re_execute_operations_with_side_effects,false). |
| 516 | | preference_default_value(warn_if_definition_hides_variable,true). |
| 517 | | preference_default_value(type_check_definitions,false). % can consume time, see test 778; and produces error messages for some tests |
| 518 | | %preference_default_value(warn_when_expanding_infinite_closures,5). |
| 519 | | preference_default_value(allow_enumeration_of_infinite_types,true). |
| 520 | | 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 |
| 521 | | preference_default_value(strict_raise_enum_warnings,false). |
| 522 | | preference_default_value(clash_strict_checks,false). |
| 523 | | preference_default_value(perform_stricter_static_checks,false). |
| 524 | | preference_default_value(ignore_prj_types,false). |
| 525 | | %preference_default_value(never_convert_closures_into_explicit_form,false). |
| 526 | | %preference_default_value(convert_types_into_closures,true). |
| 527 | | %preference_default_value(convert_closures_into_explicit_form_for_store,true). % <--- maybe remove preference |
| 528 | | %preference_default_value(allow_empty_global_sets,false). |
| 529 | | %preference_default_value(test_case_gen_stop_at_first_error,false). |
| 530 | | preference_default_value(prefix_internal_operation_arguments,'$none'). %all operations arguments are external and shown in testcases |
| 531 | | preference_default_value(generate_minimal_nr_of_testcases,true). |
| 532 | | preference_default_value(use_tk_custom_state_viewer,true). |
| 533 | | preference_default_value(tk_custom_state_viewer_font_name,''). |
| 534 | | preference_default_value(tk_custom_state_viewer_font_size,0). |
| 535 | | preference_default_value(tk_custom_state_viewer_padding,0). |
| 536 | | preference_default_value(tk_custom_state_viewer_str_padding,10). |
| 537 | | preference_default_value(use_small_window,false). |
| 538 | | preference_default_value(tk_show_source_pane,true). |
| 539 | | preference_default_value(ignore_hash_collisions,false). |
| 540 | | preference_default_value(forget_state_space,false). |
| 541 | | preference_default_value(store_only_one_incoming_transition,false). |
| 542 | | %preference_default_value(enable_permutation_reducation,false). |
| 543 | | %preference_default_value(use_symmetry_marker_hash,false). |
| 544 | | %preference_default_value(enable_canonical_symmetry,false). |
| 545 | | %preference_default_value(use_nauty_symmetry_reduction,false). |
| 546 | | preference_default_value(symmetry_mode,off). |
| 547 | | preference_default_value(use_static_symmetry_detection,true). |
| 548 | | preference_default_value(bool_expression_as_predicate,false). |
| 549 | | preference_default_value(allow_untyped_identifiers,false). |
| 550 | | preference_default_value(repl_unicode,false). |
| 551 | | preference_default_value(repl_cache_parsing,false). |
| 552 | | preference_default_value(latex_encoding,auto). |
| 553 | | preference_default_value(latex_pp_greek_ids,false). |
| 554 | | preference_default_value(xml_encoding,auto). |
| 555 | | preference_default_value(view_probcli_errors_using_bbresults,false). |
| 556 | | preference_default_value(eventtrace,false). |
| 557 | | preference_default_value(store_event_transinfo,false). |
| 558 | | preference_default_value(try_kodkod_on_load,false). |
| 559 | | preference_default_value(kodkod_for_components,true). |
| 560 | | preference_default_value(kodkod_raise_warnings,false). |
| 561 | | preference_default_value(kodkod_max_nr_solutions,22). |
| 562 | | preference_default_value(kodkod_symmetry_level,0). |
| 563 | | preference_default_value(kodkod_sat_solver,sat4j). |
| 564 | | preference_default_value(smt_supported_interpreter,false). |
| 565 | | preference_default_value(use_record_construction,true). % was false |
| 566 | | preference_default_value(seen_machines_included,false). |
| 567 | | preference_default_value(allow_sequence_operators_on_strings,true). |
| 568 | | |
| 569 | | preference_default_value(dot_print_edge_labels,true). |
| 570 | | preference_default_value(dot_print_action_arguments,true). |
| 571 | | preference_default_value(dot_print_functions,false). |
| 572 | | preference_default_value(dot_print_self_loops,true). |
| 573 | | preference_default_value(dot_print_arc_colors,true). |
| 574 | | preference_default_value(dot_print_root,true). |
| 575 | | %preference_default_value(dot_print_leaves,true). |
| 576 | | preference_default_value(dot_print_node_ids,false). |
| 577 | | preference_default_value(dot_print_use_constants,true). |
| 578 | | preference_default_value(dot_print_node_info,true). |
| 579 | | preference_default_value(dot_use_ps_viewer,false). |
| 580 | | preference_default_value(path_to_dot,Path) :- try_get_program_path('dot',Path). |
| 581 | | preference_default_value(dot_default_engine,dot). |
| 582 | | preference_default_value(path_to_dotty,VIEWER) :- (possible_program(dot_viewer,E) -> VIEWER=E ; VIEWER ='dotty'). |
| 583 | | %preference_default_value(path_to_dotty,'/Applications/OmniGraffle/OmniGraffle.app/Contents/MacOS/OmniGraffle'). |
| 584 | | 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 |
| 585 | | preference_default_value(path_to_ps_viewer,VIEWER) :- |
| 586 | | (possible_program(ps_viewer,E) -> VIEWER=E ; VIEWER ='gv'). |
| 587 | | %preference_default_value(path_to_ps_viewer,'open -a /Applications/Preview.app') :- host_platform(darwin). |
| 588 | | %preference_default_value(path_to_ps_viewer,'C:/Program Files/Ghostgum/gsview/gsview32') :- host_platform(windows). |
| 589 | | %preference_default_value(path_to_ps_viewer,'gv') :- host_platform(linux) ; host_platform(unknown). |
| 590 | | %preference_default_value(path_to_ps_viewer,'open -a /Applications/MacGhostViewX_Folder/MacGhostViewX.app'). |
| 591 | | preference_default_value(dot_root_shape,invtriangle). |
| 592 | | preference_default_value(dot_node_penwidth,2). |
| 593 | | preference_default_value(dot_normal_node_shape,box). % egg,ellipse |
| 594 | | preference_default_value(dot_current_node_shape,doubleoctagon). |
| 595 | | preference_default_value(dot_open_node_colour,'#F4E3C1'). %'#E88C59' '#C96D37' |
| 596 | | preference_default_value(dot_scope_limit_node_colour,gray). |
| 597 | | preference_default_value(dot_normal_node_colour,'#99BF38'). |
| 598 | | preference_default_value(dot_invariant_violated_node_colour,'#FF3800'). %'#FF4409' |
| 599 | | preference_default_value(dot_fill_normal_nodes,false). |
| 600 | | preference_default_value(dot_normal_arc_colour,'#006391'). |
| 601 | | preference_default_value(dot_node_font_size,12). |
| 602 | | preference_default_value(dot_edge_font_size,12). |
| 603 | | preference_default_value(dot_colour_goal_nodes,true). |
| 604 | | preference_default_value(dot_goal_node_colour,orange). |
| 605 | | preference_default_value(dot_print_node_properties,false). |
| 606 | | preference_default_value(dot_counterexample_node_colour,brown). |
| 607 | | preference_default_value(dot_counterexample_op_colour,brown). |
| 608 | | preference_default_value(dot_hierarchy_max_ids,0). |
| 609 | | |
| 610 | | preference_default_value(dot_event_hierarchy_horizontal,true). |
| 611 | | preference_default_value(dot_event_hierarchy_machine_colour,gray95). |
| 612 | | preference_default_value(dot_event_hierarchy_refines_colour,'#C0A060'). % Dark Khaki; see http://www.gpeters.com/color/color-schemes.php?search_term=Art+Nouveau |
| 613 | | preference_default_value(dot_event_hierarchy_new_event_colour,'#C06040'). % Coral '#C08040'). % Peru |
| 614 | | preference_default_value(dot_event_hierarchy_rename_event_colour,'#E0E0A0'). % Pale Goldenrod |
| 615 | | preference_default_value(dot_event_hierarchy_rename_unchanged_event_colour,'#E0F0E0'). % Honeydew |
| 616 | | preference_default_value(dot_event_hierarchy_unchanged_event_colour,gray92). |
| 617 | | preference_default_value(dot_event_hierarchy_grd_strengthening_event_colour,gray83). |
| 618 | | preference_default_value(dot_event_hierarchy_grd_keeping_event_colour,'#E0C080'). % Burlywood |
| 619 | | preference_default_value(dot_event_hierarchy_edge_colour,'#806040'). % Sienna |
| 620 | | preference_default_value(dot_event_hierarchy_extends_colour,gray50). |
| 621 | | |
| 622 | | preference_default_value(dot_projection_non_det_edge_colour,'#806040'). % Sienna; alternative :#A06040 Light Salmon |
| 623 | | preference_default_value(dot_projection_det_edge_colour,black). |
| 624 | | preference_default_value(dot_projection_non_definite_edge_style,dashed). |
| 625 | | preference_default_value(dot_projection_definite_edge_style,solid). |
| 626 | | preference_default_value(dot_projection_label_limit,75). |
| 627 | | preference_default_value(dot_use_unicode,true). |
| 628 | | preference_default_value(dot_predicate_node_shape,rect). |
| 629 | | preference_default_value(dot_expression_node_shape,record). |
| 630 | | preference_default_value(dot_var_mod_hide_only_written,false). |
| 631 | | |
| 632 | | |
| 633 | | preference_default_value(mc_dc_default_level,2). |
| 634 | | |
| 635 | | preference_default_value(dot_enabling_show_readwrites,true). |
| 636 | | |
| 637 | | preference_default_value(dot_definitions_use_sub_graph,true). |
| 638 | | preference_default_value(dot_definitions_show_all,false). |
| 639 | | preference_default_value(dot_state_graph_decompose,true). |
| 640 | | |
| 641 | | preference_default_value(font_size,'Monaco 12') :- host_platform(darwin). |
| 642 | | % Monaco looks better than Courier on Mac, Consolas |
| 643 | | % Note: ctext seems to use a non-monospaced font for TkFixedFont |
| 644 | | preference_default_value(font_size,'TkFixedFont 12') :- host_platform(X), X\==darwin. % alternative: Courier, Monaco, Consolas |
| 645 | | preference_default_value(font_name,'Monaco') :- host_platform(darwin). |
| 646 | | preference_default_value(font_name,'TkFixedFont') :- host_platform(X), X\==darwin. % alternative: Courier, Monaco |
| 647 | | preference_default_value(font_size_only,12). |
| 648 | | preference_default_value(use_font_size_for_columns,false). |
| 649 | | preference_default_value(allow_source_code_editing,true). |
| 650 | | preference_default_value(show_line_numbers,false). |
| 651 | | %preference_default_value(show_full_error_span,true). |
| 652 | | preference_default_value(highlight_brackets,true). |
| 653 | | preference_default_value(highlight_current_line,true). |
| 654 | | preference_default_value(ask_when_content_changed,false). |
| 655 | | preference_default_value(user_not_beginner,false). |
| 656 | | preference_default_value(user_is_an_expert_with_accessto_source_distribution,false). |
| 657 | | %preference_default_value(default_to_runtime_type_checking_on_startup_for_expert,false). |
| 658 | | preference_default_value(path_to_probe,'C:/probe/probe-1.30-windows/probe.exe') :- host_platform(windows). |
| 659 | | preference_default_value(path_to_probe,'more') :- host_platform(X), X\==windows. |
| 660 | | preference_default_value(path_to_spin,'xspin'). |
| 661 | | preference_default_value(path_to_cspm,'/usr/bin/cspm'). |
| 662 | | preference_default_value(path_to_text_editor,EDITOR) :- |
| 663 | | (possible_program(editor,E) -> EDITOR=E ; EDITOR =''). |
| 664 | | preference_default_value(path_to_text_editor_launch,EDITOR) :- |
| 665 | | (possible_program(editor_launch,E) -> EDITOR=E ; EDITOR ='vi'). |
| 666 | | %preference_default_value(path_to_fuzz,'fuzz'). |
| 667 | | preference_default_value(path_to_fdr,'fdr2'). |
| 668 | | preference_default_value(path_to_csp_typechecker,FDR3) :- |
| 669 | | (possible_program(fdr3,E) -> FDR3=E ; FDR3 ='refines'). |
| 670 | | preference_default_value(path_to_bcomp,'bcomp'). |
| 671 | | preference_default_value(path_to_atb_krt,Default) :- try_get_program_path('krt',KRT),!,Default=KRT. |
| 672 | | preference_default_value(path_to_java,Default) :- try_get_program_path('java',JJ),!,Default=JJ. |
| 673 | | preference_default_value(try_atb_provers,false). |
| 674 | | preference_default_value(symbolic_mc_try_other_solvers,false). |
| 675 | | preference_default_value(ltl_to_ba_tool,'lib/ltl2ba'). |
| 676 | | preference_default_value(prob2_trace_file,''). % no tracing |
| 677 | | preference_default_value(prob2_trace_file_gen_unique_name,false). |
| 678 | | |
| 679 | | |
| 680 | | preference_default_value(number_of_recent_documents,25). |
| 681 | | preference_default_value(number_of_searched_patterns,9). |
| 682 | | preference_default_value(number_of_replaced_patterns,9). |
| 683 | | preference_default_value(number_of_eval_history_elements,50). |
| 684 | | preference_default_value(number_of_eval_csp_history_elements,50). |
| 685 | | preference_default_value(number_of_checked_ltl_formulas,20). |
| 686 | | |
| 687 | | preference_default_value(do_syntax_highlighting,true). |
| 688 | | preference_default_value(sh_type_colour,darkred). |
| 689 | | preference_default_value(sh_logical_colour,tomato). |
| 690 | | preference_default_value(sh_assignments_colour,darkslateblue). |
| 691 | | preference_default_value(sh_operators,'#5883be'). |
| 692 | | preference_default_value(sh_top_level_keywords,blue). |
| 693 | | preference_default_value(sh_control_keywords,darkviolet). |
| 694 | | %preference_default_value(sh_includes_keywords,darkslateblue). |
| 695 | | preference_default_value(sh_comments,'#784e50'). |
| 696 | | preference_default_value(sh_pragmas,'#5b5b5b'). |
| 697 | | preference_default_value(sh_unsupported_background,yellow). |
| 698 | | |
| 699 | | preference_default_value(expand_forall_upto,100). |
| 700 | | preference_default_value(double_evaluation_when_analysing,true). |
| 701 | | preference_default_value(expand_avl_upto,100). |
| 702 | | preference_default_value(show_function_tuples_in_property,true). |
| 703 | | preference_default_value(bugly_pp_scrambling,false). |
| 704 | | preference_default_value(pp_propositional_logic_mode,false). |
| 705 | | |
| 706 | | preference_default_value(allow_new_ops_in_refinement,false). |
| 707 | | preference_default_value(allow_local_operation_calls,false). |
| 708 | | preference_default_value(allow_operation_calls_in_expr,false). |
| 709 | | preference_default_value(allow_let_to_reuse_introduced_ids,false). |
| 710 | | preference_default_value(use_po,true). |
| 711 | | preference_default_value(try_operation_reuse,false). |
| 712 | | preference_default_value(randomise_operation_order,false). |
| 713 | | preference_default_value(randomise_enumeration_order,false). |
| 714 | | preference_default_value(set_rand,false). |
| 715 | | preference_default_value(rand_seed,2342452). |
| 716 | | |
| 717 | | preference_default_value(use_cbc_analysis,true). |
| 718 | | preference_default_value(timeout_cbc_analysis,300). |
| 719 | | |
| 720 | | preference_default_value(use_scope_predicate,true). |
| 721 | | preference_default_value(use_ignore_pragmas,false). |
| 722 | | |
| 723 | | preference_default_value(pge,off). |
| 724 | | preference_default_value(por,off). |
| 725 | | preference_default_value(por_heur,random). |
| 726 | | preference_default_value(use_por_for_ltl,false). |
| 727 | | preference_default_value(use_safety_ltl_model_checker,false). |
| 728 | | |
| 729 | | preference_default_value(enable_graph,false). |
| 730 | | preference_default_value(enable_graph_depth,1). |
| 731 | | |
| 732 | | preference_default_value(dependency_enable_predicates,false). |
| 733 | | |
| 734 | | preference_default_value(filter_unused_constants,false). |
| 735 | | preference_default_value(translate_force_all_typing_infos,false). |
| 736 | | preference_default_value(translate_print_typing_infos,false). |
| 737 | | preference_default_value(translate_print_frozen_infos,false). |
| 738 | | preference_default_value(translate_ids_to_parseable_format,false). |
| 739 | | preference_default_value(translate_suppress_rodin_positions_flag,false). |
| 740 | | preference_default_value(translate_print_all_sequences,false). |
| 741 | | preference_default_value(translate_print_cs_style_sequences,false). |
| 742 | | |
| 743 | | /* Disprover mode - deactivates some optimizations only valid for animation */ |
| 744 | | preference_default_value(disprover_mode,false). |
| 745 | | preference_default_value(trace_upon_error,false). |
| 746 | | preference_default_value(error_log_file,''). |
| 747 | | preference_default_value(tlc_number_of_workers,2). |
| 748 | | preference_default_value(unsat_core_algorithm,divide_and_conquer). |
| 749 | | |
| 750 | | preference_default_value(port, 5000). |
| 751 | | preference_default_value(ip, localhost). |
| 752 | | preference_default_value(max_states, 0). |
| 753 | | preference_default_value(tmpdir, '/tmp/'). |
| 754 | | preference_default_value(logdir, './distb-logs/'). |
| 755 | | preference_default_value(proxynumber, 0). |
| 756 | | preference_default_value(queue_threshold, 20). /* TODO: this is not used an implemented in the proxy (pk, 12.01.18) */ |
| 757 | | preference_default_value(hash_cycle, 25). |
| 758 | | |
| 759 | | preference_default_value(machines_path,Dir) :- |
| 760 | | catch(absolute_file_name(examples('.'),Dir),_,Dir='.'). |
| 761 | | |
| 762 | | |
| 763 | | |
| 764 | | :- use_module(library(file_systems),[file_exists/1,directory_exists/1]). |
| 765 | | try_get_program_path(Name,Path) :- |
| 766 | | (possible_program(Name,R) -> Path=R |
| 767 | | ; Path=Name). % hope in PATH |
| 768 | ? | possible_program(Type,E) :- host_platform(P),possible_program_aux(Type,P,E), |
| 769 | | (file_exists(E) -> true ; P=darwin, directory_exists(E)). |
| 770 | | |
| 771 | | :-use_module(library(system),[environ/2]). |
| 772 | | possible_program_aux(editor_launch,darwin,'/usr/local/bin/bbedit'). |
| 773 | | possible_program_aux(editor_launch,darwin,'/usr/local/bin/edit'). % Text Wrangler |
| 774 | | possible_program_aux(editor_launch,_,PATH) :- environ('EDITOR',PATH). |
| 775 | | possible_program_aux(editor_launch,darwin,'/usr/local/bin/atom'). |
| 776 | | possible_program_aux(editor_launch,linux,'/usr/local/bin/atom'). |
| 777 | | possible_program_aux(editor_launch,linux,'/usr/bin/kwrite'). |
| 778 | | possible_program_aux(editor_launch,linux,'/usr/bin/gedit'). |
| 779 | | possible_program_aux(editor_launch,linux,'/usr/bin/vim'). |
| 780 | | possible_program_aux(editor,darwin,'/Applications/BBEdit.app'). |
| 781 | | possible_program_aux(editor,darwin,'/Applications/TextWrangler.app'). |
| 782 | | possible_program_aux(editor,darwin,'/Applications/Atom.app'). |
| 783 | | possible_program_aux(editor,darwin,'/Applications/Sublime Text 2.app'). |
| 784 | | possible_program_aux(editor,darwin,'/Applications/TextMate.app'). |
| 785 | | possible_program_aux(editor,darwin,'/Applications/TextEdit.app'). |
| 786 | | 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 |
| 787 | | possible_program_aux(ps_viewer,darwin,'/Applications/Preview.app') :- prob_application_type(tcltk). % probcli cannot use open -a yet. |
| 788 | | possible_program_aux(ps_viewer,darwin,'/usr/bin/open'). |
| 789 | | possible_program_aux(ps_viewer,windows,'C:/Program Files/Ghostgum/gsview/gsview32'). |
| 790 | | possible_program_aux(dot_viewer,darwin,'/Applications/Graphviz.app') :- prob_application_type(tcltk). % probcli cannot use open -a yet |
| 791 | | possible_program_aux(dot_viewer,darwin,'/usr/bin/open'). |
| 792 | | possible_program_aux(dot_viewer,windows,'C:/Program Files/Graphviz2.38/bin/dotty.exe'). |
| 793 | | possible_program_aux(dot_viewer,windows,'C:/Program Files (x86)/Graphviz2.38/bin/dotty.exe'). |
| 794 | | possible_program_aux(krt,darwin,'/Applications/AtelierB.app/AB/bbin/macosx/krt'). |
| 795 | | possible_program_aux(java,windows,'C:/Program Files/Java/jre7/bin/java.exe'). |
| 796 | | possible_program_aux(java,P,'/usr/bin/java') :- unix(P). |
| 797 | | possible_program_aux(fdr3,darwin,'/Applications/FDR3.app/Contents/MacOS/refines'). |
| 798 | | possible_program_aux(fdr3,darwin,'/Applications/FDR4.app/Contents/MacOS/refines'). |
| 799 | | %possible_program_aux(sfdp,P,'/usr/local/bin/sfdp') :- unix(P). |
| 800 | | possible_program_aux(dot,P,'/usr/local/bin/dot') :- unix(P). |
| 801 | | possible_program_aux(dot,P,'/opt/local/bin/dot') :- unix(P). |
| 802 | | |
| 803 | | unix(darwin). |
| 804 | | unix(linux). |
| 805 | | |
| 806 | | /* ------------------------- */ |
| 807 | | |
| 808 | | % now in basic_tests.pl |
| 809 | | %:- assert_must_succeed( \+((preference_description(P,_D),\+preference_default_value(P,_Val)))). |
| 810 | | %:- assert_must_succeed( \+((preference_default_value(P,_D), \+preference_description(P,_Val)))). |
| 811 | | preference_description(maxNrOfInitialisations,'Max Number of Initialisations and Constant-Setups Computed'). |
| 812 | | 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)'). |
| 813 | | preference_description(maxNrOfEnablingsPerOperation,'Max Number of Enablings per Operation Computed'). |
| 814 | | 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)'). |
| 815 | | preference_description(globalsets_fdrange,'Size of unspecified deferred sets in SETS section'). |
| 816 | | preference_description(maxint,'value of MAXINT, used for expressions such as xx::NAT (2147483647 for 4 byte ints)'). |
| 817 | | preference_description(minint,'value of MININT, used for expressions such as xx::INT (-2147483648 for 4 byte ints)'). % Atelier-B uses 2147483647 |
| 818 | | preference_description(number_animated_abstractions,'How many levels of refined models are animated by default'). |
| 819 | | %preference_description(findOnlyOneSol,'Find only one solution per Operation or Initialisation'). |
| 820 | | preference_description(debug_time_out_factor,'Debug Properties: Multiplying Factor for Timeout'). |
| 821 | | %preference_description(use_large_jvm_for_parser,'Use large Heap and Stack size for Java Parser'). |
| 822 | | preference_description(do_invariant_checking,'Check invariant while animating and model checking'). |
| 823 | | %preference_description(do_neginvariant_checking,'Check negation of invariant'). |
| 824 | | %preference_description(do_full_invariant_checking,'Check types when checking invariant'). |
| 825 | | %preference_description(use_new_kernel,'Use new Kernel (only some basic operations supported, only fore PRE and INITs)'). |
| 826 | | 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'). |
| 827 | | 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; possible values false,true,full)'). |
| 828 | | preference_description(cspm_animate_all_processes,'Animate all CSP-M processes (also processes with arguments)'). |
| 829 | | preference_description(cspm_animate_all_processes_without_arguments,'Animate all CSP-M processes without arguments (not just MAIN)'). |
| 830 | | %preference_description(cspm_display_inout,'Display unsynchronised inputs/outputs as ?/!'). |
| 831 | | preference_description(cspm_detailed_animation,'Provide more fine-grained source-location animation for CSP (can slow model checking down)'). |
| 832 | | preference_description(cspm_strip_source_location,'Strip CSP source-location information (for RHS of processes, except for internal choice)'). |
| 833 | | %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).'). |
| 834 | | %preference_description(cspm_allow_incomplete_records,'Allow construction of incomplete records (e.g., for Casper files)'). |
| 835 | | preference_description(use_clpfd_solver,'Use CLP(FD) solver for B integers (restricts range to -2^28..2^28-1 on 32 bit machines)'). |
| 836 | | preference_description(use_chr_solver,'Use CHR based solver. Should speed up detection of unsolvable predicates, but might slow down solving in general.'). |
| 837 | | preference_description(data_validation_mode,'Assume everything can be computed without constraint solving.'). |
| 838 | | preference_description(convert_comprehension_sets_into_closures,'Lazy expansion of lambdas and set comprehensions'). |
| 839 | | preference_description(use_smt_mode,'Enable SMT-Mode (aggressive treatment of : and /: inside predicates)'). % will be set automatically in CBC mode; should normally not be set by user |
| 840 | | preference_description(solver_strength,'Strength of certain Solver propagations (0 is default)'). |
| 841 | | preference_description(remove_implied_constraints,'Remove unnecessary constraints implied by other constraints'). |
| 842 | | preference_description(lift_existential_quantifiers,'Lift existential quantifiers, i.e., treat existentially quantified variables like ordinary variables'). |
| 843 | | preference_description(use_common_subexpression_elimination,'Enable CSE (Common Subexpression Elimination)'). |
| 844 | | preference_description(use_common_subexpression_also_for_predicates,'Apply CSE (if enabled) also to predicates'). |
| 845 | | preference_description(use_common_subexpression_also_for_substitutions,'Apply CSE (if enabled) also to substitutions (operation/event bodies) [EXPERIMENTAL]'). |
| 846 | | preference_description(use_common_subexpression_wd_only,'Apply CSE (if enabled) only to well-defined sub-formulas'). |
| 847 | | preference_description(normalize_ast,'Normalize AST before passing to ProB kernel (rewrites many B predicates into simpler form)'). |
| 848 | | preference_description(optimize_ast,'Optimize AST (Abstract Syntax Tree) before passing to ProB kernel (rewrites many B predicates into more efficient form)'). |
| 849 | | preference_description(useless_code_elimination,'Useless Code Elimination: try and find useless statements which have no influence on the result of an operation.'). |
| 850 | | preference_description(compile_while_body,'Compile bodies of WHILE loops if variant large'). |
| 851 | | preference_description(detect_lambdas,'Detect set comprehensions which can be rewritten into lambdas.'). |
| 852 | | 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'). |
| 853 | | preference_description(ltsmin_do_not_evaluate_top_level_guards,'Do not evaluate top-level GUARDS detected when ltsmin_guard_splitting is true'). |
| 854 | | preference_description(fail_if_clpfd_timeout,'Assume failure if posting a CLP(FD) constraint times-out'). |
| 855 | | %preference_description(allow_recursive_closures,'Lazy expansion of *Recursive* set Comprehensions and lambdas'). |
| 856 | | preference_description(use_static_ordering,'Use static ordering to enumerate constants which occur in most PROPERTIES first'). |
| 857 | | preference_description(use_state_packing,'Use more aggressive COMPRESSION when storing states'). |
| 858 | | preference_description(provide_trace_information,'Provide various tracing information on the terminal/console.'). |
| 859 | | preference_description(performance_monitoring_on,'Provide performance monitoring information on the terminal/console.'). |
| 860 | | preference_description(partition_predicates,'Partition predicates (PROPERTIES) into components'). |
| 861 | | preference_description(partition_predicates_inline_equalities,'Inline equalities when partitioning into components'). |
| 862 | | preference_description(use_closure_expansion_memoization,'MEMOize expansions of set comprehensions and lambda abstractions.'). |
| 863 | | preference_description(use_function_memoization,'MEMOIZE function applications of all functions defined in ABSTRACT_CONSTANTS (even if not marked with /*@desc memo */).'). |
| 864 | | preference_description(allow_incomplete_partial_setup_constants,'Allow ProB to proceed even if only part of the CONSTANTS have been found.'). |
| 865 | | 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).'). |
| 866 | | preference_description(warn_if_definition_hides_variable,'Warn if a DEFINITION hides a variable with the same name'). |
| 867 | | preference_description(type_check_definitions,'Type check all visible DEFINITIONs (not just used ones)'). |
| 868 | | %preference_description(warn_when_expanding_infinite_closures,'Warn when expanding infinite closures if MAXINT larger than: '). |
| 869 | | preference_description(allow_enumeration_of_infinite_types,'Allow enumeration of infinite types'). |
| 870 | | preference_description(strict_raise_warnings,'Treat warnings as errors (Warning: can generate spurious NOT-WELL-DEFINED messages).'). |
| 871 | | preference_description(strict_raise_enum_warnings,'Treat ENUMERATION warnings (aka VIRTUAL TIME-OUTS) as errors (Warning: can generate spurious NOT-WELL-DEFINED messages).'). |
| 872 | | preference_description(clash_strict_checks,'Do a stricter checking for name CLASHES in B machines'). |
| 873 | | preference_description(perform_stricter_static_checks,'Perform stricter additional static checks on formulas (automatically set by ProB).'). |
| 874 | | preference_description(ignore_prj_types,'Ignore types of prj1 and prj2 (i.e., prj1({1},{1})(2,3) is considered well-defined'). |
| 875 | | |
| 876 | | %preference_description(never_convert_closures_into_explicit_form,'Never convert closures back into explicit form (only use for debugging !)'). |
| 877 | | %preference_description(convert_types_into_closures,'Lazy expansion of type expressions (POW,-->,...)'). |
| 878 | | %preference_description(convert_closures_into_explicit_form_for_store,'Convert lazy form back into explicit form for Variables, Constants, Operation Arguments'). |
| 879 | | %preference_description(allow_empty_global_sets,'Allow empty global SETs'). |
| 880 | | %preference_description(test_case_gen_stop_at_first_error,'Stop at first error in test case generation'). |
| 881 | | preference_description(prefix_internal_operation_arguments,'Prefix of internal operation arguments (these are not included in test cases)'). |
| 882 | | preference_description(generate_minimal_nr_of_testcases,'Generate minimal suite of mcm testcases (and not one per event)'). |
| 883 | | preference_description(use_tk_custom_state_viewer,'Use custom Tk viewer to represent state of B Machine'). |
| 884 | | preference_description(tk_custom_state_viewer_font_name,'Font for animation strings (if empty, the editor font will be used)'). |
| 885 | | preference_description(tk_custom_state_viewer_font_size,'Font size for animation strings (if 0, the editor font size will be used)'). |
| 886 | | preference_description(tk_custom_state_viewer_padding,'Padding (in pixels) between images of custom TK state viewer'). |
| 887 | | preference_description(tk_custom_state_viewer_str_padding,'Padding (in pixels) between strings of custom TK state viewer'). |
| 888 | | preference_description(use_small_window,'Use a small main window for ProB (useful on small screens)'). |
| 889 | | preference_description(tk_show_source_pane,'Show the B Source Code'). |
| 890 | | preference_description(ignore_hash_collisions,'Ignore Hash Collisions (if true not all states may be computed, visited states are not memorised !)'). |
| 891 | | preference_description(forget_state_space,'Do not remember state space (mainly useful in conjunction with IGNORE_HASH_COLLISIONS)'). |
| 892 | | 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, deadlocks, assertions). Do not use for LTL model checking, deadlock checking or animation.'). |
| 893 | | %preference_description(enable_permutation_reducation,'Enable Permutation Flooding'). |
| 894 | | %preference_description(use_symmetry_marker_hash,'Use Symmetry Hash Marker'). |
| 895 | | %preference_description(enable_canonical_symmetry,'Enable Symmetry Reduction by Canonical Form Computation'). |
| 896 | | %preference_description(use_nauty_symmetry_reduction,'Use Nauty ((c) McKay) C Library for Symmetry Reduction with Canonical Form Computation'). |
| 897 | | preference_description(symmetry_mode,'Symmetry Mode: off,flood,canon,nauty,hash'). |
| 898 | | preference_description(use_static_symmetry_detection,'Detect symmetries in forall/exists and in PROPERTIES for deferred sets'). |
| 899 | | 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)' ). |
| 900 | | preference_description(allow_untyped_identifiers,'Allow UNTYPED identifiers (they will be assigned new deferred sets as type)' ). |
| 901 | | preference_description(repl_unicode,'Use UNICODE in REPL and editing window'). |
| 902 | | preference_description(repl_cache_parsing,'Cache parsing in REPL (useful if same formula gets parsed multiple times, e.g., for Latex processing)'). |
| 903 | | preference_description(latex_encoding,'Encoding used for Latex processing with -latex (auto,ISO-8859-1,ISO-8859-2,UTF-8,UTF-16,...)'). |
| 904 | | preference_description(latex_pp_greek_ids,'Prety-print Greek identifiers (Sigma,...) in Latex mode'). |
| 905 | | preference_description(xml_encoding,'Encoding used for XML processing, e.g., with -logxml (auto,ISO-8859-1,ISO-8859-2,UTF-8,UTF-16,...)'). |
| 906 | | preference_description(view_probcli_errors_using_bbresults,'Show probcli errors using the BBEdit (11.6 or newer) bbresults command'). |
| 907 | | |
| 908 | | preference_description(eventtrace,'Store trace for each event (may cause large memory requirement)'). |
| 909 | | preference_description(store_event_transinfo,'Store Event-B Event-Info for each event (may cause larger memory requirement)'). |
| 910 | | preference_description(try_kodkod_on_load,'Apply translation to KODKOD on PROPERTIES when loading machines'). |
| 911 | | preference_description(kodkod_for_components,'Translate only complete components to KODKOD'). |
| 912 | | preference_description(kodkod_raise_warnings,'Raise WARNING when component or predicate cannot be translated to KODKOD'). |
| 913 | | preference_description(kodkod_max_nr_solutions,'Maximum number of solutions computed and sent by KODKOD per batch.'). |
| 914 | | 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'). |
| 915 | | % 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. |
| 916 | | preference_description(kodkod_sat_solver,'SAT solver used for Kodkod (sat4j, minisat, lingeling, glucose)'). |
| 917 | | preference_description(smt_supported_interpreter,'Use Z3 / CVC4 for predicates inside the B interpreter'). |
| 918 | | preference_description(use_record_construction,'Records: Check if axioms/properties describe a record pattern'). |
| 919 | | preference_description(seen_machines_included,'Seen/used machines are included (no operations available) instead of extended'). |
| 920 | | preference_description(allow_sequence_operators_on_strings,'Allow sequence operators (^) to be applied to STRINGs'). |
| 921 | | preference_description(show_eventb_any_arguments,'Show top-level ANY variable values of B Operations without parameters as parameters'). |
| 922 | | 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 |
| 923 | | %preference_description(animate_skip_operations,'Animate operations which are skip or PRE C THEN skip'). |
| 924 | | preference_description(deterministic_trace_replay,'Replay Traces without backtracking (to reduce memory consumption)'). |
| 925 | | preference_description(treat_outermost_pre_as_select,'Treat outermost PRE as SELECT'). |
| 926 | | preference_description(require_operations_to_assign_all_outputs,'Require operations to assign to all outputs'). |
| 927 | | preference_description(allow_operations_to_read_outputs,'Allow B operations to read outputs; output values will be initialised to default value in animator.'). |
| 928 | | preference_description(allow_simultaneous_assignments,'Allow B operations to assign multiple times to same variable (ASM style)'). |
| 929 | | |
| 930 | | %preference_description(check_prolog_b_ast,'Check the abstract syntax tree for B machines'). |
| 931 | | preference_description(dot_print_edge_labels,'Show Edge Labels (Operation Names)'). |
| 932 | | preference_description(dot_print_action_arguments,'Print Operation Arguments (when Edge Labels shown)'). |
| 933 | | preference_description(dot_print_functions,'Print Functions (operations that return values w/o changing state)'). |
| 934 | | preference_description(dot_print_self_loops,'Print Self-Loops'). |
| 935 | | %preference_description(dot_print_leaves,'Print Leaves'). |
| 936 | | preference_description(dot_print_arc_colors,'Colour the arcs (disable for import in OmniGraffle)'). |
| 937 | | preference_description(dot_print_root,'Print Root Node'). |
| 938 | | preference_description(dot_print_node_ids,'Print Node Identifiers'). |
| 939 | | preference_description(dot_print_node_info,'Print Node information (values of variables)'). |
| 940 | | preference_description(dot_print_use_constants,'Use constants for deferred set values if possible'). |
| 941 | | preference_description(dot_use_ps_viewer,'Use Postscript Viewer'). |
| 942 | | preference_description(path_to_dot,'Path/Command for dot program (using "/" even on Windows. Try avoiding spaces in path)'). |
| 943 | | preference_description(dot_default_engine,'Default layout engine used for dot (dot,neato,sfdp,fdp,twopi,circo)'). |
| 944 | | preference_description(path_to_dotty,'Path/Command for dot viewer (e.g., dotty)'). |
| 945 | | %preference_description(path_to_sfdp,'Path/Command for sfdp program for dot files (using "/" even on Windows. Try avoiding spaces in path)'). |
| 946 | | preference_description(path_to_ltsmin,'Path to LTSmin commands, such as prob2lts-sym for symbolic model checking (not available for Windows.)'). |
| 947 | | preference_description(path_to_ps_viewer,'Path/Command for Postscript viewer'). |
| 948 | | preference_description(dot_root_shape,'Shape for root node (invtriangle,triangle, ellipse, box, diamond,...)'). |
| 949 | | preference_description(dot_normal_node_shape,'Shape for normal node'). |
| 950 | | preference_description(dot_current_node_shape,'Shape for current node'). |
| 951 | | 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'). |
| 952 | | preference_description(dot_scope_limit_node_colour,'Colour for open, but uninteresting nodes (red,green,blue,gray,... or rgb hex #ff00ff)'). |
| 953 | | preference_description(dot_normal_node_colour,'Colour for normal node'). |
| 954 | | preference_description(dot_node_penwidth,'Pen width for nodes'). |
| 955 | | preference_description(dot_invariant_violated_node_colour,'Colour for invariant violation'). |
| 956 | | preference_description(dot_fill_normal_nodes,'Fill normal nodes with color'). |
| 957 | | preference_description(dot_normal_arc_colour,'Colour for normal arcs'). |
| 958 | | preference_description(dot_node_font_size,'Font Size for Node labels'). |
| 959 | | preference_description(dot_edge_font_size,'Font Size for Edge labels'). |
| 960 | | preference_description(dot_colour_goal_nodes,'Colour the nodes that satisfy the GOAL predicate'). |
| 961 | | preference_description(dot_goal_node_colour,'Colour for nodes satisfying the GOAL predicate'). |
| 962 | | preference_description(dot_print_node_properties,'Show properties of statespace node (useful for CSP models)'). |
| 963 | | preference_description(dot_counterexample_node_colour,'Colour for counterexample nodes'). |
| 964 | | preference_description(dot_counterexample_op_colour,'Colour for counterexample transitions'). |
| 965 | | preference_description(dot_hierarchy_max_ids,'Max. number of identifiers shown in hierarchy view (-1 to show all)'). |
| 966 | | |
| 967 | | preference_description(dot_event_hierarchy_horizontal,'Organize refinements horizontally'). |
| 968 | | preference_description(dot_event_hierarchy_machine_colour,'Colour for machine event cluster'). |
| 969 | | preference_description(dot_event_hierarchy_refines_colour,'Colour for events refining themselves (i.e., not renamed and modifying guard or action)'). |
| 970 | | preference_description(dot_event_hierarchy_new_event_colour,'Colour for new events (not refining any event)'). |
| 971 | | preference_description(dot_event_hierarchy_rename_event_colour,'Colour for renamed events (with change in guard or action)'). |
| 972 | | preference_description(dot_event_hierarchy_rename_unchanged_event_colour,'Colour for renamed unchanged events'). |
| 973 | | preference_description(dot_event_hierarchy_unchanged_event_colour,'Colour for unchanged events (not renamed, no guards or actions added)'). |
| 974 | | preference_description(dot_event_hierarchy_grd_strengthening_event_colour,'Colour for events just adding a guard (not renamed, no actions added)'). |
| 975 | | preference_description(dot_event_hierarchy_grd_keeping_event_colour,'Colour for events just changing an action (not renamed, keeping guard unchanged)'). |
| 976 | | preference_description(dot_event_hierarchy_edge_colour,'Edge colour for refine relation'). |
| 977 | | preference_description(dot_event_hierarchy_extends_colour,'Edge colour for extends relation'). |
| 978 | | |
| 979 | | preference_description(dot_projection_non_det_edge_colour,'Edge colour for deterministic edges'). |
| 980 | | preference_description(dot_projection_det_edge_colour,'Edge colour for non-deterministic edges'). |
| 981 | | preference_description(dot_projection_non_definite_edge_style,'Style for non-definite edges (solid,dashed,dotted,bold,invis)'). |
| 982 | | preference_description(dot_projection_definite_edge_style,'Style for definite edges (solid,dashed,dotted,bold,invis)'). |
| 983 | | preference_description(dot_projection_label_limit,'Max. nr of characters for node labels'). |
| 984 | | preference_description(dot_use_unicode,'Use Unicode symbols for values and formulas'). |
| 985 | | preference_description(dot_predicate_node_shape,'Shape for predicate nodes in formula trees'). |
| 986 | | preference_description(dot_expression_node_shape,'Shape for expression nodes in formula trees'). |
| 987 | | preference_description(dot_var_mod_hide_only_written,'Hide variables which are only written and not read in any guard'). |
| 988 | | |
| 989 | | |
| 990 | | preference_description(mc_dc_default_level,'Default Predicate Expansion Level for MC/DC Coverage Analyses (0=no expansion, 1=only top level connective expanded,...)'). |
| 991 | | |
| 992 | | preference_description(dot_enabling_show_readwrites,'Show read/write info for enabling diagrams'). |
| 993 | | |
| 994 | | preference_description(dot_definitions_use_sub_graph,'Show expression-, predicate-, substitution-DEFINITIONS as sub-graphs'). |
| 995 | | preference_description(dot_definitions_show_all,'Show all DEFINITIONS'). |
| 996 | | preference_description(dot_state_graph_decompose,'Decompose sets and complex pairs into individual vertices'). |
| 997 | | |
| 998 | | preference_description(font_size,'Font size in main window'). |
| 999 | | preference_description(font_name,'Font name in text editor'). |
| 1000 | | preference_description(font_size_only,'Font size in text editor'). |
| 1001 | | preference_description(use_font_size_for_columns,'Use font size also for columns (you need to reselect font size + Courier will be used)'). |
| 1002 | | preference_description(allow_source_code_editing,'Allow editing and saving of main B machine file'). |
| 1003 | | preference_description(show_line_numbers,'Show line numbers in main window'). |
| 1004 | | %preference_description(show_full_error_span,'Show also the end line and column in error messages'). |
| 1005 | | preference_description(highlight_brackets,'Highlights brackets'). |
| 1006 | | preference_description(highlight_current_line,'Highlights current line'). |
| 1007 | | preference_description(ask_when_content_changed,'Asking when file content changed from external program'). |
| 1008 | | preference_description(user_not_beginner,'User is not a beginner'). |
| 1009 | | preference_description(user_is_an_expert_with_accessto_source_distribution,'User is expert with access to source distribution of ProB'). |
| 1010 | | %preference_description(default_to_runtime_type_checking_on_startup_for_expert,'When starting up (in expert mode) turn runtime type checking on'). |
| 1011 | | preference_description(path_to_probe,'Path to Probe or other tool to view .csp files'). |
| 1012 | | preference_description(path_to_spin,'Path to Spin or other tool to view .prom files'). |
| 1013 | | preference_description(path_to_cspm,'Path to cspm to view and analyze .csp files.'). |
| 1014 | | preference_description(path_to_text_editor,'Path to external GUI text editor'). |
| 1015 | | 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 ??! |
| 1016 | | %preference_description(path_to_fuzz,'Path to the fuzz tool for ProZ'). |
| 1017 | | preference_description(path_to_fdr,'Path to the FDR2 tool'). |
| 1018 | | preference_description(path_to_csp_typechecker,'Path to a CSP type checking tool, such as refines from FDR3 (taking --typecheck as argument)'). |
| 1019 | | preference_description(path_to_bcomp,'Path to a bcomp (Atelier B Parser and type checker )'). |
| 1020 | | preference_description(path_to_java,'Path to the "java" command (in case java is not found on the PATH)'). |
| 1021 | | preference_description(path_to_atb_krt,'Path to Atelier B Provers krt tool'). |
| 1022 | | preference_description(try_atb_provers,'Try Atelier B Provers for unknown SMTLIB specifications'). |
| 1023 | | preference_description(symbolic_mc_try_other_solvers,'Symbolic Model Checking: Try different solver / settings combinations'). |
| 1024 | | preference_description(number_of_recent_documents,'Number of recently opened file names memorised'). |
| 1025 | | preference_description(number_of_searched_patterns,'Number of recently searched patterns in text'). |
| 1026 | | preference_description(number_of_replaced_patterns,'Number of recently replaced patterns in text'). |
| 1027 | | preference_description(number_of_eval_history_elements,'Number of recently runs of commands in the eval window'). |
| 1028 | | preference_description(number_of_eval_csp_history_elements,'Number of recently runs of commands in the eval window'). |
| 1029 | | preference_description(number_of_checked_ltl_formulas,'Number of recently checked LTL formulas'). |
| 1030 | | preference_description(ltl_to_ba_tool,'Tool in lib/ directory for generatin a Buechi automaton from LTL.'). |
| 1031 | | preference_description(prob2_trace_file,'Path to file to store prob2_execute_custom_operation results for later replay'). |
| 1032 | | preference_description(prob2_trace_file_gen_unique_name,'Make the file name for prob2_execute_custom_operation unique'). |
| 1033 | | |
| 1034 | | preference_description(do_syntax_highlighting,'Enable Syntax Colour Highlighting'). |
| 1035 | | preference_description(sh_type_colour,'Colour of typing constructs: NAT,POW,... (red,green,... or rgb hex #ff00ff)'). |
| 1036 | | preference_description(sh_logical_colour,'Colour of logical operators: &,or,...'). |
| 1037 | | preference_description(sh_assignments_colour,'Colour of assignments: :=, <-- and strings'). |
| 1038 | | preference_description(sh_operators,'Colour of normal operators ran,dom,...'). |
| 1039 | | preference_description(sh_top_level_keywords,'Colour of top level keywords: MACHINE, INVARIANT,...'). |
| 1040 | | preference_description(sh_control_keywords,'Colour of control keywords: IF, CASE,...'). |
| 1041 | | %preference_description(sh_includes_keywords,'Colour of inclusion related keywords: USES,...'). |
| 1042 | | preference_description(sh_comments,'Colour of comments /* ... */'). |
| 1043 | | preference_description(sh_pragmas,'Colour of pragmas /*@ ... */'). |
| 1044 | | preference_description(sh_unsupported_background,'Background colour for unsupported features (closure,...)'). |
| 1045 | | |
| 1046 | | preference_description(expand_forall_upto,'When analysing predicates: max. domain size for expansion of forall:'). |
| 1047 | | preference_description(double_evaluation_when_analysing,'Evaluate PREDICATES positively and negatively when analysing:'). |
| 1048 | | preference_description(expand_avl_upto,'Max size for pretty-printing sets (-1 means no limit) :'). |
| 1049 | | preference_description(show_function_tuples_in_property,'Show function tuples in state view or dot files (f(1)=2 instead of f={(1,2)})'). |
| 1050 | | preference_description(bugly_pp_scrambling,'Scramble identifiers when pretty-printing (BUGLY):'). |
| 1051 | | preference_description(pp_propositional_logic_mode,'Try and pretty-print formulas using propositional variables (A=TRUE will be printed as A)'). |
| 1052 | | |
| 1053 | | |
| 1054 | | preference_description(allow_new_ops_in_refinement,'Allow introduction of new operations in refinements (automatically set to TRUE for SYSTEM machines)'). |
| 1055 | | preference_description(allow_local_operation_calls,'Allow to call (local) operations in same machine'). |
| 1056 | | preference_description(allow_operation_calls_in_expr,'Allow to call query operations in (some) expressions'). |
| 1057 | | 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 ...)'). |
| 1058 | | |
| 1059 | | |
| 1060 | | preference_description(use_po,'Use PROOF information to restrict invariant checking to affected clauses.'). |
| 1061 | | %preference_description(use_po,'Restrict invariant checking to affected clauses. Also remove clauses that are proven (EventB)'). |
| 1062 | | preference_description(try_operation_reuse,'Reuse previously computed operation effects in B/Event-B (false,true:local propagation,full:cache projected state space per operation)'). % true: perfroms local propagation to successor states for statically computed operation pairs, full: caches a projected state space per eligible operation in LTSmin style |
| 1063 | | preference_description(randomise_operation_order,'Randomise order of operations when computing successor states.'). |
| 1064 | | preference_description(randomise_enumeration_order,'Randomise enumeration of variables.'). |
| 1065 | | preference_description(set_rand,'Use a fix seed for random number generator. Allows to reproduce results.'). |
| 1066 | | preference_description(rand_seed,'Seed for Random Number Generator'). |
| 1067 | | |
| 1068 | | preference_description(machines_path,'Last open directory'). |
| 1069 | | |
| 1070 | | % Options for enabling/disabling the POR and PGE optimisations for Model Checking of B and Event-B models |
| 1071 | | 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).'). |
| 1072 | | preference_description(timeout_cbc_analysis,'Time out for computing independence and enable relations between operations.'). |
| 1073 | | |
| 1074 | | preference_description(use_scope_predicate, |
| 1075 | | 'Use SCOPE predicate (if defined) to restrict state space exploration for model checking and animation.'). |
| 1076 | | preference_description(use_ignore_pragmas, 'Use /*@desc prob-ignore */ pragmas when checking predicates (PROPERTIES,...)'). |
| 1077 | | preference_description(pge, |
| 1078 | | 'Use the Partial Guard Evaluation optimisation for the state space exploration of B models.'). |
| 1079 | | |
| 1080 | | preference_description(por,'Type of Partial Order Reduction Technique (ample_sets, ample_sets2).'). |
| 1081 | | preference_description(por_heur,'Type of heuritic for choosing a valid ample set.'). |
| 1082 | | preference_description(use_por_for_ltl,'Use Partial Order Reduction for LTL.'). |
| 1083 | | preference_description(use_safety_ltl_model_checker,'Rocognise safety properties and check these using the safety property model checker'). |
| 1084 | | |
| 1085 | | preference_description(enable_graph,'Option for using the enable graph module for partial order reduction.'). |
| 1086 | | preference_description(enable_graph_depth,'The depth of evaluating the weakest-preconditions along a path in an enable graph.'). |
| 1087 | | |
| 1088 | | preference_description(dependency_enable_predicates,'Compute in each state whether two events can disable each other.'). |
| 1089 | | |
| 1090 | | preference_description(filter_unused_constants,'Filter out unused constants'). |
| 1091 | | preference_description(translate_force_all_typing_infos,'Print all typing infos when pretty-printing'). |
| 1092 | | preference_description(translate_print_typing_infos,'Print needed typing infos when pretty-printing'). |
| 1093 | | preference_description(translate_print_frozen_infos,'Print Prolog frozen goal infos for unbound variables'). |
| 1094 | | preference_description(translate_ids_to_parseable_format,'Print Identifiers in a format that can be parsed again'). |
| 1095 | | preference_description(translate_suppress_rodin_positions_flag,'Suppres Rodin position information when pretty-printing'). |
| 1096 | | preference_description(translate_print_all_sequences,'Print B relations as sequences when possible during pretty-printing.'). |
| 1097 | | preference_description(translate_print_cs_style_sequences,'Print B sequences in theoretical CS style without separators.'). |
| 1098 | | % Note: also influenced by expand_avl_upto preference |
| 1099 | | |
| 1100 | | preference_description(disprover_mode,'Skip certain optimizations that effect soundness of proofs (for Rodin DISPROVER Plugin)'). |
| 1101 | | preference_description(trace_upon_error,'Trace upon error (requires running from source)'). |
| 1102 | | preference_description(error_log_file, 'File were all errors and warnings are logged (NDJSON format). Can be set to stderr or stdout.'). |
| 1103 | | preference_description(tlc_number_of_workers,'Number of parallel workers for external tool TLC (for -workers option)'). |
| 1104 | | preference_description(unsat_core_algorithm,'Algorithm to compute the unsat core of predicates. (divide_and_conquer or linear)'). |
| 1105 | | |
| 1106 | | |
| 1107 | | preference_description(port, 'First number to be used by distb/ZMQ. Default: 5000'). |
| 1108 | | preference_description(ip, 'The IP addess or hostname of the current machine that should be used. Default: localhost. Must be overriden in a distributed setting.'). |
| 1109 | | preference_description(max_states, 'The amount of states that shall be checked. Zero means explore entire state space. Default: 0'). |
| 1110 | | preference_description(tmpdir, 'The directory where temporary files should be stored. Default: /tmp/.'). |
| 1111 | | preference_description(logdir, 'The directory where log files should be stored. Default: ./distb-logs/'). |
| 1112 | | preference_description(proxynumber, 'The number of the proxy the component should connect to. Relevant if multiple proxies run on the same machine. Default: 0'). |
| 1113 | | preference_description(queue_threshold, 'The amount of states that may be kept in a queue before it is allowed to share. Default: 20'). |
| 1114 | | preference_description(hash_cycle, 'Minimum amount of milliseconds that has to pass between hash code updates from the master. Default: 25'). |
| 1115 | | |
| 1116 | | |
| 1117 | | |
| 1118 | | /* ------------------------- */ |
| 1119 | | |
| 1120 | | |
| 1121 | | %preference_update_action(do_full_invariant_checking,_) :- !, b_types_precompile. |
| 1122 | | %preference_change_requires_reload(enable_canonical_symmetry,true) :- !, . |
| 1123 | | %preference_update_action(use_nauty_symmetry_reduction,true) :- !, graph_iso_nauty:nauty_init. |
| 1124 | | %:- use_module(probsrc(bmachine),[bmachine_is_precompiled/0]). |
| 1125 | | %:- use_module(probsrc(graph_iso_nauty),[nauty_init/0]). |
| 1126 | | preference_update_action(symmetry_mode,nauty) :- !, |
| 1127 | | (bmachine:bmachine_is_precompiled -> graph_iso_nauty:nauty_init ; true). |
| 1128 | | preference_update_action(_,_). |
| 1129 | | |
| 1130 | | /* ------------------------- */ |
| 1131 | | |
| 1132 | | % now in basic_tests.pl |
| 1133 | | %:- assert_must_succeed( \+((preference_val_type(P,_D),\+preference_default_value(P,_Val)))). |
| 1134 | | %:- assert_must_succeed( \+((preference_default_value(P,_D), \+preference_val_type(P,_Val)))). |
| 1135 | | preference_val_type(maxint,nat1). |
| 1136 | | preference_val_type(minint,neg). |
| 1137 | | preference_val_type(number_animated_abstractions,nat). |
| 1138 | | preference_val_type(globalsets_fdrange,nat). |
| 1139 | | preference_val_type(do_invariant_checking,bool). |
| 1140 | | preference_val_type(find_abort_values,xbool). |
| 1141 | | preference_val_type(raise_abort_immediately,xbool). |
| 1142 | | preference_val_type(treat_outermost_pre_as_select,bool). |
| 1143 | | preference_val_type(require_operations_to_assign_all_outputs,bool). |
| 1144 | | preference_val_type(allow_operations_to_read_outputs,bool). |
| 1145 | | preference_val_type(allow_simultaneous_assignments,bool). |
| 1146 | | preference_val_type(cspm_animate_all_processes_without_arguments,bool). |
| 1147 | | preference_val_type(cspm_animate_all_processes,bool). |
| 1148 | | preference_val_type(cspm_detailed_animation,bool). |
| 1149 | | preference_val_type(cspm_strip_source_location,bool). |
| 1150 | | %preference_val_type(csp_event_visible_to_user,bool). |
| 1151 | | preference_val_type(show_initialisation_arguments,bool). |
| 1152 | | preference_val_type(deterministic_trace_replay,bool). |
| 1153 | | preference_val_type(show_eventb_any_arguments,bool). |
| 1154 | | preference_val_type(maxNrOfInitialisations,nat). |
| 1155 | | preference_val_type(randomisedRestartInitalisations,bool). |
| 1156 | | preference_val_type(maxNrOfEnablingsPerOperation,nat). |
| 1157 | | preference_val_type(time_out,nat1). |
| 1158 | | preference_val_type(debug_time_out_factor,nat1). |
| 1159 | | %preference_val_type(use_large_jvm_for_parser,bool). |
| 1160 | | preference_val_type(convert_comprehension_sets_into_closures,bool). |
| 1161 | | preference_val_type(use_clpfd_solver,bool). |
| 1162 | | preference_val_type(use_chr_solver,bool). |
| 1163 | | preference_val_type(data_validation_mode,bool). |
| 1164 | | preference_val_type(use_smt_mode,bool). |
| 1165 | | preference_val_type(solver_strength,nat). |
| 1166 | | preference_val_type(use_common_subexpression_elimination,bool). |
| 1167 | | preference_val_type(remove_implied_constraints,bool). |
| 1168 | | preference_val_type(lift_existential_quantifiers,bool). |
| 1169 | | preference_val_type(use_common_subexpression_also_for_predicates,bool). |
| 1170 | | preference_val_type(use_common_subexpression_also_for_substitutions,bool). |
| 1171 | | preference_val_type(use_common_subexpression_wd_only,bool). |
| 1172 | | preference_val_type(normalize_ast,bool). |
| 1173 | | preference_val_type(optimize_ast,bool). |
| 1174 | | preference_val_type(useless_code_elimination,bool). |
| 1175 | | preference_val_type(compile_while_body,bool). |
| 1176 | | preference_val_type(detect_lambdas,bool). |
| 1177 | | preference_val_type(ltsmin_guard_splitting,bool). |
| 1178 | | preference_val_type(ltsmin_do_not_evaluate_top_level_guards,bool). |
| 1179 | | preference_val_type(fail_if_clpfd_timeout,bool). |
| 1180 | | %preference_val_type(allow_recursive_closures,bool). |
| 1181 | | preference_val_type(use_static_ordering,bool). |
| 1182 | | preference_val_type(use_state_packing,bool). |
| 1183 | | preference_val_type(provide_trace_information,bool). |
| 1184 | | preference_val_type(performance_monitoring_on,bool). |
| 1185 | | preference_val_type(partition_predicates,bool). |
| 1186 | | preference_val_type(partition_predicates_inline_equalities,bool). |
| 1187 | | preference_val_type(use_closure_expansion_memoization,bool). |
| 1188 | | preference_val_type(use_function_memoization,bool). |
| 1189 | | preference_val_type(allow_incomplete_partial_setup_constants,bool). |
| 1190 | | preference_val_type(re_execute_operations_with_side_effects,bool). |
| 1191 | | preference_val_type(warn_if_definition_hides_variable,bool). |
| 1192 | | preference_val_type(type_check_definitions,bool). |
| 1193 | | %preference_val_type(warn_when_expanding_infinite_closures,int). |
| 1194 | | preference_val_type(allow_enumeration_of_infinite_types,bool). |
| 1195 | | preference_val_type(strict_raise_warnings,bool). |
| 1196 | | preference_val_type(strict_raise_enum_warnings,bool). |
| 1197 | | preference_val_type(clash_strict_checks,bool). |
| 1198 | | preference_val_type(perform_stricter_static_checks,bool). |
| 1199 | | preference_val_type(ignore_prj_types,bool). |
| 1200 | | preference_val_type(prefix_internal_operation_arguments,string). |
| 1201 | | preference_val_type(generate_minimal_nr_of_testcases,bool). |
| 1202 | | preference_val_type(use_tk_custom_state_viewer,bool). |
| 1203 | | preference_val_type(tk_custom_state_viewer_font_name,string). |
| 1204 | | preference_val_type(tk_custom_state_viewer_font_size,nat). |
| 1205 | | preference_val_type(tk_custom_state_viewer_padding,nat). |
| 1206 | | preference_val_type(tk_custom_state_viewer_str_padding,nat). |
| 1207 | | preference_val_type(use_small_window,bool). |
| 1208 | | preference_val_type(tk_show_source_pane,bool). |
| 1209 | | preference_val_type(ignore_hash_collisions,bool). |
| 1210 | | preference_val_type(forget_state_space,bool). |
| 1211 | | preference_val_type(store_only_one_incoming_transition,bool). |
| 1212 | | preference_val_type(symmetry_mode,[off,flood,nauty,hash]). |
| 1213 | | preference_val_type(use_static_symmetry_detection,bool). |
| 1214 | | preference_val_type(bool_expression_as_predicate,bool). |
| 1215 | | preference_val_type(allow_untyped_identifiers,[true,false,true_with_string_type]). |
| 1216 | | preference_val_type(repl_unicode,bool). |
| 1217 | | preference_val_type(repl_cache_parsing,bool). |
| 1218 | | preference_val_type(latex_encoding,text_encoding). |
| 1219 | | preference_val_type(latex_pp_greek_ids,bool). |
| 1220 | | preference_val_type(xml_encoding,text_encoding). |
| 1221 | | preference_val_type(view_probcli_errors_using_bbresults,bool). |
| 1222 | | preference_val_type(eventtrace,bool). |
| 1223 | | preference_val_type(store_event_transinfo,bool). |
| 1224 | | preference_val_type(try_kodkod_on_load,bool). |
| 1225 | | preference_val_type(kodkod_for_components,bool). |
| 1226 | | preference_val_type(kodkod_raise_warnings,bool). |
| 1227 | | preference_val_type(kodkod_max_nr_solutions,nat1). |
| 1228 | | preference_val_type(kodkod_symmetry_level,nat). |
| 1229 | | preference_val_type(kodkod_sat_solver,[sat4j,minisat,lingeling,glucose]). |
| 1230 | | preference_val_type(smt_supported_interpreter,bool). |
| 1231 | | preference_val_type(use_record_construction,bool). |
| 1232 | | preference_val_type(seen_machines_included,bool). |
| 1233 | | preference_val_type(allow_sequence_operators_on_strings,bool). |
| 1234 | | |
| 1235 | | preference_val_type(dot_print_node_ids,bool). |
| 1236 | | preference_val_type(dot_print_use_constants,bool). |
| 1237 | | preference_val_type(dot_print_node_info,bool). |
| 1238 | | preference_val_type(dot_print_edge_labels,bool). |
| 1239 | | preference_val_type(dot_print_action_arguments,bool). |
| 1240 | | preference_val_type(dot_print_functions,bool). |
| 1241 | | preference_val_type(dot_print_self_loops,bool). |
| 1242 | | preference_val_type(dot_print_root,bool). |
| 1243 | | %preference_val_type(dot_print_leaves,bool). |
| 1244 | | preference_val_type(dot_print_arc_colors,bool). |
| 1245 | | preference_val_type(dot_use_ps_viewer,bool). |
| 1246 | | preference_val_type(path_to_dot,path). |
| 1247 | | preference_val_type(dot_default_engine,[dot,neato,sfdp,fdp,twopi,circo]). |
| 1248 | | preference_val_type(path_to_dotty,path). |
| 1249 | | preference_val_type(path_to_ltsmin,path). |
| 1250 | | preference_val_type(path_to_ps_viewer,path). |
| 1251 | | preference_val_type(dot_root_shape,dot_shape). |
| 1252 | | preference_val_type(dot_node_penwidth,nat). |
| 1253 | | preference_val_type(dot_normal_node_shape,dot_shape). |
| 1254 | | preference_val_type(dot_current_node_shape,dot_shape). |
| 1255 | | preference_val_type(dot_open_node_colour,rgb_color). |
| 1256 | | preference_val_type(dot_scope_limit_node_colour,rgb_color). |
| 1257 | | preference_val_type(dot_normal_node_colour,rgb_color). |
| 1258 | | preference_val_type(dot_invariant_violated_node_colour,rgb_color). |
| 1259 | | preference_val_type(dot_fill_normal_nodes,bool). |
| 1260 | | preference_val_type(dot_normal_arc_colour,rgb_color). |
| 1261 | | preference_val_type(dot_node_font_size,nat1). |
| 1262 | | preference_val_type(dot_edge_font_size,nat1). |
| 1263 | | preference_val_type(dot_colour_goal_nodes,bool). |
| 1264 | | preference_val_type(dot_goal_node_colour,rgb_color). |
| 1265 | | preference_val_type(dot_print_node_properties,bool). |
| 1266 | | preference_val_type(dot_counterexample_node_colour,rgb_color). |
| 1267 | | preference_val_type(dot_counterexample_op_colour,rgb_color). |
| 1268 | | preference_val_type(dot_hierarchy_max_ids,int). |
| 1269 | | |
| 1270 | | preference_val_type(dot_event_hierarchy_horizontal,bool). |
| 1271 | | preference_val_type(dot_event_hierarchy_machine_colour,rgb_color). |
| 1272 | | preference_val_type(dot_event_hierarchy_refines_colour,rgb_color). |
| 1273 | | preference_val_type(dot_event_hierarchy_new_event_colour,rgb_color). |
| 1274 | | preference_val_type(dot_event_hierarchy_rename_event_colour,rgb_color). |
| 1275 | | preference_val_type(dot_event_hierarchy_rename_unchanged_event_colour,rgb_color). |
| 1276 | | preference_val_type(dot_event_hierarchy_unchanged_event_colour,rgb_color). |
| 1277 | | preference_val_type(dot_event_hierarchy_grd_strengthening_event_colour,rgb_color). |
| 1278 | | preference_val_type(dot_event_hierarchy_grd_keeping_event_colour,rgb_color). |
| 1279 | | preference_val_type(dot_event_hierarchy_edge_colour,rgb_color). |
| 1280 | | preference_val_type(dot_event_hierarchy_extends_colour,rgb_color). |
| 1281 | | |
| 1282 | | preference_val_type(dot_projection_non_det_edge_colour,rgb_color). |
| 1283 | | preference_val_type(dot_projection_det_edge_colour,rgb_color). |
| 1284 | | preference_val_type(dot_projection_non_definite_edge_style,dot_line_style). |
| 1285 | | preference_val_type(dot_projection_definite_edge_style,dot_line_style). |
| 1286 | | preference_val_type(dot_projection_label_limit,nat). |
| 1287 | | preference_val_type(dot_use_unicode,bool). |
| 1288 | | preference_val_type(dot_predicate_node_shape,dot_shape). |
| 1289 | | preference_val_type(dot_expression_node_shape,dot_shape). |
| 1290 | | preference_val_type(dot_var_mod_hide_only_written,bool). |
| 1291 | | |
| 1292 | | preference_val_type(mc_dc_default_level,nat). |
| 1293 | | |
| 1294 | | preference_val_type(dot_enabling_show_readwrites,bool). |
| 1295 | | |
| 1296 | | preference_val_type(dot_definitions_use_sub_graph,bool). |
| 1297 | | preference_val_type(dot_definitions_show_all,bool). |
| 1298 | | preference_val_type(dot_state_graph_decompose,bool). |
| 1299 | | |
| 1300 | | preference_val_type(font_name,string). |
| 1301 | | preference_val_type(font_size_only,nat1). |
| 1302 | | preference_val_type(font_size,string). |
| 1303 | | preference_val_type(use_font_size_for_columns,bool). |
| 1304 | | preference_val_type(allow_source_code_editing,bool). |
| 1305 | | preference_val_type(show_line_numbers,bool). |
| 1306 | | %preference_val_type(show_full_error_span,bool). |
| 1307 | | preference_val_type(highlight_brackets,bool). |
| 1308 | | preference_val_type(highlight_current_line,bool). |
| 1309 | | preference_val_type(ask_when_content_changed,bool). |
| 1310 | | |
| 1311 | | preference_val_type(user_not_beginner,bool). |
| 1312 | | preference_val_type(user_is_an_expert_with_accessto_source_distribution,bool). |
| 1313 | | %preference_val_type(default_to_runtime_type_checking_on_startup_for_expert,bool). |
| 1314 | | preference_val_type(path_to_probe,path). |
| 1315 | | %preference_val_type(path_to_fuzz,path). |
| 1316 | | preference_val_type(path_to_fdr,path). |
| 1317 | | preference_val_type(path_to_csp_typechecker,path). |
| 1318 | | preference_val_type(path_to_bcomp,path). % Atelier B parser & type checker |
| 1319 | | preference_val_type(path_to_java,path). % Path to Java |
| 1320 | | preference_val_type(path_to_atb_krt,path). |
| 1321 | | preference_val_type(try_atb_provers,bool). |
| 1322 | | preference_val_type(symbolic_mc_try_other_solvers,bool). |
| 1323 | | preference_val_type(path_to_spin,path). |
| 1324 | | preference_val_type(path_to_cspm,path). |
| 1325 | | preference_val_type(path_to_text_editor,path). |
| 1326 | | preference_val_type(path_to_text_editor_launch,path). |
| 1327 | | preference_val_type(number_of_recent_documents,nat). |
| 1328 | | preference_val_type(number_of_searched_patterns,nat). |
| 1329 | | preference_val_type(number_of_replaced_patterns,nat). |
| 1330 | | preference_val_type(number_of_eval_history_elements,nat). |
| 1331 | | preference_val_type(number_of_eval_csp_history_elements,nat). |
| 1332 | | preference_val_type(number_of_checked_ltl_formulas,nat). |
| 1333 | | preference_val_type(ltl_to_ba_tool,path). |
| 1334 | | preference_val_type(prob2_trace_file,path). |
| 1335 | | preference_val_type(prob2_trace_file_gen_unique_name,bool). |
| 1336 | | |
| 1337 | | |
| 1338 | | preference_val_type(do_syntax_highlighting,bool). |
| 1339 | | preference_val_type(sh_type_colour,rgb_color). |
| 1340 | | preference_val_type(sh_logical_colour,rgb_color). |
| 1341 | | preference_val_type(sh_assignments_colour,rgb_color). |
| 1342 | | preference_val_type(sh_operators,rgb_color). |
| 1343 | | preference_val_type(sh_top_level_keywords,rgb_color). |
| 1344 | | preference_val_type(sh_control_keywords,rgb_color). |
| 1345 | | %preference_val_type(sh_includes_keywords,rgb_color). |
| 1346 | | preference_val_type(sh_comments,rgb_color). |
| 1347 | | preference_val_type(sh_pragmas,rgb_color). |
| 1348 | | preference_val_type(sh_unsupported_background,rgb_color). |
| 1349 | | |
| 1350 | | preference_val_type(expand_forall_upto,nat). |
| 1351 | | preference_val_type(double_evaluation_when_analysing,bool). |
| 1352 | | preference_val_type(expand_avl_upto,int). |
| 1353 | | preference_val_type(show_function_tuples_in_property,bool). |
| 1354 | | preference_val_type(bugly_pp_scrambling,bool). |
| 1355 | | preference_val_type(pp_propositional_logic_mode,bool). |
| 1356 | | |
| 1357 | | preference_val_type(allow_new_ops_in_refinement,bool). |
| 1358 | | preference_val_type(allow_local_operation_calls,bool). |
| 1359 | | preference_val_type(allow_operation_calls_in_expr,bool). |
| 1360 | | preference_val_type(allow_let_to_reuse_introduced_ids,bool). |
| 1361 | | preference_val_type(use_po,bool). |
| 1362 | | preference_val_type(try_operation_reuse,xbool). |
| 1363 | | preference_val_type(randomise_operation_order,bool). |
| 1364 | | preference_val_type(randomise_enumeration_order,bool). |
| 1365 | | |
| 1366 | | preference_val_type(set_rand,bool). |
| 1367 | | preference_val_type(rand_seed,nat). |
| 1368 | | |
| 1369 | | preference_val_type(use_scope_predicate,bool). |
| 1370 | | preference_val_type(use_ignore_pragmas,bool). |
| 1371 | | %% Options' meaning |
| 1372 | | % disabled: skipping guard evaluation of actions known to be disabled at state |
| 1373 | | % enabled: skipping guard evaluation of actions known to be enabled at state |
| 1374 | | % full: skipping guard evaluations of actions known to be enabled or disabled at state |
| 1375 | | % disabled2, enabled2, full2: same for these, but another (more precise) way for computing the sets of enabled and disabled actions is used |
| 1376 | | preference_val_type(pge,[off,disabled,enabled,full,disabled2,enabled2,full2]). |
| 1377 | | |
| 1378 | | preference_val_type(use_cbc_analysis,bool). |
| 1379 | | preference_val_type(timeout_cbc_analysis,nat1). |
| 1380 | | |
| 1381 | | preference_val_type(por,[off,ample_sets,ample_sets2]). |
| 1382 | | preference_val_type(por_heur,[first,random,minimal]). |
| 1383 | | preference_val_type(use_por_for_ltl,bool). |
| 1384 | | preference_val_type(use_safety_ltl_model_checker,bool). |
| 1385 | | |
| 1386 | | preference_val_type(enable_graph,bool). |
| 1387 | | preference_val_type(enable_graph_depth,int). |
| 1388 | | |
| 1389 | | preference_val_type(dependency_enable_predicates,bool). |
| 1390 | | |
| 1391 | | preference_val_type(filter_unused_constants,bool). |
| 1392 | | preference_val_type(translate_force_all_typing_infos,bool). |
| 1393 | | preference_val_type(translate_print_typing_infos,bool). |
| 1394 | | preference_val_type(translate_print_frozen_infos,bool). |
| 1395 | | preference_val_type(translate_ids_to_parseable_format,bool). |
| 1396 | | preference_val_type(translate_suppress_rodin_positions_flag,bool). |
| 1397 | | preference_val_type(translate_print_all_sequences,bool). |
| 1398 | | preference_val_type(translate_print_cs_style_sequences,bool). |
| 1399 | | |
| 1400 | | |
| 1401 | | preference_val_type(disprover_mode,bool). |
| 1402 | | preference_val_type(trace_upon_error,bool). |
| 1403 | | preference_val_type(tlc_number_of_workers,nat1). |
| 1404 | | preference_val_type(error_log_file,path). |
| 1405 | | |
| 1406 | | preference_val_type(unsat_core_algorithm,[divide_and_conquer,linear]). |
| 1407 | | |
| 1408 | | preference_val_type(port, nat1). |
| 1409 | | preference_val_type(ip, string). |
| 1410 | | preference_val_type(max_states, nat). |
| 1411 | | preference_val_type(tmpdir, path). |
| 1412 | | preference_val_type(logdir, path). |
| 1413 | | preference_val_type(proxynumber, nat). |
| 1414 | | preference_val_type(queue_threshold, nat1). |
| 1415 | | preference_val_type(hash_cycle, nat). |
| 1416 | | |
| 1417 | | preference_val_type(machines_path,path). %directory_path). % preference not so critical; default value may not exist |
| 1418 | | |
| 1419 | | |
| 1420 | | |
| 1421 | | /* ------------------------- */ |
| 1422 | | |
| 1423 | | |
| 1424 | | % now in basic_tests.pl |
| 1425 | | %:- assert_must_succeed( \+((preference_category(P,_D),\+preference_default_value(P,_Val)))). |
| 1426 | | %:- assert_must_succeed( \+((preference_default_value(P,_D), \+preference_category(P,_Val)))). |
| 1427 | | preference_category(unsat_core_algorithm,advanced). |
| 1428 | | preference_category(maxint,animation). |
| 1429 | | preference_category(minint,animation). |
| 1430 | | preference_category(globalsets_fdrange,animation). |
| 1431 | | preference_category(do_invariant_checking,advanced). |
| 1432 | | %preference_category(do_full_invariant_checking,animation). |
| 1433 | | %preference_category(use_new_kernel,advanced). |
| 1434 | | preference_category(find_abort_values,animation). |
| 1435 | | preference_category(raise_abort_immediately,advanced). |
| 1436 | | preference_category(treat_outermost_pre_as_select,animation). |
| 1437 | | preference_category(require_operations_to_assign_all_outputs,animation). |
| 1438 | | preference_category(allow_operations_to_read_outputs,advanced). |
| 1439 | | preference_category(allow_simultaneous_assignments,hidden). |
| 1440 | | preference_category(cspm_animate_all_processes_without_arguments,csp_prefs). |
| 1441 | | preference_category(cspm_animate_all_processes,csp_prefs). |
| 1442 | | %preference_category(cspm_display_inout,csp_prefs). |
| 1443 | | preference_category(cspm_detailed_animation,csp_prefs). |
| 1444 | | preference_category(cspm_strip_source_location,csp_prefs). |
| 1445 | | %preference_category(csp_event_visible_to_user,csp_prefs). |
| 1446 | | %preference_category(cspm_allow_incomplete_records,csp_prefs). |
| 1447 | | %preference_category(findOnlyOneSol,advanced). |
| 1448 | | preference_category(show_eventb_any_arguments,animation). |
| 1449 | | preference_category(maxNrOfInitialisations,animation). |
| 1450 | | preference_category(randomisedRestartInitalisations,advanced). |
| 1451 | | preference_category(maxNrOfEnablingsPerOperation,animation). |
| 1452 | | preference_category(time_out,animation). |
| 1453 | | preference_category(number_animated_abstractions,animation). |
| 1454 | | preference_category(show_initialisation_arguments,animation). |
| 1455 | | preference_category(deterministic_trace_replay,hidden). |
| 1456 | | %preference_category(animate_skip_operations,animation). |
| 1457 | | preference_category(debug_time_out_factor,advanced). |
| 1458 | | %preference_category(use_large_jvm_for_parser,advanced). |
| 1459 | | preference_category(convert_comprehension_sets_into_closures,animation). |
| 1460 | | preference_category(use_clpfd_solver,animation). |
| 1461 | | preference_category(use_chr_solver,animation). |
| 1462 | | preference_category(data_validation_mode,advanced). |
| 1463 | | preference_category(use_smt_mode,advanced). |
| 1464 | | preference_category(solver_strength,advanced). |
| 1465 | | preference_category(use_common_subexpression_elimination,advanced). |
| 1466 | | preference_category(remove_implied_constraints,advanced). |
| 1467 | | preference_category(lift_existential_quantifiers,advanced). |
| 1468 | | preference_category(use_common_subexpression_also_for_predicates,advanced). |
| 1469 | | preference_category(use_common_subexpression_also_for_substitutions,advanced). |
| 1470 | | preference_category(use_common_subexpression_wd_only,advanced). |
| 1471 | | preference_category(normalize_ast,hidden). |
| 1472 | | preference_category(optimize_ast,advanced). |
| 1473 | | preference_category(useless_code_elimination,advanced). |
| 1474 | | preference_category(compile_while_body,advanced). |
| 1475 | | preference_category(detect_lambdas,advanced). |
| 1476 | | preference_category(ltsmin_guard_splitting,hidden). |
| 1477 | | preference_category(ltsmin_do_not_evaluate_top_level_guards,hidden). |
| 1478 | | preference_category(fail_if_clpfd_timeout,advanced). |
| 1479 | | %preference_category(allow_recursive_closures,hidden). |
| 1480 | | preference_category(use_static_ordering,advanced). |
| 1481 | | preference_category(use_state_packing,advanced). |
| 1482 | | preference_category(provide_trace_information,advanced). |
| 1483 | | preference_category(performance_monitoring_on,advanced). |
| 1484 | | preference_category(partition_predicates,advanced). |
| 1485 | | preference_category(partition_predicates_inline_equalities,advanced). |
| 1486 | | preference_category(use_closure_expansion_memoization,advanced). |
| 1487 | | preference_category(use_function_memoization,advanced). |
| 1488 | | preference_category(allow_incomplete_partial_setup_constants,advanced). |
| 1489 | | preference_category(re_execute_operations_with_side_effects,advanced). |
| 1490 | | preference_category(warn_if_definition_hides_variable,advanced). |
| 1491 | | preference_category(type_check_definitions,advanced). |
| 1492 | | %preference_category(warn_when_expanding_infinite_closures,advanced). |
| 1493 | | preference_category(allow_enumeration_of_infinite_types,advanced). |
| 1494 | | preference_category(strict_raise_warnings,advanced). |
| 1495 | | preference_category(strict_raise_enum_warnings,hidden). % only for testing |
| 1496 | | preference_category(clash_strict_checks,advanced). |
| 1497 | | preference_category(perform_stricter_static_checks,hidden). % set by prob |
| 1498 | | preference_category(ignore_prj_types,advanced). |
| 1499 | | %preference_category(never_convert_closures_into_explicit_form,hidden). |
| 1500 | | %preference_category(convert_types_into_closures,animation). |
| 1501 | | %preference_category(convert_closures_into_explicit_form_for_store,animation). |
| 1502 | | %preference_category(allow_empty_global_sets,advanced). |
| 1503 | | preference_category(ignore_hash_collisions,advanced). |
| 1504 | | preference_category(forget_state_space,advanced). |
| 1505 | | preference_category(store_only_one_incoming_transition,advanced). |
| 1506 | | %preference_category(enable_permutation_reducation,advanced). |
| 1507 | | %preference_category(use_symmetry_marker_hash,advanced). |
| 1508 | | %preference_category(enable_canonical_symmetry,advanced). |
| 1509 | | %preference_category(use_nauty_symmetry_reduction,advanced). |
| 1510 | | preference_category(symmetry_mode,hidden). |
| 1511 | | preference_category(use_static_symmetry_detection,advanced). |
| 1512 | | preference_category(bool_expression_as_predicate,hidden). |
| 1513 | | preference_category(allow_untyped_identifiers,hidden). |
| 1514 | | preference_category(repl_unicode,syntax_highlighting). |
| 1515 | | preference_category(repl_cache_parsing,hidden). |
| 1516 | | preference_category(latex_encoding,hidden). |
| 1517 | | preference_category(latex_pp_greek_ids,hidden). |
| 1518 | | preference_category(xml_encoding,hidden). |
| 1519 | | preference_category(view_probcli_errors_using_bbresults,hidden). |
| 1520 | | preference_category(eventtrace,animation). |
| 1521 | | preference_category(store_event_transinfo,hidden). % automatically set by probcli |
| 1522 | | preference_category(try_kodkod_on_load,hidden). |
| 1523 | | preference_category(kodkod_for_components,advanced). |
| 1524 | | preference_category(kodkod_raise_warnings,advanced). |
| 1525 | | preference_category(kodkod_max_nr_solutions,advanced). |
| 1526 | | preference_category(kodkod_symmetry_level,advanced). |
| 1527 | | preference_category(kodkod_sat_solver,advanced). |
| 1528 | | preference_category(smt_supported_interpreter,advanced). |
| 1529 | | preference_category(use_record_construction,advanced). |
| 1530 | | preference_category(seen_machines_included,animation). |
| 1531 | | preference_category(allow_sequence_operators_on_strings,animation). |
| 1532 | | |
| 1533 | | %preference_category(test_case_gen_stop_at_first_error,advanced). |
| 1534 | | preference_category(prefix_internal_operation_arguments,advanced). |
| 1535 | | preference_category(generate_minimal_nr_of_testcases,advanced). |
| 1536 | | preference_category(use_tk_custom_state_viewer,hidden). % actually : if user wants to turn it off; simply do not define ANIMATION_FUNCTION |
| 1537 | | preference_category(tk_custom_state_viewer_font_name,hidden). |
| 1538 | | preference_category(tk_custom_state_viewer_font_size,hidden). |
| 1539 | | preference_category(tk_custom_state_viewer_padding,animation). |
| 1540 | | preference_category(tk_custom_state_viewer_str_padding,animation). |
| 1541 | | preference_category(use_small_window,animation). |
| 1542 | | preference_category(tk_show_source_pane,animation). |
| 1543 | | |
| 1544 | | preference_category(path_to_ltsmin,advanced). |
| 1545 | | |
| 1546 | | |
| 1547 | | preference_category(dot_print_node_ids,dot). |
| 1548 | | preference_category(dot_print_use_constants,dot). |
| 1549 | | preference_category(dot_print_node_info,dot). |
| 1550 | | preference_category(dot_print_edge_labels,dot). |
| 1551 | | preference_category(dot_print_action_arguments,dot). |
| 1552 | | preference_category(dot_print_functions,dot). |
| 1553 | | preference_category(dot_print_self_loops,dot). |
| 1554 | | preference_category(dot_print_root,dot). |
| 1555 | | %preference_category(dot_print_leaves,dot). |
| 1556 | | preference_category(dot_print_arc_colors,dot). |
| 1557 | | preference_category(dot_use_ps_viewer,hidden). |
| 1558 | | preference_category(path_to_dotty,dot). |
| 1559 | | preference_category(path_to_dot,dot). |
| 1560 | | preference_category(dot_default_engine,dot). |
| 1561 | | preference_category(path_to_ps_viewer,dot). |
| 1562 | | preference_category(dot_root_shape,dot). |
| 1563 | | preference_category(dot_node_penwidth,dot). |
| 1564 | | preference_category(dot_normal_node_shape,dot). |
| 1565 | | preference_category(dot_current_node_shape,dot). |
| 1566 | | preference_category(dot_open_node_colour,dot). |
| 1567 | | preference_category(dot_scope_limit_node_colour,dot). |
| 1568 | | preference_category(dot_normal_node_colour,dot). |
| 1569 | | preference_category(dot_invariant_violated_node_colour,dot). |
| 1570 | | preference_category(dot_fill_normal_nodes,dot). |
| 1571 | | preference_category(dot_normal_arc_colour,dot). |
| 1572 | | |
| 1573 | | %preference_category(dot_font_size,hidden). |
| 1574 | | preference_category(dot_node_font_size,dot). |
| 1575 | | preference_category(dot_edge_font_size,dot). |
| 1576 | | preference_category(dot_colour_goal_nodes,dot). |
| 1577 | | preference_category(dot_goal_node_colour,dot). |
| 1578 | | preference_category(dot_print_node_properties,dot). |
| 1579 | | preference_category(dot_counterexample_node_colour,dot). |
| 1580 | | preference_category(dot_counterexample_op_colour,dot). |
| 1581 | | preference_category(dot_hierarchy_max_ids,dot). |
| 1582 | | |
| 1583 | | preference_category(dot_event_hierarchy_horizontal,dot_event_hierarchy). |
| 1584 | | preference_category(dot_event_hierarchy_machine_colour,dot_event_hierarchy). |
| 1585 | | preference_category(dot_event_hierarchy_refines_colour,dot_event_hierarchy). |
| 1586 | | preference_category(dot_event_hierarchy_new_event_colour,dot_event_hierarchy). |
| 1587 | | preference_category(dot_event_hierarchy_rename_event_colour,dot_event_hierarchy). |
| 1588 | | preference_category(dot_event_hierarchy_unchanged_event_colour,dot_event_hierarchy). |
| 1589 | | preference_category(dot_event_hierarchy_rename_unchanged_event_colour,dot_event_hierarchy). |
| 1590 | | preference_category(dot_event_hierarchy_grd_strengthening_event_colour,dot_event_hierarchy). |
| 1591 | | preference_category(dot_event_hierarchy_grd_keeping_event_colour,dot_event_hierarchy). |
| 1592 | | preference_category(dot_event_hierarchy_edge_colour,dot_event_hierarchy). |
| 1593 | | preference_category(dot_event_hierarchy_extends_colour,dot_event_hierarchy). |
| 1594 | | |
| 1595 | | preference_category(dot_projection_non_det_edge_colour,dot_projection). |
| 1596 | | preference_category(dot_projection_det_edge_colour,dot_projection). |
| 1597 | | preference_category(dot_projection_non_definite_edge_style,dot_projection). |
| 1598 | | preference_category(dot_projection_definite_edge_style,dot_projection). |
| 1599 | | preference_category(dot_projection_label_limit,dot_projection). |
| 1600 | | preference_category(dot_use_unicode,dot_projection). |
| 1601 | | |
| 1602 | | preference_category(dot_predicate_node_shape,dot_formula_tree). |
| 1603 | | preference_category(dot_expression_node_shape,dot_formula_tree). |
| 1604 | | preference_category(dot_var_mod_hide_only_written,dot_variable_modification). |
| 1605 | | |
| 1606 | | preference_category(mc_dc_default_level,mc_dc_commands). |
| 1607 | | |
| 1608 | | preference_category(dot_enabling_show_readwrites,dot). |
| 1609 | | |
| 1610 | | preference_category(dot_definitions_use_sub_graph,dot_definitions). |
| 1611 | | preference_category(dot_definitions_show_all,dot_definitions). |
| 1612 | | |
| 1613 | | preference_category(dot_state_graph_decompose,dot_state_graph). |
| 1614 | | |
| 1615 | | preference_category(font_size,gui_prefs). |
| 1616 | | preference_category(font_name,gui_prefs). |
| 1617 | | preference_category(font_size_only,gui_prefs). |
| 1618 | | preference_category(use_font_size_for_columns,advanced). |
| 1619 | | preference_category(allow_source_code_editing,gui_prefs). |
| 1620 | | preference_category(show_line_numbers,gui_prefs). |
| 1621 | | preference_category(highlight_brackets,gui_prefs). |
| 1622 | | preference_category(highlight_current_line,gui_prefs). |
| 1623 | | preference_category(ask_when_content_changed,gui_prefs). |
| 1624 | | preference_category(user_not_beginner,gui_prefs). |
| 1625 | | |
| 1626 | | preference_category(user_is_an_expert_with_accessto_source_distribution,hidden). |
| 1627 | | %preference_category(default_to_runtime_type_checking_on_startup_for_expert,hidden). |
| 1628 | | preference_category(path_to_probe,csp_prefs). |
| 1629 | | %preference_category(path_to_fuzz,advanced). |
| 1630 | | preference_category(path_to_fdr,csp_prefs). |
| 1631 | | preference_category(path_to_csp_typechecker,csp_prefs). |
| 1632 | | preference_category(path_to_bcomp,advanced). |
| 1633 | | preference_category(path_to_java,advanced). |
| 1634 | | preference_category(path_to_atb_krt,advanced). % not yet used from within ProB Tcl/Tk, ... |
| 1635 | | preference_category(try_atb_provers,advanced). |
| 1636 | | preference_category(symbolic_mc_try_other_solvers,advanced). |
| 1637 | | preference_category(path_to_spin,advanced). |
| 1638 | | preference_category(path_to_cspm,advanced). |
| 1639 | | preference_category(path_to_text_editor,advanced). |
| 1640 | | preference_category(path_to_text_editor_launch,hidden). |
| 1641 | | preference_category(number_of_recent_documents,advanced). |
| 1642 | | preference_category(number_of_searched_patterns,advanced). |
| 1643 | | preference_category(number_of_replaced_patterns,advanced). |
| 1644 | | preference_category(number_of_eval_history_elements,advanced). |
| 1645 | | preference_category(number_of_eval_csp_history_elements,advanced). |
| 1646 | | preference_category(number_of_checked_ltl_formulas,advanced). |
| 1647 | | preference_category(allow_new_ops_in_refinement,advanced). |
| 1648 | | preference_category(allow_local_operation_calls,advanced). |
| 1649 | | preference_category(allow_operation_calls_in_expr,advanced). |
| 1650 | | preference_category(allow_let_to_reuse_introduced_ids,advanced). |
| 1651 | | preference_category(use_po,advanced). |
| 1652 | | preference_category(try_operation_reuse,advanced). |
| 1653 | | preference_category(randomise_operation_order,advanced). |
| 1654 | | preference_category(randomise_enumeration_order,advanced). |
| 1655 | | preference_category(set_rand,advanced). |
| 1656 | | preference_category(rand_seed,advanced). |
| 1657 | | preference_category(ltl_to_ba_tool,advanced). |
| 1658 | | preference_category(prob2_trace_file,hidden). |
| 1659 | | preference_category(prob2_trace_file_gen_unique_name,hidden). |
| 1660 | | |
| 1661 | | |
| 1662 | | preference_category(do_syntax_highlighting,syntax_highlighting). |
| 1663 | | preference_category(sh_type_colour,syntax_highlighting). |
| 1664 | | preference_category(sh_logical_colour,syntax_highlighting). |
| 1665 | | preference_category(sh_assignments_colour,syntax_highlighting). |
| 1666 | | preference_category(sh_operators,syntax_highlighting). |
| 1667 | | preference_category(sh_top_level_keywords,syntax_highlighting). |
| 1668 | | preference_category(sh_control_keywords,syntax_highlighting). |
| 1669 | | %preference_category(sh_includes_keywords,syntax_highlighting). |
| 1670 | | preference_category(sh_comments,syntax_highlighting). |
| 1671 | | preference_category(sh_pragmas,syntax_highlighting). |
| 1672 | | preference_category(sh_unsupported_background,syntax_highlighting). |
| 1673 | | |
| 1674 | | preference_category(expand_forall_upto,advanced). |
| 1675 | | preference_category(double_evaluation_when_analysing,advanced). |
| 1676 | | preference_category(expand_avl_upto,advanced). |
| 1677 | | preference_category(show_function_tuples_in_property,animation). |
| 1678 | | preference_category(bugly_pp_scrambling,advanced). |
| 1679 | | preference_category(pp_propositional_logic_mode,hidden). |
| 1680 | | %preference_category(show_full_error_span,hidden). |
| 1681 | | |
| 1682 | | preference_category(machines_path,hidden). |
| 1683 | | |
| 1684 | | /* Partial techniques for optimising the Model Checker */ |
| 1685 | | |
| 1686 | | preference_category(use_scope_predicate,advanced). |
| 1687 | | preference_category(use_ignore_pragmas,advanced). |
| 1688 | | preference_category(pge,model_checker). |
| 1689 | | |
| 1690 | | preference_category(use_cbc_analysis,advanced). |
| 1691 | | preference_category(timeout_cbc_analysis,advanced). |
| 1692 | | preference_category(por,model_checker). |
| 1693 | | preference_category(por_heur,model_checker). |
| 1694 | | preference_category(use_por_for_ltl,model_checker). |
| 1695 | | preference_category(use_safety_ltl_model_checker,model_checker). |
| 1696 | | preference_category(enable_graph,model_checker). |
| 1697 | | preference_category(enable_graph_depth,model_checker). |
| 1698 | | preference_category(dependency_enable_predicates,model_checker). |
| 1699 | | |
| 1700 | | %------------------------------------ |
| 1701 | | |
| 1702 | | preference_category(filter_unused_constants,advanced). |
| 1703 | | preference_category(translate_force_all_typing_infos,hidden). |
| 1704 | | preference_category(translate_print_typing_infos,hidden). |
| 1705 | | preference_category(translate_print_frozen_infos,hidden). |
| 1706 | | preference_category(translate_ids_to_parseable_format,hidden). |
| 1707 | | preference_category(translate_suppress_rodin_positions_flag,hidden). |
| 1708 | | preference_category(translate_print_all_sequences,hidden). |
| 1709 | | preference_category(translate_print_cs_style_sequences,hidden). |
| 1710 | | |
| 1711 | | preference_category(disprover_mode,advanced). |
| 1712 | | preference_category(trace_upon_error,hidden). |
| 1713 | | preference_category(error_log_file,advanced). |
| 1714 | | preference_category(tlc_number_of_workers,hidden). |
| 1715 | | |
| 1716 | | preference_category(port, distb). |
| 1717 | | preference_category(ip, distb). |
| 1718 | | preference_category(max_states, distb). |
| 1719 | | preference_category(tmpdir, distb). |
| 1720 | | preference_category(logdir, distb). |
| 1721 | | preference_category(proxynumber, distb). |
| 1722 | | preference_category(queue_threshold, distb). |
| 1723 | | preference_category(hash_cycle, distb). |
| 1724 | | |
| 1725 | | |
| 1726 | | /* ------------------------- */ |
| 1727 | | |
| 1728 | | % secondary, alternate categories: |
| 1729 | | alternate_preference_category(dot_print_node_ids,dot_state_space). |
| 1730 | | alternate_preference_category(dot_print_use_constants,dot_state_space). %? |
| 1731 | | alternate_preference_category(dot_print_node_info,dot_state_space). |
| 1732 | | alternate_preference_category(dot_print_edge_labels,dot_state_space). |
| 1733 | | alternate_preference_category(dot_print_action_arguments,dot_state_space). |
| 1734 | | alternate_preference_category(dot_print_functions,dot_state_space). |
| 1735 | | alternate_preference_category(dot_print_self_loops,dot_state_space). |
| 1736 | | alternate_preference_category(dot_print_root,dot_state_space). |
| 1737 | | alternate_preference_category(dot_print_arc_colors,dot_state_space). |
| 1738 | | alternate_preference_category(dot_root_shape,dot_state_space). |
| 1739 | | alternate_preference_category(dot_node_penwidth,dot_state_space). |
| 1740 | | alternate_preference_category(dot_normal_node_shape,dot_state_space). |
| 1741 | | alternate_preference_category(dot_current_node_shape,dot_state_space). |
| 1742 | | alternate_preference_category(dot_open_node_colour,dot_state_space). |
| 1743 | | alternate_preference_category(dot_scope_limit_node_colour,dot_state_space). |
| 1744 | | alternate_preference_category(dot_normal_node_colour,dot_state_space). |
| 1745 | | alternate_preference_category(dot_invariant_violated_node_colour,dot_state_space). |
| 1746 | | alternate_preference_category(dot_fill_normal_nodes,dot_state_space). |
| 1747 | | alternate_preference_category(dot_normal_arc_colour,dot_state_space). |
| 1748 | | alternate_preference_category(dot_node_font_size,dot_state_space). |
| 1749 | | alternate_preference_category(dot_edge_font_size,dot_state_space). |
| 1750 | | alternate_preference_category(dot_colour_goal_nodes,dot_state_space). |
| 1751 | | alternate_preference_category(dot_goal_node_colour,dot_state_space). |
| 1752 | | alternate_preference_category(dot_print_node_properties,dot_state_space). |
| 1753 | | alternate_preference_category(dot_use_unicode,dot_formula_tree). |
| 1754 | | |
| 1755 | | /* ------------------------- */ |
| 1756 | | % now in basic_tests.pl |
| 1757 | | %:- assert_must_succeed( \+((preferences:obsolete_preference(P),preference_default_value(P,_Val)))). |
| 1758 | | obsolete_preference(warn_when_expanding_infinite_closures). |
| 1759 | | obsolete_preference(do_neginvariant_checking). % use double_evaluation_when_analysing |
| 1760 | | obsolete_preference(check_prolog_b_ast). |
| 1761 | | obsolete_preference(use_large_jvm_for_parser). |
| 1762 | | obsolete_preference(default_to_runtime_type_checking_on_startup_for_expert). |
| 1763 | | obsolete_preference(animate_skip_operations). |
| 1764 | | obsolete_preference(debug_try_minimise). |
| 1765 | | obsolete_preference(convert_types_into_closures). |
| 1766 | | obsolete_preference(use_avl_trees_for_sets). |
| 1767 | | obsolete_preference(dot_font_size). |
| 1768 | | obsolete_preference(only_label_base_types). |
| 1769 | | obsolete_preference(use_new_kernel). |
| 1770 | | obsolete_preference(findOnlyOneSol). |
| 1771 | | obsolete_preference(enable_permutation_reducation). |
| 1772 | | obsolete_preference(use_symmetry_marker_hash). |
| 1773 | | obsolete_preference(enable_canonical_symmetry). |
| 1774 | | obsolete_preference(use_nauty_symmetry_reduction). |
| 1775 | | obsolete_preference(do_full_invariant_checking). |
| 1776 | | obsolete_preference(test_case_gen_stop_at_first_error). |
| 1777 | | obsolete_preference(use_failure_refinement). |
| 1778 | | obsolete_preference(do_on_the_fly_refinement). |
| 1779 | | obsolete_preference(never_convert_closures_into_explicit_form). |
| 1780 | | obsolete_preference(allow_empty_global_sets). |
| 1781 | | obsolete_preference(multilevel_animation). |
| 1782 | | obsolete_preference(remove_multilevel_prefix). |
| 1783 | | obsolete_preference(cspm_allow_incomplete_records). |
| 1784 | | obsolete_preference(cspm_display_inout). |
| 1785 | | obsolete_preference(allow_recursive_closures). |
| 1786 | | obsolete_preference(absint_abstract_domain_module). |
| 1787 | | obsolete_preference(absint_use_widening). |
| 1788 | | obsolete_preference(absint_soft_widening). |
| 1789 | | obsolete_preference(absint_extrapolation_threshold). |
| 1790 | | obsolete_preference(convert_closures_into_explicit_form_for_store). |
| 1791 | | obsolete_preference(use_por). |
| 1792 | | obsolete_preference(use_pge). |
| 1793 | | obsolete_preference(pge_dis). |
| 1794 | | obsolete_preference(pge_ind). |
| 1795 | | obsolete_preference(pge_keep). |
| 1796 | | obsolete_preference(use_pge_keep). |
| 1797 | | obsolete_preference(use_pge_dis). |
| 1798 | | obsolete_preference(use_pge_ind). |
| 1799 | | obsolete_preference(selected_bparser). |
| 1800 | | obsolete_preference(dot_print_leaves). |
| 1801 | | obsolete_preference(csp_event_visible_to_user). |
| 1802 | | obsolete_preference(path_to_fuzz). |
| 1803 | | obsolete_preference(use_optimistic_por). |
| 1804 | | obsolete_preference(show_full_error_span). |
| 1805 | | obsolete_preference(path_to_sfdp). |
| 1806 | | obsolete_preference(dot_use_alterate_dot_viewer). |
| 1807 | | obsolete_preference(path_to_dotty2). |
| 1808 | | |
| 1809 | | % might be re-included later |
| 1810 | | obsolete_preference(plugin(absint,use_widening)). |
| 1811 | | obsolete_preference(plugin(absint,soft_widening)). |
| 1812 | | obsolete_preference(plugin(absint,extrapolation_threshold)). |
| 1813 | | obsolete_preference(plugin(absint,retract_widening_related_states)). |
| 1814 | | |
| 1815 | | % replaced by api calls |
| 1816 | | obsolete_preference(path_to_smt_solver). |
| 1817 | | |
| 1818 | | % has been renamed |
| 1819 | | obsolete_preference(try_atb_provers_for_smtlib). |
| 1820 | | |
| 1821 | | |
| 1822 | | % VOLATILE |
| 1823 | | % not necessary to store in file; value will not be changed when loading pref file |
| 1824 | | % dangerous preferences: user should explicitly reset it every time or put it explicitly into file |
| 1825 | | volatile_preference(store_event_transinfo). |
| 1826 | | volatile_preference(fail_if_clpfd_timeout). |
| 1827 | | volatile_preference(ignore_hash_collisions). |
| 1828 | | volatile_preference(forget_state_space). |
| 1829 | | volatile_preference(store_only_one_incoming_transition). |
| 1830 | | volatile_preference(filter_unused_constants). |
| 1831 | | volatile_preference(disprover_mode). |
| 1832 | | volatile_preference(trace_upon_error). |
| 1833 | | volatile_preference(performance_monitoring_on). |
| 1834 | | volatile_preference(translate_force_all_typing_infos). |
| 1835 | | volatile_preference(translate_print_typing_infos). |
| 1836 | | volatile_preference(translate_ids_to_parseable_format). |
| 1837 | | volatile_preference(translate_suppress_rodin_positions_flag). |
| 1838 | | volatile_preference(prob2_trace_file). |
| 1839 | | volatile_preference(prob2_trace_file_gen_unique_name). |
| 1840 | | volatile_preference(deterministic_trace_replay). |
| 1841 | | volatile_preference(bool_expression_as_predicate). % Deprecated |
| 1842 | | |
| 1843 | | /* ------------------------- */ |
| 1844 | ? | is_of_type(El,Type) :- type_element(Type,El). |
| 1845 | | |
| 1846 | | type_element(bool,true). |
| 1847 | | type_element(bool,false). |
| 1848 | ? | type_element(xbool,X) :- member(X,[false,true,full]). |
| 1849 | | type_element(directory_path,X) :- atomic(X),check_directory_exists(X). |
| 1850 | | type_element(int,X) :- number(X). |
| 1851 | | type_element(neg,X) :- number(X), X=<0. |
| 1852 | | type_element(nat,X) :- number(X), X>=0. |
| 1853 | | type_element(nat1,X) :- number(X), X>0. |
| 1854 | | type_element(range(Low,Up),X) :- number(X), X>=Low, X=<Up. |
| 1855 | | type_element(string,X) :- atomic(X). |
| 1856 | | type_element(path,X) :- atomic(X). % some paths are files, some directorys (.app) and some aliases |
| 1857 | | type_element(file_path,X) :- atomic(X),check_file_exists(X). |
| 1858 | | type_element(term,X) :- nonvar(X). |
| 1859 | ? | type_element(ListOfCsts,X) :- ListOfCsts=[_|_], member(X,ListOfCsts). |
| 1860 | | type_element(por,X) :- |
| 1861 | | member(X,[off,ample_sets,ample_sets2]). |
| 1862 | ? | type_element(dot_shape,X) :- is_of_type(X,[triangle,box,diamond,hexagon,octagon,house, |
| 1863 | | invtriangle,invhouse,invtrapez,invtrapezium, |
| 1864 | | egg,ellipse,oval,circle, |
| 1865 | | parallelogram,pentagon,trapezium,septagon, |
| 1866 | | square,rect,rectangle, |
| 1867 | | record, |
| 1868 | | 'Mcircle','Msquare', 'Mdiamond', |
| 1869 | | doublecircle,doubleoctagon,tripleoctagon, |
| 1870 | | none,plain,plaintext,point]). |
| 1871 | | type_element(dot_node_style,X) :- |
| 1872 | | is_of_type(X,[solid,dashed,dotted,bold,rounded,filled,diagonals,striped,wedged]). |
| 1873 | ? | type_element(dot_line_style,X) :- is_of_type(X,[solid, dashed, dotted, bold, invis]). |
| 1874 | ? | type_element(rgb_color,X) :- valid_rgb_color(X). |
| 1875 | | type_element(text_encoding,X) :- |
| 1876 | ? | is_of_type(X,[auto,'ISO-8859-1','ISO-8859-2','ISO-8859-15', |
| 1877 | | 'UTF-8','UTF-16','UTF-16LE','UTF-16BE','UTF-32','UTF-32LE','UTF-32BE', |
| 1878 | | 'ANSI_X3.4-1968', 'windows 1252']). |
| 1879 | | |
| 1880 | | valid_rgb_color(X) :- tk_color(X). |
| 1881 | | valid_rgb_color(X) :- % check for composed colors like chocolate3 |
| 1882 | ? | atom_codes(X,Codes), append(Prefix,[Digit],Codes), |
| 1883 | | Digit >= 48, Digit =< 57, Nr is Digit - 48, atom_codes(ColorName,Prefix), |
| 1884 | | tk_color(ColorName,Low,Up), |
| 1885 | | Nr >= Low, Nr =< Up. |
| 1886 | | valid_rgb_color(X) :- valid_gray(X). |
| 1887 | ? | valid_rgb_color(X) :- atom(X),atom_codes(X,[35,H1,H2,H3,H4,H5,H6]), |
| 1888 | ? | hex(H1),hex(H2),hex(H3),hex(H4),hex(H5),hex(H6). /* should be of the form #ff00ff */ |
| 1889 | | |
| 1890 | | % colors which also accept numbers at end: |
| 1891 | | tk_color(aquamarine,1,4). |
| 1892 | | tk_color(azure,1,4). |
| 1893 | | tk_color(bisque,1,4). |
| 1894 | | tk_color(blue,1,4). |
| 1895 | | tk_color(brown,1,4). |
| 1896 | | tk_color(burlywood,1,4). |
| 1897 | | tk_color('CadetBlue',1,4). |
| 1898 | | tk_color(chartreuse,1,4). |
| 1899 | | tk_color(chocolate,1,4). |
| 1900 | | tk_color(coral,1,4). |
| 1901 | | tk_color(cornsilk,1,4). |
| 1902 | | tk_color(cyan,1,4). |
| 1903 | | tk_color(deepskyblue,1,4). |
| 1904 | | tk_color('DarkGoldenrod',1,4). |
| 1905 | | tk_color('DarkOliveGreen',1,4). |
| 1906 | | tk_color('DarkOrange',1,4). |
| 1907 | | tk_color('DarkSeaGreen',1,4). |
| 1908 | | tk_color('DarkSlateGray',1,4). |
| 1909 | | tk_color('DeepPink',1,4). |
| 1910 | | tk_color('DeepSkyBlue',1,4). |
| 1911 | | tk_color('DodgerBlue',1,4). |
| 1912 | | tk_color(firebrick,1,4). |
| 1913 | | tk_color(gold,1,4). |
| 1914 | | tk_color(goldenrod,1,4). |
| 1915 | | tk_color(gray,0,99). |
| 1916 | | tk_color(green,1,4). |
| 1917 | | tk_color(grey,0,99). |
| 1918 | | tk_color(honeydew,1,4). |
| 1919 | | tk_color('HotPink',1,4). |
| 1920 | | tk_color(indianred,1,4). |
| 1921 | | tk_color('IndianRed',1,4). |
| 1922 | | tk_color(ivory,1,4). |
| 1923 | | tk_color(khaki,1,4). |
| 1924 | | tk_color('LavenderBlush',1,4). |
| 1925 | | tk_color('LemonChiffon',1,4). |
| 1926 | | tk_color('LightBlue',1,4). |
| 1927 | | tk_color('LightCyan',1,4). |
| 1928 | | tk_color('LightGoldenrod',1,4). |
| 1929 | | tk_color('LightPink',1,4). |
| 1930 | | tk_color('LightSalmon',1,4). |
| 1931 | | tk_color('LightSkyBlue',1,4). |
| 1932 | | tk_color('LightSteelBlue',1,4). |
| 1933 | | tk_color('LightYellow',1,4). |
| 1934 | | tk_color(magenta,1,4). |
| 1935 | | tk_color(maroon,1,4). |
| 1936 | | tk_color('MediumOrchid',1,4). |
| 1937 | | tk_color('MediumPurple',1,4). |
| 1938 | | tk_color('MistyRose',1,4). |
| 1939 | | tk_color('NavajoWhite',1,4). |
| 1940 | | tk_color(orchid,1,4). |
| 1941 | | tk_color(orange,1,4). |
| 1942 | | tk_color(olivedrab,1,4). |
| 1943 | | tk_color('OliveDrab',1,4). |
| 1944 | | tk_color('OrangeRed',1,4). |
| 1945 | | tk_color(mistyrose,1,4). |
| 1946 | | tk_color(peachpuff,1,4). |
| 1947 | | tk_color(pink,1,4). |
| 1948 | | tk_color(plum,1,4). |
| 1949 | | tk_color(purple,1,4). |
| 1950 | | tk_color('PaleGreen',1,4). |
| 1951 | | tk_color('PaleTurquoise',1,4). |
| 1952 | | tk_color('PaleVioletRed',1,4). |
| 1953 | | tk_color('PeachPuff',1,4). |
| 1954 | | tk_color(red,1,4). |
| 1955 | | tk_color(royalblue,1,4). |
| 1956 | | tk_color('RosyBrown',1,4). |
| 1957 | | tk_color('RoyalBlue',1,4). |
| 1958 | | tk_color(salmon,1,4). |
| 1959 | | tk_color(seagreen,1,4). |
| 1960 | | tk_color(seashell,1,4). |
| 1961 | | tk_color(sienna,1,4). |
| 1962 | | tk_color(skyblue,1,4). |
| 1963 | | tk_color(snow,1,4). |
| 1964 | | tk_color(springgreen,1,4). |
| 1965 | | tk_color(steelblue,1,4). |
| 1966 | | tk_color('SeaGreen',1,4). |
| 1967 | | tk_color('SkyBlue',1,4). |
| 1968 | | tk_color('SlateBlue',1,4). |
| 1969 | | tk_color('SlateGray',1,4). |
| 1970 | | tk_color('SpringGreen',1,4). |
| 1971 | | tk_color('SteelBlue',1,4). |
| 1972 | | tk_color(tan,1,4). |
| 1973 | | tk_color(thistle,1,4). |
| 1974 | | tk_color(tomato,1,4). |
| 1975 | | tk_color(turquoise,1,4). |
| 1976 | | tk_color('VioletRed',1,4). |
| 1977 | | tk_color(wheat,1,4). |
| 1978 | | tk_color(yellow,1,4). |
| 1979 | | |
| 1980 | | |
| 1981 | | tk_color(X) :- tk_color(X,_,_). |
| 1982 | | tk_color('AliceBlue'). |
| 1983 | | tk_color(beige). |
| 1984 | | tk_color(black). |
| 1985 | | tk_color('BlanchedAlmond'). |
| 1986 | | tk_color('BlueViolet'). |
| 1987 | | tk_color(darkblue). |
| 1988 | | tk_color(darkgray). % this is not a valid X11 color; but it is recognised by Tk (but not by sfdp) |
| 1989 | | tk_color(darkgreen). |
| 1990 | | tk_color(darkorange). |
| 1991 | | tk_color(darkorchid). |
| 1992 | | tk_color(darkred). |
| 1993 | | tk_color(darkslateblue). |
| 1994 | | tk_color(darkviolet). |
| 1995 | | tk_color('DarkBlue'). |
| 1996 | | tk_color('DarkCyan'). |
| 1997 | | tk_color('DarkGray'). |
| 1998 | | tk_color('DarkGreen'). |
| 1999 | | tk_color('DarkGrey'). |
| 2000 | | tk_color('DarkKhaki'). |
| 2001 | | tk_color('DarkMagenta'). |
| 2002 | | tk_color('DarkRed'). |
| 2003 | | tk_color('DarkSalmon'). |
| 2004 | | tk_color('DarkSlateBlue'). |
| 2005 | | tk_color('DarkTurquoise'). |
| 2006 | | tk_color('DarkViolet'). |
| 2007 | | tk_color('DimGray'). |
| 2008 | | tk_color('DimGrey'). |
| 2009 | | tk_color('FloralWhite'). |
| 2010 | | tk_color('ForestGreen'). |
| 2011 | | tk_color(lightblue). |
| 2012 | | tk_color(lightgray). |
| 2013 | | tk_color('LawnGreen'). |
| 2014 | | tk_color('LightCoral'). |
| 2015 | | tk_color('LightGray'). |
| 2016 | | tk_color('LightGreen'). |
| 2017 | | tk_color('LightGrey'). |
| 2018 | | tk_color('LightSeaGreen'). |
| 2019 | | tk_color('LimeGreen'). |
| 2020 | | tk_color(moccasin). |
| 2021 | | tk_color('MediumAquamarine'). |
| 2022 | | tk_color('MediumBlue'). |
| 2023 | | tk_color('MediumSeaGreen'). |
| 2024 | | tk_color('MediumSlateBlue'). |
| 2025 | | tk_color('MediumSpringGreen'). |
| 2026 | | tk_color('MediumTurquoise'). |
| 2027 | | tk_color('MediumVioletRed'). |
| 2028 | | tk_color('MidnightBlue'). |
| 2029 | | tk_color('MintCream'). |
| 2030 | | tk_color(navy). |
| 2031 | | tk_color('NavyBlue'). |
| 2032 | | tk_color('OldLace'). |
| 2033 | | tk_color('PapayaWhip'). |
| 2034 | | tk_color('PowderBlue'). |
| 2035 | | tk_color(slateblue). |
| 2036 | | tk_color(steelblue). |
| 2037 | | tk_color('SaddleBrown'). |
| 2038 | | tk_color('SandyBrown'). |
| 2039 | | tk_color(violet). |
| 2040 | | tk_color(white). |
| 2041 | | tk_color('WhiteSmoke'). |
| 2042 | | tk_color('YellowGreen'). |
| 2043 | | |
| 2044 | | valid_gray(G) :- atom(G), atom_codes(G,GC), append("gray",[N1|T],GC), digit(N1), |
| 2045 | | (T=[] -> true ; T=[N2],digit(N2)). |
| 2046 | | digit(N) :- N >47, N<58. |
| 2047 | | |
| 2048 | | |
| 2049 | ? | hex(X) :- atomic(X), number(X), ((X<103,X>96) ; (X<71,X>64) ; (X>47,X<58)). |
| 2050 | | |
| 2051 | | :- use_module(library(file_systems)). |
| 2052 | | check_file_exists(X) :- file_exists(X) -> true ; add_message(preferences,'Warning file for preference does not exist: ',X). |
| 2053 | | check_directory_exists(X) :- |
| 2054 | | directory_exists(X) -> true ; add_message(preferences,'Warning directory for preference does not exist: ',X). |
| 2055 | | :- public check_path_exists/1. |
| 2056 | | check_path_exists(X) :- (file_exists(X) -> true |
| 2057 | | ; directory_exists(X) -> true |
| 2058 | | ; add_message(preferences,'Warning path for preference does not exist: ',X)). |
| 2059 | | |
| 2060 | | :- dynamic temp_pref/3. |
| 2061 | | % use to temporarily set preferences; |
| 2062 | | % changes can be undone with reset_temporary_preference |
| 2063 | | % change will not be saved if reset_temporary_preference not called (e.g., due to bug/timeout/Ctrl-C) |
| 2064 | | temporary_set_preference(Pref,Val) :- temporary_set_preference(Pref,Val,_). |
| 2065 | | temporary_set_preference(Pref,Val,ChangeOccured) :- get_preference(Pref,OldVal),!, |
| 2066 | | (OldVal=Val -> ChangeOccured=false |
| 2067 | | ; set_preference_direct(Pref,Val,_,_), ChangeOccured = true, |
| 2068 | | asserta(temp_pref(Pref,OldVal,Val)) |
| 2069 | | %,debug:debug_println(9,temp_set_pref(Pref,Val)) |
| 2070 | | ). |
| 2071 | | % Note: assert(p(1)), assert(p(2)), retract(p(X)), retract(p(Y)) -> X=1, Y=2 |
| 2072 | | % Note: asserta(p(1)), asserta(p(2)), retract(p(X)), retract(p(Y)) -> X=2, Y=1 |
| 2073 | | |
| 2074 | | reset_temporary_preference(P) :- reset_temporary_preference(P,_). |
| 2075 | | reset_temporary_preference(_,ChangeOccured) :- ChangeOccured==false,!. % nothing to do |
| 2076 | | reset_temporary_preference(Pref,_) :- |
| 2077 | | (retract(temp_pref(Pref,OldVal,_NewVal)) |
| 2078 | | -> set_preference_direct(Pref,OldVal,_,_) |
| 2079 | | ; true). |
| 2080 | | |
| 2081 | ? | reset_all_temporary_preferences :- retract(temp_pref(Pref,OldVal,_)),set_preference(Pref,OldVal),fail. |
| 2082 | | reset_all_temporary_preferences. |
| 2083 | | |
| 2084 | | % this set_preference does not update change flag and performs no preference_update_action |
| 2085 | | set_preference_direct(Pref,Val,_,_) :- var(Pref),!, |
| 2086 | | print_error('Variable as preference not allowed'), |
| 2087 | | print_error(set_preference(Pref,Val)), |
| 2088 | | fail. |
| 2089 | | set_preference_direct(Pref,Val,OldVal,New) :- |
| 2090 | | % format(user_output,'~nset_preference ~w to ~w (~w)~n~n',[Pref,Val,OldVal]), |
| 2091 | | (preference_val_type(Pref,Type) |
| 2092 | ? | -> (is_of_type(Val,Type) |
| 2093 | | -> true |
| 2094 | | ; print_error('New Preference value of incorrect type: '), |
| 2095 | | print_error(Pref), print_error(Val), |
| 2096 | | %Val =.. L, print_error(val(L)), |
| 2097 | | %print_error(expected(Type)), |
| 2098 | | print_error('No changes performed!'), |
| 2099 | | fail |
| 2100 | | ) |
| 2101 | | ; print_error('Do not know type of preference'), print_error(Pref) |
| 2102 | | ), |
| 2103 | | (retract(preference(Pref,OldVal)) -> New=false ; New=true), |
| 2104 | | assert(preference(Pref,Val)), |
| 2105 | | (New=false,OldVal=Val -> true ; preference_update_action(Pref,Val)). |
| 2106 | | |
| 2107 | | set_preference(Pref,Val) :- |
| 2108 | | set_preference_direct(Pref,Val,OldVal,New), |
| 2109 | | retractall(temp_pref(Pref,_,_)), % user has overriden temporary choice |
| 2110 | | (New=false,OldVal=Val -> true ; assert_change_flag). |
| 2111 | | |
| 2112 | | |
| 2113 | | |
| 2114 | | tcltk_get_preference(Pref,Val) :- /* same as get_preference, but convert non-atomic into atoms */ |
| 2115 | | get_preference(Pref,V), |
| 2116 | | (atomic(V) -> Val=V |
| 2117 | | ; translate_term_into_atom(V,Val) |
| 2118 | | ). |
| 2119 | | |
| 2120 | | get_preference(Pref,Val) :- |
| 2121 | | (preference(Pref,V) |
| 2122 | | -> Val=V |
| 2123 | | ; (preference_default_value(Pref,V) |
| 2124 | | -> Val=V |
| 2125 | | ; print_error('Invalid Preference in get_preference:'), |
| 2126 | | print_error(Pref), |
| 2127 | | Val = 0 |
| 2128 | | ) |
| 2129 | | ). |
| 2130 | | |
| 2131 | | % rules for computed/derived preferences: |
| 2132 | | get_computed_preference(debug_time_out,Res) :- |
| 2133 | | preference(debug_time_out_factor,TFactor), !, |
| 2134 | | get_time_out_preference_with_factor(TFactor,Res). |
| 2135 | | get_computed_preference(convert_closures_into_explicit_form_for_store,Value) :- |
| 2136 | | preference(convert_comprehension_sets_into_closures,SymbolicV),!, |
| 2137 | | (SymbolicV=true -> Value=false ; Value=true). |
| 2138 | | get_computed_preference(X,_) :- print_error('Invalid Preference in get_computed_preference:'), |
| 2139 | | print_error(X). |
| 2140 | | |
| 2141 | | get_time_out_preference_with_factor(TFactor,Res) :- |
| 2142 | | preference(time_out,CurTO), |
| 2143 | | (disabled_time_out(CurTO) |
| 2144 | | -> disabled_time_out(Res) % keep disabled_time_out value |
| 2145 | | ; DTimeOut is integer(CurTO * TFactor), |
| 2146 | | prune_time_out_preference(DTimeOut,Res)). |
| 2147 | | add_time_outs(TO1,TO2,ResTO) :- |
| 2148 | | (disabled_time_out(TO1) -> ResTO=TO1 |
| 2149 | | ; disabled_time_out(TO2) -> ResTO=TO2 |
| 2150 | | ; ResTO is TO1+TO2 |
| 2151 | | ). |
| 2152 | | |
| 2153 | | % value of 2147483646 means time-out was disabled, 600 hours; should we move to 64 bits ? |
| 2154 | | disabled_time_out(2147483646). |
| 2155 | | prune_time_out_preference(X,Res) :- (X>= 2147483646 -> disabled_time_out(Res) ; Res=X). |
| 2156 | | |
| 2157 | | time_out_preference_disabled :- preference(time_out,2147483646). |
| 2158 | | |
| 2159 | | cur_pref_string(Pref,String) :- |
| 2160 | | preference_description(Pref,Desc), |
| 2161 | | (eclipse_preference(ECLPREF,Pref) -> ajoin([ECLPREF,': ',Desc],String) |
| 2162 | | ; String=Desc). %string_concatenate(Desc,';',String)). |
| 2163 | | /* preference(Pref,Val), |
| 2164 | | string_concatenate(Val,';',V1), |
| 2165 | | string_concatenate(' = ',V1,V2), |
| 2166 | | string_concatenate(Desc,V2,String). */ |
| 2167 | | |
| 2168 | | /* useful predicates for Tcl/Tk listbox interaction: */ |
| 2169 | | get_preferences_list(List) :- |
| 2170 | | findall(S,cur_pref_string(_,S),List). |
| 2171 | | get_preferences_list(Category,list(List)) :- |
| 2172 | | findall(S,(virtual_preference_category(Pref,Category),cur_pref_string(Pref,S)),List). |
| 2173 | | |
| 2174 | | % add some virtual categories like eclipse |
| 2175 | | virtual_preference_category(Pref,Category) :- Category==eclipse,!, |
| 2176 | | findall(e(E,P),(eclipse_preference(E,P), \+ preference_category(P,hidden)),List), |
| 2177 | | sort(List,SList), |
| 2178 | | member(e(_,Pref),SList). |
| 2179 | | virtual_preference_category(Pref,Category) :- preference_description(Pref,_Desc), preference_category(Pref,Category). |
| 2180 | | virtual_preference_category(Pref,Category) :- preference_description(Pref,_Desc), |
| 2181 | | alternate_preference_category(Pref,Category). |
| 2182 | | |
| 2183 | | |
| 2184 | | get_ith_preference_type(Pos,Type) :- get_ith_preference_type(_,Pos,Type). |
| 2185 | | get_ith_preference_type(Category,Pos,Type) :- |
| 2186 | | findall(S, (virtual_preference_category(Pref,Category), |
| 2187 | | preference_val_type(Pref,S)), List), |
| 2188 | | (nth1(Pos,List,FType) -> Type=FType |
| 2189 | | ; (add_error(get_ith_preference_type,'Could not find preference: ',nth1(Pos,List)),fail)). |
| 2190 | | |
| 2191 | | get_ith_preference_value(Pos,Val) :- get_ith_preference_value(_,Pos,Val). |
| 2192 | | get_ith_preference_value(Category,Pos,Val) :- |
| 2193 | | findall(S, (virtual_preference_category(Pref,Category), |
| 2194 | | tcltk_get_preference(Pref,S)), List), |
| 2195 | | (nth1(Pos,List,FVal) -> Val=FVal |
| 2196 | | ; (add_error(get_ith_preference_value,'Could not find preference: ',nth1(Pos,List)),fail)). |
| 2197 | | |
| 2198 | | set_ith_preference_value(Pos,Val) :- set_ith_preference_value(_,Pos,Val). |
| 2199 | | set_ith_preference_value(Category,Pos,Val) :- |
| 2200 | | findall(S, virtual_preference_category(S,Category), List), |
| 2201 | | (nth1(Pos,List,Pref) -> set_preference(Pref,Val) |
| 2202 | | ; add_error(set_ith_preference_value,'Could not find preference: ',nth1(Pos,List)),fail). |
| 2203 | | |
| 2204 | | |
| 2205 | | /* ------------------------- */ |
| 2206 | | |
| 2207 | | :- dynamic nr_of_recent_documents/1. |
| 2208 | | :- dynamic recent_documents/1. |
| 2209 | | nr_of_recent_documents(0). |
| 2210 | | |
| 2211 | | recompute_nr_of_recent_documents :- |
| 2212 | | retractall(nr_of_recent_documents(_)), |
| 2213 | | findall(X,recent_documents(X),List), |
| 2214 | | length(List,Nr), |
| 2215 | | assert(nr_of_recent_documents(Nr)). |
| 2216 | | |
| 2217 | | |
| 2218 | | :- dynamic add_recent_documents_active/0. |
| 2219 | | add_recent_documents_active. |
| 2220 | | |
| 2221 | | activate_recent_documents :- (add_recent_documents_active -> true ; assert(add_recent_documents_active)). |
| 2222 | | |
| 2223 | | deactivate_recent_documents :- retractall(add_recent_documents_active). |
| 2224 | | |
| 2225 | | /* use to add a file to recent documents list */ |
| 2226 | | add_recent_document(_) :- \+ add_recent_documents_active, !. |
| 2227 | | add_recent_document(Document) :- |
| 2228 | | (retract(nr_of_recent_documents(Nr)) -> true ; Nr=0), |
| 2229 | | (retract(recent_documents(Document)) |
| 2230 | | -> N1 =Nr ; N1 is Nr+1 |
| 2231 | | ), |
| 2232 | | (preference(number_of_recent_documents,Max) -> true ; Max=25), |
| 2233 | | (N1>Max -> (retract(recent_documents(_)),assert(nr_of_recent_documents(Nr))) |
| 2234 | | ; assert(nr_of_recent_documents(N1))), |
| 2235 | | assertz(recent_documents(Document)), |
| 2236 | | assert_change_flag. |
| 2237 | | |
| 2238 | | get_recent_documents(list(Res)) :- |
| 2239 | | findall(X,recent_documents(X),List), |
| 2240 | | reverse(List,Res). |
| 2241 | | |
| 2242 | | clear_recent_documents :- |
| 2243 | | retractall(recent_documents(_)), |
| 2244 | | retractall(nr_of_recent_documents(_)), |
| 2245 | | assert(nr_of_recent_documents(0)). |
| 2246 | | |
| 2247 | | |
| 2248 | | /* use to add a string to the searched patterns list */ |
| 2249 | | :- dynamic searched_patterns/1. |
| 2250 | | :- dynamic replaced_patterns/1. |
| 2251 | | :- dynamic eval_history_elements/1. |
| 2252 | | :- dynamic eval_csp_history_elements/1. |
| 2253 | | :- dynamic checked_ltl_formulas/1. |
| 2254 | | |
| 2255 | | |
| 2256 | | add_element_to_history(Predicate,Pattern,MaxNumb) :- |
| 2257 | | merge_prefix_with_suffix(number_of_,Predicate,Name), |
| 2258 | | get_predicate_term_with_single_argument(Name,Nr,TermNum), |
| 2259 | | (retract(TermNum) -> true ; Nr=0), |
| 2260 | | get_predicate_term_with_single_argument(Predicate,Pattern,Term), |
| 2261 | | (retract(Term) -> N1=Nr ; N1 is Nr+1), |
| 2262 | | (preference(TermNum,Max) -> true ; Max=MaxNumb), |
| 2263 | | get_predicate_term_with_single_argument(Predicate,_,Term1), |
| 2264 | | (N1>Max -> (retract(Term1),assert(TermNum)) |
| 2265 | | ; get_predicate_term_with_single_argument(Name,N1,TermNum1), |
| 2266 | | assert(TermNum1)),assertz(Term), |
| 2267 | | assert_change_flag. |
| 2268 | | |
| 2269 | | % this will be used with checked_ltl_formulas, ... from tcltk_gui.tcl |
| 2270 | | :- public searched_patterns/1, replaced_patterns/1, eval_history_elements/1, eval_csp_history_elements/1, checked_ltl_formulas/1. |
| 2271 | | get_history_elements_list(Predicate,Reversed,list(Res)) :- |
| 2272 | | get_predicate_term_with_single_argument(Predicate,X,Term), |
| 2273 | | findall(X,Term,List), |
| 2274 | | (Reversed=true -> reverse(List,Res); Res=List). |
| 2275 | | |
| 2276 | | |
| 2277 | | |
| 2278 | | /* not used |
| 2279 | | :- dynamic number_of_checked_ltl_formulas/1. |
| 2280 | | number_of_checked_ltl_formulas(0). |
| 2281 | | recompute_nr_of_checked_ltl_formulas :- |
| 2282 | | retractall(number_of_checked_ltl_formulas(_)), |
| 2283 | | findall(F,checked_ltl_formulas(F),List), |
| 2284 | | length(List,Nr),assert(number_of_checked_ltl_formulas(Nr)). */ |
| 2285 | | |
| 2286 | | merge_prefix_with_suffix(Prefix,Ending,Name) :- |
| 2287 | | atom_codes(Prefix,Pr),atom_codes(Ending,End), |
| 2288 | | append(Pr,End,CodeName),atom_codes(Name,CodeName). |
| 2289 | | |
| 2290 | | get_predicate_term_with_single_argument(Name,Arg,Term) :- |
| 2291 | | functor(Term,Name,1),arg(1,Term,Arg). |
| 2292 | | |
| 2293 | | |
| 2294 | | /* ------------------------- */ |
| 2295 | | |
| 2296 | | :- dynamic prob_application_type/1. |
| 2297 | | prob_application_type(unknown). |
| 2298 | | |
| 2299 | | get_prob_application_type(X) :- prob_application_type(X). |
| 2300 | | set_prob_application_type(X) :- retractall(prob_application_type(_)), assert(prob_application_type(X)). |
| 2301 | | % can be tcltk, probcli, prob2, ... |
| 2302 | | |
| 2303 | | /* ------------------------- */ |
| 2304 | | |
| 2305 | | set_preference_group(Group,_) :- \+ preference_group_description(Group,_),!, |
| 2306 | | add_error(set_preference_mode,'Preference mode does not exist: ',Group). |
| 2307 | | set_preference_group(Group,default) :- preference_group_val(Group,Scheme,_,_),!, |
| 2308 | | ( preference_group_val(Group,Scheme,Pref,_),preference_default_value(Pref,Val), |
| 2309 | | set_preference(Pref,Val),fail |
| 2310 | | ; true). |
| 2311 | ? | set_preference_group(Group,Scheme) :- preference_group_val(Group,Scheme,Pref,Val), |
| 2312 | | set_preference(Pref,Val),fail. |
| 2313 | | set_preference_group(_,_). |
| 2314 | | |
| 2315 | | |
| 2316 | | preference_group_description(integer,'Values for MAXINT and MININT'). |
| 2317 | | preference_group_description(time_out,'To disable TIME_OUT'). |
| 2318 | | preference_group_description(model_check,'Model Checking Limits'). |
| 2319 | | preference_group_description(dot_colors,'Colours for Dot graphs'). |
| 2320 | | |
| 2321 | | preference_group_val(integer,int32,maxint,2147483647). % 2147483647 |
| 2322 | | preference_group_val(integer,int32,minint,-2147483648). %-2147483648 |
| 2323 | | preference_group_val(integer,int8,maxint,127). |
| 2324 | | preference_group_val(integer,int8,minint,-128). |
| 2325 | | |
| 2326 | | 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 |
| 2327 | | |
| 2328 | | preference_group_val(model_check,unlimited,time_out,TO) :- disabled_time_out(TO). % this value turns time_out off |
| 2329 | | preference_group_val(model_check,unlimited,maxNrOfInitialisations,Max) :- prolog_flag(max_tagged_integer,Max). |
| 2330 | | preference_group_val(model_check,unlimited,maxNrOfEnablingsPerOperation,Max) :- prolog_flag(max_tagged_integer,Max). |
| 2331 | | preference_group_val(model_check,disable_max,maxNrOfInitialisations,Max) :- prolog_flag(max_tagged_integer,Max). |
| 2332 | | preference_group_val(model_check,disable_max,maxNrOfEnablingsPerOperation,Max) :- prolog_flag(max_tagged_integer,Max). |
| 2333 | | |
| 2334 | | preference_group_val(dot_colors,classic,dot_normal_node_colour, olivedrab2). |
| 2335 | | preference_group_val(dot_colors,classic,dot_normal_arc_colour,steelblue). |
| 2336 | | preference_group_val(dot_colors,classic,dot_open_node_colour,red). |
| 2337 | | preference_group_val(dot_colors,classic,dot_goal_node_colour,orange). |
| 2338 | | preference_group_val(dot_colors,classic,dot_invariant_violated_node_colour,maroon2). |
| 2339 | | preference_group_val(dot_colors,classic,dot_counterexample_node_colour,brown). |
| 2340 | | preference_group_val(dot_colors,classic,dot_counterexample_op_colour,brown). |
| 2341 | | |
| 2342 | | preference_group_val(dot_colors,winter,dot_normal_node_colour, '#425955'). |
| 2343 | | preference_group_val(dot_colors,winter,dot_normal_arc_colour,'#1B1D26'). |
| 2344 | | preference_group_val(dot_colors,winter,dot_open_node_colour,'#BFBD9F'). |
| 2345 | | preference_group_val(dot_colors,winter,dot_goal_node_colour,'#CC8604'). |
| 2346 | | preference_group_val(dot_colors,winter,dot_invariant_violated_node_colour,'#9C080C'). |
| 2347 | | |
| 2348 | | preference_group_val(dot_colors,dreams,dot_normal_node_colour, '#5D7359'). |
| 2349 | | preference_group_val(dot_colors,dreams,dot_invariant_violated_node_colour,'#661C0E'). |
| 2350 | | preference_group_val(dot_colors,dreams,dot_normal_arc_colour,'#8C5430'). |
| 2351 | | preference_group_val(dot_colors,dreams,dot_open_node_colour,'#D6AA5C'). |
| 2352 | | preference_group_val(dot_colors,dreams,dot_goal_node_colour,'#FFC800'). |
| 2353 | | |
| 2354 | | |
| 2355 | | :- use_module(eventhandling,[register_event_listener/3]). |
| 2356 | | :- register_event_listener(startup_prob,init_preferences, |
| 2357 | | 'Initialise Preferences'). |
| 2358 | | :- register_event_listener(clear_specification,reset_all_temporary_preferences, |
| 2359 | | 'Reset Temporary Preferences.'). |
| 2360 | | :- register_event_listener(start_unit_tests,(backup_preferences, |
| 2361 | | set_preference(minint,-1), |
| 2362 | | set_preference(maxint,3), |
| 2363 | | set_preference(translate_print_all_sequences,false), |
| 2364 | | set_preference(translate_print_cs_style_sequences,false) |
| 2365 | | ), |
| 2366 | | 'Setting up Preferences for Unit Tests'). |
| 2367 | | :- register_event_listener(stop_unit_tests, revert_preferences, 'Reverting Preferences'). |