1		% (c) 2009-2024 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, load_constants/2,
8		cache_is_activated/0, clear_applicable_flag/0,
9		load_partial_constants/3,
10		lookup_cached_transitions/3,
11		add_new_transitions_to_cache/1,
12		tcltk_load_constants/1,
13		show_cache_file_contents/1]).
14
15
16		:- use_module(library(lists)).
17		:- use_module(library(file_systems)).
18		:- use_module(library(fastrw)). % fast_read/2
19
20		:- use_module(debug).
21		:- use_module(tools).
22		:- use_module(error_manager, [add_error/2,add_error/3]).
23		:- use_module(state_space, [transition/3,visited_expression/2,
24		time_out_for_node/1,not_all_transitions_added/1,
25		time_out_for_node/3,transition/4,
26		transition_info/2 %,max_reached_for_node/1
27		]).
28		:- use_module(succeed_max, [max_reached/1]).
29		:- use_module(preferences).
30		:- use_module(b_machine_hierarchy).
31		:- use_module(specfile, [animation_mode/1, classical_b_mode/0,
32		state_corresponds_to_initialised_b_machine/2]).
33		:- use_module(store, [lookup_value/3]).
34		:- use_module(kernel_objects, [equal_object/2]).
35		:- use_module(bmachine, [b_get_machine_refinement_hierarchy/1,
36		get_operation_info/2]).
37		%:- use_module(bmachine_structure, [get_section/3]).
38		:- use_module(b_global_sets, [is_b_global_constant/3,b_global_set/1]).
39		:- use_module(bsyntaxtree).
40		:- use_module(extension('probhash/probhash'),[raw_sha_hash/2]).
41
42		:- use_module(module_information).
43		:- module_info(group,interpreter).
44		:- module_info(description,'This module is responsible for caching constants and operations on disk').
45
46		:- dynamic storage_directory/1.
47		% storage_directory('/home/plagge/svn/alstomprob/examples/cache/').
48		:- volatile storage_directory/1.
49		:- dynamic is_applicable_internal/1.
50		:- volatile is_applicable_internal/1.
51
52		/**********************************************************************/
53		/* common for loading and saving: */
54		/**********************************************************************/
55
56		cache_is_activated :-
57		storage_directory(_).
58
59		cache_is_applicable_for_transitions :-
60		cache_is_applicable,
61		get_preference(cache_operations,true).
62
63		cache_is_applicable :-
64		is_applicable_internal(Applicable),!,Applicable=true.
65		cache_is_applicable :-
66		cache_is_activated,
67		% b_mode, % only for B models
68		classical_b_mode,
69		b_get_machine_refinement_hierarchy([_]), % only if there is no refinement - we cache no refinements
70		preferences:get_preference(symmetry_mode,off), % with symmetry on: you cannot simply patch operation updates
71		formatsilent('value persistance, cache IS applicable~n',[]),
72		assert_once( is_applicable_internal(true) ),!.
73		cache_is_applicable :-
74		debug_format(19,'value persistance, cache NOT applicable~n',[]),
75		assert_once( is_applicable_internal(false) ),fail.
76
77		:- use_module(tools,[get_parent_directory_of_directory/2]).
78		set_storage_directory(Dir) :- set_storage_directory(Dir,strict).
79		set_storage_directory(Dir,Create) :-
80		unset_storage_directory,
81		(absolute_file_name(Dir,AbsDir,[file_type(directory),access(exist),fileerrors(fail)])
82		-> assertz(storage_directory(AbsDir))
83		; Create=create_if_needed,
84		get_parent_directory_of_directory(Dir,ParentDir),
85		directory_exists(ParentDir),
86		% parent directory exists; try to create the directory itself
87		absolute_file_name(Dir,AbsDir,[file_type(directory),access(none),fileerrors(fail)]),
88		format('Trying to create cache directory: ~w~n',[AbsDir]),
89		make_directory(AbsDir)
90		-> assertz(storage_directory(AbsDir))
91		; add_error(cache,'Could not set cache directory, directory does not exist: ',Dir)).
92
93		unset_storage_directory :-
94		retractall(storage_directory(_)),
95		clear_applicable_flag.
96
97		% should be called if e.g. animation mode information changes (csp_and_b mode)
98		clear_applicable_flag :-
99		retractall(is_applicable_internal(_)).
100		:- use_module(eventhandling,[register_event_listener/3]).
101		:- register_event_listener(change_of_animation_mode,clear_applicable_flag,
102		'Clear Cache Info.').
103		:- register_event_listener(reset_prob,unset_storage_directory,
104		'Reset Cache').
105
106		%:- use_module(version, [revision/1]).
107		:- use_module(version,[version/4]).
108		get_revision_info(info(V1,V2,V3,V4,ValuePersistanceRevision)) :-
109		% revision(Revision), % revision not used: it differs between probcli and ProB Tcl/Tk
110		version(V1,V2,V3,V4),
111		ValuePersistanceRevision = '$Rev$'.
112
113		collect_computation_parameters(Name,[machine_name(Name)
114		,prob_revision(Revision)
115		%,machine_hash(Hash)
116		,constants_signature(ConstSig)
117		|Prefs]) :-
118		find_relevant_preferences(Prefs),
119		get_revision_info(Revision),
120		%machine_hash(Name,Hash),
121		compute_constants_signature(Name,ConstSig).
122
123		/* returns a list of Pref/Value pairs for each preference that is regarded
124		a relevant when computing values for constants. See is_relevant_preference/2
125		below */
126		find_relevant_preferences(Prefs) :-
127		findall(preference(Pref,Value), relevant_preference(Pref,Value), Unsorted),
128		sort(Unsorted,Prefs).
129
130		% value_persistance:find_relevant_preferences(L), member(preference(P,_),L), print(P),nl,fail.
131
132		relevant_preference(Pref,Value) :-
133		preference_category(Pref,Category),
134		( is_relevant_preference(Pref,Category) -> true; fail), % just to introduce a local cut
135		get_preference(Pref,Value).
136
137		/* is_relevant_preference(+Preference,+Category)
138		is used to specify those preferencees whose values are stored in the constants file.
139		If such a preference changes, the constants have to be recomputed */
140
141		is_relevant_preference(Pref,_) :- nonvar(Pref),
142		irrelevant_preference(Pref),!,fail.
143		is_relevant_preference(_Pref,animation).
144		is_relevant_preference(_Pref,hidden).
145		is_relevant_preference(_Pref,advanced).
146
147		% number_animated_abstractions : only relevant for Event-B + if refinement
148		irrelevant_preference(expand_avl_upto). % only affects pretty-printing
149		irrelevant_preference(bool_expression_as_predicate). % only used inside REPL/eval
150		irrelevant_preference(use_large_jvm_for_parser).
151		irrelevant_preference(expand_forall_upto). % only relevant in predicate analysis
152		irrelevant_preference(time_out). % if time_out occurs: no re-use anyway
153		irrelevant_preference(performance_monitoring_on). % just prints messages
154		irrelevant_preference(performance_monitoring_expansion_limit).
155		irrelevant_preference(kodkod_for_components) :- \+ preference(use_solver_on_load,kodkod).
156		irrelevant_preference(do_neginvariant_checking). % just indicates whether invariant evaluated doubly
157		irrelevant_preference(provide_trace_information). % just provides feedback; should not change values
158		irrelevant_preference(use_closure_expansion_memoization). % only influences performance
159		irrelevant_preference(warn_when_expanding_infinite_closures). % only generates extra warnings
160		irrelevant_preference(use_small_window).
161		irrelevant_preference(tk_show_source_pane).
162		irrelevant_preference(check_prolog_b_ast).
163		irrelevant_preference(use_font_size_for_columns).
164		irrelevant_preference(user_is_an_expert_with_accessto_source_distribution).
165		irrelevant_preference(default_to_runtime_type_checking_on_startup_for_expert).
166		irrelevant_preference(number_of_recent_documents).
167		irrelevant_preference(number_of_searched_patterns).
168		irrelevant_preference(number_of_replaced_patterns).
169		irrelevant_preference(number_of_eval_history_elements).
170		irrelevant_preference(number_of_eval_csp_history_elements).
171		irrelevant_preference(number_of_checked_ltl_formulas).
172		irrelevant_preference(machines_path).
173		irrelevant_preference(tlc_number_of_workers).
174		irrelevant_preference(unsat_core_algorithm).
175
176		irrelevant_preference(deterministic_trace_replay).
177		irrelevant_preference(dot_use_ps_viewer).
178		%irrelevant_preference(double_evaluation_when_analysing).% not used when computing constants or events
179		irrelevant_preference(generate_minimal_nr_of_testcases).
180		irrelevant_preference(ltl_to_ba_tool).
181		irrelevant_preference(path_to_atb_krt).
182		irrelevant_preference(path_to_bcomp).
183		irrelevant_preference(path_to_cspm).
184		irrelevant_preference(path_to_csp_typechecker).
185		irrelevant_preference(path_to_dot).
186		irrelevant_preference(path_to_dotty).
187		irrelevant_preference(path_to_fdr).
188		irrelevant_preference(path_to_fuzz). %% ??
189		irrelevant_preference(path_to_latex).
190		irrelevant_preference(path_to_ltsmin).
191		irrelevant_preference(path_to_probe).
192		irrelevant_preference(path_to_ps_viewer).
193		irrelevant_preference(path_to_spin).
194		irrelevant_preference(path_to_text_editor).
195		irrelevant_preference(path_to_text_editor_launch).
196		irrelevant_preference(repl_cache_parsing).
197		irrelevant_preference(show_bvisual_formula_explanations).
198		irrelevant_preference(show_bvisual_formula_functor_from).
199		irrelevant_preference(show_function_tuples_in_property).
200		irrelevant_preference(symbolic_mc_try_other_solvers).
201		irrelevant_preference(use_scope_predicate).
202
203		irrelevant_preference(path_to_java).
204		irrelevant_preference(translate_print_all_sequences).
205		irrelevant_preference(translate_print_cs_style_sequences).
206		irrelevant_preference(view_probcli_errors_using_bbresults).
207		irrelevant_preference(trace_upon_error).
208		irrelevant_preference(error_log_file).
209		irrelevant_preference(tk_custom_state_viewer_padding).
210		irrelevant_preference(tk_custom_state_viewer_str_padding).
211		irrelevant_preference(tk_custom_state_viewer_font_name).
212		irrelevant_preference(tk_custom_state_viewer_font_size).
213		irrelevant_preference(use_tk_custom_state_viewer).
214		irrelevant_preference(X) :- preference_category(X,Cat), irrelevant_category(Cat).
215
216		irrelevant_category(alloy2b).
217		irrelevant_category(cbc_commands). %cbc_provide_explanations
218		irrelevant_category(distb).
219		irrelevant_category(dot).
220		irrelevant_category(dot_definitions).
221		irrelevant_category(dot_event_hierarchy).
222		irrelevant_category(dot_formula_tree).
223		irrelevant_category(dot_machine_hierarchy).
224		irrelevant_category(dot_graph_generator).
225		irrelevant_category(dot_projection).
226		irrelevant_category(dot_state_graph).
227		irrelevant_category(dot_state_space).
228		irrelevant_category(dot_variable_modification).
229		irrelevant_category(gui_prefs).
230		irrelevant_category(latex).
231		irrelevant_category(mc_dc_commands).
232		irrelevant_category(smtlib2b).
233		irrelevant_category(state_as_graph).
234		irrelevant_category(syntax_highlighting).
235		irrelevant_category(table_commands).
236		irrelevant_category(trace_generator).
237		irrelevant_category(wd_commands).
238		% alternate categories already covered by dot category:
239		%irrelevant_category(state_as_graph).
240		%irrelevant_category(dot_graph_generator).
241		%irrelevant_category(dot_state_space).
242
243		compute_constants_signature(Name,constsig(Name,PropHash,Sublist)) :-
244		properties_hash(Name,PropHash),
245		findall(Sig,
246		( referenced_machine_with_constants_or_properties(Name,RefName),
247		compute_constants_signature(RefName,Sig)),
248		SubSigs),
249		sort(SubSigs,Sublist).
250
251		referenced_machine_with_constants_or_properties(OrigName,RefName) :-
252		referenced_machine(OrigName,RefName,_,_),
253		machine_has_constants_or_properties_trans(RefName).
254
255		machine_has_constants_or_properties_trans(Name) :-
256		machine_has_constants_or_properties(Name),!.
257		machine_has_constants_or_properties_trans(Name) :-
258		referenced_machine(Name,Ref,_,_),
259		machine_has_constants_or_properties_trans(Ref),!.
260		machine_has_constants_or_properties(Name) :-
261		machine_identifiers(Name,_Params,Sets,_AVars,_CVars,AConsts,CConsts),
262		( Sets=[_|_] ; AConsts==[_|_] ; CConsts=[_|_]),!.
263
264		referenced_machine(SrcName,DstName,Type,Prefix) :-
265		machine_references(SrcName,Refs),
266		member(ref(Type,DstName,Prefix),Refs).
267
268		/**********************************************************************/
269		/* saving values of constants */
270		/**********************************************************************/
271		:- use_module(state_packing).
272
273		save_constants(MaxReached) :-
274		cache_is_applicable,
275		\+ constants_loaded_from_file, % we have just loaded the constants from file; no need to re-write them
276		main_machine_name(Name), % this fails e.g. in Z mode
277		!,
278		(save_constants2(Name,MaxReached) -> true ; add_error(value_persistance,'Storing constants failed.')).
279		save_constants(_MaxReached).
280
281		save_constants2(Name,MaxReached) :-
282		statistics(runtime,[Start,_]),
283		statistics(walltime,[WStart,_]),
284		save_constants_for_machine(Name,MaxReached),
285		statistics(runtime,[Stop,_]), Time is Stop - Start,
286		statistics(walltime,[WStop,_]), WTime is WStop - WStart,
287		%% tools:print_memory_used_wo_gc,
288		formatsilent('value caching: storing constants for ~w (maxr: ~w) (~w [~w] ms).~n',
289		[Name,MaxReached,Time,WTime]).
290
291		save_constants_for_machine(Name,MaxReached) :-
292		find_constants(Name,Constants),
293		Constants = [_|_], % at least one constant exists, check before computing findall !
294		find_constants_stores(Stores),
295		is_usable_data(Constants,Stores),!,
296		debug_println(9,saving_constants(Name)),
297		maplist(generate_bindings(Constants),Stores,ConstantBindings),
298		debug_println(9,collect_computation_parameters(Name)),
299		collect_computation_parameters(Name,CompParams),
300		debug_println(9,save_values_into_file(Name)),
301		save_values_into_file(Name,CompParams,ConstantBindings,MaxReached).
302		save_constants_for_machine(Name,_MaxReached) :-
303		formatsilent('value caching: no constants stored for ~w~n',[Name]).
304
305		find_constants(Name,Constants) :-
306		machine_identifiers(Name,Params,_Sets,_AVars,_CVars,AbstractConstants,ConcreteConstants),
307		( Params=[_|_]
308		-> add_warning(value_persistance,'Parameters not yet supported.'), % ok to just issue warning ?? or should we generate error ?
309		fail
310		; true),
311		append(AbstractConstants,ConcreteConstants,RawConstants),
312		maplist(get_raw_identifier,RawConstants,Unsorted),
313		sort(Unsorted,Constants).
314		get_raw_identifier(identifier(_Pos,Id),Id).
315		get_raw_identifier(description(_Pos,_Desc,Raw),Id) :- get_raw_identifier(Raw,Id).
316
317		/* Returns the stores of values in the state space that contain values for contants */
318		find_constants_stores(Stores) :-
319		findall(S,
320		( transition(root,Trans,I),
321		functor(Trans,'$setup_constants',_),
322		visited_expression(I,concrete_constants(S))
323		),
324		Stores).
325
326		/* is_usable_data/2 succeeds if there are constants that are ready to store */
327		is_usable_data(Constants,Stores) :-
328		% at least one constant exists
329		Constants = [_|_],
330		% at least one state with computed constants was generated
331		Stores = [_|_],
332		% all constants have been computed
333		\+ not_all_transitions_added(root),
334		% no time-out in the root node
335		\+ time_out_for_node(root).
336
337		%generate_bindings(Constants,Store,ConstantsBinding) :-
338		% maplist(generate_binding2(Store),Constants,ConstantsBinding).
339		%generate_binding2(Store,Constant,bind(Constant,Value)) :-
340		% lookup_value(Constant,Store,Value).
341		generate_bindings(_Constants,Store,ConstantsBinding) :-
342		% TODO: review this
343		Store = ConstantsBinding.
344
345		save_values_into_file(Name,CompParams,ConstantBindings,MaxReached) :-
346		storage_file_name(constants,Name,Filename),
347		open(Filename,write,S,[type(binary)]),
348		call_cleanup(save_values_into_file2(S,CompParams,ConstantBindings,MaxReached),
349		my_close(S)).
350		save_values_into_file2(S,CompParams,ConstantBindings,MaxReached) :-
351		fast_write(S,comp_parameters(CompParams)),
352		fast_write(S,maximum_reached(MaxReached)),
353		maplist(write_bind(S,constants),ConstantBindings),
354		fast_write(S,end_of_file).
355		write_bind(S,Type,Store) :-
356		preferences:get_preference(use_state_packing,PREF),
357		preferences:set_preference(use_state_packing,false),
358		state_packing:pack_values(Store,PS), % does not seem to bring major performance benefit; but reduces file size
359		% print(packed(Store,PS)),nl,
360		preferences:set_preference(use_state_packing,PREF),
361		fast_write(S,values(Type,PS)).
362		% fast_write(S,values(Type)), fast_write_list(PS,S). % should we do something like this to reduce memory consumption ?
363
364		%fast_write_list([],S) :- fast_write(S,end_of_list).
365		%fast_write_list('$bind_var'(Var,Val,T),S) :- fast_write(S,bind(Var,Val)), fast_write_list(T,S).
366
367		/* compute the full file name for the stored constants for the machine
368		the predicate uses the specified directory where constants values
369		should be stored */
370		storage_file_name(Type,MachineName,FullName) :-
371		file_suffix(Type,Suffix),
372		storage_directory(Directory),
373		atom_concat(MachineName,Suffix,Name),
374		atom_concat(Directory,Name,FullName).
375
376		file_suffix(constants,'.probcst').
377		file_suffix(operations,'.probops').
378		file_suffix(operations_data,'.opdata').
379
380
381		/**********************************************************************/
382		/* load constants */
383		/**********************************************************************/
384
385		% a predicate to see which constant values have been saved
386		tcltk_load_constants(list(CS)) :-
387		load_constants(ConstantsStores,_),
388		maplist(translate:translate_bstate,ConstantsStores,CS).
389
390
391		/* load_constants/2 returns a list of stores if the constants have been
392		saved before for the same computation parameters.
393		The predicate fails if no constants can be loaded.
394		MaxReached is 'true' if the maximum number of computed solutions was reached
395		or 'false' otherwise.
396		*/
397
398		:- dynamic constants_loaded_from_file/0.
399		:- volatile constants_loaded_from_file/0.
400		load_constants(ConstantStores,MaxReached) :-
401		cache_is_applicable, % check if storing/re-using constants is activated
402		main_machine_name(Name),
403		machine_file_exists(Name,FullName),
404		open(FullName,read,S,[type(binary)]),
405		call_cleanup(load_constants2(S,Name,ConstantStores,MaxReached),
406		my_close(S)),!.
407		load_constants2(S,Name,ConstantStores,MaxReached) :-
408		load_parameters(S,StoredParameters), % if the relevant computation parameters
409		collect_computation_parameters(Name,CurrentParameters), % are different, we cannot re-use the
410		(compare_computation_parameters(StoredParameters,CurrentParameters) % values stored in the file
411		-> true
412		; formatsilent('value caching: parameters changed; not reusing previously computed constants for ~w.~n',[Name]),
413		fail
414		),
415		load_max_reached(S,MaxReached),
416		load_constant_values(S,ConstantStores),
417		(debug_mode(off) -> true
418		; length(ConstantStores,Len),
419		get_ids(ConstantStores,CstNames),
420		formatsilent('value caching: re-using ~w previously computed solutions for constants ~w for ~w.~n',[Len,CstNames,Name])
421		),
422		assert_once( constants_loaded_from_file ).
423
424
425		machine_file_exists(Name,FullName) :-
426		cache_file_exists(constants,Name,FullName).
427		cache_file_exists(Type,Name,FullName) :-
428		storage_file_name(Type,Name,FullName),
429		(file_exists(FullName) -> true
430		; get_tail_filename(FullName,Tail),
431		formatsilent('value caching: ~w cache file ~w does not yet exist for ~w.~n',[Type, Tail, Name]),
432		fail
433		).
434
435		load_parameters(S,StoredParameters) :-
436		safe_constants_read(S,comp_parameters(StoredParameters)).
437
438		load_max_reached(S,MR) :-
439		safe_constants_read(S,maximum_reached(MR)).
440
441		load_constant_values(S,Stores) :-
442		safe_constants_read(S,Term),
443		( Term = end_of_file ->
444		Stores = []
445		; Term = values(constants,Store) ->
446		unpack_constants(Store,UPS),
447		Stores = [UPS|Rest],
448		load_constant_values(S,Rest)).
449
450		unpack_constants(Store,UPS) :-
451		preferences:get_preference(use_state_packing,PREF),
452		preferences:set_preference(use_state_packing,false),
453		state_packing:unpack_values(Store,UPS),
454		% print(unpacked(Store,UPS)),nl,
455		preferences:set_preference(use_state_packing,PREF).
456
457		safe_constants_read(S,Term) :-
458		read_syntax_safe(S,T,Error),
459		( Error==true ->
460		write('Invalid cache file content. File skipped.\n'),
461		fail
462		;
463		Term = T).
464
465		load_partial_constants(ConstantsBindings,InProperties,OutProperties) :-
466		% TODO: - check if parameters / constraints have been used (what are the implications?)
467		cache_is_applicable, % check if storing/re-using constants is activated
468		main_machine_name(Name),
469		findall( partial(MName,NewBindings),
470		try_to_reuse_referenced_machine(Name,MName,NewBindings),
471		PSol),
472		PSol = [_|_],!,
473		remove_evaluated_properties(PSol,InProperties,OutProperties),
474		select_and_apply_binding(PSol,ConstantsBindings).
475		load_partial_constants(_ConstantsBindings,Properties,Properties).
476
477		/**********************************************************************/
478
479		:- meta_predicate open_cache_file(+,+,-,0).
480		open_cache_file(Type,Name,Stream,Call) :-
481		cache_file_exists(Type,Name,FullName),
482		my_open(FullName,read,Stream,[type(binary)]),
483		call_cleanup( (call(Call),!),my_close(Stream)).
484
485		/**********************************************************************/
486
487		try_to_reuse_referenced_machine(OrigName,Name,Bindings) :-
488		referenced_machine_with_constants_or_properties(OrigName,RefName),
489		try_to_reuse_referenced_machine2(OrigName,RefName,Name,Bindings).
490		try_to_reuse_referenced_machine2(OrigName,RefName,Name,Bindings) :-
491		% try to re-use values of a machine directly referenced by OrigName that
492		% contains constants
493		open_cache_file(constants,RefName,S,try_load_ref_values2(RefName,OrigName,S,Bindings1)),!,
494		RefName = Name,
495		Bindings1 = Bindings.
496		try_to_reuse_referenced_machine2(_,RefName,Name,Bindings) :-
497		% using the directly referenced machine failed, using a machine
498		% that is referenced by the referenced machine
499		try_to_reuse_referenced_machine(RefName,Name,Bindings).
500		try_load_ref_values2(RefName,OrigName,S,Bindings) :-
501		check_if_machine_has_no_parameters(RefName),
502		load_parameters(S,StoredParameters),
503		check_if_all_constants_computed(RefName,S),
504		collect_computation_parameters(RefName,CurrentParameters),
505		compare_computation_parameters(StoredParameters,CurrentParameters),
506		load_constant_values(S,Bindings),
507		(debug_mode(off) -> true
508		; length(Bindings,Len),
509		get_ids(Bindings,CstNames),
510		formatsilent('value caching: re-using ~w previously computed solutions for constants ~w of referenced machine ~w within ~w.~n',[Len,CstNames,RefName,OrigName])
511		% TODO: show names of constants ...
512		).
513
514		get_name(bind(ID,_),ID) :- !.
515		get_name(X,X).
516
517		get_ids([Binding|_],Names) :- maplist(get_name,Binding,Names).
518
519		check_if_machine_has_no_parameters(RefName) :-
520		machine_identifiers(RefName,Params,_Sets,_AVars,_CVars,_AConsts,_CConsts),
521		( Params=[] -> true
522		;
523		formatsilent('value caching: constants of referenced machine ~w are not used because it uses parameters',[Params]),
524		fail).
525
526		compare_computation_parameters([],[]) :- !.
527		compare_computation_parameters([CH|CT],[SH|ST]) :-
528		!,compare_computation_parameters(CH,SH),
529		compare_computation_parameters(CT,ST).
530		compare_computation_parameters(C,C) :- !.
531		compare_computation_parameters(C,S) :-
532		debug_format(19,'parameter difference:~ncurrent is ~w,~n stored is ~w~n',[C,S]),
533		fail.
534
535		check_if_all_constants_computed(_RefName,S) :-
536		% make sure that all solutions have been generated
537		load_max_reached(S,false),!.
538		check_if_all_constants_computed(RefName,_S) :-
539		formatsilent('value caching: constants for referenced machine ~w not used because not all solutions were computed.~n',[RefName]),
540		fail.
541
542		select_and_apply_binding(Solutions,Store) :-
543		maplist(select_solutions,Solutions,Bindings),
544		maplist(select_and_apply_binding2(Store),Bindings).
545		select_and_apply_binding2(Store,Binding) :-
546		maplist(apply_binding(Store),Binding).
547		apply_binding(Store,bind(Id,Value)) :-
548		lookup_value(Id,Store,SValue),
549		equal_object(SValue,Value).
550		select_solutions(partial(_Name,Bindings),Binding) :-
551		member(Binding,Bindings).
552
553		:- use_module(bmachine,[get_machine_file_number/4]).
554		machine_file_number(Name,Nr) :-
555		get_machine_file_number(Name,Ext,Nr,_),
556		Ext \= 'def',!.
557		machine_file_number(Name,Nr) :-
558		add_error(value_persistance,'Could not find machine name:',Name),
559		bmachine:portray_filenumbers,
560		Nr = -99.
561
562		:- use_module(tools_positions, [get_position_filenumber/2]).
563		% remove the properties from those machines whose constants have already been set from file
564		remove_evaluated_properties(PSol,InProperties,OutProperties) :-
565		findall(Name,member(partial(Name,_),PSol),UnsortedNames),
566		sort(UnsortedNames,Names),
567		maplist(machine_file_number,Names,FileNumbers),
568		debug_println(9,filtering(Names,FileNumbers)),
569		conjunction_to_list(InProperties,InAsList),
570		% exclude all properties who are in one of the files for which we have restored (all) constant values
571		exclude(belongs_to_file(FileNumbers),InAsList,OutAsList), % this is exclude/3 from library(lists)
572		conjunct_predicates(OutAsList,OutProperties).
573		belongs_to_file(FileNumbers,TPred) :-
574		get_texpr_info(TPred,Info),
575		memberchk(nodeid(Pos),Info),
576		get_position_filenumber(Pos,FilePos),
577		memberchk(FilePos,FileNumbers).
578
579		/**********************************************************************/
580
581		:- dynamic loadable_operation/5, storable_operation/4, stored_transition/4, index_file_opened/1.
582		:- volatile loadable_operation/5, storable_operation/4, stored_transition/4, index_file_opened/1.
583
584		initialise_operation_caching :-
585		clear_applicable_flag,
586		cache_is_applicable_for_transitions,
587		main_machine_name(MachName), % if we have no machine name, fail silently (for default machine)
588		!,
589		% check wich operations are cachable and prepare information for them
590		debug_println(9,initialise_operation_caching),
591		retract_all_op_cache_data,
592		try_to_load_operations_cache_for_all_machines,
593		get_operation_names(MachName,OperationNames),
594		maplist(init_operation_cache(MachName),OperationNames),
595		save_operations_cache_survey(MachName,OperationNames),
596		open_data_file(MachName).
597		initialise_operation_caching :-
598		retract_all_op_cache_data.
599
600		:- use_module(eventhandling,[register_event_listener/3]).
601		:- register_event_listener(specification_initialised,initialise_operation_caching,
602		'Initialise operation caching info.').
603
604
605		retract_all_op_cache_data :-
606		retractall(constants_loaded_from_file),
607		retractall(loadable_operation(_,_,_,_,_)),
608		retractall(storable_operation(_,_,_,_)),
609		retractall(stored_transition(_,_,_,_)),
610		( index_file_opened(S) ->
611		catch( my_close(S), _, true ),
612		retractall(index_file_opened(_))
613		; true).
614
615		% index_file_opened(Stream) contains a possibly open stream for the operations (probops) file
616		reset_index_file_opened :-
617		( index_file_opened(S) ->
618		my_close(S),retractall(index_file_opened(_))
619		; true).
620
621		get_operation_names(MachName,OperationNames) :-
622		machine_operations(MachName,RawOperationNames),
623		maplist(get_raw_identifier,RawOperationNames,OperationNames).
624
625		try_to_load_operations_cache_for_all_machines :-
626		find_loadable_machines(LoadableMachines),
627		maplist(try_to_load_operations_cache,LoadableMachines).
628
629		try_to_load_operations_cache(loadable(_Type,MachName)) :-
630		get_operations_computation_parameters(MachName,OpParams),
631		open_cache_file(operations,MachName,S,read_cached_operations(S,MachName,OpParams,Error)),!,
632		( Error==true ->
633		format('value caching: corrupted index file for machine ~w, deleting file.~n',[MachName]),
634		delete_cache_file(MachName)
635		; true).
636		try_to_load_operations_cache(loadable(main,MachName)) :-
637		% delete the data file if one exists -- only for main machine
638		delete_cache_file(MachName),!.
639		try_to_load_operations_cache(_Loadable).
640
641		delete_cache_file(MachName) :-
642		cache_file_exists(operations_data,MachName,Filename),!,
643		delete_file(Filename).
644
645		read_cached_operations(S,MachName,CurrentOpParams,SyntaxError) :-
646		read_syntax_safe(S,StoredOpParams,SyntaxError),
647		( SyntaxError==true -> true
648		; CurrentOpParams = StoredOpParams ->
649		formatsilent('value caching: re-use of stored operations for ~w~n',[MachName]),
650		read_cached_operations2(S,MachName,SyntaxError)
651		;
652		write('value caching: general computations parameters have changed, no re-use of stored operations\n'),
653		debug_params(CurrentOpParams,StoredOpParams),
654		fail).
655		read_cached_operations2(S,MachName,SyntaxError) :-
656		read_syntax_safe(S,Term,SyntaxError),
657		( SyntaxError==true -> true
658		; Term == end_of_file -> true
659		; read_cached_operations3(Term,MachName) ->
660		read_cached_operations2(S,MachName,SyntaxError)
661		;
662		functor(Term,F,A),
663		format('value caching: unrecognised entry in cache file for ~w: ~w/~w~n',[MachName,F,A]),
664		fail
665		).
666		debug_params(op_comp_parameters(A),op_comp_parameters(B)) :- !,
667		debug_params(A,B).
668		debug_params(preference(P,A),preference(P,B)) :- !,
669		(A=B -> true ; print(P), print(':'), print(A/B), print(' ')).
670		debug_params([],[]) :- !,nl.
671		debug_params([Cur|CT],[Stored|ST]) :- !,
672		debug_params(Cur,Stored),
673		debug_params(CT,ST).
674		debug_params(A,B) :- (A=B -> true ; print(A/B),nl).
675
676		% -----------------
677
678		:- meta_predicate show_cache_file_contents_for_machine(-,0,-,-).
679		% a small utility to print out the contents of the cache files:
680
681
682		:- use_module(tools_printing,[format_with_colour_nl/4]).
683		show_cache_file_contents(Verbose) :-
684		(storage_directory(Dir) -> true ; Dir='?'),
685		format_with_colour_nl(user_output,[blue],'Cache contents (directory: ~w)',[Dir]),
686		reset_index_file_opened, % otherwise on Windows we are not able to open the probobs file as it is already open
687		show_cache_file_operations(Verbose).
688
689
690		show_cache_file_operations(Verbose) :-
691		reset_index_file_opened, % otherwise on Windows we are not able to open the probobs file as it is already open
692		find_loadable_machines(LoadableMachines),
693		maplist(show_cache_file_contents_for_machine(_,show_facts(S,Verbose),S),LoadableMachines).
694
695		cache_applicable(operations) :- !, cache_is_applicable_for_transitions.
696		cache_applicable(_) :- cache_is_applicable.
697
698		:- use_module(tools,[get_tail_filename/2]).
699		show_cache_file_contents_for_machine(ExpectedType,Call,Stream,loadable(_MType,MachName)) :-
700		file_type(Type),
701		(var(ExpectedType) -> true ; ExpectedType=Type),
702		(cache_file_exists(Type,MachName,FullName) ->
703		get_tail_filename(FullName,FF),
704		format_with_colour_nl(user_output,[blue],'Contents of ~w cache file for machine ~w: ~w',[Type,MachName,FF]),
705		(cache_applicable(Type) -> true
706		; format_with_colour_nl(user_output,[blue],' (Cache not applicable for ~w)',[Type])),
707		(open_cache_file(Type,MachName,Stream,Call)
708		-> format_with_colour_nl(user_output,[blue],'End of contents (~w)',[FF])
709		; format_with_colour_nl(user_error,[red],'Failed to show cache contents of ~w.',[FF])
710		)
711		; \+ cache_applicable(Type) -> true
712		; Type=operations, machine_operations(MachName,_)
713		-> format_with_colour_nl(user_output,[blue],'No cache file of type ~w for machine with operations ~w.~n',[Type,MachName])
714		; Type=constants, machine_has_constants(MachName)
715		-> format_with_colour_nl(user_output,[blue],'No cache file of type ~w for machine with constants ~w.~n',[Type,MachName])
716		; debug_format(19,'No cache file of type ~w for machine ~w.~n',[Type,MachName]) % TODO: check if MachName has constants,...
717		),
718		fail.
719		show_cache_file_contents_for_machine(_,_,_,_).
720
721		show_facts(S,Verbose) :- read_syntax_safe(S,Term,Error),
722		(nonvar(Error)
723		-> add_error(value_persistance,'Error occured reading cache stream: ',S)
724		; Term = end_of_file -> reset_and_show_stats
725		; portray_content_fact(Term,Verbose),
726		show_facts(S,Verbose)).
727
728		:- use_module(tools_strings,[get_hex_bytes/2]).
729		:- use_module(translate,[print_bstate/1]).
730		% operations:
731		portray_content_fact(op_comp_parameters(OpParams),Verbose) :- OpParams=[H|_], !,
732		format_verbose(Verbose,' op_comp_parameters([~w,...]).~n',[H]).
733		portray_content_fact(operation(OpName,Hash),_) :- get_hex_bytes(Hash,Hex), !,
734		format(' operation(~w,~s).~n',[OpName,Hex]).
735		portray_content_fact(transition(OpName,Hash,Index),Verbose) :- get_hex_bytes(Hash,Hex), !,
736		format_verbose(Verbose,' transition(~w,~s,~w).~n',[OpName,Hex,Index]),
737		inc_counter(OpName).
738		% constants:
739		portray_content_fact(comp_parameters(OpParams),Verbose) :- OpParams=[H|_], !,
740		format_verbose(Verbose,' comp_parameters([~w,...]).~n',[H]).
741		portray_content_fact(maximum_reached(MaxReached),Verbose) :- !,
742		format_verbose(Verbose,' maximum_reached(~w).~n',[MaxReached]),
743		inc_counter(maximum_reached).
744		portray_content_fact(values(constants,Store),_Verbose) :- !,
745		unpack_constants(Store,UPS),
746		print_bstate(UPS),nl.
747		portray_content_fact(Term,_) :- portray_clause(Term).
748
749		format_verbose(verbose,Str,A) :- !, format(Str,A).
750		format_verbose(_,_,_).
751
752		file_type(constants).
753		file_type(operations).
754
755		:- dynamic counter/2.
756		reset_and_show_stats :- retract(counter(C,Nr)), format(' # of ~w : ~w~n',[C,Nr]),fail.
757		reset_and_show_stats.
758
759		inc_counter(C) :- (retract(counter(C,Nr)) -> N1 is Nr+1 ; N1 = 1),
760		assertz(counter(C,N1)).
761
762		:- use_module(error_manager).
763		% variation of tools_fastread:fastrw_read/3
764		read_syntax_safe(S,Term,Error) :-
765		catch( fast_read(S,Term1), % from library fastrw
766		error(E,_),
767		( E=syntax_error(_) -> Error = true
768		; E=permission_error(_,_,_) -> Term1 = end_of_file
769		; E=consistency_error(_,_,_)
770		-> add_error(value_persistance,'Consistency error when reading from stream: ',E),
771		Error = true
772		;
773		add_error(value_persistance,'Unknown error when reading from stream: ',E),
774		throw(E))
775		),
776		Term1 = Term.
777
778
779		read_cached_operations3(operation(OpName,StoredHash),MachName) :-
780		( operation_hash(MachName,OpName,CurrentHash) ->
781		( CurrentHash = StoredHash % we can reuse operation; the hash includes DEFINITIONS and called operations
782		->
783		formatsilent('value caching: operation ~w unchanged for ~w.~n',[OpName,MachName]),
784		%TODO: what if the machine has parameters? Can we reuse the transitions from the generic machine?
785		find_matching_operations(OpName,MachName,PrefixedOpNames), % find includes with renaming, ...
786		( PrefixedOpNames = [] ->
787		format('value caching: no operation found for ~w in ~w~n', [OpName,MachName])
788		;
789		formatsilent('value caching: (composed/renamed) operations ~w found for ~w in ~w~n',
790		[PrefixedOpNames,OpName,MachName]),
791		maplist(store_loadable_operation(OpName,MachName),PrefixedOpNames) )
792		;
793		get_hex_bytes(CurrentHash,CH), get_hex_bytes(StoredHash,SH),
794		format('value caching: operation ~w has changed (~s, was ~s).~n',[OpName, CH, SH])
795		)
796		;
797		format('value caching: unrecognised operation ~w.~n',[OpName])
798		).
799		read_cached_operations3(transition(OpName,Hash,Index),MachName) :-
800		( loadable_operation(_,OpName,MachName,_InputPattern,_OutputPattern) ->
801		compute_short_hash(Hash,Short),
802		formatsilent('value caching: loading stored_transition ~w (~w) : hash ~w~n',[OpName,Index,Short]),
803		assertz( stored_transition(Short,Hash,OpName,Index) )
804		;
805		% ignore
806		true
807		).
808
809		store_loadable_operation(_OpName,_MachName,PrefixedOpName) :-
810		loadable_operation(PrefixedOpName,_,_,_,_),!.
811		store_loadable_operation(OpName,MachName,PrefixedOpName) :-
812		find_operation_input_output(PrefixedOpName,Input,Output) ->
813		create_output_pattern(Output,OutputPattern),
814		lookup_pattern(Input,InputPattern),!,
815		formatsilent('value persistance, loadable_operation from cache: ~w in ~w~n',[OpName,MachName]),
816		assertz( loadable_operation(PrefixedOpName,OpName,MachName,InputPattern,OutputPattern) ).
817		store_loadable_operation(_OpName,_MachName,PrefixedOpName) :-
818		format('value caching: unable to generate input/output pattern for operation ~w.~n',
819		[PrefixedOpName]).
820
821		find_matching_operations(Operation,MachName,FullNames) :-
822		findall(O, is_matching_operation(Operation,MachName,O), FullNames).
823
824		is_matching_operation(Operation,MachName,Operation) :-
825		% there is an operation with exactly the same name
826		operation_with_machine(Operation,MachName).
827		is_matching_operation(Operation,MachName,FullName) :-
828		atom_concat('.',Operation,DottedOp),
829		operation_with_machine(FullName,MachName),
830		atom_concat(_,DottedOp,FullName).
831
832		operation_with_machine(OpName,MachName) :-
833		get_operation_info(OpName,Infos),
834		( memberchk(origin(Origin),Infos), % for c1.Inc the origin will be the included machine
835		last(Origin,_/MachName) -> true
836		; main_machine_name(MachName)
837		).
838
839		create_output_pattern(Ids,Values/Bindings) :-
840		maplist(create_output_pattern2,Ids,Values,Bindings).
841		create_output_pattern2(Id,Value,bind(Id,Value)).
842
843		init_operation_cache(MachName,OpName) :-
844		storable_operation(OpName,MachName,_InputPattern,_Output),!. % ignore, already registered
845		init_operation_cache(MachName,OpName) :-
846		( find_operation_input_output(OpName,Input,Output) ->
847		lookup_pattern(Input,InputPattern),
848		debug_println(9,find_operation_input_output(OpName,Input,Output)),
849		assertz( storable_operation(OpName,MachName,InputPattern,Output) ),
850		% Operations of the main machine are never prefixed
851		create_output_pattern(Output,OutputPattern),
852		assertz( loadable_operation(OpName,OpName,MachName,InputPattern,OutputPattern) )
853		;
854		format('value caching: unable to generate input/output pattern for operation ~w.~n',
855		[OpName])
856		).
857
858		get_operations_computation_parameters(Name,op_comp_parameters(OpParams)) :-
859		find_relevant_preferences(Prefs),
860		get_revision_info(Revision),
861		OpParams = [machine_name(Name),prob_revision(Revision)|Prefs].
862
863		lookup_cached_transitions(PrefixedOpName,InState,OutputBindings) :-
864		cache_is_applicable_for_transitions,
865		loadable_operation(PrefixedOpName,OpName,MachName,InputPattern,OutputPattern),
866		sort(InState,SortedInState),
867		% statistics(runtime,[Start,_]), statistics(walltime,[WStart,_]),
868		hash_input_values(OpName,MachName,InputPattern,SortedInState,ShortHash,InputHash),
869		stored_transition(ShortHash,InputHash,OpName,Index),!,
870		formatsilent('value caching: re-using values for operation ~w (~w -> ~w).~n',[OpName,ShortHash,Index]),
871		( load_solutions(MachName,Index,Solutions) -> true
872		%length(Solutions,Sn),
873		%format('value caching: re-using ~w solutions for operation ~w of machine ~w.~n',
874		% [Sn,OpName,MachName])
875		;
876		format('value caching: re-using values for operation ~w failed.~n',[OpName]),
877		fail),
878		%print(solution(Solutions)),nl, print(pattern(OutputPattern)),nl,
879		% OutputPattern is of the form [V1,...]/[bind(v1,V1),...]
880		maplist(create_output_binding(OutputPattern),Solutions,OutputBindings).
881		%statistics(runtime,[Stop,_]), Time is Stop - Start,
882		%statistics(walltime,[WStop,_]), WTime is WStop - WStart,
883		%tools:print_memory_used_wo_gc,
884		%format('caching time: ~w (~w)~n',[Time,WTime]).
885		load_solutions(MachName,Index,Solutions) :-
886		storage_file_name(operations_data,MachName,FilenameData),
887		open(FilenameData,read,S,[type(binary),reposition(true)]),
888		call_cleanup((seek(S,Index,bof,_),
889		fast_read(S,Solutions)),
890		my_close(S)).
891		create_output_binding(Pattern,transition(Param,Result,New,Info),
892		transition(Param,Result,Update,Info)) :-
893		copy_term(Pattern,New/Update).
894
895		select_values(Ids,State,Values) :- sort(State,SState),
896		select_values_sorted(Ids,SState,Values).
897		% Note: as Identifiers are sorted then we can avoid quadratic complexity here and scan State only once for all Ids
898		select_values_sorted(Ids,SState,Values) :-
899		(select_values_sorted_aux(Ids,SState,Values) -> true
900		; print('Lookup: '),print(Ids), nl,
901		print('State: '), maplist(get_bind_id,SState,SIds), print(SIds),nl,fail).
902		select_values_sorted_aux([],_,[]).
903		select_values_sorted_aux([Id|Irest],State,[Value|Vrest]) :-
904		( ordered_select(State,Id,StoredValue,RestState) ->
905		Value=StoredValue,
906		select_values_sorted_aux(Irest,RestState,Vrest)
907		;
908		ajoin(['Looking up "', Id, '" failed.'], Msg),
909		(maplist(get_bind_id,State,Ids) -> true ; Ids = '<<cannot print state ids>>'),
910		add_error(value_persistance,Msg,Ids),
911		fail
912		).
913		ordered_select([bind(Id,Value)|T],Id,Value,T).
914		ordered_select([_|T],Id,Value,R) :- ordered_select(T,Id,Value,R).
915		get_bind_id(bind(Id,_),Id).
916
917		hash_input_values(OpName,MachName,InputPattern,SortedInState,Short,Long) :-
918		%%statistics(runtime,[Start,_]), statistics(walltime,[WStart,_]),
919		( hash_input_values2(OpName,MachName,InputPattern,SortedInState,Short,Long) ->
920		true
921		%, statistics(runtime,[Stop,_]), Time is Stop - Start,
922		% statistics(walltime,[WStop,_]), WTime is WStop - WStart,
923		% tools:print_memory_used_wo_gc,
924		% format('hashing time for ~w:~w = ~w (~w)~n',[OpName,MachName,Time,WTime])
925		; add_failed_call_error(hash_input_values2(OpName,MachName,InputPattern,SortedInState,Short,Long)),
926		fail).
927
928		hash_input_values2(OpName,MachName,InputPattern,SortedInState,Short,Long) :-
929		copy_term(InputPattern,lookup_pattern(SortedVars,SortedInputValues,_,InputValues)),
930		select_values_sorted(SortedVars,SortedInState,SortedInputValues),
931		raw_sha_hash(OpName/MachName/InputValues,Long),
932		compute_short_hash(Long,Short).
933		compute_short_hash([A,B,C,D|_],Short) :-
934		Short is A<<24 + B<<16 + C<<8 + D.
935
936		save_operations_cache_survey(MachName,OperationNames) :-
937		get_operations_computation_parameters(MachName,OpParams),
938		storage_file_name(operations,MachName,FileName),
939		my_open(FileName,write,S,[type(binary)]),
940		fast_write(S,OpParams),
941		save_operation_info(S,MachName,OperationNames),
942		my_close(S).
943
944		save_operation_info(S,MachName,OperationNames) :-
945		member(OpName,OperationNames),
946		storable_operation(OpName,MachName,_InputPattern,_Output),
947		operation_hash(MachName,OpName,OpHash),
948		fast_write(S,operation(OpName,OpHash)),
949		stored_transition(_Short,InputHash,OpName,Index),
950		formatsilent('value caching: storing transition for ~w (~w)~n',[OpName,Index]),
951		fast_write(S,transition(OpName,InputHash,Index)),
952		fail.
953		save_operation_info(_S,_MachName,_OperationNames).
954
955		find_operation_input_output(OpName,Input,Output) :-
956		get_operation_info(OpName,Info),
957		memberchk(reads(Input1),Info),
958		% remove references to global sets and their elements
959		get_all_sets_and_enum_ids(SEIds),
960		remove_all(Input1,SEIds,Input),
961		memberchk(modifies(Output),Info).
962
963		get_all_sets_and_enum_ids(SEIds) :-
964		findall(Id,
965		( is_b_global_constant(_,_,Id)
966		; b_global_set(Id)),
967		SEIds).
968
969		add_new_transitions_to_cache(InStateId) :-
970		cache_is_applicable_for_transitions,!,
971		( get_all_max_reached_operations(MaxReachedList),
972		add_new_transitions_to_cache1(InStateId,MaxReachedList) ->
973		true
974		;
975		add_failed_call_error(add_new_transitions_to_cache1(InStateId,_))).
976		add_new_transitions_to_cache(_InStateId).
977
978		get_all_max_reached_operations(MaxReachedList) :-
979		findall(Op, max_reached(Op), MaxReached), sort(MaxReached,MaxReachedList).
980
981		:- use_module(library(ordsets),[ord_member/2]).
982		add_new_transitions_to_cache1(InStateId,MaxReached) :-
983		visited_expression(InStateId,InState1),
984		state_corresponds_to_initialised_b_machine(InState1,InState),
985		main_machine_name(MachName),
986		storable_operation(OpName,MachName,InputPattern,Output),
987		\+ time_out_for_node(InStateId,OpName,_),
988		\+ ord_member(OpName,MaxReached),
989		sort(InState,SortedInState),
990		add_new_transitions_to_cache2(InStateId,SortedInState,OpName,InputPattern,Output,MachName),
991		fail.
992		add_new_transitions_to_cache1(_InStateId,_MaxReached) :-
993		flush_data.
994
995		add_new_transitions_to_cache2(InStateId,SortedInState,OpName,InputPattern,Output,MachName) :-
996		hash_input_values(OpName,MachName,InputPattern,SortedInState,ShortHash,InputHash),
997		\+ stored_transition(ShortHash,InputHash,_,_), % Is there already a cache entry?
998		find_all_transitions(InStateId,OpName,Output,Transitions),
999		length(Transitions,Length),
1000		%format('value caching: storing ~w transitions for operation ~w in state ~w.~n',
1001		% [Length,OpName,InStateId]),
1002		%print(Transitions),nl,
1003		statistics(runtime,[Start,_]),
1004		statistics(walltime,[WStart,_]),
1005		store_transition_into_cache(OpName,ShortHash,InputHash,Transitions,MachName),
1006		statistics(runtime,[Stop,_]), Time is Stop - Start,
1007		statistics(walltime,[WStop,_]), WTime is WStop - WStart,
1008		%%tools:print_memory_used_wo_gc,
1009		formatsilent('value caching: storing ~w transitions for operation ~w in state ~w (~w, ~w [~w] ms).~n',
1010		[Length,OpName,InStateId,ShortHash,Time,WTime]).
1011
1012		store_transition_into_cache(OpName,ShortHash,Hash,Transitions,MachName) :-
1013		storage_file_name(operations_data,MachName,FilenameData),
1014		my_open(FilenameData,read,SR,[type(binary),reposition(true)]),
1015		call_cleanup(seek(SR,0,eof,Index),
1016		my_close(SR)),
1017		my_open(FilenameData,append,SW,[type(binary)]),
1018		call_cleanup(fast_write(SW,Transitions),
1019		my_close(SW)),
1020		assertz( stored_transition(ShortHash,Hash,OpName,Index) ),
1021		index_file_opened(OI),
1022		fast_write(OI,transition(OpName,Hash,Index)).
1023
1024		find_all_transitions(InStateId,OpName,Output,Transitions) :-
1025		findall( transition(ParaValues,ResultValues,Updates,TransInfo),
1026		find_transition(InStateId,OpName,Output,ParaValues,ResultValues,Updates,TransInfo),
1027		Transitions).
1028		find_transition(InStateId,OpName,Output,ParaValues,ResultValues,Updates,TransInfo) :-
1029		transition(InStateId,Operation,TransId,OutStateId),
1030		operation_name(Operation,OpName,ParaValues,ResultValues),
1031		findall(TI,transition_info(TransId,TI),TransInfo),
1032		visited_expression(OutStateId,OutState1), % we could use packed_visited_expression here ?
1033		state_corresponds_to_initialised_b_machine(OutState1,OutState),
1034		select_values(Output,OutState,Updates).
1035		operation_name('-->'(Operation,ResultValues),OpName,ParaValues,ResultValues) :-
1036		!,operation_name(Operation,OpName,ParaValues,_).
1037		operation_name(Operation,OpName,ParaValues,[]) :-
1038		Operation =.. [OpName|ParaValues].
1039
1040		open_data_file(Name) :-
1041		reset_index_file_opened,
1042		storage_file_name(operations,Name,FilenameIndex),
1043		my_open(FilenameIndex,append,FI,[type(binary)]),
1044		assertz(index_file_opened(FI)),
1045		storage_file_name(operations_data,Name,FilenameData),
1046		( file_exists(FilenameData) -> true
1047		;
1048		my_open(FilenameData,write,SD,[type(binary)]),
1049		my_close(SD)).
1050
1051		flush_data :-
1052		index_file_opened(S),
1053		flush_output(S).
1054
1055		find_loadable_machines(Solutions) :-
1056		findall(loadable(Type,Machine),
1057		find_loadable_machines2(Type,Machine),
1058		Solutions).
1059		find_loadable_machines2(Type,Machine) :-
1060		main_machine_name(Main),
1061		find_loadable_machines_sees_includes(Main,Type,Machine).
1062		find_loadable_machines_sees_includes(Main,main,Main).
1063		find_loadable_machines_sees_includes(Main,sub,Seen) :-
1064		machine_sees(Main,Seen).
1065		find_loadable_machines_sees_includes(Start,sub,Included) :-
1066		find_loadable_machines_includes(Start,Included).
1067		find_loadable_machines_includes(Start,Included) :-
1068		machine_includes(Start,_Prefix1,M),
1069		( Included=M
1070		; find_loadable_machines_includes(M,Included)).
1071
1072		machine_sees(MachA,MachB) :-
1073		machine_references(MachA,References),
1074		member(ref(Type,MachB,''),References),
1075		memberchk(Type,[sees,uses]).
1076		machine_includes(MachA,Prefix,MachB) :-
1077		machine_references(MachA,References),
1078		member(ref(Type,MachB,Prefix),References),
1079		memberchk(Type,[includes,extends]).
1080
1081		% lookup_pattern/2:
1082		% To enable a fast lookup of values in a state, we have to sort the variables.
1083		% On the other hand, we must not sort the variables when storing them, their order
1084		% is significant.
1085		% This predicate generates a "lookup_pattern" that sorts the variables and their
1086		% corresponding values and enables to map the sorted values to the original order
1087		% by a simple unification.
1088		lookup_pattern(Variables,lookup_pattern(SortedVariables,SortedValues,Variables,Values)) :-
1089		maplist(variable_value_pair,Variables,VarValues,Values),
1090		sort(VarValues,SortedVarValues),
1091		maplist(variable_value_pair,SortedVariables,SortedVarValues,SortedValues).
1092		variable_value_pair(I,I/V,V).
1093
1094
1095		% utility for debugging:
1096		:- use_module(tools_io,[safe_open_file/4]).
1097		my_open(File,Mode,St,Opt) :- !, safe_open_file(File,Mode,St,Opt).
1098		my_open(File,Mode,St,Opt) :-
1099		safe_open_file(File,Mode,St,Opt),
1100		formatsilent('Opened file (~w) ~w -> ~w~n',[Mode,File,St]).
1101
1102		my_close(Stream) :- !, close(Stream).
1103		my_close(Stream) :- stream_property(Stream,file_name(F)),!,
1104		formatsilent('Closing ~w -> ~w~n',[F, Stream]),
1105		close(Stream).
1106		my_close(Stream) :-
1107		formatsilent('Closing -> ~w~n',[Stream]),
1108		close(Stream).