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