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 \= []. |