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