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