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