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