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