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(value_persistance, [set_storage_directory/1,set_storage_directory/2,
6		unset_storage_directory/0,
7		save_constants/1,
8		load_constants/2,
9		cache_is_activated/0, clear_applicable_flag/0,
10		load_partial_constants/3, % load saved constants for sub-machines
11		lookup_cached_transitions/4,
12		add_new_transitions_to_cache/1,
13		add_new_transition_to_cache_from_expanded_state/4, % mainly for execute_modus
14		start_cache_execute_modus/1, stop_cache_execute_modus/0,
15		tcltk_load_constants/1,
16		delete_cache_files/0,
17		delete_cache_files_for_machine/1,
18		show_cache_file_contents/1, % portray contents of cache files
19		print_value_persistance_stats/0,
20		get_value_persistance_stats/1
21		]).
22
23
24		:- use_module(library(lists)).
25		:- use_module(library(file_systems)).
26		:- use_module(library(fastrw)). % fast_read/2
27
28		:- use_module(debug).
29		:- use_module(tools).
30		:- use_module(error_manager, [add_error/2,add_error/3]).
31		:- use_module(state_space, [transition/3,visited_expression/2,
32		time_out_for_node/1,not_all_transitions_added/1,
33		time_out_for_node/3,transition/4,
34		transition_info/2 %,max_reached_for_node/1
35		]).
36		:- use_module(succeed_max, [max_reached/1]).
37		:- use_module(preferences).
38		:- use_module(b_machine_hierarchy).
39		:- use_module(specfile, [animation_mode/1, classical_b_mode/0,
40		state_corresponds_to_initialised_b_machine/2]).
41		:- use_module(store, [lookup_value/3]).
42		:- use_module(kernel_objects, [equal_object/2]).
43		:- use_module(bmachine, [b_get_machine_refinement_hierarchy/1,
44		b_top_level_operation/1, get_operation_info/2]).
45		%:- use_module(bmachine_structure, [get_section/3]).
46		:- use_module(b_global_sets, [is_b_global_constant/3,b_global_set/1]).
47		:- use_module(bsyntaxtree).
48		:- use_module(extension('probhash/probhash'),[raw_sha_hash/2]).
49		:- use_module(tools_printing,[format_with_colour_nl/4]).
50		:- use_module(runtime_profiler,[start_profile/2, stop_profile/4]).
51
52		:- use_module(module_information).
53		:- module_info(group,interpreter).
54		:- module_info(description,'This module is responsible for caching constants and operations on disk').
55
56		:- dynamic storage_directory/1.
57		% storage_directory('/home/plagge/svn/alstomprob/examples/cache/').
58		:- volatile storage_directory/1.
59		:- dynamic is_applicable_internal/1.
60		:- volatile is_applicable_internal/1.
61
62		/**********************************************************************/
63		/* common for loading and saving: */
64		/**********************************************************************/
65
66		cache_is_activated :-
67		storage_directory(_).
68
69		cache_is_applicable_for_constants :-
70		cache_is_applicable, get_preference(cache_constants,true).
71		cache_is_applicable_for_transitions :-
72		cache_is_applicable, get_preference(cache_operations,true).
73
74		cache_is_applicable :-
75		is_applicable_internal(Applicable),!,Applicable=true.
76		cache_is_applicable :-
77		cache_is_activated,
78		% b_mode, % only for B models
79	?	classical_b_mode,
80		b_get_machine_refinement_hierarchy([_]), % only if there is no refinement - we cache no refinements
81		preferences:get_preference(symmetry_mode,off), % with symmetry on: you cannot simply patch operation updates
82		formatinfo('value caching: cache IS applicable',[]),
83		assert_once( is_applicable_internal(true) ),!.
84		cache_is_applicable :-
85		debug_format(19,'value persistance, cache NOT applicable~n',[]),
86		assert_once( is_applicable_internal(false) ),fail.
87
88		:- use_module(tools,[get_parent_directory_of_directory/2]).
89		set_storage_directory(Dir) :- set_storage_directory(Dir,strict).
90		set_storage_directory(Dir,Create) :-
91		unset_storage_directory,
92		(absolute_file_name(Dir,AbsDir,[file_type(directory),access(exist),fileerrors(fail)])
93		-> assertz(storage_directory(AbsDir))
94		; Create=create_if_needed,
95		get_parent_directory_of_directory(Dir,ParentDir),
96		directory_exists(ParentDir),
97		% parent directory exists; try to create the directory itself
98		absolute_file_name(Dir,AbsDir,[file_type(directory),access(none),fileerrors(fail)]),
99		formatinfo('Trying to create cache directory: ~w',[AbsDir]),
100		make_directory(AbsDir)
101		-> assertz(storage_directory(AbsDir))
102		; add_error(cache,'Could not set cache directory, directory does not exist: ',Dir)).
103
104		reset_value_persistance :-
105		unset_storage_directory,
106		reset_counters.
107		unset_storage_directory :-
108		retractall(storage_directory(_)),
109		clear_applicable_flag.
110
111		% should be called if e.g. animation mode information changes (csp_and_b mode)
112		clear_applicable_flag :-
113		retractall(is_applicable_internal(_)).
114		:- use_module(eventhandling,[register_event_listener/3]).
115		:- register_event_listener(change_of_animation_mode,clear_applicable_flag, 'Clear Cache Info.').
116		:- register_event_listener(reset_prob,reset_value_persistance, 'Reset Cache').
117
118		%:- use_module(version, [revision/1]).
119		:- use_module(version,[version/4]).
120		get_revision_info(info(V1,V2,V3,V4,ValuePersistanceRevision)) :-
121		% revision(Revision), % revision not used: it differs between probcli and ProB Tcl/Tk
122		version(V1,V2,V3,V4),
123		ValuePersistanceRevision = '$Rev$'.
124
125		collect_computation_parameters(Name,[machine_name(Name)
126		,prob_revision(Revision)
127		%,machine_hash(Hash)
128		,constants_signature(ConstSig)
129		|Prefs]) :-
130		find_relevant_preferences(Prefs),
131		get_revision_info(Revision),
132		%machine_hash(Name,Hash),
133		compute_constants_signature(Name,ConstSig).
134
135		/* returns a list of Pref/Value pairs for each preference that is regarded
136		a relevant when computing values for constants. See is_relevant_preference/2
137		below */
138		find_relevant_preferences(Prefs) :-
139		findall(preference(Pref,Value), relevant_preference(Pref,Value), Unsorted),
140		sort(Unsorted,Prefs).
141
142		% value_persistance:find_relevant_preferences(L), member(preference(P,_),L), print(P),nl,fail.
143
144		relevant_preference(Pref,Value) :-
145	?	preference_category(Pref,Category),
146	?	( is_relevant_preference(Pref,Category) -> true; fail), % just to introduce a local cut
147		get_preference(Pref,Value).
148
149		/* is_relevant_preference(+Preference,+Category)
150		is used to specify those preferencees whose values are stored in the constants file.
151		If such a preference changes, the constants have to be recomputed */
152
153		is_relevant_preference(Pref,_) :- nonvar(Pref),
154	?	irrelevant_preference(Pref),!,fail.
155		is_relevant_preference(_Pref,animation).
156		is_relevant_preference(_Pref,hidden).
157		is_relevant_preference(_Pref,advanced).
158
159		% number_animated_abstractions : only relevant for Event-B + if refinement
160		irrelevant_preference(cache_operations_runtime_limit). % only influences what gets stored; re-use always safe
161		irrelevant_preference(cache_constants). % ditto
162		irrelevant_preference(cache_operations). % ditto
163		irrelevant_preference(clash_strict_checks). % no influence on values computed
164		irrelevant_preference(strict_raise_warnings). % no influence on values computed
165		irrelevant_preference(warn_if_definition_hides_variable). % no influence on values computed
166		%irrelevant_preference(strict_raise_enum_warnings). % no sure if it can affect outcome in meaningful; could result in symbolic instead values??
167		irrelevant_preference(jvm_parser_heap_size_mb). % no influence on values computed
168		irrelevant_preference(jvm_parser_additional_args). % ditto
169		irrelevant_preference(use_safety_ltl_model_checker). % ditto
170		irrelevant_preference(store_only_one_incoming_transition). % ditto
171		irrelevant_preference(forget_state_space). % ditto
172		irrelevant_preference(type_check_definitions). % ditto
173		irrelevant_preference(expand_avl_upto). % only affects pretty-printing
174		irrelevant_preference(bool_expression_as_predicate). % only used inside REPL/eval
175		irrelevant_preference(use_large_jvm_for_parser).
176		irrelevant_preference(expand_forall_upto). % only relevant in predicate analysis
177		irrelevant_preference(time_out). % if time_out occurs: no re-use anyway
178		irrelevant_preference(performance_monitoring_on). % just prints messages
179		irrelevant_preference(performance_monitoring_expansion_limit).
180		irrelevant_preference(kodkod_for_components) :- \+ preference(use_solver_on_load,kodkod).
181		irrelevant_preference(do_neginvariant_checking). % just indicates whether invariant evaluated doubly
182		irrelevant_preference(provide_trace_information). % just provides feedback; should not change values
183		irrelevant_preference(prob_profiling_on). % ditto
184		irrelevant_preference(prob_source_profiling_on). % ditto
185		irrelevant_preference(use_closure_expansion_memoization). % only influences performance
186		irrelevant_preference(warn_when_expanding_infinite_closures). % only generates extra warnings
187		irrelevant_preference(use_small_window).
188		irrelevant_preference(tk_show_source_pane).
189		irrelevant_preference(check_prolog_b_ast).
190		irrelevant_preference(use_font_size_for_columns).
191		irrelevant_preference(user_is_an_expert_with_accessto_source_distribution).
192		irrelevant_preference(default_to_runtime_type_checking_on_startup_for_expert).
193		irrelevant_preference(number_of_recent_documents).
194		irrelevant_preference(number_of_searched_patterns).
195		irrelevant_preference(number_of_replaced_patterns).
196		irrelevant_preference(number_of_eval_history_elements).
197		irrelevant_preference(number_of_eval_csp_history_elements).
198		irrelevant_preference(number_of_checked_ltl_formulas).
199		irrelevant_preference(machines_path).
200		irrelevant_preference(tlc_number_of_workers).
201		irrelevant_preference(tlc_use_prob_constant_setup).
202		irrelevant_preference(unsat_core_algorithm).
203
204		irrelevant_preference(deterministic_trace_replay).
205		irrelevant_preference(dot_use_ps_viewer).
206		%irrelevant_preference(double_evaluation_when_analysing).% not used when computing constants or events
207		irrelevant_preference(generate_minimal_nr_of_testcases).
208		irrelevant_preference(ltl_to_ba_tool).
209		irrelevant_preference(path_to_atb_krt).
210		irrelevant_preference(path_to_bcomp).
211		irrelevant_preference(path_to_clingo).
212		irrelevant_preference(path_to_cspm).
213		irrelevant_preference(path_to_csp_typechecker).
214		irrelevant_preference(path_to_dot).
215		irrelevant_preference(path_to_dotty).
216		irrelevant_preference(path_to_fdr).
217		irrelevant_preference(path_to_fuzz). %% ??
218		irrelevant_preference(path_to_latex).
219		irrelevant_preference(path_to_ltsmin).
220		irrelevant_preference(path_to_probe).
221		irrelevant_preference(path_to_ps_viewer).
222		irrelevant_preference(path_to_spin).
223		irrelevant_preference(path_to_text_editor).
224		irrelevant_preference(path_to_text_editor_launch).
225		irrelevant_preference(repl_cache_parsing).
226		irrelevant_preference(show_bvisual_formula_explanations).
227		irrelevant_preference(show_bvisual_formula_functor_from).
228		irrelevant_preference(show_bvisual_proof_info_icons).
229		irrelevant_preference(show_function_tuples_in_property).
230		irrelevant_preference(symbolic_mc_try_other_solvers).
231		irrelevant_preference(use_scope_predicate).
232
233		irrelevant_preference(path_to_java).
234		irrelevant_preference(translate_print_all_sequences).
235		irrelevant_preference(translate_print_cs_style_sequences).
236		irrelevant_preference(view_probcli_errors_using_bbresults).
237		irrelevant_preference(trace_upon_error).
238		irrelevant_preference(error_log_file).
239		irrelevant_preference(tk_custom_state_viewer_padding).
240		irrelevant_preference(tk_custom_state_viewer_str_padding).
241		irrelevant_preference(tk_custom_state_viewer_font_name).
242		irrelevant_preference(tk_custom_state_viewer_font_size).
243		irrelevant_preference(use_tk_custom_state_viewer).
244		irrelevant_preference(translate_suppress_rodin_positions_flag).
245		irrelevant_preference(translate_ids_to_parseable_format).
246		irrelevant_preference(translate_print_frozen_infos).
247		irrelevant_preference(translate_print_typing_infos).
248		irrelevant_preference(translate_force_all_typing_infos).
249		irrelevant_preference(prob_lastchangedate_info). % what about prob_revision_info ?
250		irrelevant_preference(X) :- preference_category(X,Cat), irrelevant_category(Cat).
251
252		irrelevant_category(alloy2b).
253		irrelevant_category(cbc_commands). %cbc_provide_explanations
254		irrelevant_category(distb).
255		irrelevant_category(dot).
256		irrelevant_category(dot_definitions).
257		irrelevant_category(dot_event_hierarchy).
258		irrelevant_category(dot_formula_tree).
259		irrelevant_category(dot_machine_hierarchy).
260		irrelevant_category(dot_graph_generator).
261		irrelevant_category(dot_projection).
262		irrelevant_category(dot_state_graph).
263		irrelevant_category(dot_state_space).
264		irrelevant_category(dot_variable_modification).
265		irrelevant_category(gui_prefs).
266		irrelevant_category(latex).
267		irrelevant_category(mc_dc_commands).
268		irrelevant_category(smtlib2b).
269		irrelevant_category(state_as_graph).
270		irrelevant_category(syntax_highlighting).
271		irrelevant_category(table_commands).
272		irrelevant_category(trace_generator).
273		irrelevant_category(visb).
274		irrelevant_category(wd_commands).
275		% alternate categories already covered by dot category:
276		%irrelevant_category(state_as_graph).
277		%irrelevant_category(dot_graph_generator).
278		%irrelevant_category(dot_state_space).
279
280		compute_constants_signature(Name,constsig(Name,PropHash,Sublist)) :-
281		properties_hash(Name,PropHash),
282		findall(Sig,
283		( referenced_machine_with_constants_or_properties(Name,RefName),
284		compute_constants_signature(RefName,Sig)),
285		SubSigs),
286		sort(SubSigs,Sublist).
287
288		referenced_machine_with_constants_or_properties(OrigName,RefName) :-
289		referenced_machine(OrigName,RefName,_,_),
290		machine_has_constants_or_properties_trans(RefName).
291
292		machine_has_constants_or_properties_trans(Name) :-
293		machine_has_constants_or_properties(Name),!.
294		machine_has_constants_or_properties_trans(Name) :-
295		referenced_machine(Name,Ref,_,_),
296		machine_has_constants_or_properties_trans(Ref),!.
297		machine_has_constants_or_properties(Name) :-
298		machine_identifiers(Name,_Params,Sets,_AVars,_CVars,AConsts,CConsts),
299		( Sets=[_|_] ; AConsts==[_|_] ; CConsts=[_|_]),!.
300
301		referenced_machine(SrcName,DstName,Type,Prefix) :-
302		machine_references(SrcName,Refs),
303		member(ref(Type,DstName,Prefix),Refs).
304
305		/**********************************************************************/
306		/* saving values of constants */
307		/**********************************************************************/
308		:- use_module(state_packing).
309
310		save_constants(MaxReached) :-
311		cache_is_applicable,
312		main_machine_name(Name), % this fails e.g. in Z mode
313		\+ constants_loaded_from_file(Name), % we have just loaded the constants from file; no need to re-write them
314		!,
315		save_constants1(Name,MaxReached).
316		%(machine_name(MName), save_constants1(MName,MaxReached), fail ; true). % this would save all constants; not just the one's from the main machine; but we should probably only save the constants whose value is already deterministic in the original included machine
317		save_constants(_MaxReached).
318
319		save_constants1(Name,MaxReached) :-
320		(save_constants2(Name,MaxReached) -> true ; add_error(value_persistance,'Storing constants failed for:',Name)).
321
322		save_constants2(Name,MaxReached) :-
323		statistics(runtime,[Start,_]),
324		statistics(walltime,[WStart,_]),
325		save_constants_for_machine(Name,MaxReached),
326		statistics(runtime,[Stop,_]), Time is Stop - Start,
327		statistics(walltime,[WStop,_]), WTime is WStop - WStart,
328		%% tools:print_memory_used_wo_gc,
329		formatinfo('value caching: storing constants for ~w (max_reached: ~w) (~w [~w] ms).',
330		[Name,MaxReached,Time,WTime]).
331
332		save_constants_for_machine(Name,MaxReached) :-
333		find_constants(Name,Constants), % At the moment this only returns top-level constants and is ignored!
334		Constants = [_|_], % at least one constant exists, check before computing findall !
335		find_constants_stores(Stores), % find all concrete_constants(_) nodes in state_space
336		is_usable_data(Name,Constants,Stores),!,
337		save_constants_stores(Name,MaxReached,Constants,Stores).
338		save_constants_for_machine(Name,_MaxReached) :-
339		formatinfo('value caching: no constants stored for ~w',[Name]).
340
341		% called by add_new_transition_to_cache_from_expanded_state:
342		save_constants_from_expanded_state(SingleState) :-
343		cache_is_applicable_for_constants,
344		main_machine_name(Name),
345		\+ constants_loaded_from_file(Name), % we have just loaded the constants from file; no need to re-write them
346		SingleState = concrete_constants(Store),
347		length(Store,Len), formatinfo('value caching: saving ~w constants from expanded state',[Len]),
348		find_constants(Name,Constants),
349		!,
350		MaxReached=true, % we do not know if there are more constants states
351		save_constants_stores(Name,MaxReached,Constants,[Store]).
352		save_constants_from_expanded_state(_) :-
353		(cache_is_applicable,main_machine_name(Name)
354		-> formatinfo('value caching: no constants stored for ~w',[Name]) ; true).
355
356		% TODO: at the moment memoisation closures will not work and Memo id info also need to be stored and re-loaded
357		save_constants_stores(Name,MaxReached,Constants,Stores) :-
358		debug_println(9,saving_constants(Name)),
359		maplist(generate_bindings(Constants),Stores,ConstantBindings), % Constants currently not used
360		collect_computation_parameters(Name,CompParams),
361		length(ConstantBindings,Len),formatinfo('value caching: saving ~w constant solutions of machine ~w to file.',[Len,Name]),
362		bb_inc_by(value_persistance_stored_constants,Len),
363		save_values_into_file(Name,CompParams,ConstantBindings,MaxReached).
364
365		find_main_constants(Constants) :- b_get_machine_constants(C),
366		sort(C,Constants).
367		find_constants(Name,Constants) :-
368		machine_identifiers(Name,Params,_Sets,_AVars,_CVars,AbstractConstants,ConcreteConstants),
369		( Params=[_|_]
370		-> add_warning(value_persistance,'Parameters not yet supported.'), % ok to just issue warning ?? or should we generate error ?
371		fail
372		; true),
373		append(AbstractConstants,ConcreteConstants,RawConstants),
374		maplist(get_raw_identifier,RawConstants,Unsorted),
375		sort(Unsorted,Constants).
376		get_raw_identifier(identifier(_Pos,Id),Id).
377		get_raw_identifier(description(_Pos,_Desc,Raw),Id) :- get_raw_identifier(Raw,Id).
378
379		/* Returns the stores of values in the state space that contain values for contants */
380		find_constants_stores(Stores) :-
381		findall(S,
382		( transition(root,Trans,I),
383		functor(Trans,'$setup_constants',_),
384		visited_expression(I,concrete_constants(S))
385		),
386		Stores).
387
388		/* is_usable_data/2 succeeds if there are constants that are ready to store */
389		is_usable_data(MachName,Constants,Stores) :-
390		% at least one constant exists
391		Constants = [_|_],
392		% at least one state with computed constants was generated
393		Stores = [_|_],
394		% all constants have been computed
395		(not_all_transitions_added(root)
396		-> formatwarn('value caching: not storing constants for ~w as not all transitions computed.',[MachName]), fail
397		; true),
398		% no time-out in the root node
399		(time_out_for_node(root)
400		-> formatwarn('value caching: not storing constants for ~w as TIME_OUT occured.',[MachName]), fail
401		; true).
402
403		%generate_bindings(Constants,Store,ConstantsBinding) :-
404		% maplist(generate_binding2(Store),Constants,ConstantsBinding).
405		%generate_binding2(Store,Constant,bind(Constant,Value)) :-
406		% lookup_value(Constant,Store,Value).
407		generate_bindings(_Constants,Store,ConstantsBinding) :-
408		% TODO: review this
409		Store = ConstantsBinding.
410
411		save_values_into_file(Name,CompParams,ConstantBindings,MaxReached) :-
412		storage_file_name(constants,Name,Filename),
413		open(Filename,write,S,[type(binary)]),
414		call_cleanup(save_values_into_file2(S,CompParams,ConstantBindings,MaxReached),
415		my_close(S)).
416		save_values_into_file2(S,CompParams,ConstantBindings,MaxReached) :-
417		fast_write(S,comp_parameters(CompParams)),
418		fast_write(S,maximum_reached(MaxReached)),
419		maplist(write_bind(S,constants),ConstantBindings),
420		fast_write(S,end_of_file).
421		write_bind(S,Type,Store) :-
422		preferences:get_preference(use_state_packing,PREF),
423		preferences:set_preference(use_state_packing,false),
424		state_packing:pack_values(Store,PS), % does not seem to bring major performance benefit; but reduces file size
425		% print(packed(Store,PS)),nl,
426		preferences:set_preference(use_state_packing,PREF),
427		fast_write(S,values(Type,PS)).
428		% fast_write(S,values(Type)), fast_write_list(PS,S). % should we do something like this to reduce memory consumption ?
429
430		%fast_write_list([],S) :- fast_write(S,end_of_list).
431		%fast_write_list('$bind_var'(Var,Val,T),S) :- fast_write(S,bind(Var,Val)), fast_write_list(T,S).
432
433		/* compute the full file name for the stored constants for the machine
434		the predicate uses the specified directory where constants values
435		should be stored */
436		storage_file_name(Type,MachineName,FullName) :-
437		cache_file_suffix(Type,Suffix),!,
438		storage_directory(Directory),
439		atom_concat(MachineName,Suffix,Name),
440		atom_concat(Directory,Name,FullName).
441		storage_file_name(Type,MachineName,_) :-
442		add_internal_error('Illegal cache file type: ',storage_file_name(Type,MachineName,_)),fail.
443
444		cache_file_suffix(constants,'.probcst').
445		cache_file_suffix(operations_index,'.probops').
446		cache_file_suffix(operations_data,'.opdata').
447
448		cache_file_type(constants).
449		cache_file_type(operations_index).
450
451		/**********************************************************************/
452		/* load constants */
453		/**********************************************************************/
454
455		% a predicate to see which constant values have been saved
456		tcltk_load_constants(list(CS)) :-
457		load_constants(ConstantsStores,_),
458		maplist(translate:translate_bstate,ConstantsStores,CS).
459
460
461		/* load_constants/2 returns a list of stores if the constants have been
462		saved before for the same computation parameters.
463		The predicate fails if no constants can be loaded.
464		MaxReached is 'true' if the maximum number of computed solutions was reached
465		or 'false' otherwise.
466		*/
467
468		:- dynamic constants_loaded_from_file/1.
469		:- volatile constants_loaded_from_file/1.
470		% load constants for main machine
471		load_constants(ConstantStores,MaxReached) :-
472		cache_is_applicable_for_constants, % check if storing/re-using constants is activated
473		main_machine_name(Name),
474		machine_constants_cache_file_exists(Name,FullName),
475		open(FullName,read,S,[type(binary)]),
476		call_cleanup(load_constants2(S,Name,ConstantStores,MaxReached),
477		my_close(S)),!.
478		load_constants2(S,Name,ConstantStores,MaxReached) :-
479		load_parameters(S,StoredParameters), % if the relevant computation parameters
480		collect_computation_parameters(Name,CurrentParameters), % are different, we cannot re-use the
481		(compare_computation_parameters(StoredParameters,CurrentParameters) % values stored in the file
482		-> true
483		; formatinfo('value caching: parameters changed; not reusing previously computed constants for ~w.',[Name]),
484		fail
485		),
486		load_max_reached(S,MaxReached),
487		load_constant_values(S,ConstantStores),
488		bb_inc(value_persistance_constants_loaded),
489		(debug_mode(off)
490		-> formatgood('value caching: re-using stored solutions for constants for ~w.', [Name])
491		; length(ConstantStores,Len),
492		get_ids(ConstantStores,CstNames),
493		formatgood('value caching: re-using ~w stored solutions for constants ~w for ~w.',
494		[Len,CstNames,Name])
495		),
496		assert_once( constants_loaded_from_file(Name) ).
497
498
499		machine_constants_cache_file_exists(Name,FullName) :-
500		cache_file_exists(constants,Name,FullName).
501		cache_file_exists(Type,Name,FullName) :-
502		storage_file_name(Type,Name,FullName),
503		(file_exists(FullName)
504		-> debug_format(19,'value caching: ~w cache file ~w exists for ~w.~n',[Type, FullName, Name])
505		; get_tail_filename(FullName,Tail),
506		formatinfo('value caching: ~w cache file ~w does not yet exist for ~w.',[Type, Tail, Name]),
507		fail
508		).
509
510		load_parameters(S,StoredParameters) :-
511		safe_constants_read(S,comp_parameters(StoredParameters)).
512
513		load_max_reached(S,MR) :-
514		safe_constants_read(S,maximum_reached(MR)).
515
516		load_constant_values(S,Stores) :-
517		safe_constants_read(S,Term),
518		( Term = end_of_file ->
519		Stores = []
520		; Term = values(constants,Store) ->
521		unpack_constants(Store,UPS),
522		Stores = [UPS|Rest],
523		load_constant_values(S,Rest)).
524
525		unpack_constants(Store,UPS) :-
526		preferences:get_preference(use_state_packing,PREF),
527		preferences:set_preference(use_state_packing,false),
528		state_packing:unpack_values(Store,UPS),
529		% print(unpacked(Store,UPS)),nl,
530		preferences:set_preference(use_state_packing,PREF).
531
532		safe_constants_read(S,Term) :-
533		read_syntax_safe(S,T,Error),
534		( Error==true ->
535		write('Invalid cache file content. File skipped.\n'),
536		fail
537		;
538		Term = T).
539
540		% load constant solutions from subsidiary referenced machines
541		load_partial_constants(ConstantsBindings,InProperties,OutProperties) :-
542		% TODO: - check if parameters / constraints have been used (what are the implications?)
543		cache_is_applicable_for_constants, % check if storing/re-using constants is activated
544		main_machine_name(Name),
545		findall( partial(MName,NewBindings),
546		try_to_reuse_referenced_machine(Name,MName,NewBindings),
547		PSol),
548		PSol = [_|_],!,
549		remove_evaluated_properties(PSol,InProperties,OutProperties),
550	?	select_and_apply_binding(PSol,ConstantsBindings).
551		load_partial_constants(_ConstantsBindings,Properties,Properties).
552
553		/**********************************************************************/
554
555		:- meta_predicate open_cache_file(+,+,-,0).
556		open_cache_file(Type,Name,Stream,Call) :-
557		cache_file_exists(Type,Name,FullName),
558		my_open(FullName,read,Stream,[type(binary)]),
559		debug_format(19,'Opened cache file ~w~n',[FullName]),
560		call_cleanup( (call(Call),!),my_close(Stream)).
561
562		/**********************************************************************/
563
564		:- dynamic referenced_machine/1.
565
566		:- mode try_to_reuse_referenced_machine(+,-,-).
567		try_to_reuse_referenced_machine(OrigName,Name,Bindings) :-
568		retractall(referenced_machine(_)),
569		try_to_reuse_referenced_machine1(OrigName,Name,Bindings).
570		try_to_reuse_referenced_machine1(OrigName,Name,Bindings) :-
571		referenced_machine_with_constants_or_properties(OrigName,RefName),
572		(referenced_machine(RefName) -> fail ; true), % we have already processed it
573		assert(referenced_machine(RefName)),
574		try_to_reuse_referenced_machine2(OrigName,RefName,Name,Bindings).
575		try_to_reuse_referenced_machine2(OrigName,RefName,Name,Bindings) :-
576		% try to re-use values of a machine directly referenced by OrigName that
577		% contains constants
578		open_cache_file(constants,RefName,S,try_load_ref_values2(RefName,OrigName,S,Bindings1)),
579		!,
580		RefName = Name,
581		Bindings1 = Bindings.
582		try_to_reuse_referenced_machine2(_,RefName,Name,Bindings) :-
583		% using the directly referenced machine failed, using a machine
584		% that is referenced by the referenced machine
585		try_to_reuse_referenced_machine1(RefName,Name,Bindings).
586
587		try_load_ref_values2(RefName,OrigName,S,Bindings) :-
588		check_if_machine_has_no_parameters(RefName),
589		load_parameters(S,StoredParameters),
590		check_if_all_constants_computed(RefName,S),
591		collect_computation_parameters(RefName,CurrentParameters),
592		compare_computation_parameters(StoredParameters,CurrentParameters),
593		load_constant_values(S,Bindings),
594		bb_inc(value_persistance_ref_constants_loaded),
595		(debug_mode(off)
596		-> formatgood('value caching: re-using stored solutions for constants for referenced machine ~w.', [RefName])
597		; length(Bindings,Len),
598		get_ids(Bindings,CstNames),
599		formatgood('value caching: re-using ~w previously computed solutions for constants ~w of referenced machine ~w within ~w.',[Len,CstNames,RefName,OrigName])
600		% TODO: show names of constants ...
601		).
602
603		get_name(bind(ID,_),ID) :- !.
604		get_name(X,X).
605
606		get_ids([Binding|_],Names) :- maplist(get_name,Binding,Names).
607
608		check_if_machine_has_no_parameters(RefName) :-
609		machine_identifiers(RefName,Params,_Sets,_AVars,_CVars,_AConsts,_CConsts),
610		( Params=[] -> true
611		;
612		formatwarn('value caching: constants of referenced machine ~w are not used because it uses parameters',[Params]),
613		fail).
614
615		compare_computation_parameters([],[]) :- !.
616		compare_computation_parameters([CH|CT],[SH|ST]) :-
617		!,compare_computation_parameters(CH,SH),
618		compare_computation_parameters(CT,ST).
619		compare_computation_parameters(op_comp_parameters(C),op_comp_parameters(S)) :- !,
620		compare_computation_parameters(C,S).
621		compare_computation_parameters(C,C) :- !.
622		compare_computation_parameters(C,S) :-
623		formatwarn('value caching: parameter difference:~ncurrent is ~w,~n stored is ~w.',[C,S]),
624		fail.
625
626		check_if_all_constants_computed(_RefName,S) :-
627		% make sure that all solutions have been generated
628		load_max_reached(S,false),!.
629		check_if_all_constants_computed(RefName,_S) :-
630		formatwarn('value caching: constants for referenced machine ~w not used because not all solutions were computed.',[RefName]),
631		fail.
632
633		select_and_apply_binding(Solutions,Store) :-
634	?	maplist(select_solutions,Solutions,Bindings),
635		maplist(select_and_apply_binding2(Store),Bindings).
636		select_and_apply_binding2(Store,Binding) :-
637		maplist(apply_binding(Store),Binding).
638		apply_binding(Store,bind(Id,Value)) :-
639		lookup_value(Id,Store,SValue),
640		equal_object(SValue,Value).
641		select_solutions(partial(_Name,Bindings),Binding) :-
642	?	member(Binding,Bindings).
643
644		:- use_module(bmachine,[get_machine_file_number/4]).
645		machine_file_number(Name,Nr) :-
646		get_machine_file_number(Name,Ext,Nr,_),
647		Ext \= 'def',!.
648		machine_file_number(Name,Nr) :-
649		add_error(value_persistance,'Could not find machine name:',Name),
650		bmachine:portray_filenumbers,
651		Nr = -99.
652
653		:- use_module(tools_positions, [get_position_filenumber/2]).
654		% remove the properties from those machines whose constants have already been set from file
655		remove_evaluated_properties(PSol,InProperties,OutProperties) :-
656		findall(Name,member(partial(Name,_),PSol),UnsortedNames),
657		sort(UnsortedNames,Names),
658		maplist(machine_file_number,Names,FileNumbers),
659		debug_println(9,filtering(Names,FileNumbers)),
660		conjunction_to_list(InProperties,InAsList),
661		% exclude all properties who are in one of the files for which we have restored (all) constant values
662		exclude(belongs_to_file(FileNumbers),InAsList,OutAsList), % this is exclude/3 from library(lists)
663		conjunct_predicates(OutAsList,OutProperties).
664		belongs_to_file(FileNumbers,TPred) :-
665		get_texpr_info(TPred,Info),
666		memberchk(nodeid(Pos),Info),
667		get_position_filenumber(Pos,FilePos),
668		memberchk(FilePos,FileNumbers).
669
670		/**********************************************************************/
671
672		:- dynamic loadable_operation/5, storable_operation/4, stored_transition/4, operation_has_stored_transition/1,
673		operations_index_file_opened/2.
674		:- volatile loadable_operation/5, storable_operation/4, stored_transition/4, operation_has_stored_transition/1,
675		operations_index_file_opened/2.
676
677		initialise_operation_caching :-
678		clear_applicable_flag,
679		cache_is_applicable_for_transitions,
680		main_machine_name(MachName), % if we have no machine name, fail silently (for default machine)
681		!,
682		% check wich operations are cachable and prepare information for them
683		debug_println(9,initialise_operation_caching(MachName)),
684		retract_all_op_cache_data,
685		try_to_load_operations_cache_for_all_machines,
686		%initialise_op_cache_for_machine(MachName),
687		find_loadable_machines(LoadableMachines),
688		formatinfo('value caching: loadable machines: ~w',[LoadableMachines]),
689		maplist(initialise_op_cache_for_machine,LoadableMachines).
690		initialise_operation_caching :-
691		retract_all_op_cache_data.
692
693		initialise_op_cache_for_machine(loadable(_,MachName)) :-
694		bb_inc(value_persistance_op_cache_machines),
695		get_operation_names(MachName,OperationNames),
696		maplist(init_operation_cache(MachName),OperationNames),
697		save_operations_index_cache(MachName,OperationNames),
698		open_data_file(MachName).
699
700		:- use_module(eventhandling,[register_event_listener/3]).
701		:- register_event_listener(specification_initialised,initialise_operation_caching,
702		'Initialise operation caching info.').
703
704
705		retract_all_op_cache_data :-
706		retractall(constants_loaded_from_file(_)),
707		retractall(loadable_operation(_,_,_,_,_)),
708		retractall(storable_operation(_,_,_,_)),
709		retractall(stored_transition(_,_,_,_)),
710		retractall(operation_has_stored_transition(_)),
711		retractall(cst_id_to_hash(_,_)),
712		retractall(constant_pre_hash_cache_active),
713		reset_operations_index_file_opened.
714
715		% operations_index_file_opened(Stream) contains a possibly open stream for the operations (probops) file
716		reset_operations_index_file_opened :-
717	?	( operations_index_file_opened(M,S) ->
718		my_close(S),retractall(operations_index_file_opened(M,_)),
719		reset_operations_index_file_opened
720		; true).
721
722		get_operation_names(MachName,OperationNames) :-
723		if(machine_operations(MachName,RawOperationNames),
724		maplist(get_raw_identifier,RawOperationNames,OperationNames),
725		add_error_fail(value_persistance,'Cannot find machine:',MachName)).
726
727		try_to_load_operations_cache_for_all_machines :-
728		find_loadable_machines(LoadableMachines),
729		maplist(try_to_load_operations_cache,LoadableMachines).
730
731		try_to_load_operations_cache(loadable(Type,MachName)) :-
732		formatinfo('value caching: try loading cached operations for machine ~w (~w)',[MachName,Type]),
733		get_operations_computation_parameters(MachName,OpParams),
734		open_cache_file(operations_index,MachName,S,read_cached_operations(S,MachName,OpParams,Error)),!,
735		( Error==true ->
736		formatwarn('value caching: corrupted index file for machine ~w, deleting file.',[MachName]),
737		delete_cache_file(MachName)
738		; true).
739		try_to_load_operations_cache(loadable(main,MachName)) :-
740		% delete the data file if one exists -- only for main machine
741		delete_cache_file(MachName),!.
742		try_to_load_operations_cache(_Loadable).
743
744		delete_cache_file(MachName) :-
745		cache_file_exists(operations_data,MachName,Filename),!,
746		formatinfo('value caching: deleting opdata cache file of machine ~w: ~w',[MachName,Filename]),
747		delete_file(Filename).
748
749		read_cached_operations(S,MachName,CurrentOpParams,SyntaxError) :-
750		read_syntax_safe(S,StoredOpParams,SyntaxError),
751		( SyntaxError==true -> true
752		; compare_computation_parameters(StoredOpParams,CurrentOpParams) ->
753		formatgood('value caching: parameters unchanged, re-use of stored operations possible for ~w',[MachName]),
754		read_cached_operations2(S,MachName,SyntaxError)
755		;
756		formatwarn('value caching: general computations parameters have changed, no re-use of stored operations',[]),
757		debug_params(CurrentOpParams,StoredOpParams),
758		fail).
759		read_cached_operations2(S,MachName,SyntaxError) :-
760		read_syntax_safe(S,Term,SyntaxError),
761		( SyntaxError==true -> true
762		; Term == end_of_file -> true
763		; read_cached_operations3(Term,MachName) ->
764		read_cached_operations2(S,MachName,SyntaxError)
765		;
766		functor(Term,F,A),
767		formatwarn('value caching: unrecognised entry in cache file for ~w: ~w/~w~n',[MachName,F,A]),
768		fail
769		).
770		debug_params(op_comp_parameters(A),op_comp_parameters(B)) :- !,
771		debug_params(A,B).
772		debug_params(preference(P,A),preference(P,B)) :- !,
773		(A=B -> true ; print(P), print(':'), print(A/B), print(' ')).
774		debug_params([],[]) :- !,nl.
775		debug_params([preference(P1,A)|CT],[preference(P2,B)|ST]) :- !,
776		(P1=P2 -> (A=B -> true ; format('Difference in preference ~w : current = ~w, stored = ~w~n',[P1,A,B])),
777		debug_params(CT,ST)
778		; P1 @< P2 -> format('New preference ~w = ~w (not stored)~n',[P1,A]), debug_params(CT,[preference(P2,B)|ST])
779		; format('Stored preference removed ~w = ~w~n',[P2,B]), debug_params([preference(P1,A)|CT],ST)
780		).
781		debug_params([Cur|CT],[Stored|ST]) :- !,
782		debug_params(Cur,Stored),
783		debug_params(CT,ST).
784		debug_params(A,B) :- (A=B -> true ; print(A/B),nl).
785
786		% -----------------
787
788		% a way to clean/delete all cache files for current machine; useful for tests
789		delete_cache_files :-
790		reset_operations_index_file_opened, % to ensure we can delete the files
791		find_loadable_machines(LoadableMachines),
792		maplist(delete_cache_files_for_machine(_),LoadableMachines).
793
794		% delete a single cache file only
795		delete_cache_files_for_machine(Machine) :-
796		reset_operations_index_file_opened, % to ensure we can delete the files
797		delete_cache_files_for_machine(_,loadable(main,Machine)).
798
799		delete_cache_files_for_machine(ExpectedType,loadable(_MType,MachName)) :-
800	?	cache_file_suffix(Type,_), % backtracks and also matches operations_data
801		(var(ExpectedType) -> true ; ExpectedType=Type),
802		(cache_file_exists(Type,MachName,FullName)
803		-> get_tail_filename(FullName,FF),
804		format_with_colour_nl(user_output,[blue],'Deleting ~w cache file for machine ~w: ~w',[Type,MachName,FF]),
805		delete_file(FullName)
806		; format_with_colour_nl(user_output,[blue],'No cache file of type ~w found for machine ~w',[Type,MachName])
807		),fail.
808		delete_cache_files_for_machine(_,_).
809
810		:- meta_predicate show_cache_file_contents_for_machine(-,0,-,-).
811		% a small utility to print out the contents of the cache files:
812
813		% called by -show_cache and -show_cache_verbose commands of probcli
814		show_cache_file_contents(Verbose) :-
815		(storage_directory(Dir) -> true ; Dir='?'),
816		format_with_colour_nl(user_output,[blue],'Cache contents (directory: ~w)',[Dir]),
817		reset_operations_index_file_opened, % otherwise on Windows we are not able to open the probobs file as it is already open
818		show_cache_file_operations(Verbose).
819
820
821		show_cache_file_operations(Verbose) :-
822		reset_operations_index_file_opened, % otherwise on Windows we are not able to open the probobs file as it is already open
823		find_loadable_machines(LoadableMachines),
824		maplist(show_cache_file_contents_for_machine(_,show_facts(S,Verbose),S),LoadableMachines).
825
826		cache_applicable(operations) :- !, cache_is_applicable_for_transitions.
827		cache_applicable(constants) :- !, cache_is_applicable_for_constants.
828		cache_applicable(_) :- cache_is_applicable.
829
830		:- use_module(tools,[get_tail_filename/2]).
831		show_cache_file_contents_for_machine(ExpectedType,Call,Stream,loadable(_MType,MachName)) :-
832	?	cache_file_type(Type), % backtracks
833		(var(ExpectedType) -> true ; ExpectedType=Type),
834		(cache_file_exists(Type,MachName,FullName) ->
835		get_tail_filename(FullName,FF),
836		format_with_colour_nl(user_output,[blue],'Contents of ~w cache file for machine ~w: ~w',[Type,MachName,FF]),
837		(cache_applicable(Type) -> true
838		; format_with_colour_nl(user_output,[blue],' (Cache not applicable for ~w)',[Type])),
839		(open_cache_file(Type,MachName,Stream,Call)
840		-> format_with_colour_nl(user_output,[blue],'End of contents (~w)',[FF])
841		; format_with_colour_nl(user_error,[red],'Failed to show cache contents of ~w.',[FF])
842		)
843		; \+ cache_applicable(Type) -> true
844		; Type=operations_index, machine_operations(MachName,_)
845		-> format_with_colour_nl(user_output,[blue],'No cache file of type ~w for machine with operations ~w.~n',[Type,MachName])
846		; Type=constants, machine_has_constants(MachName)
847		-> format_with_colour_nl(user_output,[blue],'No cache file of type ~w for machine with constants ~w.~n',[Type,MachName])
848		; debug_format(19,'No cache file of type ~w for machine ~w.~n',[Type,MachName]) % TODO: check if MachName has constants,...
849		),
850		fail.
851		show_cache_file_contents_for_machine(_,_,_,_).
852
853		show_facts(S,Verbose) :- read_syntax_safe(S,Term,Error),
854		(nonvar(Error)
855		-> add_error(value_persistance,'Error occured reading cache stream: ',S)
856		; Term = end_of_file -> reset_and_show_stats
857		; portray_content_fact(Term,Verbose),
858		show_facts(S,Verbose)).
859
860		:- use_module(tools_strings,[get_hex_bytes/2]).
861		:- use_module(translate,[print_bstate/1]).
862		% operations:
863		portray_content_fact(op_comp_parameters(OpParams),Verbose) :- OpParams=[H|_], !,
864		format_verbose(Verbose,' op_comp_parameters([~w,...]).~n',[H]).
865		portray_content_fact(operation(OpName,Hash),_) :- get_hex_bytes(Hash,Hex), !,
866		format(' operation(~w,~s).~n',[OpName,Hex]).
867		portray_content_fact(trans_index(OpName,Hash,Index),Verbose) :- get_hex_bytes(Hash,Hex), !,
868		format_verbose(Verbose,' transition(~w,~s,~w).~n',[OpName,Hex,Index]),
869		inc_counter(OpName).
870		% constants:
871		portray_content_fact(comp_parameters(OpParams),Verbose) :- OpParams=[H|_], !,
872		format_verbose(Verbose,' comp_parameters([~w,...]).~n',[H]).
873		portray_content_fact(maximum_reached(MaxReached),Verbose) :- !,
874		format_verbose(Verbose,' maximum_reached(~w).~n',[MaxReached]),
875		(MaxReached=true -> inc_counter(maximum_reached) ; true).
876		portray_content_fact(values(constants,Store),_Verbose) :- !,
877		unpack_constants(Store,UPS),
878		print_bstate(UPS),nl.
879		portray_content_fact(Term,_) :- portray_clause(Term).
880
881		format_verbose(verbose,Str,A) :- !, format(Str,A).
882		format_verbose(_,_,_).
883
884
885		:- dynamic counter/2.
886		reset_and_show_stats :- retract(counter(C,Nr)), format(' # of ~w : ~w~n',[C,Nr]),fail.
887		reset_and_show_stats.
888
889		inc_counter(C) :- (retract(counter(C,Nr)) -> N1 is Nr+1 ; N1 = 1),
890		assertz(counter(C,N1)).
891
892		:- use_module(error_manager).
893		% variation of tools_fastread:fastrw_read/3
894		read_syntax_safe(S,Term,Error) :-
895		catch( fast_read(S,Term1), % from library fastrw
896		error(E,_),
897		( E=syntax_error(_) -> Error = true
898		; E=permission_error(_,_,_) -> Term1 = end_of_file
899		; E=consistency_error(_,_,_)
900		-> add_error(value_persistance,'Consistency error when reading from stream: ',E),
901		Error = true
902		;
903		add_error(value_persistance,'Unknown error when reading from stream: ',E),
904		throw(E))
905		),
906		Term1 = Term.
907
908
909		read_cached_operations3(operation(OpName,StoredHash),MachName) :-
910		( operation_hash(MachName,OpName,CurrentHash) ->
911		( CurrentHash = StoredHash % we can reuse operation; the hash includes DEFINITIONS and called operations
912		->
913		formatgood('value caching: operation ~w unchanged for ~w.',[OpName,MachName]),
914		%TODO: what if the machine has parameters? Can we reuse the transitions from the generic machine?
915		find_matching_operations(OpName,MachName,PrefixedOpNames), % find includes with renaming, ...
916		( PrefixedOpNames = [] ->
917		formatwarn('value caching: no operation found for ~w in ~w', [OpName,MachName])
918		;
919		(PrefixedOpNames = [OpName] -> true
920		; formatinfo('value caching: (composed/renamed) operations ~w found for ~w in ~w',
921		[PrefixedOpNames,OpName,MachName])
922		),
923		maplist(store_loadable_operation(OpName,MachName),PrefixedOpNames) )
924		;
925		get_hex_bytes(CurrentHash,CH), get_hex_bytes(StoredHash,SH),
926		formatwarn('value caching: operation ~w has changed (~s, was ~s).',[OpName, CH, SH])
927		)
928		;
929		formatwarn('value caching: unrecognised operation ~w.',[OpName])
930		).
931		read_cached_operations3(trans_index(OpName,Hash,Index),MachName) :-
932		( loadable_operation(_,OpName,MachName,_InputPattern,_OutputPattern) ->
933		compute_short_hash(Hash,Short),
934		formatinfo('value caching: loading stored_transition ~w (~w) : hash ~w',[OpName,Index,Short]),
935		assert_stored_transition(Short,Hash,OpName,Index)
936		;
937		% ignore
938		true
939		).
940
941		store_loadable_operation(_OpName,_MachName,PrefixedOpName) :-
942		loadable_operation(PrefixedOpName,_,_,_,_),!.
943		store_loadable_operation(OpName,MachName,PrefixedOpName) :-
944		(find_operation_input_output(PrefixedOpName,Input,Output) ->
945		create_output_pattern(Output,OutputPattern),
946		lookup_pattern(Input,InputPattern)),
947		!,
948		bb_inc(value_persistance_loadable_operations),
949		formatinfo('value caching: register loadable_operation from cache: ~w in ~w',[OpName,MachName]),
950		assertz( loadable_operation(PrefixedOpName,OpName,MachName,InputPattern,OutputPattern) ).
951		store_loadable_operation(_OpName,_MachName,PrefixedOpName) :-
952		formatwarn('value caching: unable to generate input/output pattern for operation ~w.',
953		[PrefixedOpName]).
954
955		find_matching_operations(Operation,MachName,FullNames) :-
956		findall(O, is_matching_operation(Operation,MachName,O), FullNames).
957
958		is_matching_operation(Operation,MachName,Operation) :-
959		% there is an operation with exactly the same name
960		operation_with_machine(Operation,MachName).
961		is_matching_operation(Operation,MachName,FullName) :-
962		atom_concat('.',Operation,DottedOp),
963	?	operation_with_machine(FullName,MachName),
964		atom_concat(_,DottedOp,FullName).
965
966		operation_with_machine(OpName,MachName) :-
967	?	get_operation_info(OpName,Infos),
968		( memberchk(origin(Origin),Infos), % for c1.Inc the origin will be the included machine
969		last(Origin,_/MachName) -> true
970		; main_machine_name(MachName)
971		).
972
973		create_output_pattern(Ids,Values/Bindings) :-
974		maplist(create_output_pattern2,Ids,Values,Bindings).
975		create_output_pattern2(Id,Value,bind(Id,Value)).
976
977		init_operation_cache(MachName,OpName) :-
978		storable_operation(OpName,MachName,_InputPattern,_Output),!. % ignore, already registered
979		init_operation_cache(MachName,OpName) :-
980		\+ b_top_level_operation(OpName), !,
981		% only store top-level operations for which we compute all solutions at the moment
982		% for subsidiary operations we do a call by predicate; much more difficult to cache/store
983		formatinfo('value caching: Not storing subsidiary operation ~w in machine ~w',[OpName,MachName]).
984		init_operation_cache(MachName,OpName) :-
985		( find_operation_input_output(OpName,Input,Output) ->
986		lookup_pattern(Input,InputPattern),
987		debug_println(9,find_operation_input_output(OpName,Input,Output)),
988		formatinfo('value caching: Storable operation ~w in machine ~w',[OpName,MachName]),
989		bb_inc(value_persistance_storeable_operations),
990		assertz( storable_operation(OpName,MachName,InputPattern,Output) ),
991		% Operations of the main machine are never prefixed
992		create_output_pattern(Output,OutputPattern),
993		(loadable_operation(OpName,_,_,_,_) -> true
994		; bb_inc(value_persistance_loadable_operations), % see also store_loadable_operation
995		assertz( loadable_operation(OpName,OpName,MachName,InputPattern,OutputPattern) )
996		)
997		;
998		formatwarn('value caching: unable to generate input/output pattern for operation ~w.~n',[OpName])
999		).
1000
1001
1002		get_operations_computation_parameters(Name,op_comp_parameters(OpParams)) :-
1003		find_relevant_preferences(Prefs),
1004		get_revision_info(Revision),
1005		OpParams = [machine_name(Name),prob_revision(Revision)|Prefs].
1006
1007		lookup_cached_transitions(PrefixedOpName,InState,Info,OutputBindings) :-
1008		cache_is_applicable_for_transitions,
1009		loadable_operation(PrefixedOpName,OpName,MachName,InputPattern,OutputPattern),
1010		operation_has_stored_transition(OpName), % otherwise no use in computing hash here
1011		sort(InState,SortedInState),
1012		% tools:start_ms_timer(T1),
1013		hash_input_values(OpName,MachName,InputPattern,SortedInState,ShortHash,InputHash),
1014		% tools:stop_ms_walltimer_with_msg(T1,hash_input(OpName)),
1015		(stored_transition(ShortHash,InputHash,OpName,Index) -> true
1016		; %formatwarn('value caching: no cached operation transition found ~w (~w -> ...).',[OpName,ShortHash]),
1017		fail
1018		), !,
1019		formatgood('value caching: re-using values for operation ~w (~w -> ~w).',[OpName,ShortHash,Index]),
1020		%formatdetails('value caching: state=~w',[SortedInState]),
1021		start_profile(OpName,T1),
1022		( load_solutions(MachName,Index,Info,Solutions) -> true
1023		%length(Solutions,Sn),
1024		%format('value caching: re-using ~w solutions for operation ~w of machine ~w.~n',
1025		% [Sn,OpName,MachName])
1026		;
1027		formatwarn('value caching: re-using values for operation ~w failed.',[OpName]),
1028		fail),
1029		%print(solution(Solutions)),nl, print(pattern(OutputPattern)),nl,
1030		% OutputPattern is of the form [V1,...]/[bind(v1,V1),...]
1031		bb_inc(value_persistance_reused_transitions),
1032		maplist(create_output_binding(OutputPattern),Solutions,OutputBindings),
1033		%tools:stop_ms_walltimer_with_msg(T1,time_caching(OpName)),
1034		stop_profile(OpName,cache_load_transitions,unknown,T1).
1035		load_solutions(MachName,Index,Info,Solutions) :-
1036		storage_file_name(operations_data,MachName,FilenameData),
1037		catch(load_sol_aux(FilenameData,Index,ReadSolutions),
1038		Exc,
1039		(ajoin(['Corrupt opdata cache file for ',MachName,':'],Msg),
1040		add_error_fail(value_persistance,Msg,Exc))
1041		),
1042		(ReadSolutions = trans_info(II,S) -> Solutions=S, Info=II ; Solutions=ReadSolutions, Info=[]).
1043		load_sol_aux(FilenameData,Index,Solutions) :-
1044		open(FilenameData,read,S,[type(binary),reposition(true)]),
1045		call_cleanup((seek(S,Index,bof,_),
1046		fast_read(S,Solutions)), % read list of transition terms
1047		my_close(S)).
1048
1049		create_output_binding(Pattern,trans_cached(Param,Result,New,Info),
1050		trans_cached(Param,Result,Update,Info)) :-
1051		copy_term(Pattern,New/Update).
1052
1053		select_values(Ids,State,Values) :- sort(State,SState),
1054		select_values_sorted(Ids,SState,Values).
1055		% Note: as Identifiers are sorted then we can avoid quadratic complexity here and scan State only once for all Ids
1056		select_values_sorted(Ids,SState,Values) :-
1057		(select_values_sorted_aux(Ids,SState,Values) -> true
1058		; print('Lookup: '),print(Ids), nl,
1059		print('State: '), maplist(get_bind_id,SState,SIds), print(SIds),nl,fail).
1060		select_values_sorted_aux([],_,[]).
1061		select_values_sorted_aux([Id|Irest],State,[Value|Vrest]) :-
1062	?	( ordered_select(State,Id,StoredValue,RestState) ->
1063		Value=StoredValue,
1064		select_values_sorted_aux(Irest,RestState,Vrest)
1065		;
1066		ajoin(['Looking up "', Id, '" failed.'], Msg),
1067		(maplist(get_bind_id,State,Ids) -> true ; Ids = '<<cannot print state ids>>'),
1068		add_error(value_persistance,Msg,Ids),
1069		fail
1070		).
1071		ordered_select([bind(Id,Value)|T],Id,Value,T).
1072	?	ordered_select([_|T],Id,Value,R) :- ordered_select(T,Id,Value,R).
1073		get_bind_id(bind(Id,_),Id).
1074
1075		hash_input_values(OpName,MachName,InputPattern,SortedInState,Short,Long) :-
1076		% tools:start_ms_timer(T1),
1077		% write(hash(OpName,MachName,InputPattern,SortedInState)),nl,
1078		( hash_input_values2(OpName,MachName,InputPattern,SortedInState,Short,Long) ->
1079		true
1080		%,tools:stop_ms_walltimer_with_msg(T1,time_hashing(OpName,MachName))
1081		% tools:print_memory_used_wo_gc,
1082		; add_failed_call_error(hash_input_values2(OpName,MachName,InputPattern,SortedInState,Short,Long)),
1083		fail).
1084
1085		hash_input_values2(OpName,MachName,InputPattern,SortedInState,Short,Long) :-
1086		start_profile(OpName,T1),
1087		copy_term(InputPattern,lookup_pattern(SortedVars,SortedInputValues,InputVarsAndCsts,InputValues)),
1088		select_values_sorted(SortedVars,SortedInState,SortedInputValues),
1089		l_pre_hash(InputVarsAndCsts,InputValues,PreHashedInputValues),
1090		% terms:term_size(PreHashedInputValues,Sz), write(hash(OpName,SortedVars,Sz)),nl,
1091		% tools_printing:print_term_summary(raw_sha_hash(OpName,PreHashedInputValues)),nl,
1092		raw_sha_hash(OpName/MachName/PreHashedInputValues,Long),
1093		compute_short_hash(Long,Short),
1094		stop_profile(OpName,cache_hashing_input_values,unknown,T1).
1095		compute_short_hash([A,B,C,D|_],Short) :-
1096		Short is A<<24 + B<<16 + C<<8 + D.
1097
1098		% pre-hash certain potentially large values, so that we do not have to send them to raw_sha_hash every time
1099		l_pre_hash([],[],[]).
1100		l_pre_hash([ID|T],[Val|TV],[PreHashVal|PT]) :-
1101		pre_hash(Val,ID,PreHashVal),
1102		l_pre_hash(T,TV,PT).
1103
1104		:- dynamic constant_pre_hash_cache_active/0.
1105
1106		:- dynamic cst_id_to_hash/2.
1107		:- use_module(probsrc(memoization),[is_memoization_closure/2]).
1108		%pre_hash(Val,_ID,PreHashVal) :-
1109		% is_memoization_closure(Val,MemoID),!, %write(memo(ID,MemoID)),nl,
1110		% PreHashVal = '$MEMO'(MemoID).
1111		pre_hash(Val,CstId,PreHashVal) :- bmachine:b_is_constant(CstId),
1112		value_can_be_large(Val),!,
1113		(constant_pre_hash_cache_active
1114		-> (cst_id_to_hash(CstId,StoredHash)
1115		-> PreHashVal = StoredHash % used stored value
1116		; raw_sha_hash(Val,Hash),
1117		assert(cst_id_to_hash(CstId,Hash)),
1118		debug_println(4,storing_cache_hash_for_constant(CstId)),
1119		PreHashVal = Hash
1120		)
1121		; raw_sha_hash(Val,PreHashVal) % there can be multiple constant values active
1122		).
1123		pre_hash(V,_,V).
1124
1125		:- use_module(probsrc(avl_tools),[avl_height_less_than/2]).
1126		value_can_be_large(avl_set(A)) :- \+ avl_height_less_than(A,7).
1127		value_can_be_large(closure(_,_,_)).
1128		value_can_be_large((A,B)) :- value_can_be_large(A) -> true ; value_can_be_large(B).
1129		value_can_be_large(rec(Fields)) :- (member(field(_,V),Fields), value_can_be_large(V) -> true).
1130
1131		% TODO: separate constants from variables? or do full incremental hashing; by hashing all large sets first
1132		% we also could detect memoization closures and just store their id? or pre-compute their hash and store it?
1133
1134		% save operations_index file for machine
1135		save_operations_index_cache(MachName,OperationNames) :-
1136		get_operations_computation_parameters(MachName,OpParams),
1137		storage_file_name(operations_index,MachName,FileName),
1138		my_open(FileName,write,S,[type(binary)]),
1139		fast_write(S,OpParams),
1140		get_tail_filename(FileName,TailFileName),
1141		save_operation_info(S,TailFileName,MachName,OperationNames),
1142		my_close(S).
1143
1144		% is this really required: it seems to re-write already loaded information to the file; at least in some cases
1145		save_operation_info(S,FileName,MachName,OperationNames) :-
1146	?	member(OpName,OperationNames),
1147		storable_operation(OpName,MachName,_InputPattern,_Output),
1148		operation_hash(MachName,OpName,OpHash),
1149		fast_write(S,operation(OpName,OpHash)),
1150	?	stored_transition(_Short,InputHash,OpName,Index),
1151		formatinfo('value caching: storing/refreshing transition for ~w (index ~w) from ~w to ~w',[OpName,Index,MachName,FileName]),
1152		fast_write(S,trans_index(OpName,InputHash,Index)),
1153		bb_inc(value_persistance_refresh_transitions),
1154		fail.
1155		save_operation_info(_S,_F,_MachName,_OperationNames).
1156
1157		find_operation_input_output(OpName,Input,Output) :-
1158		get_operation_info(OpName,Info),
1159		memberchk(reads(Input1),Info),
1160		% remove references to global sets and their elements
1161		get_all_sets_and_enum_ids(SEIds),
1162		remove_all(Input1,SEIds,Input),
1163		memberchk(modifies(Output),Info).
1164
1165		get_all_sets_and_enum_ids(SEIds) :-
1166		findall(Id,
1167		( is_b_global_constant(_,_,Id)
1168		; b_global_set(Id)),
1169		SEIds).
1170
1171
1172
1173		% add new transitions from the state space
1174		add_new_transitions_to_cache(InStateId) :-
1175		cache_is_applicable_for_transitions,
1176		visited_expression(InStateId,InState1),
1177		state_corresponds_to_initialised_b_machine(InState1,InState),
1178		!,
1179		add_new_transitions_to_cache1(InStateId,InState).
1180		add_new_transitions_to_cache(_InStateId).
1181
1182		get_all_max_reached_operations(MaxReachedList) :-
1183		findall(OpName, max_reached(OpName), MaxReached),
1184		sort(MaxReached,MaxReachedList).
1185
1186		:- use_module(library(ordsets),[ord_member/2]).
1187
1188		add_new_transitions_to_cache1(InStateId,InState) :-
1189		get_all_max_reached_operations(MaxReachedList),
1190		%main_machine_name(MachName),
1191	?	storable_operation(OpName,MachName,InputPattern,Output),
1192		\+ time_out_for_node(InStateId,OpName,_),
1193		(ord_member(OpName,MaxReachedList) -> MaxReached=true ; MaxReached=false),
1194		sort(InState,SortedInState),
1195		add_new_transitions_to_cache2(InStateId,SortedInState,OpName,InputPattern,Output,MaxReached,MachName),
1196		fail.
1197		add_new_transitions_to_cache1(_InStateId,_) :-
1198		flush_data.
1199
1200		add_new_transitions_to_cache2(InStateId,SortedInState,OpName,InputPattern,Output,MaxReached,MachName) :-
1201		hash_input_values(OpName,MachName,InputPattern,SortedInState,ShortHash,InputHash),
1202		\+ stored_transition(ShortHash,InputHash,_,_), % Is there already a cache entry?
1203		find_all_transitions(InStateId,OpName,Output,Transitions),
1204		length(Transitions,Length),
1205		%format('value caching: storing ~w transitions for operation ~w in state ~w.~n',
1206		% [Length,OpName,InStateId]),
1207		%print(Transitions),nl,
1208		statistics(runtime,[Start,_]),
1209		statistics(walltime,[WStart,_]),
1210		store_transition_into_cache(OpName,ShortHash,InputHash,Transitions,MaxReached,MachName),
1211		statistics(runtime,[Stop,_]), Time is Stop - Start,
1212		statistics(walltime,[WStop,_]), WTime is WStop - WStart,
1213		%%tools:print_memory_used_wo_gc,
1214		bb_inc_by(value_persistance_stored_transitions,Length),
1215		formatinfo('value caching: storing ~w transitions for operation ~w in state ~w (~w, state ~w, [~w] ms).',
1216		[Length,OpName,InStateId,ShortHash,Time,WTime]).
1217
1218		store_transition_into_cache(OpName,ShortHash,Hash,Transitions,MaxReached,MachName) :-
1219		start_profile(OpName,T1),
1220		storage_file_name(operations_data,MachName,FilenameData),
1221		my_open(FilenameData,read,SR,[type(binary),reposition(true)]),
1222		call_cleanup(seek(SR,0,eof,Index), % gets the end of file
1223		my_close(SR)),
1224		%formatdetails('storing ~w (~w), EOF index is ~w for file ~w~n',[OpName,ShortHash,Index,FilenameData]),
1225		my_open(FilenameData,append,SW,[type(binary)]),
1226		(MaxReached = true -> Term = trans_info([max_reached],Transitions) ; Term=Transitions),
1227		call_cleanup(fast_write(SW,Term),
1228		my_close(SW)),
1229		assert_stored_transition(ShortHash,Hash,OpName,Index),
1230		get_operations_index_file(MachName,OI),
1231		fast_write(OI,trans_index(OpName,Hash,Index)),
1232		stop_profile(OpName,cache_store_transitions,unknown,T1).
1233
1234		assert_stored_transition(ShortHash,Hash,OpName,Index) :- store_operation_has_stored_transition(OpName),
1235		assertz( stored_transition(ShortHash,Hash,OpName,Index) ).
1236
1237		store_operation_has_stored_transition(X) :- operation_has_stored_transition(X),!.
1238		store_operation_has_stored_transition(X) :- assertz( operation_has_stored_transition(X) ).
1239
1240		find_all_transitions(InStateId,OpName,Output,Transitions) :-
1241		findall( trans_cached(ParaValues,ResultValues,Updates,TransInfo),
1242		find_transition(InStateId,OpName,Output,ParaValues,ResultValues,Updates,TransInfo),
1243		Transitions).
1244		find_transition(InStateId,OpName,Output,ParaValues,ResultValues,Updates,TransInfo) :-
1245	?	transition(InStateId,Operation,TransId,OutStateId),
1246		operation_name(Operation,OpName,ParaValues,ResultValues),
1247		findall(TI,transition_info(TransId,TI),TransInfo),
1248		visited_expression(OutStateId,OutState1), % we could use packed_visited_expression here ?
1249		state_corresponds_to_initialised_b_machine(OutState1,OutState),
1250		select_values(Output,OutState,Updates).
1251		operation_name('-->'(Operation,ResultValues),OpName,ParaValues,ResultValues) :-
1252		!,operation_name(Operation,OpName,ParaValues,_).
1253		operation_name(Operation,OpName,ParaValues,[]) :-
1254		Operation =.. [OpName|ParaValues].
1255
1256
1257		% add a single new transition, found by execute by predicate or -execute
1258		add_new_transition_to_cache_from_expanded_state(root,_OpTerm,OutState,_CacheInfo) :-
1259		OutState = concrete_constants(_),!,
1260		save_constants_from_expanded_state(OutState).
1261		add_new_transition_to_cache_from_expanded_state(InState,OpTerm,OutState,CacheInfo) :-
1262		cache_is_applicable_for_transitions,
1263		main_machine_name(MachName),
1264		operation_name(OpTerm,OpName,ParaValues,ResultValues),
1265		storable_operation(OpName,MachName,InputPattern,Output),
1266	?	\+ new_transition_not_worthwhile(CacheInfo,OpName),
1267		sort(InState,SortedInState),
1268		hash_input_values(OpName,MachName,InputPattern,SortedInState,ShortHash,InputHash), % can be expensive
1269		\+ stored_transition(ShortHash,InputHash,_,_), % Is there already a cache entry?
1270		!,
1271		MaxReached=true, % TODO: should we check that MAX_OPERATIONS is set to exactly 1
1272		TransInfo = [], % TODO: preference(eventtrace,true), preference(store_event_transinfo,true)
1273		Transitions = [trans_cached(ParaValues,ResultValues,Updates,TransInfo)],
1274		select_values(Output,OutState,Updates),
1275		bb_inc(value_persistance_stored_transitions),
1276		store_transition_into_cache(OpName,ShortHash,InputHash,Transitions,MaxReached,MachName),
1277		formatinfo('value caching: storing single transition for operation ~w in execute mode (~w).', [OpName,ShortHash]),
1278		flush_data.
1279		add_new_transition_to_cache_from_expanded_state(_,_,_,_).
1280
1281		% add_deadlock_to_cache_from_expanded_state(InState,OpName) % TODO: worthwhile to store failure info
1282
1283		start_cache_execute_modus(cache_info(StartRuntime,Counter)) :-
1284		statistics(runtime,[StartRuntime,_]),
1285		bb_safe_get(value_persistance_reused_transitions,Counter),
1286		(constant_pre_hash_cache_active -> true
1287		; assert(constant_pre_hash_cache_active)).
1288
1289		stop_cache_execute_modus :-
1290		retractall(constant_pre_hash_cache_active).
1291
1292		new_transition_not_worthwhile(cache_info(_,OldCounter),OpName) :-
1293		bb_safe_get(value_persistance_reused_transitions,Counter),
1294		Counter > OldCounter, % we cannot reuse subsidiary operation calls, so this must be the main operation itself
1295		formatinfo('value caching: not storing transition for ~w; it has been extracted from cache itself',[OpName]).
1296		new_transition_not_worthwhile(cache_info(StartRuntime,_),OpName) :-
1297		get_preference(cache_operations_runtime_limit,Limit), Limit>0,
1298		statistics(runtime,[CurrentTime,_]), Delta is CurrentTime-StartRuntime,
1299		Delta < Limit,
1300		bb_inc(value_persistance_not_worth_transitions),
1301		formatinfo('value caching: not storing transition for ~w, runtime (ms) ~w smaller than limit ~w',
1302		[OpName,Delta,Limit]).
1303
1304
1305
1306		% --------------------
1307
1308		open_data_file(Name) :-
1309		storage_file_name(operations_index,Name,FilenameIndex),
1310		my_open(FilenameIndex,append,FI,[type(binary)]),
1311		assertz(operations_index_file_opened(Name,FI)),
1312		storage_file_name(operations_data,Name,FilenameData),
1313		( file_exists(FilenameData) -> true
1314		;
1315		my_open(FilenameData,write,SD,[type(binary)]),
1316		my_close(SD)).
1317
1318		flush_data :-
1319		findall(M,(operations_index_file_opened(M,S),flush_output(S)),L),
1320		(L=[] -> add_internal_error('No index file opened',flush_data) ; true).
1321
1322		get_operations_index_file(Machine,OI) :-
1323		operations_index_file_opened(Machine,F),!,OI=F.
1324		get_operations_index_file(Machine,OI) :-
1325		add_internal_error('No operations_index file opened',get_operations_index_file(Machine,OI)),fail.
1326
1327		find_loadable_machines(Solutions) :-
1328		findall(loadable(Type,Machine),
1329		find_loadable_machines2(Type,Machine),
1330		Solutions).
1331		find_loadable_machines2(Type,Machine) :-
1332		main_machine_name(Main),
1333	?	find_loadable_machines_sees_includes(Main,Type,Machine).
1334		find_loadable_machines_sees_includes(Main,main,Main).
1335		find_loadable_machines_sees_includes(Main,sub,Seen) :-
1336		machine_sees(Main,Seen).
1337		find_loadable_machines_sees_includes(Start,sub,Included) :-
1338	?	find_loadable_machines_includes(Start,Included).
1339		find_loadable_machines_includes(Start,Included) :-
1340		machine_includes(Start,_Prefix1,M),
1341		( Included=M
1342		; find_loadable_machines_includes(M,Included)).
1343
1344		machine_sees(MachA,MachB) :-
1345		machine_references(MachA,References),
1346		member(ref(Type,MachB,''),References),
1347		memberchk(Type,[sees,uses]).
1348		machine_includes(MachA,Prefix,MachB) :-
1349		machine_references(MachA,References),
1350		member(ref(Type,MachB,Prefix),References),
1351		memberchk(Type,[includes,extends]).
1352
1353		% lookup_pattern/2:
1354		% To enable a fast lookup of values in a state, we have to sort the variables.
1355		% On the other hand, we must not sort the variables when storing them, their order
1356		% is significant.
1357		% This predicate generates a "lookup_pattern" that sorts the variables and their
1358		% corresponding values and enables to map the sorted values to the original order
1359		% by a simple unification.
1360		lookup_pattern(Variables,lookup_pattern(SortedVariables,SortedValues,Variables,Values)) :-
1361		maplist(variable_value_pair,Variables,VarValues,Values),
1362		sort(VarValues,SortedVarValues),
1363		maplist(variable_value_pair,SortedVariables,SortedVarValues,SortedValues).
1364		variable_value_pair(I,I/V,V).
1365
1366
1367		% utility for statistics:
1368
1369		reset_counters :- write(reset),nl,
1370	?	(is_counter(C), bb_reset(C), fail ; true).
1371
1372		print_value_persistance_stats :-
1373		format_with_colour_nl(user_output,[blue],'ProB Value Persistance Caching Statistics',[]),
1374		(storage_directory(Dir)
1375		-> format_with_colour_nl(user_output,[blue],'* Cache storage directory: ~w',[Dir])
1376		; format_with_colour_nl(user_output,[orange],'* No cache storage directory set!',[])
1377		),
1378		format_with_colour_nl(user_output,[blue],'ProB Value Persistance Caching Statistics',[]),
1379		bb_safe_get(value_persistance_constants_loaded,C),
1380		format_with_colour_nl(user_output,[blue],' * Nr. of machines for which stored constants were reused: ~w',[C]),
1381		bb_safe_get(value_persistance_ref_constants_loaded,RC),
1382		format_with_colour_nl(user_output,[blue],' * Nr. of referenced machines for which stored constants were reused: ~w',[RC]),
1383		bb_safe_get(value_persistance_stored_constants,StCs),
1384		format_with_colour_nl(user_output,[blue],' * Nr. of constants stored: ~w',[StCs]),
1385		bb_safe_get(value_persistance_op_cache_machines,OCM),
1386		format_with_colour_nl(user_output,[blue],' * Nr. of machines for which operations can be reused/stored: ~w',[OCM]),
1387		bb_safe_get(value_persistance_loadable_operations,LO),
1388		format_with_colour_nl(user_output,[blue],' * Nr. of stored operations which can be re-used: ~w',[LO]),
1389		bb_safe_get(value_persistance_storeable_operations,SO),
1390		format_with_colour_nl(user_output,[blue],' * Nr. of operations which can be stored: ~w',[SO]),
1391		bb_safe_get(value_persistance_reused_transitions,R),
1392		format_with_colour_nl(user_output,[blue],' * Nr. of stored operation calls reused: ~w',[R]),
1393		bb_safe_get(value_persistance_stored_transitions,S),
1394		format_with_colour_nl(user_output,[blue],' * Nr. of operation calls *not* reused and stored: ~w',[S]),
1395		bb_safe_get(value_persistance_not_worth_transitions,WW),
1396		format_with_colour_nl(user_output,[blue],' * Nr. of operation calls *not* reused and *not* stored: ~w',[WW]),
1397		bb_safe_get(value_persistance_refresh_transitions,RF),
1398		format_with_colour_nl(user_output,[blue],' * Nr. of operation calls refreshed: ~w',[RF]).
1399
1400		get_value_persistance_stats(List) :-
1401		findall(Counter-Value,(is_counter(Counter),bb_safe_get(Counter,Value)),List).
1402
1403		is_counter(value_persistance_constants_loaded).
1404		is_counter(value_persistance_ref_constants_loaded).
1405		is_counter(value_persistance_loadable_operations).
1406		is_counter(value_persistance_op_cache_machines).
1407		is_counter(value_persistance_loadable_operations).
1408		is_counter(value_persistance_storeable_operations).
1409		is_counter(value_persistance_reused_transitions).
1410		is_counter(value_persistance_stored_transitions).
1411		is_counter(value_persistance_not_worth_transitions).
1412		is_counter(value_persistance_refresh_transitions).
1413
1414		bb_reset(Counter) :- bb_put(Counter,0).
1415
1416
1417		% utility for debugging:
1418
1419		formatwarn(Format,Args) :-
1420		format_with_colour_nl(user_output,[orange],Format,Args).
1421
1422		formatinfo(_Format,_Args) :- silent_mode(on),!.
1423		formatinfo(Format,Args) :-
1424		format_with_colour_nl(user_output,[grey],Format,Args).
1425
1426		formatdetails(_Format,_Args) :- silent_mode(on), debug_mode(on),
1427		!.
1428		formatdetails(Format,Args) :-
1429		format_with_colour_nl(user_output,[grey],Format,Args).
1430
1431		formatgood(_Format,_Args) :- silent_mode(on),!.
1432		formatgood(Format,Args) :-
1433		format_with_colour_nl(user_output,[green],Format,Args).
1434
1435		:- use_module(tools_io,[safe_open_file/4]).
1436		my_open(File,Mode,St,Opt) :- !, safe_open_file(File,Mode,St,Opt).
1437		my_open(File,Mode,St,Opt) :-
1438		safe_open_file(File,Mode,St,Opt),
1439		formatinfo('Opened file (~w) ~w -> ~w',[Mode,File,St]).
1440
1441		my_close(Stream) :- !, close(Stream).
1442		my_close(Stream) :- stream_property(Stream,file_name(F)),!,
1443		formatinfo('Closing ~w -> ~w',[F, Stream]),
1444		close(Stream).
1445		my_close(Stream) :-
1446		formatinfo('Closing -> ~w',[Stream]),
1447		close(Stream).