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