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