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
6		/* visualize_graph.pl */
7		:- module(visualize_graph,[tcltk_print_states_for_dot/1, tcltk_print_states_for_dot/2,
8		tcltk_print_states_for_dot_sfdp/1, tcltk_print_states_for_dot_sfdp/2,
9		tcltk_print_neighbourhood_states_for_dot/2,
10		tcltk_print_current_state_for_dot/1,
11		tcltk_print_shortest_trace_to_current_state_for_dot/1,
12		%tcltk_print_trace_to_current_state_for_dot/1, % removed
13		tcltk_print_current_state_as_graph_for_dot/1, tcltk_print_state_as_graph_for_dot/2,
14		tcltk_print_history_to_current_state_for_dot/1,
15		tcltk_print_history_to_current_state_with_neighbors_for_dot/1,
16		% tcltk_print_transition_diagram_for_variable_or_expr/2, % moved to state_space_reduction
17		tcltk_print_definitions_as_graph_for_dot/1,
18		tcltk_print_predicate_dependency_as_graph_for_dot/2,
19		tcltk_print_csp_process_states_for_dot/2,
20		print_graph_header/1,
21		print_graph_footer/0,
22
23		convert_state_to_string/2]).
24
25
26		:- use_module(probsrc(module_information)).
27		:- module_info(group,dot).
28		:- module_info(description,'This module generates various dot graphs (state space, single state, transition diagram,...).').
29
30		:- use_module(library(lists)).
31		:- use_module(probsrc(preferences)).
32
33		:- use_module(probsrc(debug)).
34		:- use_module(probsrc(translate)).
35		:- use_module(probsrc(bmachine),[b_is_constant/1]).
36
37		:- use_module(probsrc(state_space)).
38		:- use_module(dotsrc(dot_graph_generator),[translate_bvalue_to_colour/2, translate_int_col/2]).
39		:- use_module(probsrc(state_space_exploration_modes),[compute_heuristic_function_for_state_id/2]).
40
41		/* --------------------------------------------------- */
42		/* MAIN ENTRY POINTS FOR TCL */
43		/* --------------------------------------------------- */
44
45
46		% print full state space for dot:
47
48		% a version for large graphs; where we automatically turn off some details
49		tcltk_print_states_for_dot_sfdp(F) :-
50		tcltk_print_states_for_dot_sfdp(F,colour_transitions).
51		tcltk_print_states_for_dot_sfdp(F,ColourTransitions) :-
52		temporary_set_preference(dot_print_node_info,false,CHNG1),
53		temporary_set_preference(dot_print_node_properties,false,CHNG2),
54		temporary_set_preference(dot_print_self_loops,false,CHNG3),
55		temporary_set_preference(dot_fill_normal_nodes,true,CHNG4),
56		call_cleanup(tcltk_print_states_for_dot(F,ColourTransitions),
57		(preferences:reset_temporary_preference(dot_print_node_info,CHNG1),
58		preferences:reset_temporary_preference(dot_print_node_properties,CHNG2),
59		preferences:reset_temporary_preference(dot_print_self_loops,CHNG3),
60		preferences:reset_temporary_preference(dot_fill_normal_nodes,CHNG4))).
61
62		tcltk_print_states_for_dot(F) :- tcltk_print_states_for_dot(F,no_colour_for_transitions).
63		tcltk_print_states_for_dot(F,ColourTransitions) :-
64		format('Writing states to dot file ~w~n',[F]),
65		tell(F),(tcltk_print_states_for_dot_aux(ColourTransitions) -> true ; true),told.
66
67		tcltk_print_states_for_dot_aux(ColourTransitions) :-
68		reset_label_nr(ColourTransitions),
69		print_graph_header(visited_states),
70	?	visited_expression_id(NodeID),
71		tcltk_print_node_for_dot(NodeID),
72		tcltk_print_transitions_for_dot(NodeID,_),
73		fail.
74		tcltk_print_states_for_dot_aux(_ColourTransitions) :-
75		print_graph_footer.
76
77
78		tcltk_print_neighbourhood_states_for_dot(Dist,F) :-
79		retractall(unfiltered_state(_,_)),
80		current_state_id(CurID),
81		(dfs(CurID,Dist) -> true ; true), % mark neighbours until distance Dist
82		tell(F),(tcltk_print_unfiltered_states_for_dot -> true ; true),told.
83
84		:- dynamic unfiltered_state/2.
85		dfs(ID,Dist) :- unfiltered_state(ID,D1), (D1>=Dist -> ! ; retract(unfiltered_state(ID,D1))),fail.
86		dfs(ID,Dist) :- assertz(unfiltered_state(ID,Dist)), D1 is Dist-1,
87		D1>0,
88		any_transition(ID,_,NodeID),
89		dfs(NodeID,D1).
90
91		tcltk_print_unfiltered_states_for_dot :- reset_label_nr,
92		print_graph_header_with_layout(neighbourhood,sfdp),
93		unfiltered_state(NodeID,Dist),
94		tcltk_print_node_for_dot(NodeID,[pendwidth/Dist]),
95		tcltk_print_transitions_for_dot(NodeID,_),
96		fail.
97		tcltk_print_unfiltered_states_for_dot :-
98		print_graph_footer.
99
100		% --------------------------
101		tcltk_print_csp_process_states_for_dot(F,ProcID) :-
102		tell(F),(tcltk_print_csp_process_states_for_dot_root(ProcID) -> true ; true),told.
103
104		tcltk_print_csp_process_states_for_dot_root(ProcID) :-
105		reset_label_nr,
106		print_graph_header(csp_process),
107		tcltk_print_node_for_dot(root),
108		tcltk_print_transitions_for_dot(root,ProcID),
109		tcltk_print_csp_process_states_for_dot.
110
111		:- use_module(extrasrc(refinement_checker),[dvisited/1]).
112		tcltk_print_csp_process_states_for_dot :-
113		dvisited(NodeID),
114		tcltk_print_node_for_dot(NodeID),
115		tcltk_print_transitions_for_dot(NodeID,_),
116		fail.
117		tcltk_print_csp_process_states_for_dot :-
118		print_graph_footer.
119
120		% --------------------------
121
122		% just print the current state in the state space, not showing internal structure as graph!
123		tcltk_print_current_state_for_dot(F) :-
124		tell(F), (tcltk_print_current_state_for_dot -> true ; true),told.
125		tcltk_print_current_state_for_dot :-
126		reset_label_nr,
127		print_graph_header(current_state),
128		current_state_id(CurID),
129		( NodeID=CurID ;
130		any_transition(CurID,_,NodeID)),
131		tcltk_print_node_for_dot(NodeID),
132		fail.
133		tcltk_print_current_state_for_dot :-
134		current_state_id(CurID),
135		tcltk_print_transitions_for_dot(CurID,_),
136		fail.
137		tcltk_print_current_state_for_dot :-
138		print_graph_footer.
139
140		:- use_module(probsrc(tcltk_interface),[find_shortest_trace_to_node/4]).
141		tcltk_print_shortest_trace_to_current_state_for_dot(F) :-
142		tell(F), (tcltk_print_shortest_trace_to_current_state_for_dot -> true ; true),told.
143		tcltk_print_shortest_trace_to_current_state_for_dot :-
144		reset_label_nr,
145		print_graph_header(shortest_trace_to_current_state),
146		current_state_id(CurID),
147		find_shortest_trace_to_node(root,CurID,_,StateIDList),
148		print_trace_to_current_state(StateIDList),
149		print_graph_footer.
150
151
152		tcltk_print_history_to_current_state_for_dot(F) :-
153		tell(F), (tcltk_print_history_to_current_state_for_dot -> true ; true),told.
154		tcltk_print_history_to_current_state_for_dot :-
155		reset_label_nr,
156		print_graph_header(history),
157		current_state_id(CurID),
158		history(H),
159		reverse([CurID|H],IDList),
160		print_trace_to_current_state(IDList),
161		print_graph_footer.
162
163		% called for fairness formulas (currently only in CSP refinement checking mode)
164		tcltk_print_history_to_current_state_with_neighbors_for_dot(F) :-
165		tell(F), (tcltk_print_history_to_current_state_with_neighbors_for_dot -> true ; true),told.
166		tcltk_print_history_to_current_state_with_neighbors_for_dot :-
167		reset_label_nr,
168		print_graph_header(history),
169		current_state_id(CurID),
170		history(H),
171		reverse([CurID|H],IDList),
172		print_trace_with_neighbors_to_current_state(IDList),
173		print_graph_footer.
174
175		/* ---------------------------------------------------------------------- */
176
177
178		:- use_module(dotsrc(dot_graph_generator), [gen_dot_graph/5, dot_no_same_rank/1]).
179
180		% this predicate is currently not used anywhere, print_cstate_graph is used instead
181		tcltk_print_current_state_as_graph_for_dot(File) :-
182		current_expression(_CurID,State),
183		tcltk_print_state_as_graph_for_dot(State,File).
184		tcltk_print_state_as_graph_for_dot(State,File) :-
185		%print(gen_graph(State)),nl,
186		gen_dot_graph(File,dot_state_node,dot_state_trans(State),dot_no_same_rank,dot_subgraph).
187
188		:- use_module(probsrc(b_global_sets),[b_global_set/1,is_b_global_constant/3,all_elements_of_type/2]).
189		dot_state_node(ID,SET,Desc,box,none,Color) :-
190		b_global_set(SET), Desc = ID,
191		if(is_b_global_constant(SET,_Nr,Cst),
192		(Color=red,ID = Cst),
193		(Color=blue,
194		all_elements_of_type(SET,AllVals),
195		member(X,AllVals),
196		translate_bvalue(X,ID)
197		)
198		).
199		dot_state_node(root,none,'','Mdiamond',none,green).
200
201		dot_subgraph(SubGraph,filled,lightgray) :-
202		b_global_set(SubGraph).
203
204		% old version:
205		%dot_same_rank(TVals) :-
206		% b_global_set(SET),all_elements_of_type(SET,AllVals),translate_values(AllVals,TVals).
207
208		:- use_module(probsrc(store),[get_id_value/3]).
209		dot_state_trans(State,NodeID,Label,SuccNodeID,Color,Style) :- Style=solid,
210		get_id_value(VarOrConstant,State,VarValue),
211		dot_state_trans_var(VarValue,NodeID,SuccNodeID,VarOrConstant,Label),
212		(b_is_constant(VarOrConstant) -> Color=blue ; Color=black).
213
214		:- use_module(probsrc(gensym)).
215
216		dot_state_trans_var(VarValue,NodeID,SuccNodeID,Var,Var) :-
217		dot_state_basic_pair(VarValue,X1,X2), /* we have a relation or a pair */
218		dot_state_basic_type(X1), El1=X1,
219		dot_state_basic_type(X2), El2=X2, /* in case it is a function: we can also accept El2 to be dot_state_basic_type_or_element */
220		translate_bvalue(El1,NodeID),
221		translate_bvalue(El2,SuccNodeID).
222		dot_state_trans_var(VarValue,NodeID,SuccNodeID,Var,Var) :-
223		dot_state_basic_type_or_element(VarValue,V),
224		NodeID = root,
225		translate_bvalue(V,SuccNodeID).
226		dot_state_trans_var(VarValue,NodeID,SuccNodeID,Var,Label) :-
227		( (member(X,VarValue),Kind=el)
228		; (VarValue=(X,_),Kind=prj1)
229		; (VarValue=(_,X),Kind=prj2)
230		),
231		\+ directly_representable_element(X),
232		gensym(Var,IntNode),
233		((NodeID = root, SuccNodeID = IntNode, Label=Var)
234		;
235		dot_state_trans_internal(IntNode,Kind,X,NodeID,SuccNodeID,Label)
236		).
237
238
239		directly_representable_element(X) :- dot_state_basic_type(X).
240		directly_representable_element((X1,X2)) :-
241		dot_state_basic_type(X1),
242		dot_state_basic_type(X2).
243
244		dot_state_basic_type(fd(_,_)).
245		dot_state_basic_type(int(_)).
246		dot_state_basic_type(pred_false /* bool_false */).
247		dot_state_basic_type(pred_true /* bool_true */).
248		dot_state_basic_type(string(_)).
249
250		dot_state_basic_type_or_element(X,X) :- dot_state_basic_type(X).
251		dot_state_basic_type_or_element(S,X) :- member(X,S), dot_state_basic_type(X).
252		dot_state_basic_type_or_element([],empty_set).
253
254		:- use_module(library(avl),[avl_member/2]).
255		dot_state_basic_pair((X1,X2),X1,X2).
256		dot_state_basic_pair([H|T],X1,X2) :- member((X1,X2),[H|T]).
257		dot_state_basic_pair(avl_set(A),X1,X2) :- avl_member((X1,X2),A).
258
259		dot_state_trans_internal(IntNode,Kind,VarValue,NodeID,SuccNodeID,Label) :-
260		dot_state_basic_type_or_element(VarValue,V),
261		translate_bvalue(V,SuccNodeID),
262		NodeID = IntNode, Label=Kind.
263		dot_state_trans_internal(IntNode,Kind,VarValue,NodeID,SuccNodeID,Label) :-
264		dot_state_basic_pair(VarValue,X1,X2), /* we have a relation or a pair */
265		dot_state_basic_type_or_element(X1,El1),
266		dot_state_basic_type_or_element(X2,El2),
267		NodeID = IntNode,
268		( (translate_bvalue(El1,SuccNodeID), Label = prj1(Kind))
269		;(translate_bvalue(El2,SuccNodeID), Label = prj2(Kind))
270		).
271		/* MISSING: recursion */
272
273		/* ---------------------------------------------------------------------- */
274
275
276		print_graph_header(Type) :-
277		format('digraph ~w {~n',[Type]),
278		% print('graph [orientation=landscape, page="8.5, 11",ratio=fill,size="7.5,10"];'),nl. % old default layout
279		% print('graph [page="8.5, 11",ratio=fill,size="7.5,10"];'),nl.
280		print('graph [nodesep=1.5, ranksep=1.5];'), nl.
281
282		% Layout = sdfp, fdp, twopi, dot, ...
283		print_graph_header_with_layout(Type,Layout) :-
284		format('digraph ~w {~n',[Type]),
285		format('graph [nodesep=1.5, ranksep=1.5, layout=~w];~n',[Layout]).
286		% other possible options for graph: splines=true overlap=false ?
287
288		print_graph_footer :- print('}'),nl.
289
290
291		/* ---------------------------------------------------------------------- */
292
293		:- use_module(library(lists),[clumps/2]).
294		:- use_module(library(samsort)).
295		:- use_module(probsrc(tools),[ajoin/2]).
296		print_trace_to_current_state(IDList) :-
297		samsort(IDList,SIDList), % keeps duplicates
298		clumps(SIDList,Clumps),
299		member([NodeID|T],Clumps),
300		(length([NodeID|T],Len),Len>1
301		-> ajoin(['repeated (',Len,')'],Lbl),
302		tcltk_print_node_for_dot(NodeID,[extralabel/Lbl])
303		; tcltk_print_node_for_dot(NodeID)),
304		fail.
305		print_trace_to_current_state(IDList) :-
306		temporary_set_preference(dot_print_self_loops,true,CHNG3),
307		print_trace_to_current_state2(IDList),
308		preferences:reset_temporary_preference(dot_print_self_loops,CHNG3).
309
310		print_trace_to_current_state2([]).
311		print_trace_to_current_state2([_]).
312		print_trace_to_current_state2([ID1,ID2|Tail]) :-
313		tcltk_print_transitions_for_dot(ID1,ID2),
314		print_trace_to_current_state2([ID2|Tail]).
315
316		print_trace_with_neighbors_to_current_state(IDList) :- sort(IDList,SIDList),
317		member(NodeID,SIDList),
318		tcltk_print_node_for_dot(NodeID),
319		fail.
320		print_trace_with_neighbors_to_current_state(IDList) :-
321		current_state_id(CurID),
322		nth1(N,IDList,CurID,_Rest),!,
323		append_length(PathToLoop,LoopIDs,IDList,N),
324		%format(user_output,'~w pos=~w : ~w , path to loop=~w, loop=~w~n',[CurID,N,IDList,PathToLoop,LoopIDs]),
325		temporary_set_preference(dot_print_self_loops,true,CHNG3),
326		print_trace_to_current_state2(PathToLoop), % print path to loop
327		print_trace_with_neighbors_to_current_state2([CurID|LoopIDs],IDList), % print loop (with neighbors, because of the fairness check),
328		preferences:reset_temporary_preference(dot_print_self_loops,CHNG3).
329
330		print_trace_with_neighbors_to_current_state2([],_).
331		print_trace_with_neighbors_to_current_state2([ID|Tail],IDList) :-
332		findall(ID,(transition(ID,_,_,SuccID),
333		\+ append(_,[ID,SuccID|_],IDList), % check if the edge is not already shown
334		% format(user_output,'Neighb: ~w -> ~w : idlist=~w, tail=~w~n',[ID,SuccID,IDList,Tail]),
335		tcltk_print_transitions_for_dot(ID,SuccID)),_IDList),
336		print_trace_with_neighbors_to_current_state2(Tail,IDList).
337
338		extract_b_store(csp_and_b(_,T),R) :- !, R=T.
339		extract_b_store(R,R).
340
341		extract_full_store(concrete_constants(C),R) :- !,R=C.
342		extract_full_store(const_and_vars(ConstID,Vars),R) :- !,
343		specfile:expand_const_and_vars(ConstID,Vars,R).
344		extract_full_store(R,R).
345
346		:- use_module(probsrc(tools),[print_escaped/1]).
347		:- use_module(probsrc(state_space),[counterexample_node/1, counterexample_op/1]).
348		:- use_module(probsrc(model_checker),[find_invariant_error/4]).
349		:- use_module(probsrc(specfile),[animation_mode/1]).
350
351		tcltk_print_node_for_dot(ID) :- tcltk_print_node_for_dot(ID,[]).
352
353		tcltk_print_node_for_dot(NodeID,Options) :-
354		animation_mode(AM),
355		visited_expression(NodeID,CurT),
356		extract_b_store(CurT,CurBT),
357		extract_full_store(CurBT,CurTemp),
358		(NodeID=root -> preference(dot_print_root,true) ; true),
359		(member(shape/Shape,Options) -> true ; dot_node_shape(NodeID,CurTemp,Shape)),
360		% TO DO: penwidth=2.0, fillcolor="#F1F2D8"
361		(find_invariant_error(AM,NodeID,CurTemp,_)
362		-> get_preference(dot_invariant_violated_node_colour,NodeColor),
363		Style=filled
364		; counterexample_node(NodeID)
365		-> get_preference(dot_counterexample_node_colour,NodeColor),
366		(is_goal_node(NodeID) -> Style = 'rounded,filled', get_preference(dot_goal_node_colour,FillColor)
367		; Style=none, FillColor=none)
368		; is_goal_node(NodeID)
369		-> get_preference(dot_goal_node_colour,NodeColor),
370		Style='rounded,filled'
371		; (preference(dot_fill_normal_nodes,true) -> Style='rounded,filled' ; Style=none),
372		(member(color/NodeColor,Options) -> true ; dot_node_color(NodeID,NodeColor))
373		),
374		(member(fontsize/FSize,Options) -> true ; get_preference(dot_node_font_size,FSize)),
375		(Style=none
376		-> format('~w [shape=~w, color=\"~w\", fontsize=~w',[NodeID,Shape,NodeColor,FSize])
377		; FillColor=none
378		-> format('~w [shape=~w, style=\"~w\", color=\"~w\", fontsize=~w',[NodeID,Shape,Style, NodeColor,FSize])
379		; format('~w [shape=~w, style=\"~w\", color=\"~w\", fillcolor=\"~w\", fontsize=~w',
380		[NodeID,Shape,Style, NodeColor,FillColor,FSize])
381		),
382
383		(member(pendwidth/PenWidth,Options) -> true ; get_preference(dot_node_penwidth,PenWidth)),
384		(PenWidth = 1 -> true ; print(', penwidth='), print(PenWidth)),
385		write(', label=\"'),
386		(member(extralabel/ExtraLbl,Options) -> print_escaped(ExtraLbl), print('\\n') ; true),
387		(preference(dot_print_node_ids,true) -> print(NodeID), print(':\\n') ; true),
388		(preference(dot_print_node_info,true)
389		-> convert_state_to_string(CurT,StateAsString),
390		print_escaped(StateAsString) % quoted encode; except for
391		; true
392		),
393		(preference(dot_print_node_properties,true)
394		-> print_node_properties(NodeID)
395		; true
396		),
397		print('\"];'),nl,
398		fail.
399		tcltk_print_node_for_dot(_NodeID,_) :- nl.
400
401
402		:- use_module(probsrc(model_checker),[node_satisfies_goal/1]).
403		is_goal_node(NodeID) :- preference(dot_colour_goal_nodes,true),
404		node_satisfies_goal(NodeID). % TO DO csp goal
405
406		dot_node_shape(_StateId,State,triangle) :-
407		% state with abort values
408		memberchk(bind(_,term(no_value_for(_))),State),!.
409		dot_node_shape(root,_State,Shape) :-
410		% the root state
411		!,get_preference(dot_root_shape,Shape).
412		dot_node_shape(StateId,_State,Shape) :-
413		% the currently displayed state in the animation
414		current_state_id(StateId),!,
415		get_preference(dot_current_node_shape,Shape).
416		dot_node_shape(StateId,_State,diamond) :-
417		% a state which was subject to permutation flooding
418		transition(StateId,'*permute*',_),!.
419		dot_node_shape(_StateId,_State,Shape) :-
420		% a normal state
421		get_preference(dot_normal_node_shape,Shape).
422
423
424		dot_node_color(StateId,Color) :-
425		% an open state where not all transitions are yet calculated
426		not_all_transitions_added(StateId),!,
427		get_preference(dot_open_node_colour,Color).
428		dot_node_color(StateId,Color) :-
429		% a state which is outside the user-defined state space that should be model-checked
430		not_interesting(StateId),!,
431		get_preference(dot_scope_limit_node_colour,Color).
432		dot_node_color(StateId,Color) :-
433		transition(StateId,'*permute*',_),!, Color = lightgray.
434		dot_node_color(StateId,Color) :-
435		%get_preference(dot_normal_node_colour,Color),
436		compute_heuristic_function_for_state_id(StateId,HRes),
437		!,
438		translate_bvalue_to_colour(HRes,Color). %tools:print_message(heur(HRes,Color)).
439		dot_node_color(_StateId,Color) :-
440		get_preference(dot_normal_node_colour,Color).
441
442
443		:- use_module(probsrc(specfile),[property/2,elementary_prop/2,b_or_z_mode/0]).
444
445		print_node_properties(ID) :-
446		print(' Prop={'),
447		visited_expression(ID,State),
448	?	get_state_property(State,PropAsString),
449		print_string_for_dot(PropAsString), print('\\'),print('n'),
450		fail.
451		print_node_properties(_) :- print('}').
452
453		get_state_property(State,PropAsString) :-
454	?	specfile:property(State,Prop),
455		translate:translate_property_with_limit(Prop,320,PropAsString).
456
457		:- use_module(probsrc(bmachine),[b_get_machine_animation_expression/2]).
458		:- use_module(probsrc(specfile),[state_corresponds_to_fully_setup_b_machine/2]).
459		get_animation_expression_value(State,PropAsString) :-
460		b_or_z_mode,
461		b_get_machine_animation_expression('ANIMATION_EXPRESSION',AExpr),
462		state_corresponds_to_fully_setup_b_machine(State,BState),
463		b_interpreter:b_compute_expression_nowf(AExpr,[],BState,AValue,'ANIMATION_EXPRESSION',0),
464		translate:translate_bvalue(AValue,PropAsString).
465
466
467		tcltk_print_transitions_for_dot(NodeID,SuccID) :-
468	?	transition(NodeID,Action,TransID,SuccID),
469		visited_expression(NodeID,State), set_translation_context(State),
470		(NodeID=root -> preference(dot_print_root,true) ; true),
471		(Action = '-->'(_Func,_)
472		-> (NodeID \= SuccID ; preference(dot_print_functions,true))
473		; true),
474		(NodeID \= SuccID -> true ; preference(dot_print_self_loops,true)),
475		format('~w -> ~w',[NodeID,SuccID]),
476		(preference(dot_print_arc_colors,true) ->
477		(NodeID==root
478		-> print(' [style = dotted, color = black, label=\"')
479		; (Action = '*permute*'
480		-> ArcCol=gray
481		; counterexample_op(TransID)
482		-> get_preference(dot_counterexample_op_colour,ArcCol)
483		; dot_arc_color(TransID, Action, ArcCol)
484		),
485		format(' [color = \"~w\", label=\"',[ArcCol])
486		)
487		; print(' [label=\"')
488		),
489		dot_print_action(Action),
490		(get_preference(dot_print_transition_ids,true) -> format('\n~w',[TransID]) ; true),
491		get_preference(dot_edge_font_size,FSize),
492		get_preference(dot_edge_penwidth,PenWidth),
493		(PenWidth = 1
494		-> format('\", fontsize=~w];~n',[FSize])
495		; format('\", fontsize=~w, penwidth=~w];~n',[FSize,PenWidth])
496		),
497		fail.
498		tcltk_print_transitions_for_dot(_NodeID,_SuccID) :- clear_translation_constants,nl.
499
500
501		%dot_arc_color(TransID, blue) :-
502		% b_abstract_mappings:widened_trans(TransID),!.
503		dot_arc_color(_,Action,ArcCol) :-
504		get_label_nr(Action,Nr), Nr>0,
505		translate_int_col(Nr,ArcCol),
506		!.
507		dot_arc_color(_TransId,_Action, ArcCol) :-
508		(preference(dot_normal_arc_colour,ArcCol) -> true ; ArcCol=blue).
509		% TO DO: enable colouring; particularly in sfdp mode
510
511		:- dynamic label_nr/2, next_label_nr/1.
512		next_label_nr(0).
513		reset_label_nr :- retractall(label_nr(_,_)), retractall(next_label_nr(_)).
514		reset_label_nr(Colour) :- reset_label_nr,
515		(Colour=colour_transitions
516		-> assertz(next_label_nr(0)) % asserts next label nr: we will colour transitions
517		; true).
518
519		get_label_nr(Action,Nr) :- functor(Action,F,_),
520		(label_nr(F,FNr) -> Nr=FNr
521		; retract(next_label_nr(N)), N1 is N+1, assertz(next_label_nr(N1)), assertz(label_nr(F,N)), Nr=N).
522
523
524		dot_print_action(_) :- preference(dot_print_edge_labels,false),!.
525		dot_print_action(Action) :- preference(dot_print_action_arguments,true),
526		translate:translate_event(Action,ActionAsString),
527		print_string_for_dot(ActionAsString),!.
528		dot_print_action('-->'(FAction,_R)) :- nonvar(FAction),
529		functor(FAction,OperationName,_),!,
530		print_string_for_dot(OperationName).
531		dot_print_action(Action) :- nonvar(Action), functor(Action,OperationName,_),!,
532		print_string_for_dot(OperationName).
533		dot_print_action(Action) :- print('err:'),print_string_for_dot(Action).
534
535		:- use_module(probsrc(tools),[wrap_and_truncate_atom/4,string_escape/2]).
536		print_string_for_dot(String) :- string_escape(String,EString),
537		wrap_and_truncate_atom(EString,50,350,NS), print(NS).
538
539		/* ------------------------------------------------------------ */
540		/* converting a state into a string for the graph visualization */
541		/* ------------------------------------------------------------ */
542
543
544		:- use_module(probsrc(tools),[string_concatenate/3]).
545		convert_state_to_string(root,'root') :- !.
546		convert_state_to_string(State,String) :-
547		get_animation_expression_value(State,V),!,
548		String=V.
549		convert_state_to_string(StateTempl,StateAsString) :- animation_mode(xtl),!,
550		convert_state_to_string_default(StateTempl,StateAsString).
551		convert_state_to_string(concrete_constants(CurTemp),StateAsString) :- !,
552		findall(FProp,elementary_prop(CurTemp,FProp),State), /* was fd_findall */
553		translate_params_for_dot(State,StateAsString).
554		convert_state_to_string(const_and_vars(ConstID,StateTempl),StateAsString) :- !,
555		set_translation_constants(ConstID),
556		convert_state_to_string(StateTempl,StateAsString),
557		clear_translation_constants.
558		convert_state_to_string(csp_and_b(CSPState,BState),StateAsString) :- !,
559		translate_cspm_state(CSPState,CSPText),
560		convert_state_to_string(BState,BString),
561		string_concatenate(CSPText,'\n',C2),
562		string_concatenate(C2,BString,StateAsString).
563		convert_state_to_string([H|T],StateAsString) :- !,
564		CurTemp=[H|T],
565		findall(FProp,elementary_prop(CurTemp,FProp),State), /* was fd_findall */
566		translate_params_for_dot(State,StateAsString).
567		convert_state_to_string(StateTempl,StateAsString) :-
568		convert_state_to_string_default(StateTempl,StateAsString).
569
570		convert_state_to_string_default(StateTempl,StateAsString) :-
571		findall(FProp,
572		(property(StateTempl,Prop),filter_elementary_prop(Prop,FProp)),
573		State), /* was fd_findall */
574		translate_params_for_dot_nl(State,StateAsString).
575
576		filter_elementary_prop(X,R) :- \+ b_or_z_mode,!,R=X.
577		filter_elementary_prop('='(Cst,_V),_) :- nonvar(Cst),
578		b_is_constant(Cst),!,fail.
579		filter_elementary_prop(Relation,_) :-
580		functor(Relation,Func,_),
581		b_is_constant(Func),!,fail.
582		filter_elementary_prop('='(_X,pred_false /* bool_false */),_) :- !,fail. /* do not show boolean variables that are false */
583		filter_elementary_prop('='( X,pred_true /* bool_true */), X) :- !. /* just show the boolean variable, not that it is = true */
584		filter_elementary_prop(X,X).
585
586
587		/* ---------------------- */
588		/* DEFINITION dependency */
589		/* ---------------------- */
590
591		% show definition call graph
592
593		:- use_module(dotsrc(dot_graph_generator), [dot_no_same_rank/1]).
594		tcltk_print_definitions_as_graph_for_dot(File) :-
595		gen_dot_graph(File,dot_def_node,dot_def_trans,dot_no_same_rank,dot_def_subgraph).
596
597
598		:- use_module(probsrc(bmachine),[b_get_definition/5]).
599		:- use_module(library(ordsets),[ord_member/2]).
600
601		dot_def_node(0,none,'No DEFINITIONS visible',box,none,red) :-
602		\+ b_get_definition(_,_,_,_,_),!.
603		dot_def_node(DEFID,SubGraph,Desc,box,none,Color) :-
604		findall(Called, (b_get_definition(_,_,_,_,Deps), member(Called,Deps)),CD),
605		(CD=[] -> get_preference(dot_definitions_show_all,true) ; true), !,
606		sort(CD,CalledDefs),
607		b_get_definition(DEFID,DefType,Args,_Body,Deps),
608		length(Args,NrArgs),
609		tools:ajoin([DEFID,'/',NrArgs],Desc), % TO DO: improve
610		(get_preference(dot_definitions_use_sub_graph,true) -> SubGraph = DefType ; SubGraph=none),
611		(get_preference(dot_definitions_show_all,true) -> true
612		; Deps = [_|_] -> true % show if it calls another one
613		; ord_member(DEFID,CalledDefs) % show if called
614		),
615		(DefType = predicate -> Color = green ; Color = blue).
616		dot_def_node(0,none,'No DEFINITIONS called',box,none,blue).
617
618		dot_def_trans(NodeID,Label,SuccNodeID,Color,Style) :- Style=solid,
619		b_get_definition(NodeID,_DefType,_Args,_Body,Deps),
620		Label = 'call',
621		member(SuccNodeID,Deps),
622		(Deps = [_] -> Color = black ; Color = blue).
623
624		dot_def_subgraph(SubGraph,filled,lightgray) :-
625		get_preference(dot_definitions_use_sub_graph,true),
626		member(SubGraph,[predicate,expression,substitution]),
627		(b_get_definition(_,SubGraph,_,_,_) -> true).
628
629
630		/* Prediate dependency */
631
632		% call -dotexpr predicate_dependency Pred File
633		% separates a predicate into conjuncts and shows edges between predicates with common variables
634
635		:- use_module(probsrc(tools),[string_escape/2]).
636		:- use_module(probsrc(bsyntaxtree),[predicate_identifiers/2,conjunction_to_list/2]).
637		%
638		tcltk_print_predicate_dependency_as_graph_for_dot(Pred,File) :-
639		my_parse_predicate(Pred,Typed),
640		print_predicate_dependency_as_graph_for_dot(Typed,File).
641
642		:- use_module(probsrc(bmachine), [type_with_errors/4]).
643		:- use_module(probsrc(error_manager), [add_error/3]).
644		my_parse_predicate(RawAST,Typed) :- compound(RawAST),!,
645		type_with_errors(RawAST,[variables],Type,Typed),
646		(Type=pred -> true
647		; add_error(visualize_graph,'Expected predicate by got:',Type),fail).
648		my_parse_predicate(Pred,Typed) :-
649		atom_codes(Pred,Codes),
650		eval_strings:repl_parse_predicate(Codes,exists,Typed,_).
651
652		:- use_module(dotsrc(dot_graph_generator), [gen_dot_graph/3]).
653		print_predicate_dependency_as_graph_for_dot(Typed,File) :-
654		my_conjunction_to_list(Typed,Conj),
655		get_pred_ids(Conj,1,Preds),
656		gen_dot_graph(File,dot_pred_node(Preds),dot_pred_trans(Preds)).
657
658		my_conjunction_to_list(b(exists(_,Body),pred,_),L) :- !, my_conjunction_to_list(Body,L).
659		my_conjunction_to_list(B,L) :- conjunction_to_list(B,L).
660
661		get_pred_ids([],_,[]).
662		get_pred_ids([Pred|T],N,[pred(N,Pred,Ids)|PT]) :- predicate_identifiers(Pred,Ids),
663		N1 is N+1, get_pred_ids(T,N1,PT).
664
665		dot_pred_node(Preds,PID,none,EDesc,box,none,blue) :- member(pred(PID,Pred,_),Preds),
666		translate:translate_bexpression_with_limit(Pred,Desc),
667		string_escape(Desc,EDesc).
668
669		:- use_module(library(ordsets),[ord_intersection/3]).
670		dot_pred_trans(Preds,NodeID,Label,SuccNodeID,Color,Style) :- Style=solid, Color=black,
671		member(pred(NodeID,_,Ids1),Preds),
672		member(pred(SuccNodeID,_,Ids2),Preds), SuccNodeID>NodeID,
673		ord_intersection(Ids1,Ids2,Label), Label \= [].