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