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