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