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		(get_preference(dot_horizontal_layout,true) -> RDir=', rankdir=LR'; RDir=''), % default is TB
281		format('graph [nodesep=1.5, ranksep=1.5~w];~n',[RDir]).
282
283		% Layout = sdfp, fdp, twopi, dot, ...
284		print_graph_header_with_layout(Type,Layout) :-
285		format('digraph ~w {~n',[Type]),
286		(get_preference(dot_horizontal_layout,true) -> RDir=', rankdir=LR'; RDir=''), % default is TB
287		format('graph [nodesep=1.5, ranksep=1.5, layout=~w~w];~n',[Layout,RDir]).
288		% other possible options for graph: splines=true overlap=false ?
289
290		print_graph_footer :- print('}'),nl.
291
292
293		/* ---------------------------------------------------------------------- */
294
295		:- use_module(library(lists),[clumps/2]).
296		:- use_module(library(samsort)).
297		:- use_module(probsrc(tools),[ajoin/2]).
298		print_trace_to_current_state(IDList) :-
299		samsort(IDList,SIDList), % keeps duplicates
300		clumps(SIDList,Clumps),
301		member([NodeID|T],Clumps),
302		(length([NodeID|T],Len),Len>1
303		-> ajoin(['repeated (',Len,')'],Lbl),
304		tcltk_print_node_for_dot(NodeID,[extralabel/Lbl])
305		; tcltk_print_node_for_dot(NodeID)),
306		fail.
307		print_trace_to_current_state(IDList) :-
308		temporary_set_preference(dot_print_self_loops,true,CHNG3),
309		print_trace_to_current_state2(IDList),
310		preferences:reset_temporary_preference(dot_print_self_loops,CHNG3).
311
312		print_trace_to_current_state2([]).
313		print_trace_to_current_state2([_]).
314		print_trace_to_current_state2([ID1,ID2|Tail]) :-
315		tcltk_print_transitions_for_dot(ID1,ID2),
316		print_trace_to_current_state2([ID2|Tail]).
317
318		print_trace_with_neighbors_to_current_state(IDList) :- sort(IDList,SIDList),
319		member(NodeID,SIDList),
320		tcltk_print_node_for_dot(NodeID),
321		fail.
322		print_trace_with_neighbors_to_current_state(IDList) :-
323		current_state_id(CurID),
324		nth1(N,IDList,CurID,_Rest),!,
325		append_length(PathToLoop,LoopIDs,IDList,N),
326		%format(user_output,'~w pos=~w : ~w , path to loop=~w, loop=~w~n',[CurID,N,IDList,PathToLoop,LoopIDs]),
327		temporary_set_preference(dot_print_self_loops,true,CHNG3),
328		print_trace_to_current_state2(PathToLoop), % print path to loop
329		print_trace_with_neighbors_to_current_state2([CurID|LoopIDs],IDList), % print loop (with neighbors, because of the fairness check),
330		preferences:reset_temporary_preference(dot_print_self_loops,CHNG3).
331
332		print_trace_with_neighbors_to_current_state2([],_).
333		print_trace_with_neighbors_to_current_state2([ID|Tail],IDList) :-
334		findall(ID,(transition(ID,_,_,SuccID),
335		\+ append(_,[ID,SuccID|_],IDList), % check if the edge is not already shown
336		% format(user_output,'Neighb: ~w -> ~w : idlist=~w, tail=~w~n',[ID,SuccID,IDList,Tail]),
337		tcltk_print_transitions_for_dot(ID,SuccID)),_IDList),
338		print_trace_with_neighbors_to_current_state2(Tail,IDList).
339
340		extract_b_store(csp_and_b(_,T),R) :- !, R=T.
341		extract_b_store(R,R).
342
343		extract_full_store(concrete_constants(C),R) :- !,R=C.
344		extract_full_store(const_and_vars(ConstID,Vars),R) :- !,
345		specfile:expand_const_and_vars(ConstID,Vars,R).
346		extract_full_store(R,R).
347
348		:- use_module(probsrc(tools),[print_escaped/1]).
349		:- use_module(probsrc(state_space),[counterexample_node/1, counterexample_op/1]).
350		:- use_module(probsrc(model_checker),[find_invariant_error/4]).
351		:- use_module(probsrc(specfile),[animation_mode/1]).
352
353		tcltk_print_node_for_dot(ID) :- tcltk_print_node_for_dot(ID,[]).
354
355		tcltk_print_node_for_dot(NodeID,Options) :-
356		animation_mode(AM),
357		visited_expression(NodeID,CurT),
358		extract_b_store(CurT,CurBT),
359		extract_full_store(CurBT,CurTemp),
360		(NodeID=root -> preference(dot_print_root,true) ; true),
361		(member(shape/Shape,Options) -> true ; dot_node_shape(NodeID,CurTemp,Shape)),
362		% TO DO: penwidth=2.0, fillcolor="#F1F2D8"
363		(find_invariant_error(AM,NodeID,CurTemp,_)
364		-> get_preference(dot_invariant_violated_node_colour,NodeColor),
365		Style=filled
366		; counterexample_node(NodeID)
367		-> get_preference(dot_counterexample_node_colour,NodeColor),
368		(is_goal_node(NodeID) -> Style = 'rounded,filled', get_preference(dot_goal_node_colour,FillColor)
369		; Style=none, FillColor=none)
370		; is_goal_node(NodeID)
371		-> get_preference(dot_goal_node_colour,NodeColor),
372		Style='rounded,filled'
373		; (preference(dot_fill_normal_nodes,true) -> Style='rounded,filled' ; Style=none),
374		(member(color/NodeColor,Options) -> true ; dot_node_color(NodeID,NodeColor))
375		),
376		(member(fontsize/FSize,Options) -> true ; get_preference(dot_node_font_size,FSize)),
377		(Style=none
378		-> format('~w [shape=~w, color=\"~w\", fontsize=~w',[NodeID,Shape,NodeColor,FSize])
379		; FillColor=none
380		-> format('~w [shape=~w, style=\"~w\", color=\"~w\", fontsize=~w',[NodeID,Shape,Style, NodeColor,FSize])
381		; format('~w [shape=~w, style=\"~w\", color=\"~w\", fillcolor=\"~w\", fontsize=~w',
382		[NodeID,Shape,Style, NodeColor,FillColor,FSize])
383		),
384
385		(member(pendwidth/PenWidth,Options) -> true ; get_preference(dot_node_penwidth,PenWidth)),
386		(PenWidth = 1 -> true ; print(', penwidth='), print(PenWidth)),
387		write(', label=\"'),
388		(member(extralabel/ExtraLbl,Options) -> print_escaped(ExtraLbl), print('\\n') ; true),
389		(preference(dot_print_node_ids,true) -> print(NodeID), print(':\\n') ; true),
390		(preference(dot_print_node_info,true)
391		-> convert_state_to_string(CurT,StateAsString),
392		print_escaped(StateAsString) % quoted encode; except for
393		; true
394		),
395		(preference(dot_print_node_properties,true)
396		-> print_node_properties(NodeID)
397		; true
398		),
399		print('\"];'),nl,
400		fail.
401		tcltk_print_node_for_dot(_NodeID,_) :- nl.
402
403
404		:- use_module(probsrc(model_checker),[node_satisfies_goal/1]).
405		is_goal_node(NodeID) :- preference(dot_colour_goal_nodes,true),
406		node_satisfies_goal(NodeID). % TO DO csp goal
407
408		dot_node_shape(_StateId,State,triangle) :-
409		% state with abort values
410		memberchk(bind(_,term(no_value_for(_))),State),!.
411		dot_node_shape(root,_State,Shape) :-
412		% the root state
413		!,get_preference(dot_root_shape,Shape).
414		dot_node_shape(StateId,_State,Shape) :-
415		% the currently displayed state in the animation
416		current_state_id(StateId),!,
417		get_preference(dot_current_node_shape,Shape).
418		dot_node_shape(StateId,_State,diamond) :-
419		% a state which was subject to permutation flooding
420		transition(StateId,'*permute*',_),!.
421		dot_node_shape(_StateId,_State,Shape) :-
422		% a normal state
423		get_preference(dot_normal_node_shape,Shape).
424
425
426		dot_node_color(StateId,Color) :-
427		% an open state where not all transitions are yet calculated
428		not_all_transitions_added(StateId),!,
429		get_preference(dot_open_node_colour,Color).
430		dot_node_color(StateId,Color) :-
431		% a state which is outside the user-defined state space that should be model-checked
432		not_interesting(StateId),!,
433		get_preference(dot_scope_limit_node_colour,Color).
434		dot_node_color(StateId,Color) :-
435		transition(StateId,'*permute*',_),!, Color = lightgray.
436		dot_node_color(StateId,Color) :-
437		%get_preference(dot_normal_node_colour,Color),
438		compute_heuristic_function_for_state_id(StateId,HRes),
439		!,
440		translate_bvalue_to_colour(HRes,Color). %tools:print_message(heur(HRes,Color)).
441		dot_node_color(_StateId,Color) :-
442		get_preference(dot_normal_node_colour,Color).
443
444
445		:- use_module(probsrc(specfile),[property/2,elementary_prop/2,b_or_z_mode/0]).
446
447		print_node_properties(ID) :-
448		print(' Prop={'),
449		visited_expression(ID,State),
450	?	get_state_property(State,PropAsString),
451		print_string_for_dot(PropAsString), print('\\'),print('n'),
452		fail.
453		print_node_properties(_) :- print('}').
454
455		get_state_property(State,PropAsString) :-
456	?	specfile:property(State,Prop),
457		translate:translate_property_with_limit(Prop,320,PropAsString).
458
459		:- use_module(probsrc(bmachine),[b_get_machine_animation_expression/2]).
460		:- use_module(probsrc(specfile),[state_corresponds_to_fully_setup_b_machine/2]).
461		get_animation_expression_value(State,PropAsString) :-
462		b_or_z_mode,
463		b_get_machine_animation_expression('ANIMATION_EXPRESSION',AExpr),
464		state_corresponds_to_fully_setup_b_machine(State,BState),
465		b_interpreter:b_compute_expression_nowf(AExpr,[],BState,AValue,'ANIMATION_EXPRESSION',0),
466		translate:translate_bvalue(AValue,PropAsString).
467
468
469		tcltk_print_transitions_for_dot(NodeID,SuccID) :-
470	?	transition(NodeID,Action,TransID,SuccID),
471		visited_expression(NodeID,State), set_translation_context(State),
472		(NodeID=root -> preference(dot_print_root,true) ; true),
473		(Action = '-->'(_Func,_)
474		-> (NodeID \= SuccID ; preference(dot_print_functions,true))
475		; true),
476		(NodeID \= SuccID -> true ; preference(dot_print_self_loops,true)),
477		format('~w -> ~w',[NodeID,SuccID]),
478		(preference(dot_print_arc_colors,true) ->
479		(NodeID==root
480		-> print(' [style = dotted, color = black, label=\"')
481		; (Action = '*permute*'
482		-> ArcCol=gray
483		; counterexample_op(TransID)
484		-> get_preference(dot_counterexample_op_colour,ArcCol)
485		; dot_arc_color(TransID, Action, ArcCol)
486		),
487		format(' [color = \"~w\", label=\"',[ArcCol])
488		)
489		; print(' [label=\"')
490		),
491		dot_print_action(Action),
492		(get_preference(dot_print_transition_ids,true) -> format('\n~w',[TransID]) ; true),
493		get_preference(dot_edge_font_size,FSize),
494		get_preference(dot_edge_penwidth,PenWidth),
495		(PenWidth = 1
496		-> format('\", fontsize=~w];~n',[FSize])
497		; format('\", fontsize=~w, penwidth=~w];~n',[FSize,PenWidth])
498		),
499		fail.
500		tcltk_print_transitions_for_dot(_NodeID,_SuccID) :- clear_translation_constants,nl.
501
502
503		%dot_arc_color(TransID, blue) :-
504		% b_abstract_mappings:widened_trans(TransID),!.
505		dot_arc_color(_,Action,ArcCol) :-
506		get_label_nr(Action,Nr), Nr>0,
507		translate_int_col(Nr,ArcCol),
508		!.
509		dot_arc_color(_TransId,_Action, ArcCol) :-
510		(preference(dot_normal_arc_colour,ArcCol) -> true ; ArcCol=blue).
511		% TO DO: enable colouring; particularly in sfdp mode
512
513		:- dynamic label_nr/2, next_label_nr/1.
514		next_label_nr(0).
515		reset_label_nr :- retractall(label_nr(_,_)), retractall(next_label_nr(_)).
516		reset_label_nr(Colour) :- reset_label_nr,
517		(Colour=colour_transitions
518		-> assertz(next_label_nr(0)) % asserts next label nr: we will colour transitions
519		; true).
520
521		get_label_nr(Action,Nr) :- functor(Action,F,_),
522		(label_nr(F,FNr) -> Nr=FNr
523		; retract(next_label_nr(N)), N1 is N+1, assertz(next_label_nr(N1)), assertz(label_nr(F,N)), Nr=N).
524
525
526		dot_print_action(_) :- preference(dot_print_edge_labels,false),!.
527		dot_print_action(Action) :- preference(dot_print_action_arguments,true),
528		translate:translate_event(Action,ActionAsString),
529		print_string_for_dot(ActionAsString),!.
530		dot_print_action('-->'(FAction,_R)) :- nonvar(FAction),
531		functor(FAction,OperationName,_),!,
532		print_string_for_dot(OperationName).
533		dot_print_action(Action) :- nonvar(Action), functor(Action,OperationName,_),!,
534		print_string_for_dot(OperationName).
535		dot_print_action(Action) :- print('err:'),print_string_for_dot(Action).
536
537		:- use_module(probsrc(tools),[wrap_and_truncate_atom/4,string_escape/2]).
538		print_string_for_dot(String) :- string_escape(String,EString),
539		wrap_and_truncate_atom(EString,50,350,NS), print(NS).
540
541		/* ------------------------------------------------------------ */
542		/* converting a state into a string for the graph visualization */
543		/* ------------------------------------------------------------ */
544
545
546		:- use_module(probsrc(tools),[string_concatenate/3]).
547		convert_state_to_string(root,'root') :- !.
548		convert_state_to_string(State,String) :-
549		get_animation_expression_value(State,V),!,
550		String=V.
551		convert_state_to_string(StateTempl,StateAsString) :- animation_mode(xtl),!,
552		convert_state_to_string_default(StateTempl,StateAsString).
553		convert_state_to_string(concrete_constants(CurTemp),StateAsString) :- !,
554		findall(FProp,elementary_prop(CurTemp,FProp),State), /* was fd_findall */
555		translate_params_for_dot(State,StateAsString).
556		convert_state_to_string(const_and_vars(ConstID,StateTempl),StateAsString) :- !,
557		set_translation_constants(ConstID),
558		convert_state_to_string(StateTempl,StateAsString),
559		clear_translation_constants.
560		convert_state_to_string(csp_and_b(CSPState,BState),StateAsString) :- !,
561		translate_cspm_state(CSPState,CSPText),
562		convert_state_to_string(BState,BString),
563		string_concatenate(CSPText,'\n',C2),
564		string_concatenate(C2,BString,StateAsString).
565		convert_state_to_string([H|T],StateAsString) :- !,
566		CurTemp=[H|T],
567		findall(FProp,elementary_prop(CurTemp,FProp),State), /* was fd_findall */
568		translate_params_for_dot(State,StateAsString).
569		convert_state_to_string(StateTempl,StateAsString) :-
570		convert_state_to_string_default(StateTempl,StateAsString).
571
572		convert_state_to_string_default(StateTempl,StateAsString) :-
573		findall(FProp,
574		(property(StateTempl,Prop),filter_elementary_prop(Prop,FProp)),
575		State), /* was fd_findall */
576		translate_params_for_dot_nl(State,StateAsString).
577
578		filter_elementary_prop(X,R) :- \+ b_or_z_mode,!,R=X.
579		filter_elementary_prop('='(Cst,_V),_) :- nonvar(Cst),
580		b_is_constant(Cst),!,fail.
581		filter_elementary_prop(Relation,_) :-
582		functor(Relation,Func,_),
583		b_is_constant(Func),!,fail.
584		filter_elementary_prop('='(_X,pred_false /* bool_false */),_) :- !,fail. /* do not show boolean variables that are false */
585		filter_elementary_prop('='( X,pred_true /* bool_true */), X) :- !. /* just show the boolean variable, not that it is = true */
586		filter_elementary_prop(X,X).
587
588
589		/* ---------------------- */
590		/* DEFINITION dependency */
591		/* ---------------------- */
592
593		% show definition call graph
594
595		:- use_module(dotsrc(dot_graph_generator), [dot_no_same_rank/1]).
596		tcltk_print_definitions_as_graph_for_dot(File) :-
597		gen_dot_graph(File,dot_def_node,dot_def_trans,dot_no_same_rank,dot_def_subgraph).
598
599
600		:- use_module(probsrc(bmachine),[b_get_definition/5]).
601		:- use_module(library(ordsets),[ord_member/2]).
602
603		dot_def_node(0,none,'No DEFINITIONS visible',box,none,red) :-
604		\+ b_get_definition(_,_,_,_,_),!.
605		dot_def_node(DEFID,SubGraph,Desc,box,none,Color) :-
606		findall(Called, (b_get_definition(_,_,_,_,Deps), member(Called,Deps)),CD),
607		(CD=[] -> get_preference(dot_definitions_show_all,true) ; true), !,
608		sort(CD,CalledDefs),
609		b_get_definition(DEFID,DefType,Args,_Body,Deps),
610		length(Args,NrArgs),
611		tools:ajoin([DEFID,'/',NrArgs],Desc), % TO DO: improve
612		(get_preference(dot_definitions_use_sub_graph,true) -> SubGraph = DefType ; SubGraph=none),
613		(get_preference(dot_definitions_show_all,true) -> true
614		; Deps = [_|_] -> true % show if it calls another one
615		; ord_member(DEFID,CalledDefs) % show if called
616		),
617		(DefType = predicate -> Color = green ; Color = blue).
618		dot_def_node(0,none,'No DEFINITIONS called',box,none,blue).
619
620		dot_def_trans(NodeID,Label,SuccNodeID,Color,Style) :- Style=solid,
621		b_get_definition(NodeID,_DefType,_Args,_Body,Deps),
622		Label = 'call',
623		member(SuccNodeID,Deps),
624		(Deps = [_] -> Color = black ; Color = blue).
625
626		dot_def_subgraph(SubGraph,filled,lightgray) :-
627		get_preference(dot_definitions_use_sub_graph,true),
628		member(SubGraph,[predicate,expression,substitution]),
629		(b_get_definition(_,SubGraph,_,_,_) -> true).
630
631
632		/* Prediate dependency */
633
634		% call -dotexpr predicate_dependency Pred File
635		% separates a predicate into conjuncts and shows edges between predicates with common variables
636
637		:- use_module(probsrc(tools),[string_escape/2]).
638		:- use_module(probsrc(bsyntaxtree),[predicate_identifiers/2,conjunction_to_list/2]).
639		%
640		tcltk_print_predicate_dependency_as_graph_for_dot(Pred,File) :-
641		my_parse_predicate(Pred,Typed),
642		print_predicate_dependency_as_graph_for_dot(Typed,File).
643
644		:- use_module(probsrc(bmachine), [type_with_errors/4]).
645		:- use_module(probsrc(error_manager), [add_error/3]).
646		my_parse_predicate(RawAST,Typed) :- compound(RawAST),!,
647		type_with_errors(RawAST,[variables],Type,Typed),
648		(Type=pred -> true
649		; add_error(visualize_graph,'Expected predicate by got:',Type),fail).
650		my_parse_predicate(Pred,Typed) :-
651		atom_codes(Pred,Codes),
652		eval_strings:repl_parse_predicate(Codes,exists,Typed,_).
653
654		:- use_module(dotsrc(dot_graph_generator), [gen_dot_graph/3]).
655		print_predicate_dependency_as_graph_for_dot(Typed,File) :-
656		my_conjunction_to_list(Typed,Conj),
657		get_pred_ids(Conj,1,Preds),
658		gen_dot_graph(File,dot_pred_node(Preds),dot_pred_trans(Preds)).
659
660		my_conjunction_to_list(b(exists(_,Body),pred,_),L) :- !, my_conjunction_to_list(Body,L).
661		my_conjunction_to_list(B,L) :- conjunction_to_list(B,L).
662
663		get_pred_ids([],_,[]).
664		get_pred_ids([Pred|T],N,[pred(N,Pred,Ids)|PT]) :- predicate_identifiers(Pred,Ids),
665		N1 is N+1, get_pred_ids(T,N1,PT).
666
667		dot_pred_node(Preds,PID,none,EDesc,box,none,blue) :- member(pred(PID,Pred,_),Preds),
668		translate:translate_bexpression_with_limit(Pred,Desc),
669		string_escape(Desc,EDesc).
670
671		:- use_module(library(ordsets),[ord_intersection/3]).
672		dot_pred_trans(Preds,NodeID,Label,SuccNodeID,Color,Style) :- Style=solid, Color=black,
673		member(pred(NodeID,_,Ids1),Preds),
674		member(pred(SuccNodeID,_,Ids2),Preds), SuccNodeID>NodeID,
675		ord_intersection(Ids1,Ids2,Label), Label \= [].