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