1		% (c) 2009-2025 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(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_or_z_mode,
230		b_get_machine_searchscope(Scope),
231		%format('Testing SCOPE in ~w~n',[NodeID]),
232		preferences:preference(use_scope_predicate,true),
233		create_negation(Scope,NotScope),
234		test_boolean_expression_in_node(NodeID,NotScope,'SCOPE').
235
236
237		% -----------------------
238
239
240		/* check whether we have visited a node already: if so return
241		id of that node; otherwise generate new id and add node */
242		:- use_module(state_packing,[pack_state/2, incremental_pack_state/4]).
243		get_id_of_node_and_add_if_required(State,ID,Res,FromID,OpName,PrecomputedInfos) :-
244		preferences:preference(symmetry_mode,SymMode),
245		% print(computing_hash(FromID,PrecomputedInfos)),nl,
246		try_incremental_pack_state(PrecomputedInfos,FromID,OpName,State,PackedState),
247		compute_hash(SymMode,State,PackedState,Hash,Marker), % TO DO: we could use PackedState
248		% print_message(hash(Hash)),
249		( packed_expression_already_visited(SymMode,PackedState,Hash,Marker,ID)
250		-> Res = exists
251		; Res = new,
252		gen_new_state_id(ID),
253		%register_back_edge(ID,FromID), % comment in to register back_edges, seems to add 250MB for 1 million states
254		% add_new_visited_expression:
255		state_space_packed_add(ID,PackedState),
256		add_open_node(ID,Hash,FromID),
257		(SymMode=flood -> add_permutations(ID,State) ; true),
258		assertz(hash_to_id(Hash,ID)),
259		(SymMode=hash -> assert_id_to_marker(ID,Marker) ; true)
260		).
261
262
263		try_incremental_pack_state([packed_state/PS|_],_FromID,OpName,State,PackedState) :-
264		% TO DO: currently the packed_state is only provided in operation_reuse full and B mode; maybe useful more generally
265		b_get_sorted_unchanged_variables(OpName,State,Unchanged),
266		!,
267		(incremental_pack_state(State,PS,Unchanged,PackedState) -> true
268		; add_internal_error('Incremental state packing failed:',incremental_pack_state(State,PS,Unchanged,PackedState)),
269		fail
270		).
271		try_incremental_pack_state(_,_,_,State,PackedState) :- pack_state(State,PackedState).
272
273		:- use_module(library(lists),[maplist/3, include/3]).
274		:- use_module(library(avl),[ord_list_to_avl/2, avl_fetch/2]).
275		:- use_module(bmachine,[b_get_operation_unchanged_variables/2]).
276		:- use_module(specfile,[extract_variables_from_state/2]).
277		% sort Unchanged variables in the order in which they appear in the store
278		b_get_sorted_unchanged_variables(OpName,_,SortedUnchanged) :-
279		b_op_sorted_unchanged_vars(OpName,R),!, SortedUnchanged=R.
280		b_get_sorted_unchanged_variables(OpName,State,SortedUnchanged) :-
281		(b_get_operation_unchanged_variables(OpName,Unchanged),
282		maplist(gen_key_val,Unchanged,U2),
283		ord_list_to_avl(U2,UnchangedAVL),
284		extract_variables_from_state(State,Vars),
285		include(is_unchanged(UnchangedAVL),Vars,UBVars),
286		maplist(get_var,UBVars,UVars) % just get the variable names
287		-> true
288		; add_internal_error('Could not sort unchanged vars: ',b_get_sorted_unchanged_variables(OpName,State,_)),
289		UVars=[]),
290		assertz(b_op_sorted_unchanged_vars(OpName,UVars)),
291		SortedUnchanged=UVars.
292
293		gen_key_val(Key,Key-true).
294		is_unchanged(UnchangedAVL,bind(Var,_)) :- avl_fetch(Var,UnchangedAVL).
295
296		get_var(bind(Var,_),Var).
297
298
299		% ------------------------------
300
301		packed_expression_already_visited(SymMode,_,Hash,_Marker,ID) :-
302		(preferences:preference(ignore_hash_collisions,true) ; SymMode=nauty),
303		!, hash_to_id(Hash,ID).
304		packed_expression_already_visited(hash,_,Hash,Marker,ID) :- Marker \= none,!,
305		hash_to_id(Hash,ID),id_to_marker(ID,Marker).
306		packed_expression_already_visited(_SymMode,PackedState,Hash,_Marker,ID) :-
307		find_hashed_packed_visited_expression(Hash,PackedState,ID).
308
309		assert_id_to_marker(ID,Marker) :-
310		((Marker = none ; preferences:preference(ignore_hash_collisions,true))
311		-> true % don't assert marker info if we ignore hash collisions anyway
312		; assertz(id_to_marker(ID,Marker))
313		).
314
315
316		% Utilities for Permutation Flooding
317
318
319		:- use_module(symsrc(state_permuter),[permute_state/2]).
320		add_permutations(ID,Expression) :- %print(add_permutations(ID,Expression)),nl,
321		permute_state(Expression,Perm), Perm \= Expression,
322		generate_new_flood_id(Perm,PermID),
323		state_space_add(PermID,Perm),
324		(preferences:preference(forget_state_space,true)
325		-> true ; store_transition(PermID,'*permute*',ID,_)),
326		fail.
327		add_permutations(_,_).
328
329		generate_new_flood_id(State,ID) :-
330		pack_state(State,PackedState),
331		compute_hash(flood,State,PackedState,Hash,Marker),
332		\+ packed_expression_already_visited(flood,PackedState,Hash,Marker,ID),
333		gen_new_state_id(ID),
334		assertz(hash_to_id(Hash,ID)).
335
336
337
338		:- use_module(symsrc(symmetry_marker),[compute_marker_for_state/2]).
339		:- use_module(hashing).
340
341
342		/* compute_hash(State, HashValue, Marker/SecondHashTerm) */
343		compute_hash(State,Hash,Marker) :- preferences:preference(symmetry_mode,SymMode),
344		pack_state(State,PackedState),
345		compute_hash(SymMode,State,PackedState,Hash,Marker).
346
347		%:- use_module(extension('probhash/probhash'),[raw_sha_hash/2]).
348		:- use_module(symsrc(graph_iso_nauty), [add_state_graph_to_nauty/2]).
349
350		compute_hash(off, S,PackedState,Hash,Marker) :- !, Marker=none,
351		(S=concrete_constants(_),
352		preferences:preference(maxNrOfInitialisations,Max),
353		Max =< 4 % default value is 4; affects hash results for tests 1532, 1646, 1699 if depth < 38
354		-> term_depth_hash(PackedState,38,Hash) % 38 is required for test 1699; but is probably too high in practice
355		% if there are few concrete_constants states: no need to hash them aggressively, and constants can be very large;
356		% this optimisation was added for PlanPro_validation.rmch
357		; my_term_hash(PackedState,Hash)).
358		compute_hash(hash,State,_PackedState,Hash,Marker) :-
359		(compute_marker_for_state(State,HMarker)
360		-> HMarker=Marker
361		%raw_sha_hash(HMarker,Marker)
362		; print(compute_marker_failed(State)),nl,fail),
363		my_term_hash(Marker,Hash),!.
364		compute_hash(nauty,State,_PackedState,Hash,Marker) :- !, Marker=none,
365		my_term_hash(State,EnvHash),
366		(hash_to_nauty_id(EnvHash,NautyID), hash_to_id(NautyID,RealID),
367		visited_expression(RealID,State)
368		-> %% print(exact_state_exists(EnvHash,NautyID,State)),nl, %%
369		% the exact same state already exists; no need to compute normal form
370		Hash=NautyID
371		; (add_state_graph_to_nauty(State,Exists)
372		-> true
373		; add_error(compute_hash,'Failed: ',add_state_graph_to_nauty(State,Exists), Exists=1)
374		),
375		(Exists>0 -> Hash=Exists
376		; /* new node */ Hash is -Exists, assertz(hash_to_nauty_id(EnvHash,Hash)))
377		),
378		% print(nauty_add(Exists,Hash,State)),nl,
379		Marker=none.
380		% my_term_hash now uses if_var(ignore) option of SICStus 4.1; no longer need to check ground
381		compute_hash(_, _Env,PackedState,Hash,none) :- my_term_hash(PackedState,Hash).
382
383
384		% --------------------------------------------
385
386		% some utilities to analyse state space:
387
388		hash_collision(ID,ID2,S1,S2) :-
389		hash_to_id(Hash,ID),
390		hash_to_id(Hash,ID2), ID2 \= root, (ID=root->true; ID2>ID),
391		visited_expression(ID,S1),
392		%print((ID,S1)),nl,
393		visited_expression(ID2,S2),
394		%print((ID2,S2)),nl,
395		nl.
396
397		:- dynamic hash_collision/2. % hash_collision(NrStatesWithSameHash, NrOfSuchClusters)
398		analyze_hash_collisions :- retractall(hash_collision(_,_)),
399		print('Analyzing Hash Collisions'),nl,
400		hash_to_id(Hash,ID),
401		\+ (hash_to_id(Hash,ID2), ID2 @< ID),
402		findall(X,hash_to_id(Hash,X),L),
403		length(L,Nr),
404		(retract(hash_collision(Nr,C))
405		-> (C1 is C+1, assertz(hash_collision(Nr,C1)))
406		; assertz(hash_collision(Nr,1))
407		),fail.
408		analyze_hash_collisions :-
409		print('Hash Collision Distribution (1=no collision): '),
410		findall((Nr,X),hash_collision(Nr,X),Coll),
411		sort(Coll,SC),
412		print(SC),nl,
413		(hash_collision(ID,ID2,S1,S2) ->
414		print('SAMPLE COLLISION: '),nl,
415		print(ID),nl,print(S1),nl, print_hash_info(S1),
416		print(ID2),nl,print(S2),nl,print_hash_info(S2)
417		; print('NO COLLISIONS')
418		),nl.
419
420
421		%ac :- analyse_collision([range(smallint),depth(infinite)]). % Runtime: 3890 ms
422		%ac0 :- analyse_collision([range(smallint),algorithm(sdbm),depth(infinite)]). % Runtime: 3760 ms
423		%ac1 :- analyse_collision([range(infinite),algorithm(sdbm),depth(infinite)]). % Runtime: 3730 ms
424		%ac2 :- analyse_collision([range(infinite),algorithm(hsieh),depth(infinite)]). % Runtime: 3970 ms
425		%ac3 :- analyse_collision([range(infinite),algorithm(jenkins),depth(infinite)]). % Runtime: 3970 ms
426		%ac4 :- analyse_collision([]). % Runtime: 3720 ms
427		%analyse_collision(Options) :- retractall(hash_collision(_,_)),
428		% statistics(runtime,[_,_]),
429		% current_prolog_flag(max_tagged_integer,Max),
430		% current_prolog_flag(min_tagged_integer,Min),
431		% visited_expression(ID,B),
432		% term_hash(B,Options,HashB), %
433		% %super_hash(B,HashB), %
434		% ((HashB>=Min, HashB =< Max) -> true ; print('*** HASH NOT GOOD FOR INDEXING: '), print(ID),nl),
435		% (hash_collision(HashB,OtherID)
436		% -> print('COLLISION : '), print(ID), print(' <-> '), print(OtherID), print(' : '), print(HashB),nl
437		% ; assertz(hash_collision(HashB,ID))
438		% ),fail.
439		%analyse_collision(_Options) :-
440		% statistics(runtime,[_,T]), print('Runtime: '), print(T), print(' ms').
441
442
443		:- use_module(library(terms),[term_hash/2]).
444		print_hash_info(S1) :-
445		%env_hash(S1,EH1), print(env_hash(EH1)),nl,
446		my_term_hash(S1,MTH1), print(my_term_hash(MTH1)),nl,
447		term_hash(S1,TH1), print(sicstus_term_hash(TH1)),nl.
448
449		:- use_module(library(lists),[maplist/2]).
450		:- public print_current_state_term_sizes/0.
451		print_current_state_term_sizes :-
452		current_expression(ID,State), %expanded
453		state_corresponds_to_initialised_b_machine(State,BState),
454		format('Term Sizes of variables and constants in current state: ~w~n',[ID]),
455		findall( TS/Var, (member(bind(Var,Term),BState),
456		term_size(Term,TS)), List),
457		sort(List,SL),
458		maplist(print_ts,SL).
459
460		print_ts(TS/Var) :- format('~w : ~w~n',[Var,TS]).
461
462		% --------------------------------------------