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