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