1		% (c) 2009-2024 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/6,
13		compute_hash/3, % maybe we should move this to state_space ?
14		compute_heuristic_function_for_state_id/2,
15		heuristic_function_active/0,
16		analyze_hash_collisions/0,
17		get_current_breadth_first_level/1
18		]).
19
20		:- use_module(state_space).
21		:- use_module(error_manager).
22		:- use_module(tools).
23		:- use_module(debug).
24
25		:- use_module(module_information,[module_info/2]).
26		:- module_info(group,state_space).
27		:- module_info(description,'This module groups various techniques for exploring the state space.').
28
29
30		:- dynamic b_op_sorted_unchanged_vars/2. % for incremental state packing
31		reset_state_space_exploration_modes :-
32		bb_put(last_step_breadth_first_in_mixed_mode,false),
33		(bb_delete(bf_level,_) -> true ; true),
34		(bb_delete(last_id_of_current_level,_) -> true ; true),
35		retractall(b_op_sorted_unchanged_vars(_,_)).
36
37		:- use_module(eventhandling,[register_event_listener/3]).
38		:- register_event_listener(reset_specification,reset_state_space_exploration_modes,
39		'Reset Model Checker BF/DF Info.').
40		:- register_event_listener(reset_prob,reset_state_space_exploration_modes,
41		'Reset Model Checker BF/DF Info.').
42
43
44		:- load_files(library(system), [when(compile_time), imports([environ/2])]).
45
46		:- dynamic depth_breadth_first_mode/1.
47		depth_breadth_first_mode(mixed).
48
49		dbf_modes(0,mixed,'Mixed DF/BF').
50		dbf_modes(1,breadth_first,'Breadth First').
51		dbf_modes(2,depth_first,'Depth First').
52		:- if(\+ environ(prob_myheap,false)).
53		dbf_modes(3,heuristic,'Heuristic Function / Random'). % Random if no Heuristic Function there
54		dbf_modes(4,hash,'Hash-Random').
55		dbf_modes(5,random,'Random'). % not sure this is necessary; Hash-Random seems better ?!
56		dbf_modes(6,out_degree_hash,'Out-Degree for Deadlock Checking').
57		dbf_modes(7,term_size,'Term-Size (smaller states first)'). % can be useful if some variables grow unboundedly
58		%dbf_modes(8,disabled_actions,'Disabled Transitions in State').
59		:- endif.
60
61		% provide a few short-cuts for convenience
62		dbf_mode_alias(df,depth_first).
63		dbf_mode_alias('depth-first',depth_first).
64		dbf_mode_alias(bf,breadth_first).
65		dbf_mode_alias('breadth-first',breadth_first).
66		dbf_mode_alias(out_degree,out_degree_hash).
67		dbf_mode_alias(dlk,out_degree_hash).
68		dbf_mode_alias(size,term_size).
69		%dbf_mode_alias(dis,disabled_actions).
70
71		reset_depth_breadth_first_mode :- set_depth_breadth_first_mode(mixed).
72
73		:- register_event_listener(startup_prob,reset_depth_breadth_first_mode,
74		'Reset Depth/Breadth-First Mode to mixed').
75
76		set_depth_breadth_first_mode(InMODE) :-
77		(dbf_mode_alias(InMODE,MODE) -> true ; MODE = InMODE),
78		(retract(depth_breadth_first_mode(_)) -> true ; true),
79		debug_println(9,depth_breadth_first_mode(MODE)),
80		assertz(depth_breadth_first_mode(MODE)),
81	?	(dbf_modes(_,MODE,_) -> true ; add_internal_error('Unknown mode: ',set_depth_breadth_first_mode(MODE))).
82
83
84		/* ---------------------------------- */
85		/* get_open_node_to_check/2 */
86		/* ---------------------------------- */
87
88		get_open_node_to_check(depth_first,NodeID) :- pop_id_from_front(NodeID).
89		get_open_node_to_check(hash,NodeID) :- pop_id_from_front(NodeID). %,print(pop(NodeID)),nl.
90		get_open_node_to_check(heuristic,NodeID) :- pop_id_from_front(NodeID).
91		get_open_node_to_check(random,NodeID) :- pop_id_from_front(NodeID).
92		get_open_node_to_check(out_degree_hash,NodeID) :- pop_id_from_front(NodeID).
93		get_open_node_to_check(term_size,NodeID) :- pop_id_from_front(NodeID).
94		get_open_node_to_check(breadth_first,NodeID) :- % TODO: keep track of levels, e.g., by pushing -1 add_id_at_front(-1) and increasing level when -1 popped
95		pop_id_from_end(NodeID),
96		update_breadth_first_level(NodeID).
97		get_open_node_to_check(mixed,NodeID) :- %%depth_breadth_first_mode(DFMODE),
98		(random(1,3,1)
99		/* random(1,4,1) ==> 33 percent chance of going DF */
100		/* random(1,3,1) ==> 50 percent chance of going DF */
101		/* (random(1,3,1);random(1,3,1)) ==> 75 % chance of going DF */
102		-> bb_put(last_step_breadth_first_in_mixed_mode,false),
103		% We are going depth_first
104		pop_id_from_front(NodeID) %, print_message(a(NodeID)).
105		; bb_put(last_step_breadth_first_in_mixed_mode,true),
106		pop_id_oldest(NodeID)
107		).
108
109		% will currently only succeed if we perform model checking with pure breadth-first
110		get_current_breadth_first_level(Level) :- bb_get(bf_level,Level).
111
112		% update the breadth-first traversal level; assumes we only use breadth_first steps
113		update_breadth_first_level(NodeID) :- bb_get(last_id_of_current_level,ID),!,
114		(ID=NodeID -> bb_delete(last_id_of_current_level,_) ; true).
115		update_breadth_first_level(_) :- % we have no last_id stored
116		increase_bf_level.
117
118		increase_bf_level :-
119		(bb_get(bf_level,Level)
120		-> L1 is Level+1, bb_put(bf_level,L1),
121		debug_format(19,'*** Starting breadth-first level: ~w~n',[L1])
122		; bb_put(bf_level,1)
123		),
124		% myheap:myheap_portray, flush_output,
125		(top_front_id(NextLevelID)
126		-> bb_put(last_id_of_current_level,NextLevelID), % the new level will be finished when we process this node
127		debug_format(9,'*** Next level will be finished after node: ~w~n',[NextLevelID])
128		; % the popped id was the only node of the current level, at the next pop we will increase level again
129		debug_format(9,'*** Next level will be finished after this node !~n',[])
130		).
131
132
133		/* ---------------------------------- */
134		/* add_open_node/3 */
135		/* ---------------------------------- */
136
137
138		add_open_node(NodeID,Hash,FromID) :- %print_message(aa(NodeID)),
139		(is_not_interesting(NodeID) ->
140		mark_as_not_interesting(NodeID)
141		; add_open_node2(NodeID,Hash,FromID)
142		).
143		:- use_module(library(terms),[term_size/2]).
144		:- use_module(library(random)).
145		add_open_node2(NodeID,Hash,FromID) :- %print_message(aa(NodeID)),
146		%(b_or_z_mode -> assertz(not_invariant_checked(NodeID)) ; true), % is now added when we pop an open node
147		(bb_get(last_step_breadth_first_in_mixed_mode,true) , \+ random(1,8,1)
148		-> add_id_at_end(NodeID) /* do not add successor of BF step at top */
149		/* avoids degeneration into BF when large branching factor */
150		; depth_breadth_first_mode(Mode) -> add_open_node_in_mode(Mode,NodeID,Hash,FromID)
151		% add_id_at_front(NodeID) % for default DF/BF behaviour
152
153		% add_id_with_weight(NodeID,_Hash) % use hash value
154
155		% add_id_random(NodeID) % use a random number
156
157		% visited_expression(NodeID,T), term_size(T,Sz),
158		% add_id_with_weight(NodeID,Sz) % use term_size as heuristic
159
160		% add_id_to_process(NodeID,_Hash,_FromID) % for out_degree as heuristic
161
162		%add_id_with_heuristic(NodeID) % for using custom heuristic if possible
163		).
164
165		:- use_module(library(terms), [term_size/2]).
166		add_open_node_in_mode(breadth_first,NodeID,_Hash,_) :- add_id_at_front(NodeID).
167		add_open_node_in_mode(depth_first,NodeID,_Hash,_) :- add_id_at_front(NodeID).
168		add_open_node_in_mode(hash,NodeID,Hash,_) :- %print(add(NodeID,Hash)),nl,
169		add_id_with_weight(NodeID,Hash). % use Hash as pseudo-random Weight
170		add_open_node_in_mode(heuristic,NodeID,_Hash,_) :- add_id_with_heuristic(NodeID).
171		add_open_node_in_mode(mixed,NodeID,_Hash,_) :- add_id_at_front(NodeID).
172		add_open_node_in_mode(random,NodeID,_Hash,_) :- add_id_random(NodeID).
173		add_open_node_in_mode(out_degree_hash,NodeID,Hash,FromID) :- add_id_to_process(NodeID,Hash,FromID).
174		add_open_node_in_mode(term_size,NodeID,_,_) :-
175		(state_space:packed_visited_expression(NodeID,PV) -> term_size(PV,Weight)
176		; add_error(add_open_node_in_mode,'Unknown state:',NodeID), Weight=1),
177		add_id_with_weight(NodeID,Weight).
178		% commented out to avoid dependence on pge_algo and because currently not used:
179		%add_open_node_in_mode(disabled_actions,NodeID,Hash,_) :-
180		% (pge_algo:disabled_operations(NodeID,DisOps,_EnabledOps) ->
181		% length(DisOps,Weight), add_id_with_weight(NodeID,Weight)
182		% ; add_id_with_weight(NodeID,Hash)).
183
184		:- use_module(bmachine,[b_get_machine_heuristic_function/1]).
185		:- use_module(specfile,[state_corresponds_to_initialised_b_machine/2, b_or_z_mode/0, b_or_z_mode/1, animation_mode/1]).
186		:- use_module(xtl_interface,[xtl_heuristic_function_result/2, xtl_heuristic_function_active/0]).
187
188		% Nodes with the smallest value of HEURISTIC_FUNCTION will be treated first
189		add_id_with_heuristic(NodeID) :- %print(adding(NodeID)),nl,
190		compute_heuristic_function_for_state_id(NodeID,HRes),
191		!,
192		(HRes = int(H)
193		-> add_id_with_weight(NodeID,H) % , print(added_id_with_weight(NodeID,H)),nl
194		; print_message('*** Illegal HEURISTIC_FUNCTION result (must be INTEGER): '), print_message(HRes),
195		add_id_random(NodeID)
196		).
197		add_id_with_heuristic(NodeID) :- add_id_random(NodeID).
198
199		compute_heuristic_function_for_state_id(NodeID,Value) :- animation_mode(Mode),
200		compute_heuristic_function_for_state_id3(Mode,NodeID,Value).
201		compute_heuristic_function_for_state_id3(Mode,NodeID,Value) :-
202		b_or_z_mode(Mode), !,
203		b_get_machine_heuristic_function(HFunction),
204		visited_expression(NodeID,State),
205		% print(cur_expr(State)),nl,
206		state_corresponds_to_initialised_b_machine(State,BState),
207		(b_interpreter:b_compute_expression_nowf(HFunction,[],BState,HRes,'HEURISTIC_FUNCTION',NodeID)
208		-> Value=HRes
209		; print_message(heuristic_function_failed(NodeID,BState)),fail
210		).
211		compute_heuristic_function_for_state_id3(xtl,NodeID,Value) :- !,
212		xtl_heuristic_function_active,
213		visited_expression(NodeID,State),
214		xtl_heuristic_function_result(State,Value).
215
216		heuristic_function_active :-
217		b_or_z_mode, !,
218		b_get_machine_heuristic_function(_).
219		heuristic_function_active :- xtl_heuristic_function_active.
220
221		% -------------------
222
223		:- use_module(bmachine,[b_get_machine_searchscope/1]).
224		:- use_module(bsyntaxtree,[create_negation/2]).
225		:- use_module(eclipse_interface,[test_boolean_expression_in_node/3]).
226
227		%is_not_interesting(NodeID) :- try_compute_depth_of_state_id(NodeID,Depth), Depth>12. % comment in to set a depth-limit
228		is_not_interesting(NodeID) :-
229		b_get_machine_searchscope(Scope),
230		%format('Testing SCOPE in ~w~n',[NodeID]),
231		preferences:preference(use_scope_predicate,true),
232		create_negation(Scope,NotScope),
233		test_boolean_expression_in_node(NodeID,NotScope,'SCOPE').
234
235
236		% -----------------------
237
238
239		/* check whether we have visited a node already: if so return
240		id of that node; otherwise generate new id and add node */
241		:- use_module(state_packing,[pack_state/2, incremental_pack_state/4]).
242		get_id_of_node_and_add_if_required(State,ID,Res,FromID,OpName,PrecomputedInfos) :-
243		preferences:preference(symmetry_mode,SymMode),
244		% print(computing_hash(FromID,PrecomputedInfos)),nl,
245		try_incremental_pack_state(PrecomputedInfos,FromID,OpName,State,PackedState),
246		compute_hash(SymMode,State,PackedState,Hash,Marker), % TO DO: we could use PackedState
247		% print_message(hash(Hash)),
248		( packed_expression_already_visited(SymMode,PackedState,Hash,Marker,ID)
249		-> Res = exists
250		; Res = new,
251		gen_new_state_id(ID),
252		%register_back_edge(ID,FromID), % comment in to register back_edges, seems to add 250MB for 1 million states
253		% add_new_visited_expression:
254		state_space_packed_add(ID,PackedState),
255		add_open_node(ID,Hash,FromID),
256		(SymMode=flood -> add_permutations(ID,State) ; true),
257		assertz(hash_to_id(Hash,ID)),
258		(SymMode=hash -> assert_id_to_marker(ID,Marker) ; true)
259		).
260
261
262		try_incremental_pack_state([packed_state/PS|_],_FromID,OpName,State,PackedState) :-
263		% TO DO: currently the packed_state is only provided in operation_reuse full and B mode; maybe useful more generally
264		b_get_sorted_unchanged_variables(OpName,State,Unchanged),
265		!,
266		(incremental_pack_state(State,PS,Unchanged,PackedState) -> true
267		; add_internal_error('Incremental state packing failed:',incremental_pack_state(State,PS,Unchanged,PackedState)),
268		fail
269		).
270		try_incremental_pack_state(_,_,_,State,PackedState) :- pack_state(State,PackedState).
271
272		:- use_module(library(lists),[maplist/3, include/3]).
273		:- use_module(library(avl),[ord_list_to_avl/2, avl_fetch/2]).
274		:- use_module(bmachine,[b_get_operation_unchanged_variables/2]).
275		:- use_module(specfile,[extract_variables_from_state/2]).
276		% sort Unchanged variables in the order in which they appear in the store
277		b_get_sorted_unchanged_variables(OpName,_,SortedUnchanged) :-
278		b_op_sorted_unchanged_vars(OpName,R),!, SortedUnchanged=R.
279		b_get_sorted_unchanged_variables(OpName,State,SortedUnchanged) :-
280		(b_get_operation_unchanged_variables(OpName,Unchanged),
281		maplist(gen_key_val,Unchanged,U2),
282		ord_list_to_avl(U2,UnchangedAVL),
283		extract_variables_from_state(State,Vars),
284		include(is_unchanged(UnchangedAVL),Vars,UBVars),
285		maplist(get_var,UBVars,UVars) % just get the variable names
286		-> true
287		; add_internal_error('Could not sort unchanged vars: ',b_get_sorted_unchanged_variables(OpName,State,_)),
288		UVars=[]),
289		assertz(b_op_sorted_unchanged_vars(OpName,UVars)),
290		SortedUnchanged=UVars.
291
292		gen_key_val(Key,Key-true).
293		is_unchanged(UnchangedAVL,bind(Var,_)) :- avl_fetch(Var,UnchangedAVL).
294
295		get_var(bind(Var,_),Var).
296
297
298		% ------------------------------
299
300		packed_expression_already_visited(SymMode,_,Hash,_Marker,ID) :-
301		(preferences:preference(ignore_hash_collisions,true) ; SymMode=nauty),
302		!, hash_to_id(Hash,ID).
303		packed_expression_already_visited(hash,_,Hash,Marker,ID) :- Marker \= none,!,
304		hash_to_id(Hash,ID),id_to_marker(ID,Marker).
305		packed_expression_already_visited(_SymMode,PackedState,Hash,_Marker,ID) :-
306		find_hashed_packed_visited_expression(Hash,PackedState,ID).
307
308		assert_id_to_marker(ID,Marker) :-
309		((Marker = none ; preferences:preference(ignore_hash_collisions,true))
310		-> true % don't assert marker info if we ignore hash collisions anyway
311		; assertz(id_to_marker(ID,Marker))
312		).
313
314
315		% Utilities for Permutation Flooding
316
317
318		:- use_module(symsrc(state_permuter),[permute_state/2]).
319		add_permutations(ID,Expression) :- %print(add_permutations(ID,Expression)),nl,
320		permute_state(Expression,Perm), Perm \= Expression,
321		generate_new_flood_id(Perm,PermID),
322		state_space_add(PermID,Perm),
323		(preferences:preference(forget_state_space,true)
324		-> true ; store_transition(PermID,'*permute*',ID,_)),
325		fail.
326		add_permutations(_,_).
327
328		generate_new_flood_id(State,ID) :-
329		pack_state(State,PackedState),
330		compute_hash(flood,State,PackedState,Hash,Marker),
331		\+ packed_expression_already_visited(flood,PackedState,Hash,Marker,ID),
332		gen_new_state_id(ID),
333		assertz(hash_to_id(Hash,ID)).
334
335
336
337		:- use_module(symsrc(symmetry_marker),[compute_marker_for_state/2]).
338		:- use_module(hashing).
339
340
341		/* compute_hash(State, HashValue, Marker/SecondHashTerm) */
342		compute_hash(State,Hash,Marker) :- preferences:preference(symmetry_mode,SymMode),
343		pack_state(State,PackedState),
344		compute_hash(SymMode,State,PackedState,Hash,Marker).
345
346		%:- use_module(extension('probhash/probhash'),[raw_sha_hash/2]).
347		:- use_module(symsrc(graph_iso_nauty), [add_state_graph_to_nauty/2]).
348
349		compute_hash(off, _,PackedState,Hash,Marker) :- !, Marker=none,
350		my_term_hash(PackedState,Hash). %, tools_printing:print_term_summary(Env),nl.
351		compute_hash(hash,State,_PackedState,Hash,Marker) :-
352		(compute_marker_for_state(State,HMarker)
353		-> HMarker=Marker
354		%raw_sha_hash(HMarker,Marker)
355		; print(compute_marker_failed(State)),nl,fail),
356		my_term_hash(Marker,Hash),!.
357		compute_hash(nauty,State,_PackedState,Hash,Marker) :- !, Marker=none,
358		my_term_hash(State,EnvHash),
359		(hash_to_nauty_id(EnvHash,NautyID), hash_to_id(NautyID,RealID),
360		visited_expression(RealID,State)
361		-> %% print(exact_state_exists(EnvHash,NautyID,State)),nl, %%
362		% the exact same state already exists; no need to compute normal form
363		Hash=NautyID
364		; (add_state_graph_to_nauty(State,Exists)
365		-> true
366		; add_error(compute_hash,'Failed: ',add_state_graph_to_nauty(State,Exists), Exists=1)
367		),
368		(Exists>0 -> Hash=Exists
369		; /* new node */ Hash is -Exists, assertz(hash_to_nauty_id(EnvHash,Hash)))
370		),
371		% print(nauty_add(Exists,Hash,State)),nl,
372		Marker=none.
373		% my_term_hash now uses if_var(ignore) option of SICStus 4.1; no longer need to check ground
374		compute_hash(_, _Env,PackedState,Hash,none) :- my_term_hash(PackedState,Hash).
375
376
377		% --------------------------------------------
378
379		% some utilities to analyse state space:
380
381		hash_collision(ID,ID2,S1,S2) :-
382		hash_to_id(Hash,ID),
383		hash_to_id(Hash,ID2), ID2 \= root, (ID=root->true; ID2>ID),
384		visited_expression(ID,S1),
385		%print((ID,S1)),nl,
386		visited_expression(ID2,S2),
387		%print((ID2,S2)),nl,
388		nl.
389
390		:- dynamic hash_collision/2. % hash_collision(NrStatesWithSameHash, NrOfSuchClusters)
391		analyze_hash_collisions :- retractall(hash_collision(_,_)),
392		print('Analyzing Hash Collisions'),nl,
393		hash_to_id(Hash,ID),
394		\+ (hash_to_id(Hash,ID2), ID2 @< ID),
395		findall(X,hash_to_id(Hash,X),L),
396		length(L,Nr),
397		(retract(hash_collision(Nr,C))
398		-> (C1 is C+1, assertz(hash_collision(Nr,C1)))
399		; assertz(hash_collision(Nr,1))
400		),fail.
401		analyze_hash_collisions :-
402		print('Hash Collision Distribution (1=no collision): '),
403		findall((Nr,X),hash_collision(Nr,X),Coll),
404		sort(Coll,SC),
405		print(SC),nl,
406		(hash_collision(ID,ID2,S1,S2) ->
407		print('SAMPLE COLLISION: '),nl,
408		print(ID),nl,print(S1),nl, print_hash_info(S1),
409		print(ID2),nl,print(S2),nl,print_hash_info(S2)
410		; print('NO COLLISIONS')
411		),nl.
412
413
414		%ac :- analyse_collision([range(smallint),depth(infinite)]). % Runtime: 3890 ms
415		%ac0 :- analyse_collision([range(smallint),algorithm(sdbm),depth(infinite)]). % Runtime: 3760 ms
416		%ac1 :- analyse_collision([range(infinite),algorithm(sdbm),depth(infinite)]). % Runtime: 3730 ms
417		%ac2 :- analyse_collision([range(infinite),algorithm(hsieh),depth(infinite)]). % Runtime: 3970 ms
418		%ac3 :- analyse_collision([range(infinite),algorithm(jenkins),depth(infinite)]). % Runtime: 3970 ms
419		%ac4 :- analyse_collision([]). % Runtime: 3720 ms
420		%analyse_collision(Options) :- retractall(hash_collision(_,_)),
421		% statistics(runtime,[_,_]),
422		% current_prolog_flag(max_tagged_integer,Max),
423		% current_prolog_flag(min_tagged_integer,Min),
424		% visited_expression(ID,B),
425		% term_hash(B,Options,HashB), %
426		% %super_hash(B,HashB), %
427		% ((HashB>=Min, HashB =< Max) -> true ; print('*** HASH NOT GOOD FOR INDEXING: '), print(ID),nl),
428		% (hash_collision(HashB,OtherID)
429		% -> print('COLLISION : '), print(ID), print(' <-> '), print(OtherID), print(' : '), print(HashB),nl
430		% ; assertz(hash_collision(HashB,ID))
431		% ),fail.
432		%analyse_collision(_Options) :-
433		% statistics(runtime,[_,T]), print('Runtime: '), print(T), print(' ms').
434
435
436		:- use_module(library(terms),[term_hash/2]).
437		print_hash_info(S1) :-
438		%env_hash(S1,EH1), print(env_hash(EH1)),nl,
439		my_term_hash(S1,MTH1), print(my_term_hash(MTH1)),nl,
440		term_hash(S1,TH1), print(sicstus_term_hash(TH1)),nl.
441
442		:- use_module(library(lists),[maplist/2]).
443		:- public print_current_state_term_sizes/0.
444		print_current_state_term_sizes :-
445		current_expression(ID,State), %expanded
446		state_corresponds_to_initialised_b_machine(State,BState),
447		format('Term Sizes of variables and constants in current state: ~w~n',[ID]),
448		findall( TS/Var, (member(bind(Var,Term),BState),
449		term_size(Term,TS)), List),
450		sort(List,SL),
451		maplist(print_ts,SL).
452
453		print_ts(TS/Var) :- format('~w : ~w~n',[Var,TS]).
454
455		% --------------------------------------------