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