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