1		% (c) 2009-2026 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(visualize_graph,[tcltk_print_states_for_dot/1, tcltk_print_states_for_dot/2,
6		tcltk_print_states_for_dot_sfdp/1, tcltk_print_states_for_dot_sfdp/2,
7		tcltk_print_neighbourhood_states_for_dot/2,
8		tcltk_print_current_state_for_dot/1,
9		tcltk_print_shortest_trace_to_current_state_for_dot/1,
10		%tcltk_print_trace_to_current_state_for_dot/1, % removed
11		tcltk_print_current_state_as_graph_for_dot/1, tcltk_print_state_as_graph_for_dot/2,
12		tcltk_print_history_to_current_state_for_dot/1,
13		tcltk_print_history_to_current_state_with_neighbors_for_dot/1,
14		% tcltk_print_transition_diagram_for_variable_or_expr/2, % moved to state_space_reduction
15		tcltk_print_definitions_as_graph_for_dot/1,
16		tcltk_print_predicate_dependency_as_graph_for_dot/2,
17		tcltk_print_csp_process_states_for_dot/2,
18		print_graph_header/1,
19		print_graph_footer/0,
20
21		convert_state_to_string/2]).
22
23
24		:- use_module(probsrc(module_information)).
25		:- module_info(group,dot).
26		:- module_info(description,'This module generates various dot graphs (state space, single state, transition diagram,...).').
27
28		:- use_module(library(lists)).
29		:- use_module(probsrc(preferences)).
30
31		:- use_module(probsrc(debug)).
32		:- use_module(probsrc(translate)).
33		:- use_module(probsrc(bmachine),[b_is_constant/1]).
34
35		:- use_module(probsrc(state_space)).
36		:- use_module(dotsrc(dot_graph_generator),[translate_bvalue_to_colour/2, translate_int_col/2]).
37		:- use_module(probsrc(state_space_exploration_modes),[compute_heuristic_function_for_state_id/2]).
38
39		/* --------------------------------------------------- */
40		/* MAIN ENTRY POINTS FOR TCL */
41		/* --------------------------------------------------- */
42
43
44		% print full state space for dot:
45
46		% a version for large graphs; where we automatically turn off some details
47		tcltk_print_states_for_dot_sfdp(F) :-
48		tcltk_print_states_for_dot_sfdp(F,colour_transitions).
49		tcltk_print_states_for_dot_sfdp(F,ColourTransitions) :-
50		temporary_set_preference(dot_print_node_info,false,CHNG1),
51		temporary_set_preference(dot_print_node_properties,false,CHNG2),
52		temporary_set_preference(dot_print_self_loops,false,CHNG3),
53		temporary_set_preference(dot_fill_normal_nodes,true,CHNG4),
54		call_cleanup(tcltk_print_states_for_dot(F,ColourTransitions),
55		(preferences:reset_temporary_preference(dot_print_node_info,CHNG1),
56		preferences:reset_temporary_preference(dot_print_node_properties,CHNG2),
57		preferences:reset_temporary_preference(dot_print_self_loops,CHNG3),
58		preferences:reset_temporary_preference(dot_fill_normal_nodes,CHNG4))).
59
60		tcltk_print_states_for_dot(F) :- tcltk_print_states_for_dot(F,no_colour_for_transitions).
61		tcltk_print_states_for_dot(F,ColourTransitions) :-
62		format('Writing states to dot file ~w~n',[F]),
63		tell(F),(tcltk_print_states_for_dot_aux(ColourTransitions) -> true ; true),told.
64
65		tcltk_print_states_for_dot_aux(ColourTransitions) :-
66		reset_label_nr(ColourTransitions),
67		print_graph_header(visited_states),
68		visited_expression_id(NodeID),
69		tcltk_print_node_for_dot(NodeID),
70		tcltk_print_transitions_for_dot(NodeID,_),
71		fail.
72		tcltk_print_states_for_dot_aux(_ColourTransitions) :-
73		print_graph_footer.
74
75
76		tcltk_print_neighbourhood_states_for_dot(Dist,F) :-
77		retractall(unfiltered_state(_,_)),
78		current_state_id(CurID),
79		(dfs(CurID,Dist) -> true ; true), % mark neighbours until distance Dist
80		tell(F),(tcltk_print_unfiltered_states_for_dot -> true ; true),told.
81
82		:- dynamic unfiltered_state/2.
83		dfs(ID,Dist) :- unfiltered_state(ID,D1), (D1>=Dist -> ! ; retract(unfiltered_state(ID,D1))),fail.
84		dfs(ID,Dist) :- assertz(unfiltered_state(ID,Dist)), D1 is Dist-1,
85		D1>0,
86		any_transition(ID,_,NodeID),
87		dfs(NodeID,D1).
88
89		tcltk_print_unfiltered_states_for_dot :- reset_label_nr,
90		print_graph_header_with_layout(neighbourhood,sfdp),
91		unfiltered_state(NodeID,Dist),
92		tcltk_print_node_for_dot(NodeID,[pendwidth/Dist]),
93		tcltk_print_transitions_for_dot(NodeID,_),
94		fail.
95		tcltk_print_unfiltered_states_for_dot :-
96		print_graph_footer.
97
98		% --------------------------
99		tcltk_print_csp_process_states_for_dot(F,ProcID) :-
100		tell(F),(tcltk_print_csp_process_states_for_dot_root(ProcID) -> true ; true),told.
101
102		tcltk_print_csp_process_states_for_dot_root(ProcID) :-
103		reset_label_nr,
104		print_graph_header(csp_process),
105		tcltk_print_node_for_dot(root),
106		tcltk_print_transitions_for_dot(root,ProcID),
107		tcltk_print_csp_process_states_for_dot.
108
109		:- use_module(extrasrc(refinement_checker),[dvisited/1]).
110		tcltk_print_csp_process_states_for_dot :-
111		dvisited(NodeID),
112		tcltk_print_node_for_dot(NodeID),
113		tcltk_print_transitions_for_dot(NodeID,_),
114		fail.
115		tcltk_print_csp_process_states_for_dot :-
116		print_graph_footer.
117
118		% --------------------------
119
120		% just print the current state in the state space, not showing internal structure as graph!
121		tcltk_print_current_state_for_dot(F) :-
122		tell(F), (tcltk_print_current_state_for_dot -> true ; true),told.
123		tcltk_print_current_state_for_dot :-
124		reset_label_nr,
125		print_graph_header(current_state),
126		current_state_id(CurID),
127		( NodeID=CurID ;
128		any_transition(CurID,_,NodeID)),
129		tcltk_print_node_for_dot(NodeID),
130		fail.
131		tcltk_print_current_state_for_dot :-
132		current_state_id(CurID),
133		tcltk_print_transitions_for_dot(CurID,_),
134		fail.
135		tcltk_print_current_state_for_dot :-
136		print_graph_footer.
137
138		:- use_module(probsrc(tcltk_interface),[find_shortest_trace_to_node/4]).
139		tcltk_print_shortest_trace_to_current_state_for_dot(F) :-
140		tell(F), (tcltk_print_shortest_trace_to_current_state_for_dot -> true ; true),told.
141		tcltk_print_shortest_trace_to_current_state_for_dot :-
142		reset_label_nr,
143		print_graph_header(shortest_trace_to_current_state),
144		current_state_id(CurID),
145		find_shortest_trace_to_node(root,CurID,_,StateIDList),
146		print_trace_to_current_state(StateIDList),
147		print_graph_footer.
148
149
150		tcltk_print_history_to_current_state_for_dot(F) :-
151		tell(F), (tcltk_print_history_to_current_state_for_dot -> true ; true),told.
152		tcltk_print_history_to_current_state_for_dot :-
153		reset_label_nr,
154		print_graph_header(history),
155		current_state_id(CurID),
156		history(H),
157		reverse([CurID|H],IDList),
158		print_trace_to_current_state(IDList),
159		print_graph_footer.
160
161		% called for fairness formulas (currently only in CSP refinement checking mode)
162		tcltk_print_history_to_current_state_with_neighbors_for_dot(F) :-
163		tell(F), (tcltk_print_history_to_current_state_with_neighbors_for_dot -> true ; true),told.
164		tcltk_print_history_to_current_state_with_neighbors_for_dot :-
165		reset_label_nr,
166		print_graph_header(history),
167		current_state_id(CurID),
168		history(H),
169		reverse([CurID|H],IDList),
170		print_trace_with_neighbors_to_current_state(IDList),
171		print_graph_footer.
172
173		/* ---------------------------------------------------------------------- */
174
175
176		:- use_module(dotsrc(dot_graph_generator), [gen_dot_graph/5, dot_no_same_rank/1]).
177
178		% this predicate is currently not used anywhere, print_cstate_graph is used instead
179		tcltk_print_current_state_as_graph_for_dot(File) :-
180		current_expression(_CurID,State),
181		tcltk_print_state_as_graph_for_dot(State,File).
182		tcltk_print_state_as_graph_for_dot(State,File) :-
183		%print(gen_graph(State)),nl,
184		gen_dot_graph(File,dot_state_node,dot_state_trans(State),dot_no_same_rank,dot_subgraph).
185
186		:- use_module(probsrc(b_global_sets),[b_global_set/1,is_b_global_constant/3,all_elements_of_type/2]).
187		dot_state_node(ID,SET,Desc,box,none,Color) :-
188		b_global_set(SET), Desc = ID,
189		if(is_b_global_constant(SET,_Nr,Cst),
190		(Color=red,ID = Cst),
191		(Color=blue,
192		all_elements_of_type(SET,AllVals),
193		member(X,AllVals),
194		translate_bvalue(X,ID)
195		)
196		).
197		dot_state_node(root,none,'','Mdiamond',none,green).
198
199		dot_subgraph(SubGraph,filled,lightgray) :-
200		b_global_set(SubGraph).
201
202		% old version:
203		%dot_same_rank(TVals) :-
204		% b_global_set(SET),all_elements_of_type(SET,AllVals),translate_values(AllVals,TVals).
205
206		:- use_module(probsrc(store),[get_id_value/3]).
207		dot_state_trans(State,NodeID,Label,SuccNodeID,Color,Style) :- Style=solid,
208		get_id_value(VarOrConstant,State,VarValue),
209		dot_state_trans_var(VarValue,NodeID,SuccNodeID,VarOrConstant,Label),
210		(b_is_constant(VarOrConstant) -> Color=blue ; Color=black).
211
212		:- use_module(probsrc(gensym)).
213
214		dot_state_trans_var(VarValue,NodeID,SuccNodeID,Var,Var) :-
215		dot_state_basic_pair(VarValue,X1,X2), /* we have a relation or a pair */
216		dot_state_basic_type(X1), El1=X1,
217		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 */
218		translate_bvalue(El1,NodeID),
219		translate_bvalue(El2,SuccNodeID).
220		dot_state_trans_var(VarValue,NodeID,SuccNodeID,Var,Var) :-
221		dot_state_basic_type_or_element(VarValue,V),
222		NodeID = root,
223		translate_bvalue(V,SuccNodeID).
224		dot_state_trans_var(VarValue,NodeID,SuccNodeID,Var,Label) :-
225		( (member(X,VarValue),Kind=el)
226		; (VarValue=(X,_),Kind=prj1)
227		; (VarValue=(_,X),Kind=prj2)
228		),
229		\+ directly_representable_element(X),
230		gensym(Var,IntNode),
231		((NodeID = root, SuccNodeID = IntNode, Label=Var)
232		;
233		dot_state_trans_internal(IntNode,Kind,X,NodeID,SuccNodeID,Label)
234		).
235
236
237		directly_representable_element(X) :- dot_state_basic_type(X).
238		directly_representable_element((X1,X2)) :-
239		dot_state_basic_type(X1),
240		dot_state_basic_type(X2).
241
242		dot_state_basic_type(fd(_,_)).
243		dot_state_basic_type(int(_)).
244		dot_state_basic_type(pred_false /* bool_false */).
245		dot_state_basic_type(pred_true /* bool_true */).
246		dot_state_basic_type(string(_)).
247
248		dot_state_basic_type_or_element(X,X) :- dot_state_basic_type(X).
249		dot_state_basic_type_or_element(S,X) :- member(X,S), dot_state_basic_type(X).
250		dot_state_basic_type_or_element([],empty_set).
251
252		:- use_module(library(avl),[avl_member/2]).
253		dot_state_basic_pair((X1,X2),X1,X2).
254		dot_state_basic_pair([H|T],X1,X2) :- member((X1,X2),[H|T]).
255		dot_state_basic_pair(avl_set(A),X1,X2) :- avl_member((X1,X2),A).
256
257		dot_state_trans_internal(IntNode,Kind,VarValue,NodeID,SuccNodeID,Label) :-
258		dot_state_basic_type_or_element(VarValue,V),
259		translate_bvalue(V,SuccNodeID),
260		NodeID = IntNode, Label=Kind.
261		dot_state_trans_internal(IntNode,Kind,VarValue,NodeID,SuccNodeID,Label) :-
262		dot_state_basic_pair(VarValue,X1,X2), /* we have a relation or a pair */
263		dot_state_basic_type_or_element(X1,El1),
264		dot_state_basic_type_or_element(X2,El2),
265		NodeID = IntNode,
266		( (translate_bvalue(El1,SuccNodeID), Label = prj1(Kind))
267		;(translate_bvalue(El2,SuccNodeID), Label = prj2(Kind))
268		).
269		/* MISSING: recursion */
270
271		/* ---------------------------------------------------------------------- */
272
273
274		print_graph_header(Type) :-
275		format('digraph ~w {~n',[Type]),
276		% print('graph [orientation=landscape, page="8.5, 11",ratio=fill,size="7.5,10"];'),nl. % old default layout
277		% print('graph [page="8.5, 11",ratio=fill,size="7.5,10"];'),nl.
278		(get_preference(dot_horizontal_layout,true) -> RDir=', rankdir=LR'; RDir=''), % default is TB
279		format('graph [nodesep=1.5, ranksep=1.5~w];~n',[RDir]).
280
281		% Layout = sdfp, fdp, twopi, dot, ...
282		print_graph_header_with_layout(Type,Layout) :-
283		format('digraph ~w {~n',[Type]),
284		(get_preference(dot_horizontal_layout,true) -> RDir=', rankdir=LR'; RDir=''), % default is TB
285		format('graph [nodesep=1.5, ranksep=1.5, layout=~w~w];~n',[Layout,RDir]).
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		% print transitions in state_space to tod
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 \= [].