1		% (c) 2009-2023 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 -> true
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		% constants:
738		portray_content_fact(comp_parameters(OpParams),Verbose) :- OpParams=[H|_], !,
739		format_verbose(Verbose,' comp_parameters([~w,...]).~n',[H]).
740		portray_content_fact(maximum_reached(MaxReached),Verbose) :- !,
741		format_verbose(Verbose,' maximum_reached(~w).~n',[MaxReached]).
742		portray_content_fact(values(constants,Store),_Verbose) :- !,
743		unpack_constants(Store,UPS),
744		print_bstate(UPS),nl.
745		portray_content_fact(Term,_) :- portray_clause(Term).
746
747		format_verbose(verbose,Str,A) :- !, format(Str,A).
748		format_verbose(_,_,_).
749
750		file_type(constants).
751		file_type(operations).
752
753
754		:- use_module(error_manager).
755		% variation of tools_fastread:fastrw_read/3
756		read_syntax_safe(S,Term,Error) :-
757		catch( fast_read(S,Term1), % from library fastrw
758		error(E,_),
759		( E=syntax_error(_) -> Error = true
760		; E=permission_error(_,_,_) -> Term1 = end_of_file
761		; E=consistency_error(_,_,_)
762		-> add_error(value_persistance,'Consistency error when reading from stream: ',E),
763		Error = true
764		;
765		add_error(value_persistance,'Unknown error when reading from stream: ',E),
766		throw(E))
767		),
768		Term1 = Term.
769
770
771		read_cached_operations3(operation(OpName,StoredHash),MachName) :-
772		( operation_hash(MachName,OpName,CurrentHash) ->
773		( CurrentHash = StoredHash % we can reuse operation; the hash includes DEFINITIONS and called operations
774		->
775		formatsilent('value caching: operation ~w unchanged for ~w.~n',[OpName,MachName]),
776		%TODO: what if the machine has parameters? Can we reuse the transitions from the generic machine?
777		find_matching_operations(OpName,MachName,PrefixedOpNames), % find includes with renaming, ...
778		( PrefixedOpNames = [] ->
779		format('value caching: no operation found for ~w in ~w~n', [OpName,MachName])
780		;
781		formatsilent('value caching: (composed/renamed) operations ~w found for ~w in ~w~n',
782		[PrefixedOpNames,OpName,MachName]),
783		maplist(store_loadable_operation(OpName,MachName),PrefixedOpNames) )
784		;
785		get_hex_bytes(CurrentHash,CH), get_hex_bytes(StoredHash,SH),
786		format('value caching: operation ~w has changed (~s, was ~s).~n',[OpName, CH, SH])
787		)
788		;
789		format('value caching: unrecognised operation ~w.~n',[OpName])
790		).
791		read_cached_operations3(transition(OpName,Hash,Index),MachName) :-
792		( loadable_operation(_,OpName,MachName,_InputPattern,_OutputPattern) ->
793		compute_short_hash(Hash,Short),
794		formatsilent('value caching: loading stored_transition ~w (~w) : hash ~w~n',[OpName,Index,Short]),
795		assertz( stored_transition(Short,Hash,OpName,Index) )
796		;
797		% ignore
798		true
799		).
800
801		store_loadable_operation(_OpName,_MachName,PrefixedOpName) :-
802		loadable_operation(PrefixedOpName,_,_,_,_),!.
803		store_loadable_operation(OpName,MachName,PrefixedOpName) :-
804		find_operation_input_output(PrefixedOpName,Input,Output) ->
805		create_output_pattern(Output,OutputPattern),
806		lookup_pattern(Input,InputPattern),!,
807		formatsilent('value persistance, loadable_operation from cache: ~w in ~w~n',[OpName,MachName]),
808		assertz( loadable_operation(PrefixedOpName,OpName,MachName,InputPattern,OutputPattern) ).
809		store_loadable_operation(_OpName,_MachName,PrefixedOpName) :-
810		format('value caching: unable to generate input/output pattern for operation ~w.~n',
811		[PrefixedOpName]).
812
813		find_matching_operations(Operation,MachName,FullNames) :-
814		findall(O, is_matching_operation(Operation,MachName,O), FullNames).
815
816		is_matching_operation(Operation,MachName,Operation) :-
817		% there is an operation with exactly the same name
818		operation_with_machine(Operation,MachName).
819		is_matching_operation(Operation,MachName,FullName) :-
820		atom_concat('.',Operation,DottedOp),
821		operation_with_machine(FullName,MachName),
822		atom_concat(_,DottedOp,FullName).
823
824		operation_with_machine(OpName,MachName) :-
825		get_operation_info(OpName,Infos),
826		( memberchk(origin(Origin),Infos), % for c1.Inc the origin will be the included machine
827		last(Origin,_/MachName) -> true
828		; main_machine_name(MachName)
829		).
830
831		create_output_pattern(Ids,Values/Bindings) :-
832		maplist(create_output_pattern2,Ids,Values,Bindings).
833		create_output_pattern2(Id,Value,bind(Id,Value)).
834
835		init_operation_cache(MachName,OpName) :-
836		storable_operation(OpName,MachName,_InputPattern,_Output),!. % ignore, already registered
837		init_operation_cache(MachName,OpName) :-
838		( find_operation_input_output(OpName,Input,Output) ->
839		lookup_pattern(Input,InputPattern),
840		debug_println(9,find_operation_input_output(OpName,Input,Output)),
841		assertz( storable_operation(OpName,MachName,InputPattern,Output) ),
842		% Operations of the main machine are never prefixed
843		create_output_pattern(Output,OutputPattern),
844		assertz( loadable_operation(OpName,OpName,MachName,InputPattern,OutputPattern) )
845		;
846		format('value caching: unable to generate input/output pattern for operation ~w.~n',
847		[OpName])
848		).
849
850		get_operations_computation_parameters(Name,op_comp_parameters(OpParams)) :-
851		find_relevant_preferences(Prefs),
852		get_revision_info(Revision),
853		OpParams = [machine_name(Name),prob_revision(Revision)|Prefs].
854
855		lookup_cached_transitions(PrefixedOpName,InState,OutputBindings) :-
856		cache_is_applicable_for_transitions,
857		loadable_operation(PrefixedOpName,OpName,MachName,InputPattern,OutputPattern),
858		sort(InState,SortedInState),
859		% statistics(runtime,[Start,_]), statistics(walltime,[WStart,_]),
860		hash_input_values(OpName,MachName,InputPattern,SortedInState,ShortHash,InputHash),
861		stored_transition(ShortHash,InputHash,OpName,Index),!,
862		formatsilent('value caching: re-using values for operation ~w.~n',[OpName]),
863		( load_solutions(MachName,Index,Solutions) -> true
864		%length(Solutions,Sn),
865		%format('value caching: re-using ~w solutions for operation ~w of machine ~w.~n',
866		% [Sn,OpName,MachName])
867		;
868		format('value caching: re-using values for operation ~w failed.~n',[OpName]),
869		fail),
870		%print(solution(Solutions)),nl, print(pattern(OutputPattern)),nl,
871		% OutputPattern is of the form [V1,...]/[bind(v1,V1),...]
872		maplist(create_output_binding(OutputPattern),Solutions,OutputBindings).
873		%statistics(runtime,[Stop,_]), Time is Stop - Start,
874		%statistics(walltime,[WStop,_]), WTime is WStop - WStart,
875		%tools:print_memory_used_wo_gc,
876		%format('caching time: ~w (~w)~n',[Time,WTime]).
877		load_solutions(MachName,Index,Solutions) :-
878		storage_file_name(operations_data,MachName,FilenameData),
879		open(FilenameData,read,S,[type(binary),reposition(true)]),
880		call_cleanup((seek(S,Index,bof,_),
881		fast_read(S,Solutions)),
882		my_close(S)).
883		create_output_binding(Pattern,transition(Param,Result,New,Info),
884		transition(Param,Result,Update,Info)) :-
885		copy_term(Pattern,New/Update).
886
887		select_values(Ids,State,Values) :- sort(State,SState),
888		select_values_sorted(Ids,SState,Values).
889		% Note: as Identifiers are sorted then we can avoid quadratic complexity here and scan State only once for all Ids
890		select_values_sorted(Ids,SState,Values) :-
891		(select_values_sorted_aux(Ids,SState,Values) -> true
892		; print('Lookup: '),print(Ids), nl,
893		print('State: '), maplist(get_bind_id,SState,SIds), print(SIds),nl,fail).
894		select_values_sorted_aux([],_,[]).
895		select_values_sorted_aux([Id|Irest],State,[Value|Vrest]) :-
896		( ordered_select(State,Id,StoredValue,RestState) ->
897		Value=StoredValue,
898		select_values_sorted_aux(Irest,RestState,Vrest)
899		;
900		ajoin(['Looking up "', Id, '" failed.'], Msg),
901		(maplist(get_bind_id,State,Ids) -> true ; Ids = '<<cannot print state ids>>'),
902		add_error(value_persistance,Msg,Ids),
903		fail
904		).
905		ordered_select([bind(Id,Value)|T],Id,Value,T).
906		ordered_select([_|T],Id,Value,R) :- ordered_select(T,Id,Value,R).
907		get_bind_id(bind(Id,_),Id).
908
909		hash_input_values(OpName,MachName,InputPattern,SortedInState,Short,Long) :-
910		%%statistics(runtime,[Start,_]), statistics(walltime,[WStart,_]),
911		( hash_input_values2(OpName,MachName,InputPattern,SortedInState,Short,Long) ->
912		true
913		%, statistics(runtime,[Stop,_]), Time is Stop - Start,
914		% statistics(walltime,[WStop,_]), WTime is WStop - WStart,
915		% tools:print_memory_used_wo_gc,
916		% format('hashing time for ~w:~w = ~w (~w)~n',[OpName,MachName,Time,WTime])
917		; add_failed_call_error(hash_input_values2(OpName,MachName,InputPattern,SortedInState,Short,Long)),
918		fail).
919
920		hash_input_values2(OpName,MachName,InputPattern,SortedInState,Short,Long) :-
921		copy_term(InputPattern,lookup_pattern(SortedVars,SortedInputValues,_,InputValues)),
922		select_values_sorted(SortedVars,SortedInState,SortedInputValues),
923		raw_sha_hash(OpName/MachName/InputValues,Long),
924		compute_short_hash(Long,Short).
925		compute_short_hash([A,B,C,D|_],Short) :-
926		Short is A<<24 + B<<16 + C<<8 + D.
927
928		save_operations_cache_survey(MachName,OperationNames) :-
929		get_operations_computation_parameters(MachName,OpParams),
930		storage_file_name(operations,MachName,FileName),
931		my_open(FileName,write,S,[type(binary)]),
932		fast_write(S,OpParams),
933		save_operation_info(S,MachName,OperationNames),
934		my_close(S).
935
936		save_operation_info(S,MachName,OperationNames) :-
937		member(OpName,OperationNames),
938		storable_operation(OpName,MachName,_InputPattern,_Output),
939		operation_hash(MachName,OpName,OpHash),
940		fast_write(S,operation(OpName,OpHash)),
941		stored_transition(_Short,InputHash,OpName,Index),
942		formatsilent('value caching: storing transition for ~w (~w)~n',[OpName,Index]),
943		fast_write(S,transition(OpName,InputHash,Index)),
944		fail.
945		save_operation_info(_S,_MachName,_OperationNames).
946
947		find_operation_input_output(OpName,Input,Output) :-
948		get_operation_info(OpName,Info),
949		memberchk(reads(Input1),Info),
950		% remove references to global sets and their elements
951		get_all_sets_and_enum_ids(SEIds),
952		remove_all(Input1,SEIds,Input),
953		memberchk(modifies(Output),Info).
954
955		get_all_sets_and_enum_ids(SEIds) :-
956		findall(Id,
957		( is_b_global_constant(_,_,Id)
958		; b_global_set(Id)),
959		SEIds).
960
961		add_new_transitions_to_cache(InStateId) :-
962		cache_is_applicable_for_transitions,!,
963		( get_all_max_reached_operations(MaxReachedList),
964		add_new_transitions_to_cache1(InStateId,MaxReachedList) ->
965		true
966		;
967		add_failed_call_error(add_new_transitions_to_cache1(InStateId,_))).
968		add_new_transitions_to_cache(_InStateId).
969
970		get_all_max_reached_operations(MaxReachedList) :-
971		findall(Op, max_reached(Op), MaxReached), sort(MaxReached,MaxReachedList).
972
973		:- use_module(library(ordsets),[ord_member/2]).
974		add_new_transitions_to_cache1(InStateId,MaxReached) :-
975		visited_expression(InStateId,InState1),
976		state_corresponds_to_initialised_b_machine(InState1,InState),
977		main_machine_name(MachName),
978		storable_operation(OpName,MachName,InputPattern,Output),
979		\+ time_out_for_node(InStateId,OpName,_),
980		\+ ord_member(OpName,MaxReached),
981		sort(InState,SortedInState),
982		add_new_transitions_to_cache2(InStateId,SortedInState,OpName,InputPattern,Output,MachName),
983		fail.
984		add_new_transitions_to_cache1(_InStateId,_MaxReached) :-
985		flush_data.
986
987		add_new_transitions_to_cache2(InStateId,SortedInState,OpName,InputPattern,Output,MachName) :-
988		hash_input_values(OpName,MachName,InputPattern,SortedInState,ShortHash,InputHash),
989		\+ stored_transition(ShortHash,InputHash,_,_), % Is there already a cache entry?
990		find_all_transitions(InStateId,OpName,Output,Transitions),
991		length(Transitions,Length),
992		%format('value caching: storing ~w transitions for operation ~w in state ~w.~n',
993		% [Length,OpName,InStateId]),
994		%print(Transitions),nl,
995		statistics(runtime,[Start,_]),
996		statistics(walltime,[WStart,_]),
997		store_transition_into_cache(OpName,ShortHash,InputHash,Transitions,MachName),
998		statistics(runtime,[Stop,_]), Time is Stop - Start,
999		statistics(walltime,[WStop,_]), WTime is WStop - WStart,
1000		%%tools:print_memory_used_wo_gc,
1001		formatsilent('value caching: storing ~w transitions for operation ~w in state ~w (~w [~w] ms).~n',
1002		[Length,OpName,InStateId,Time,WTime]).
1003
1004		store_transition_into_cache(OpName,ShortHash,Hash,Transitions,MachName) :-
1005		storage_file_name(operations_data,MachName,FilenameData),
1006		my_open(FilenameData,read,SR,[type(binary),reposition(true)]),
1007		call_cleanup(seek(SR,0,eof,Index),
1008		my_close(SR)),
1009		my_open(FilenameData,append,SW,[type(binary)]),
1010		call_cleanup(fast_write(SW,Transitions),
1011		my_close(SW)),
1012		assertz( stored_transition(ShortHash,Hash,OpName,Index) ),
1013		index_file_opened(OI),
1014		fast_write(OI,transition(OpName,Hash,Index)).
1015
1016		find_all_transitions(InStateId,OpName,Output,Transitions) :-
1017		findall( transition(ParaValues,ResultValues,Updates,TransInfo),
1018		find_transition(InStateId,OpName,Output,ParaValues,ResultValues,Updates,TransInfo),
1019		Transitions).
1020		find_transition(InStateId,OpName,Output,ParaValues,ResultValues,Updates,TransInfo) :-
1021		transition(InStateId,Operation,TransId,OutStateId),
1022		operation_name(Operation,OpName,ParaValues,ResultValues),
1023		findall(TI,transition_info(TransId,TI),TransInfo),
1024		visited_expression(OutStateId,OutState1), % we could use packed_visited_expression here ?
1025		state_corresponds_to_initialised_b_machine(OutState1,OutState),
1026		select_values(Output,OutState,Updates).
1027		operation_name('-->'(Operation,ResultValues),OpName,ParaValues,ResultValues) :-
1028		!,operation_name(Operation,OpName,ParaValues,_).
1029		operation_name(Operation,OpName,ParaValues,[]) :-
1030		Operation =.. [OpName|ParaValues].
1031
1032		open_data_file(Name) :-
1033		reset_index_file_opened,
1034		storage_file_name(operations,Name,FilenameIndex),
1035		my_open(FilenameIndex,append,FI,[type(binary)]),
1036		assertz(index_file_opened(FI)),
1037		storage_file_name(operations_data,Name,FilenameData),
1038		( file_exists(FilenameData) -> true
1039		;
1040		my_open(FilenameData,write,SD,[type(binary)]),
1041		my_close(SD)).
1042
1043		flush_data :-
1044		index_file_opened(S),
1045		flush_output(S).
1046
1047		find_loadable_machines(Solutions) :-
1048		findall(loadable(Type,Machine),
1049		find_loadable_machines2(Type,Machine),
1050		Solutions).
1051		find_loadable_machines2(Type,Machine) :-
1052		main_machine_name(Main),
1053		find_loadable_machines_sees_includes(Main,Type,Machine).
1054		find_loadable_machines_sees_includes(Main,main,Main).
1055		find_loadable_machines_sees_includes(Main,sub,Seen) :-
1056		machine_sees(Main,Seen).
1057		find_loadable_machines_sees_includes(Start,sub,Included) :-
1058		find_loadable_machines_includes(Start,Included).
1059		find_loadable_machines_includes(Start,Included) :-
1060		machine_includes(Start,_Prefix1,M),
1061		( Included=M
1062		; find_loadable_machines_includes(M,Included)).
1063
1064		machine_sees(MachA,MachB) :-
1065		machine_references(MachA,References),
1066		member(ref(Type,MachB,''),References),
1067		memberchk(Type,[sees,uses]).
1068		machine_includes(MachA,Prefix,MachB) :-
1069		machine_references(MachA,References),
1070		member(ref(Type,MachB,Prefix),References),
1071		memberchk(Type,[includes,extends]).
1072
1073		% lookup_pattern/2:
1074		% To enable a fast lookup of values in a state, we have to sort the variables.
1075		% On the other hand, we must not sort the variables when storing them, their order
1076		% is significant.
1077		% This predicate generates a "lookup_pattern" that sorts the variables and their
1078		% corresponding values and enables to map the sorted values to the original order
1079		% by a simple unification.
1080		lookup_pattern(Variables,lookup_pattern(SortedVariables,SortedValues,Variables,Values)) :-
1081		maplist(variable_value_pair,Variables,VarValues,Values),
1082		sort(VarValues,SortedVarValues),
1083		maplist(variable_value_pair,SortedVariables,SortedVarValues,SortedValues).
1084		variable_value_pair(I,I/V,V).
1085
1086
1087		% utility for debugging:
1088		:- use_module(tools_io,[safe_open_file/4]).
1089		my_open(File,Mode,St,Opt) :- !, safe_open_file(File,Mode,St,Opt).
1090		my_open(File,Mode,St,Opt) :-
1091		safe_open_file(File,Mode,St,Opt),
1092		formatsilent('Opened file (~w) ~w -> ~w~n',[Mode,File,St]).
1093
1094		my_close(Stream) :- !, close(Stream).
1095		my_close(Stream) :- stream_property(Stream,file_name(F)),!,
1096		formatsilent('Closing ~w -> ~w~n',[F, Stream]),
1097		close(Stream).
1098		my_close(Stream) :-
1099		formatsilent('Closing -> ~w~n',[Stream]),
1100		close(Stream).