| 1 | % (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
| 2 | % Heinrich Heine Universitaet Duesseldorf | |
| 3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
| 4 | ||
| 5 | :- module(state_space_exploration_modes,[ | |
| 6 | depth_breadth_first_mode/1, | |
| 7 | set_depth_breadth_first_mode/1, reset_depth_breadth_first_mode/0, | |
| 8 | dbf_modes/3, | |
| 9 | is_not_interesting/1, % classifying certain nodes as not interesting | |
| 10 | get_open_node_to_check/2, | |
| 11 | %add_new_visited_expression/6, | |
| 12 | get_id_of_node_and_add_if_required/4, | |
| 13 | compute_hash/3, % maybe we should move this to state_space ? | |
| 14 | compute_heuristic_function_for_state_id/2, | |
| 15 | analyze_hash_collisions/0 | |
| 16 | ]). | |
| 17 | ||
| 18 | :- use_module(state_space). | |
| 19 | :- use_module(error_manager). | |
| 20 | :- use_module(tools). | |
| 21 | :- use_module(debug). | |
| 22 | ||
| 23 | :- use_module(module_information,[module_info/2]). | |
| 24 | :- module_info(group,infrastructure). | |
| 25 | :- module_info(description,'This module groups various techniques for exploring the state space.'). | |
| 26 | ||
| 27 | ||
| 28 | :- dynamic last_step_breadth_first_in_mixed_mode/0. | |
| 29 | reset_state_space_exploration_modes :- retractall(last_step_breadth_first_in_mixed_mode). | |
| 30 | :- use_module(eventhandling,[register_event_listener/3]). | |
| 31 | :- register_event_listener(reset_specification,reset_state_space_exploration_modes, | |
| 32 | 'Reset Model Checker BF/DF Info.'). | |
| 33 | ||
| 34 | ||
| 35 | :- load_files(library(system), [when(compile_time), imports([environ/2])]). | |
| 36 | ||
| 37 | :- dynamic depth_breadth_first_mode/1. | |
| 38 | depth_breadth_first_mode(mixed). | |
| 39 | ||
| 40 | dbf_modes(0,mixed,'Mixed DF/BF'). | |
| 41 | dbf_modes(1,breadth_first,'Breadth First'). | |
| 42 | dbf_modes(2,depth_first,'Depth First'). | |
| 43 | :- if(\+ environ(prob_myheap,false)). | |
| 44 | dbf_modes(3,heuristic,'Heuristic Function / Random'). % Random if no Heuristic Function there | |
| 45 | dbf_modes(4,hash,'Hash-Random'). | |
| 46 | dbf_modes(5,random,'Random'). % not sure this is necessary; Hash-Random seems better ?! | |
| 47 | dbf_modes(6,out_degree_hash,'Out-Degree for Deadlock Checking'). | |
| 48 | %dbf_modes(7,disabled_actions,'Disabled Transitions in State'). | |
| 49 | :- endif. | |
| 50 | ||
| 51 | % provide a few short-cuts for convenience | |
| 52 | dbf_mode_alias(df,depth_first). | |
| 53 | dbf_mode_alias('depth-first',depth_first). | |
| 54 | dbf_mode_alias(bf,breadth_first). | |
| 55 | dbf_mode_alias('breadth-first',breadth_first). | |
| 56 | dbf_mode_alias(out_degree,out_degree_hash). | |
| 57 | dbf_mode_alias(dlk,out_degree_hash). | |
| 58 | %dbf_mode_alias(dis,disabled_actions). | |
| 59 | ||
| 60 | reset_depth_breadth_first_mode :- set_depth_breadth_first_mode(mixed). | |
| 61 | ||
| 62 | set_depth_breadth_first_mode(InMODE) :- | |
| 63 | (dbf_mode_alias(InMODE,MODE) -> true ; MODE = InMODE), | |
| 64 | retractall(depth_breadth_first_mode(_)), | |
| 65 | debug_println(9,depth_breadth_first_mode(MODE)), | |
| 66 | assert(depth_breadth_first_mode(MODE)), | |
| 67 | (dbf_modes(_,MODE,_) -> true ; add_internal_error('Unknown mode: ',set_depth_breadth_first_mode(MODE))). | |
| 68 | ||
| 69 | ||
| 70 | /* ---------------------------------- */ | |
| 71 | /* get_open_node_to_check/2 */ | |
| 72 | /* ---------------------------------- */ | |
| 73 | ||
| 74 | get_open_node_to_check(depth_first,NodeID) :- pop_id_from_front(NodeID). | |
| 75 | get_open_node_to_check(hash,NodeID) :- pop_id_from_front(NodeID). %,print(pop(NodeID)),nl. | |
| 76 | get_open_node_to_check(heuristic,NodeID) :- pop_id_from_front(NodeID). | |
| 77 | get_open_node_to_check(random,NodeID) :- pop_id_from_front(NodeID). | |
| 78 | get_open_node_to_check(out_degree_hash,NodeID) :- pop_id_from_front(NodeID). | |
| 79 | get_open_node_to_check(breadth_first,NodeID) :- pop_id_from_end(NodeID). | |
| 80 | get_open_node_to_check(mixed,NodeID) :- %%depth_breadth_first_mode(DFMODE), | |
| 81 | (random(1,3,1) | |
| 82 | /* random(1,4,1) ==> 33 percent chance of going DF */ | |
| 83 | /* random(1,3,1) ==> 50 percent chance of going DF */ | |
| 84 | /* (random(1,3,1);random(1,3,1)) ==> 75 % chance of going DF */ | |
| 85 | -> retractall(last_step_breadth_first_in_mixed_mode), | |
| 86 | % We are going depth_first | |
| 87 | pop_id_from_front(NodeID) %, print_message(a(NodeID)). | |
| 88 | ; (last_step_breadth_first_in_mixed_mode -> true ; assert(last_step_breadth_first_in_mixed_mode)), | |
| 89 | pop_id_oldest(NodeID) | |
| 90 | ). | |
| 91 | ||
| 92 | ||
| 93 | ||
| 94 | /* ---------------------------------- */ | |
| 95 | /* add_open_node/3 */ | |
| 96 | /* ---------------------------------- */ | |
| 97 | ||
| 98 | ||
| 99 | add_open_node(NodeID,Hash,FromID) :- %print_message(aa(NodeID)), | |
| 100 | (is_not_interesting(NodeID) -> | |
| 101 | asserta(not_interesting(NodeID)) | |
| 102 | ; add_open_node2(NodeID,Hash,FromID) | |
| 103 | ). | |
| 104 | :- use_module(library(terms),[term_size/2]). | |
| 105 | :- use_module(library(random)). | |
| 106 | add_open_node2(NodeID,Hash,FromID) :- %print_message(aa(NodeID)), | |
| 107 | %(b_or_z_mode -> assert(not_invariant_checked(NodeID)) ; true), % is now added when we pop an open node | |
| 108 | (last_step_breadth_first_in_mixed_mode , \+ random(1,8,1) | |
| 109 | -> add_id_at_end(NodeID) /* do not add successor of BF step at top */ | |
| 110 | /* avoids degeneration into BF when large branching factor */ | |
| 111 | ; depth_breadth_first_mode(Mode) -> add_open_node_in_mode(Mode,NodeID,Hash,FromID) | |
| 112 | % add_id_at_front(NodeID) % for default DF/BF behaviour | |
| 113 | ||
| 114 | % add_id_with_weight(NodeID,_Hash) % use hash value | |
| 115 | ||
| 116 | % add_id_random(NodeID) % use a random number | |
| 117 | ||
| 118 | % visited_expression(NodeID,T), term_size(T,Sz), | |
| 119 | % add_id_with_weight(NodeID,Sz) % use term_size as heuristic | |
| 120 | ||
| 121 | % add_id_to_process(NodeID,_Hash,_FromID) % for out_degree as heuristic | |
| 122 | ||
| 123 | %add_id_with_heuristic(NodeID) % for using custom heuristic if possible | |
| 124 | ). | |
| 125 | ||
| 126 | add_open_node_in_mode(breadth_first,NodeID,_Hash,_) :- add_id_at_front(NodeID). | |
| 127 | add_open_node_in_mode(depth_first,NodeID,_Hash,_) :- add_id_at_front(NodeID). | |
| 128 | add_open_node_in_mode(hash,NodeID,Hash,_) :- %print(add(NodeID,Hash)),nl, | |
| 129 | add_id_with_weight(NodeID,Hash). % use Hash as pseudo-random Weight | |
| 130 | add_open_node_in_mode(heuristic,NodeID,_Hash,_) :- add_id_with_heuristic(NodeID). | |
| 131 | add_open_node_in_mode(mixed,NodeID,_Hash,_) :- add_id_at_front(NodeID). | |
| 132 | add_open_node_in_mode(random,NodeID,_Hash,_) :- add_id_random(NodeID). | |
| 133 | add_open_node_in_mode(out_degree_hash,NodeID,Hash,FromID) :- add_id_to_process(NodeID,Hash,FromID). | |
| 134 | % commented out to avoid dependence on pge_algo and because currently not used: | |
| 135 | %add_open_node_in_mode(disabled_actions,NodeID,Hash,_) :- | |
| 136 | % (pge_algo:disabled_operations(NodeID,DisOps,_EnabledOps) -> | |
| 137 | % length(DisOps,Weight), add_id_with_weight(NodeID,Weight) | |
| 138 | % ; otherwise -> add_id_with_weight(NodeID,Hash)). | |
| 139 | ||
| 140 | :- use_module(bmachine,[b_get_machine_heuristic_function/1]). | |
| 141 | :- use_module(specfile,[state_corresponds_to_initialised_b_machine/2, b_or_z_mode/1, animation_mode/1]). | |
| 142 | :- use_module(xtl_interface,[xtl_heuristic_function_result/2, xtl_heuristic_function_active/0]). | |
| 143 | ||
| 144 | add_id_with_heuristic(NodeID) :- %print(adding(NodeID)),nl, | |
| 145 | compute_heuristic_function_for_state_id(NodeID,HRes), | |
| 146 | !, | |
| 147 | (HRes = int(H) | |
| 148 | -> add_id_with_weight(NodeID,H) % , print(added_id_with_weight(NodeID,H)),nl | |
| 149 | ; print_message('*** Illegal HEURISTIC_FUNCTION result (must be INTEGER): '), print_message(HRes), | |
| 150 | add_id_random(NodeID) | |
| 151 | ). | |
| 152 | add_id_with_heuristic(NodeID) :- add_id_random(NodeID). | |
| 153 | ||
| 154 | compute_heuristic_function_for_state_id(NodeID,Value) :- animation_mode(Mode), | |
| 155 | compute_heuristic_function_for_state_id3(Mode,NodeID,Value). | |
| 156 | compute_heuristic_function_for_state_id3(Mode,NodeID,Value) :- | |
| 157 | b_or_z_mode(Mode), !, | |
| 158 | b_get_machine_heuristic_function(HFunction), | |
| 159 | visited_expression(NodeID,State), | |
| 160 | % print(cur_expr(State)),nl, | |
| 161 | state_corresponds_to_initialised_b_machine(State,BState), | |
| 162 | (b_interpreter:b_compute_expression_nowf(HFunction,[],BState,HRes) | |
| 163 | -> Value=HRes | |
| 164 | ; print_message(heuristic_function_failed(NodeID,BState)),fail | |
| 165 | ). | |
| 166 | compute_heuristic_function_for_state_id3(xtl,NodeID,Value) :- !, | |
| 167 | xtl_heuristic_function_active, | |
| 168 | visited_expression(NodeID,State), | |
| 169 | xtl_heuristic_function_result(State,Value). | |
| 170 | ||
| 171 | % ------------------- | |
| 172 | ||
| 173 | :- use_module(bmachine,[b_get_machine_searchscope/1]). | |
| 174 | :- use_module(bsyntaxtree,[create_negation/2]). | |
| 175 | :- use_module(eclipse_interface,[test_boolean_expression_in_node/2]). | |
| 176 | is_not_interesting(NodeID) :- | |
| 177 | b_get_machine_searchscope(Scope), | |
| 178 | %format('Testing SCOPE in ~w~n',[NodeID]), | |
| 179 | preferences:preference(use_scope_predicate,true), | |
| 180 | create_negation(Scope,NotScope), | |
| 181 | eclipse_interface:test_boolean_expression_in_node(NodeID,NotScope). | |
| 182 | ||
| 183 | ||
| 184 | % ----------------------- | |
| 185 | ||
| 186 | ||
| 187 | ||
| 188 | ||
| 189 | /* check whether we have visited a node already: if so return | |
| 190 | id of that node; otherwise generate new id and add node */ | |
| 191 | :- use_module(state_packing,[pack_state/2]). | |
| 192 | get_id_of_node_and_add_if_required(State,ID,Res,FromID) :- | |
| 193 | preferences:preference(symmetry_mode,SymMode), | |
| 194 | % print(computing_hash),nl, | |
| 195 | pack_state(State,PackedState), % TO DO: based on FromID and TransitionID copy unchanged variables if COMPRESSION TRUE | |
| 196 | compute_hash(SymMode,State,PackedState,Hash,Marker), % TO DO: we could use PackedState | |
| 197 | % print_message(hash(Hash)), | |
| 198 | ( packed_expression_already_visited(SymMode,PackedState,Hash,Marker,ID) | |
| 199 | -> Res = exists | |
| 200 | ; Res = new, | |
| 201 | gen_new_state_id(ID), /* gensym('node',ID),*/ | |
| 202 | ||
| 203 | % add_new_visited_expression: | |
| 204 | state_space_packed_add(ID,PackedState), | |
| 205 | add_open_node(ID,Hash,FromID), | |
| 206 | (SymMode=flood -> add_permutations(ID,State) ; true), | |
| 207 | ||
| 208 | assert(hash_to_id(Hash,ID)), | |
| 209 | (SymMode=hash -> assert_id_to_marker(ID,Marker) ; true) | |
| 210 | ). | |
| 211 | ||
| 212 | packed_expression_already_visited(SymMode,_,Hash,_Marker,ID) :- | |
| 213 | (preferences:preference(ignore_hash_collisions,true) ; SymMode=nauty), | |
| 214 | !, hash_to_id(Hash,ID). | |
| 215 | packed_expression_already_visited(hash,_,Hash,Marker,ID) :- Marker \= none,!, | |
| 216 | hash_to_id(Hash,ID),id_to_marker(ID,Marker). | |
| 217 | packed_expression_already_visited(_SymMode,PackedState,Hash,_Marker,ID) :- | |
| 218 | find_hashed_packed_visited_expression(Hash,PackedState,ID). | |
| 219 | ||
| 220 | assert_id_to_marker(ID,Marker) :- | |
| 221 | (Marker = none;preferences:preference(ignore_hash_collisions,true) | |
| 222 | -> true % don't assert marker info if we ignore hash collisions anyway | |
| 223 | ; assert(id_to_marker(ID,Marker)) | |
| 224 | ). | |
| 225 | ||
| 226 | ||
| 227 | % Utilities for Permutation Flooding | |
| 228 | ||
| 229 | ||
| 230 | :- use_module(state_permuter). | |
| 231 | add_permutations(ID,Expression) :- %print(add_permutations(ID,Expression)),nl, | |
| 232 | permute_state(Expression,Perm), Perm \= Expression, | |
| 233 | generate_new_flood_id(Perm,PermID), | |
| 234 | state_space_add(PermID,Perm), | |
| 235 | (preferences:preference(forget_state_space,true) | |
| 236 | -> true ; store_transition(PermID,'*permute*',ID,_)), | |
| 237 | fail. | |
| 238 | add_permutations(_,_). | |
| 239 | ||
| 240 | generate_new_flood_id(State,ID) :- | |
| 241 | pack_state(State,PackedState), | |
| 242 | compute_hash(flood,State,PackedState,Hash,Marker), | |
| 243 | \+ packed_expression_already_visited(flood,PackedState,Hash,Marker,ID), | |
| 244 | gen_new_state_id(ID), | |
| 245 | assert(hash_to_id(Hash,ID)). | |
| 246 | ||
| 247 | ||
| 248 | ||
| 249 | :- use_module(symmetry_marker,[compute_marker_for_state/2]). | |
| 250 | :- use_module(hashing). | |
| 251 | ||
| 252 | ||
| 253 | /* compute_hash(State, HashValue, Marker/SecondHashTerm) */ | |
| 254 | compute_hash(State,Hash,Marker) :- preferences:preference(symmetry_mode,SymMode), | |
| 255 | pack_state(State,PackedState), | |
| 256 | compute_hash(SymMode,State,PackedState,Hash,Marker). | |
| 257 | ||
| 258 | %:- use_module(extension('probhash/probhash')). | |
| 259 | ||
| 260 | compute_hash(off, _,PackedState,Hash,Marker) :- !, Marker=none, | |
| 261 | my_term_hash(PackedState,Hash). %, tools_printing:print_term_summary(Env),nl. | |
| 262 | compute_hash(hash,State,_PackedState,Hash,Marker) :- | |
| 263 | (symmetry_marker:compute_marker_for_state(State,HMarker) | |
| 264 | -> HMarker=Marker | |
| 265 | %raw_sha_hash(HMarker,Marker) | |
| 266 | ; print(compute_marker_failed(State)),nl,fail), | |
| 267 | my_term_hash(Marker,Hash),!. | |
| 268 | compute_hash(nauty,State,_PackedState,Hash,Marker) :- !, Marker=none, | |
| 269 | my_term_hash(State,EnvHash), | |
| 270 | (hash_to_nauty_id(EnvHash,NautyID), hash_to_id(NautyID,RealID), | |
| 271 | visited_expression(RealID,State) | |
| 272 | -> %% print(exact_state_exists(EnvHash,NautyID,State)),nl, %% | |
| 273 | % the exact same state already exists; no need to compute normal form | |
| 274 | Hash=NautyID | |
| 275 | ; (graph_canon:add_state_graph_to_nauty(State,Exists) | |
| 276 | -> true | |
| 277 | ; add_error(compute_hash,'Failed: ',add_state_graph_to_nauty(State,Exists), Exists=1) | |
| 278 | ), | |
| 279 | (Exists>0 -> Hash=Exists | |
| 280 | ; /* new node */ Hash is -Exists, assert(hash_to_nauty_id(EnvHash,Hash))) | |
| 281 | ), | |
| 282 | % print(nauty_add(Exists,Hash,State)),nl, | |
| 283 | Marker=none. | |
| 284 | % my_term_hash now uses if_var(ignore) option of SICStus 4.1; no longer need to check ground | |
| 285 | compute_hash(_, _Env,PackedState,Hash,none) :- my_term_hash(PackedState,Hash). | |
| 286 | ||
| 287 | ||
| 288 | % -------------------------------------------- | |
| 289 | ||
| 290 | % some utilities to analyse state space: | |
| 291 | ||
| 292 | hash_collision(ID,ID2,S1,S2) :- | |
| 293 | hash_to_id(Hash,ID), | |
| 294 | hash_to_id(Hash,ID2), ID2 \= root, (ID=root->true; ID2>ID), | |
| 295 | visited_expression(ID,S1), | |
| 296 | %print((ID,S1)),nl, | |
| 297 | visited_expression(ID2,S2), | |
| 298 | %print((ID2,S2)),nl, | |
| 299 | nl. | |
| 300 | ||
| 301 | :- dynamic hash_collision/2. % hash_collision(NrStatesWithSameHash, NrOfSuchClusters) | |
| 302 | analyze_hash_collisions :- retractall(hash_collision(_,_)), | |
| 303 | print('Analyzing Hash Collisions'),nl, | |
| 304 | hash_to_id(Hash,ID), | |
| 305 | \+ (hash_to_id(Hash,ID2), ID2 @< ID), | |
| 306 | findall(X,hash_to_id(Hash,X),L), | |
| 307 | length(L,Nr), | |
| 308 | (retract(hash_collision(Nr,C)) | |
| 309 | -> (C1 is C+1, assert(hash_collision(Nr,C1))) | |
| 310 | ; assert(hash_collision(Nr,1)) | |
| 311 | ),fail. | |
| 312 | analyze_hash_collisions :- | |
| 313 | print('Hash Collision Distribution (1=no collision): '), | |
| 314 | findall((Nr,X),hash_collision(Nr,X),Coll), | |
| 315 | sort(Coll,SC), | |
| 316 | print(SC),nl, | |
| 317 | (hash_collision(ID,ID2,S1,S2) -> | |
| 318 | print('SAMPLE COLLISION: '),nl, | |
| 319 | print(ID),nl,print(S1),nl, print_hash_info(S1), | |
| 320 | print(ID2),nl,print(S2),nl,print_hash_info(S2) | |
| 321 | ; print('NO COLLISIONS') | |
| 322 | ),nl. | |
| 323 | ||
| 324 | ||
| 325 | %ac :- analyse_collision([range(smallint),depth(infinite)]). % Runtime: 3890 ms | |
| 326 | %ac0 :- analyse_collision([range(smallint),algorithm(sdbm),depth(infinite)]). % Runtime: 3760 ms | |
| 327 | %ac1 :- analyse_collision([range(infinite),algorithm(sdbm),depth(infinite)]). % Runtime: 3730 ms | |
| 328 | %ac2 :- analyse_collision([range(infinite),algorithm(hsieh),depth(infinite)]). % Runtime: 3970 ms | |
| 329 | %ac3 :- analyse_collision([range(infinite),algorithm(jenkins),depth(infinite)]). % Runtime: 3970 ms | |
| 330 | %ac4 :- analyse_collision([]). % Runtime: 3720 ms | |
| 331 | %analyse_collision(Options) :- retractall(hash_collision(_,_)), | |
| 332 | % statistics(runtime,[_,_]), | |
| 333 | % prolog_flag(max_tagged_integer,Max), | |
| 334 | % prolog_flag(min_tagged_integer,Min), | |
| 335 | % visited_expression(ID,B), | |
| 336 | % term_hash(B,Options,HashB), % | |
| 337 | % %super_hash(B,HashB), % | |
| 338 | % ((HashB>=Min, HashB =< Max) -> true ; print('*** HASH NOT GOOD FOR INDEXING: '), print(ID),nl), | |
| 339 | % (hash_collision(HashB,OtherID) | |
| 340 | % -> print('COLLISION : '), print(ID), print(' <-> '), print(OtherID), print(' : '), print(HashB),nl | |
| 341 | % ; assert(hash_collision(HashB,ID)) | |
| 342 | % ),fail. | |
| 343 | %analyse_collision(_Options) :- | |
| 344 | % statistics(runtime,[_,T]), print('Runtime: '), print(T), print(' ms'). | |
| 345 | ||
| 346 | ||
| 347 | :- use_module(library(terms),[term_hash/2]). | |
| 348 | print_hash_info(S1) :- | |
| 349 | %env_hash(S1,EH1), print(env_hash(EH1)),nl, | |
| 350 | my_term_hash(S1,MTH1), print(my_term_hash(MTH1)),nl, | |
| 351 | term_hash(S1,TH1), print(sicstus_term_hash(TH1)),nl. | |
| 352 | ||
| 353 | :- use_module(library(lists),[maplist/2]). | |
| 354 | :- public print_current_state_term_sizes/0. | |
| 355 | print_current_state_term_sizes :- | |
| 356 | current_expression(ID,State), %expanded | |
| 357 | state_corresponds_to_initialised_b_machine(State,BState), | |
| 358 | format('Term Sizes of variables and constants in current state: ~w~n',[ID]), | |
| 359 | findall( TS/Var, (member(bind(Var,Term),BState), | |
| 360 | term_size(Term,TS)), List), | |
| 361 | sort(List,SL), | |
| 362 | maplist(print_ts,SL). | |
| 363 | ||
| 364 | print_ts(TS/Var) :- format('~w : ~w~n',[Var,TS]). | |
| 365 | ||
| 366 | % -------------------------------------------- |