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