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 | :- module(state_custom_dot_graph,[tcltk_generate_state_custom_dot_graph/1, | |
7 | state_custom_dot_graph_available/0, | |
8 | tcltk_generate_state_custom_dot_graph_for_expr/2, | |
9 | is_valid_custom_dot_graph_record/1]). | |
10 | ||
11 | :- use_module(probsrc(module_information)). | |
12 | :- module_info(group,dot). | |
13 | :- module_info(description,'This module provides a way to generate custom state graphs (using info from DEFINITIONS).'). | |
14 | ||
15 | % The best way to use this feature is to describe nodes and edges by records | |
16 | % Nodes should be records with a | |
17 | % - value field, used to compute the internal id and used by the edges | |
18 | % - label field: the text shown in dot for the node | |
19 | % Here is an example: | |
20 | % CUSTOM_GRAPH_NODES == {p•p∈Pairs|rec(`value`:p, label:```${p}\nu=${u(p)}```, | |
21 | % style: IF prj2(p)=certain THEN "solid" ELSE "dashed" END, | |
22 | % color: IF prj1(p)=fair THEN "green" ELSE "red" END, shape:"rect")}; | |
23 | % Edges should be records with | |
24 | % - from and to fields which should match the value field of some node | |
25 | % - label field: the text associated with the edge | |
26 | % Here is an example: | |
27 | % CUSTOM_GRAPH_EDGES == {a,b• a∈Pairs ∧ b∈Pairs ∧ u(a) > u(b) | rec(from:a,to:b,label:">")} | |
28 | % You can also merge everything into a single CUSTOM_GRAPH definition | |
29 | % CUSTOM_GRAPH == rec(layout:"circo", nodes:mynodes, edges:myedges) | |
30 | ||
31 | :- use_module(dotsrc(dot_graph_generator)). | |
32 | ||
33 | %:- use_module(self_check). | |
34 | :- use_module(probsrc(error_manager)). | |
35 | ||
36 | :- use_module(probsrc(state_space),[current_expression/2]). | |
37 | :- use_module(probsrc(bsyntaxtree), [get_texpr_id/2]). | |
38 | :- use_module(probsrc(specfile), [state_corresponds_to_fully_setup_b_machine/2]). | |
39 | :- use_module(probsrc(debug), [debug_println/2, debug_format/3]). | |
40 | :- use_module(probsrc(bmachine), [b_get_machine_custom_nodes_function/2,b_get_machine_custom_edges_function/2, | |
41 | b_get_machine_custom_graph_function/2]). | |
42 | :- use_module(probsrc(preferences),[valid_rgb_color/1, valid_dot_shape/1, | |
43 | valid_dot_line_style/1, valid_dot_node_style/1]). | |
44 | :- use_module(probsrc(tools),[start_ms_timer/1, stop_ms_timer_with_msg/2]). | |
45 | :- use_module(library(lists),[exclude/3]). | |
46 | ||
47 | :- set_prolog_flag(double_quotes, codes). | |
48 | ||
49 | ||
50 | state_custom_dot_graph_available :- | |
51 | b_get_machine_custom_graph_function(_,_) ; | |
52 | % b_get_machine_custom_nodes_function(_,_) ; | |
53 | b_get_machine_custom_edges_function(_,_). | |
54 | ||
55 | reset_custom_defs :- | |
56 | retractall(custom_nodes(_,_,_,_)), | |
57 | retractall(custom_edges(_,_,_,_)), | |
58 | retractall(custom_graph(_,_)), | |
59 | retractall(custom_node_id(_,_)), retractall(nodectr(_)), | |
60 | retractall(custom_trans_label(_,_)), retractall(trans_ctr(_)), assertz(trans_ctr(1)). | |
61 | ||
62 | tcltk_generate_state_custom_dot_graph(File) :- | |
63 | get_state_for_graph(BState), | |
64 | (state_custom_dot_graph_available | |
65 | -> true | |
66 | ; add_error_and_fail(tcltk_generate_state_custom_dot_graph, | |
67 | 'No CUSTOM_GRAPH_EDGES or CUSTOM_GRAPH Function in DEFINITIONS')), | |
68 | reset_custom_defs, | |
69 | start_ms_timer(Timer), | |
70 | eval_defs(BState), | |
71 | gen_graph(File), | |
72 | stop_ms_timer_with_msg(Timer,'custom graph: '). | |
73 | ||
74 | :- use_module(probsrc(eval_let_store),[extend_state_with_probids_and_lets/2]). | |
75 | :- use_module(probsrc(specfile), [get_current_state_for_b_formula/2]). | |
76 | % provide a way to create a custom graph from an expression | |
77 | % this expression should be a record with nodes, nedges fields, like a CUSTOM_GRAPH definition | |
78 | tcltk_generate_state_custom_dot_graph_for_expr(GraphFunction,File) :- | |
79 | get_current_state_for_b_formula(GraphFunction,BState), | |
80 | extend_state_with_probids_and_lets(BState,BState1), | |
81 | reset_custom_defs, | |
82 | eval_custom_graph_function(GraphFunction,0,BState1), | |
83 | gen_graph(File). | |
84 | ||
85 | :- use_module(probsrc(preferences),[temporary_set_preference/3, reset_temporary_preference/2]). | |
86 | gen_graph(File) :- | |
87 | (custom_graph(_,GraphAttrs) -> true ; GraphAttrs=[]), | |
88 | temporary_set_preference(dot_print_self_loops,true,Chng), % the user provides the edges function explicitly, show all edges | |
89 | call_cleanup(gen_dot_graph(File,GraphAttrs, | |
90 | use_new_dot_attr_pred(state_custom_dot_graph:cg_node_predicate), | |
91 | use_new_dot_attr_pred(state_custom_dot_graph:cg_trans_predicate), | |
92 | dot_no_same_rank,dot_no_subgraph), | |
93 | reset_temporary_preference(dot_print_self_loops,Chng)). | |
94 | ||
95 | get_state_for_graph(BState) :- | |
96 | current_expression(_CurID,State), | |
97 | state_corresponds_to_fully_setup_b_machine(State,BState),!. | |
98 | get_state_for_graph(_) :- % we could look at type of definitions and use get_current_state_for_b_formula | |
99 | add_error_and_fail(state_custom_dot_graph,'Only possible for initialised B machine.'). | |
100 | ||
101 | % check if something is a valid record for CUSTOM_GRAPH | |
102 | % it must have a nodes and edges field | |
103 | is_valid_custom_dot_graph_record(b(rec(Fields),_,_)) :- | |
104 | member(field(NodesField,_),Fields), is_nodes_field(NodesField,_),!, | |
105 | member(field(EdgesField,_),Fields), is_edges_field(EdgesField,_),!. | |
106 | ||
107 | :- use_module(library(lists),[select/3]). | |
108 | eval_defs(BState) :- | |
109 | b_get_machine_custom_nodes_function(NodesFunction,Nr), | |
110 | eval_definition_fun(NodesFunction, Nr, nodes, BState, Infos, NodesRes), | |
111 | debug_println(19,custom_nodes(Nr,NodesRes)), | |
112 | (select(label/EFID,Infos,RestInfos) | |
113 | -> assertz(custom_nodes(EFID,Nr,RestInfos,NodesRes)) | |
114 | ; get_texpr_id(NodesFunction,EFID) | |
115 | -> assertz(custom_nodes(EFID,Nr,Infos,NodesRes)) | |
116 | ; % we cannot derive name, then generate one | |
117 | number_codes(Nr,NC), append("custom",NC,CC), atom_codes(Custom,CC), | |
118 | assertz(custom_nodes(Custom,Nr,Infos,NodesRes))), | |
119 | fail. | |
120 | eval_defs(BState) :- | |
121 | b_get_machine_custom_edges_function(EdgesFunction,Nr), | |
122 | eval_definition_fun(EdgesFunction, Nr, edges, BState, Infos, EdgesRes), | |
123 | debug_println(19,custom_edges(Nr,EdgesRes)), | |
124 | (select(label/Label,Infos,RestInfos) -> true | |
125 | ; get_texpr_id(EdgesFunction,Label) -> RestInfos=Infos | |
126 | ; b_get_machine_custom_edges_function(_,Nr2), Nr2 \= Nr % other relation exists; makes sense to use label | |
127 | -> number_codes(Nr,NC), append("custom",NC,CC), | |
128 | atom_codes(Label,CC),RestInfos=Infos | |
129 | ; Label='',RestInfos=Infos | |
130 | ), | |
131 | assertz(custom_edges(Label,Nr,RestInfos,EdgesRes)), | |
132 | % print(edges(Label,Nr,RestInfos)),nl, translate:print_bvalue(EdgesRes),nl,nl, | |
133 | fail. | |
134 | eval_defs(BState) :- | |
135 | b_get_machine_custom_graph_function(GraphFunction,Nr), | |
136 | format('Detected single CUSTOM_GRAPH DEFINITION ~w~n',[Nr]), | |
137 | eval_custom_graph_function(GraphFunction,Nr,BState), | |
138 | fail. | |
139 | eval_defs(_). | |
140 | ||
141 | % Process a single CUSTOM_GRAPH record | |
142 | % Example: | |
143 | % rec(layout:"fdp",directed:TRUE, | |
144 | % edges:rec(colorscheme:"purples9", | |
145 | % edges:{x,y•x:2..50 & y:2..(x-1) & x mod y =0| | |
146 | % rec(edge:y|->x, label:"div", color:1 + x mod 9)} ), | |
147 | % nodes:rec(colorscheme:"set312", style:"filled", | |
148 | % nodes:{x•x:2..50|rec(label:x, | |
149 | % fillcolor: 1 + x mod 11) } ) ); | |
150 | eval_custom_graph_function(GraphFunction,Nr,BState) :- | |
151 | eval_definition_fun(GraphFunction, Nr, graph, BState, GraphAttrs, rec(OtherFields)), | |
152 | exclude(process_nodes_field([],GraphFunction),OtherFields,Infos1), | |
153 | exclude(process_edges_field([],GraphFunction),Infos1,Infos2), | |
154 | % instead of passing [] above, we could auto-detect GraphAttrs which are node or edge attributes | |
155 | (Infos2 = [] -> | |
156 | (Infos1=[] | |
157 | -> add_message(state_custom_dot_graph,'No edges detected in CUSTOM_GRAPH: ',OtherFields,GraphFunction) | |
158 | ; true) | |
159 | ; add_warning(state_custom_dot_graph,'Unrecognized CUSTOM_GRAPH fields: ',Infos2,GraphFunction)), | |
160 | (custom_graph(_,_) | |
161 | -> add_warning(state_custom_dot_graph,'Duplicate CUSTOM_GRAPH definition: ',Nr,GraphFunction) | |
162 | ; assertz(custom_graph(Nr,GraphAttrs)) | |
163 | ). | |
164 | ||
165 | % process a single nodes:Nodes field and assert custom_nodes facts | |
166 | process_nodes_field(DefaultAttrs,Span,field(NodeField,Nodes)) :- | |
167 | is_nodes_field(NodeField,Nr), | |
168 | assert_custom_nodes2(Nodes,DefaultAttrs,Span,Nr). | |
169 | ||
170 | assert_custom_nodes2(Nodes,DefaultAttrs,Span,_Nr) :- Nodes = rec(_), | |
171 | extract_record_fields(Nodes,_,DotAttributes,OtherFields),!, | |
172 | % we have a nested record with default Attributes for the nodes | |
173 | add_default_attrs(DefaultAttrs,DotAttributes,NewDefaultAttrs), | |
174 | exclude(process_nodes_field(NewDefaultAttrs,Span),OtherFields,Infos1), | |
175 | (Infos1 = [] -> true | |
176 | ; add_warning(state_custom_dot_graph,'Unrecognized CUSTOM_GRAPH nodes fields: ',Infos1,Span)). | |
177 | assert_custom_nodes2(Nodes,DefaultAttrs,_,Nr) :- | |
178 | try_expand_custom_set_with_catch(Nodes, NodesRes,extract_dot_function), | |
179 | assertz(custom_nodes('custom',Nr,DefaultAttrs,NodesRes)). %translate:print_bvalue(NodesRes),nl | |
180 | ||
181 | is_nodes_field(nodes,0). | |
182 | is_nodes_field(nodes0,0). | |
183 | is_nodes_field(nodes1,1). | |
184 | is_nodes_field(nodes2,2). | |
185 | is_nodes_field(nodes3,3). | |
186 | is_nodes_field(nodes4,4). | |
187 | is_nodes_field(nodes5,5). | |
188 | is_nodes_field(nodes6,6). | |
189 | is_nodes_field(nodes7,7). | |
190 | is_nodes_field(nodes8,8). | |
191 | is_nodes_field(nodes9,9). | |
192 | ||
193 | % process a single edges:Nodes field and assert custom_edges facts | |
194 | process_edges_field(DefaultAttrs,Span,field(EdgesField,Edges)) :- | |
195 | is_edges_field(EdgesField,Nr), | |
196 | assert_custom_edges2(Edges,DefaultAttrs,Span,Nr). | |
197 | ||
198 | assert_custom_edges2(Edges,DefaultAttrs,Span,_Nr) :- Edges = rec(_), | |
199 | extract_record_fields(Edges,_,DotAttributes,OtherFields),!, | |
200 | % we have a nested record with default Attributes for the edges | |
201 | add_default_attrs(DefaultAttrs,DotAttributes,NewDefaultAttrs), | |
202 | exclude(process_edges_field(NewDefaultAttrs,Span),OtherFields,Infos1), | |
203 | (Infos1 = [] -> true | |
204 | ; add_warning(state_custom_dot_graph,'Unrecognized CUSTOM_GRAPH edges fields: ',Infos1,Span)). | |
205 | assert_custom_edges2(Edges,DefaultAttrs,_,Nr) :- | |
206 | try_expand_custom_set_with_catch(Edges, EdgesRes,extract_dot_function), | |
207 | (select(label/Label,DefaultAttrs,DA) -> true | |
208 | ; Label='edge', DA=DefaultAttrs), | |
209 | assertz(custom_edges(Label,Nr,DA,EdgesRes)). | |
210 | ||
211 | ||
212 | is_edges_field(edges,0). | |
213 | is_edges_field(edges0,0). | |
214 | is_edges_field(edges1,1). | |
215 | is_edges_field(edges2,2). | |
216 | is_edges_field(edges3,3). | |
217 | is_edges_field(edges4,4). | |
218 | is_edges_field(edges5,5). | |
219 | is_edges_field(edges6,6). | |
220 | is_edges_field(edges7,7). | |
221 | is_edges_field(edges8,8). | |
222 | is_edges_field(edges9,9). | |
223 | ||
224 | :- dynamic custom_nodes/4, custom_edges/4, custom_graph/2. | |
225 | ||
226 | :- public cg_node_predicate/3. | |
227 | :- use_module(probsrc(tools),[string_escape/2]). | |
228 | % Custom Graph node predicate for dot_graph_generator.pl | |
229 | cg_node_predicate(NodeID,SubGraph,Attributes) :- SubGraph=none, | |
230 | custom_nodes(CustomID,_Nr,DefaultAttrs,Nodes), | |
231 | debug_format(19,'Processing CUSTOM_GRAPH_NODES ~w~n',[CustomID]), | |
232 | (var(Nodes) -> add_error(cg_node_predicate,'Variable custom_nodes: ',Nodes),fail ; true), | |
233 | get_node_attributes(Nodes,DefaultAttrs,NodeVal,Attributes), | |
234 | %tools:print_message(node(NodeVal,ColVal,Color,NodeID)), | |
235 | gen_id(NodeVal,NodeID). %tools:print_message(nodeid(NodeID)). | |
236 | ||
237 | get_node_attributes(CustomNodes,DefaultAttrs,NodeVal,[label/NodeDesc|Attrs]) :- | |
238 | %(member(style/DefStyle,DefaultAttrs) -> true ; DefStyle=filled), % to do: extract multiple styles | |
239 | %(member(shape/DefShape,DefaultAttrs) -> true ; DefShape=box), | |
240 | member(Node,CustomNodes), | |
241 | deconstruct_node(Node,DefaultAttrs,NodeVal,Attrs,Label), | |
242 | (Label\='$default_no_label' -> NodeDesc=Label | |
243 | ; translate_value_and_escape(NodeVal,NodeDesc) -> true | |
244 | ; NodeDesc = '???'). | |
245 | ||
246 | ||
247 | deconstruct_node(((NodeVal,string(Shape)),ColVal),DefaultAttrs,ResNodeVal,Attrs,'$default_no_label') :- | |
248 | valid_dot_shape(Shape), | |
249 | !, % we have a triple (Node,"box","colour") = ((Node,"box"),"colour") | |
250 | ResNodeVal=NodeVal, | |
251 | translate_bvalue_to_colour(ColVal,ResColVal), | |
252 | add_default_attrs(DefaultAttrs,[color/ResColVal,shape/Shape],Attrs). | |
253 | deconstruct_node((NodeVal,string(ColVal)),DefaultAttrs,ResNodeVal,Attrs,'$default_no_label') :- | |
254 | valid_rgb_color(ColVal), | |
255 | !, % we have a pair (Node,"colour") | |
256 | ResNodeVal=NodeVal, | |
257 | add_default_attrs(DefaultAttrs,[color/ColVal],Attrs). | |
258 | deconstruct_node((NodeVal,string(Shape)),DefaultAttrs,ResNodeVal, Attrs,'$default_no_label') :- | |
259 | valid_dot_shape(Shape), | |
260 | !, % we have a pair (Node,"shape") | |
261 | ResNodeVal=NodeVal, | |
262 | add_default_attrs(DefaultAttrs,[shape/Shape],Attrs). | |
263 | deconstruct_node(Record,DefaultAttrs,NodeVal, | |
264 | Attrs,Label) :- | |
265 | % New record style: this should probably be the default now | |
266 | extract_record_fields(Record,AllFields,DotAttributes,RemainingVals), | |
267 | DotAttributes = [_|_], % at least one field recognised | |
268 | ( RemainingVals = [field(_,NodeVal)] -> true | |
269 | ; member(field(value,NodeVal),RemainingVals) -> true | |
270 | ; member(field(id,NodeVal),RemainingVals) -> true % like in VisB / SVG; note is also a valid dot_attribute_field | |
271 | ; RemainingVals=[], member(label/_,DotAttributes) | |
272 | -> member(field(label,NodeVal),AllFields) % get original value before translation to string | |
273 | % but using label as node value may not be ideal for linking edges, better use separate value/id field | |
274 | ; RemainingVals \= [] -> add_warning(state_custom_dot_graph,'Node has no label or value field:',Record,Record), | |
275 | NodeVal = rec(RemainingVals) | |
276 | ), | |
277 | !, | |
278 | % add default values if not specified: | |
279 | ( select(label/LB,DotAttributes,Attrs0) -> Label=LB | |
280 | ; select(description/LB,DotAttributes,Attrs0) -> Label=LB | |
281 | ; Label = '$default_no_label', Attrs0=DotAttributes), | |
282 | add_default_attrs(DefaultAttrs,Attrs0,Attrs). | |
283 | deconstruct_node(NodeVal,DefaultAttrs,NodeVal,Attrs,'$default_no_label') :- | |
284 | (DefaultAttrs=[] | |
285 | -> format('CUSTOM_GRAPH_NODES value not recognised:~w~nUse rec(label:L,shape:"rect",...)~n',[NodeVal]) | |
286 | ; true % user has provided attributes in outer rec(...) construct | |
287 | ), | |
288 | add_default_attrs(DefaultAttrs,[],Attrs). % will remove none attributes | |
289 | % shapes: triangle,ellipse,box,diamond,hexagon,octagon,house,invtriangle,invhouse,invtrapez,doubleoctagon,egg,parallelogram,pentagon,trapezium... | |
290 | ||
291 | add_default_attrs([],Attrs,Attrs). | |
292 | add_default_attrs([Attr/Val|T],Attrs,ResAttrs) :- | |
293 | (member(Attr/_,Attrs) -> add_default_attrs(T,Attrs,ResAttrs) | |
294 | ; Val=none, \+ none_valid(Attr) -> add_default_attrs(T,Attrs,ResAttrs) % Should we completely remove this line? | |
295 | ; ResAttrs = [Attr/Val|RT], | |
296 | add_default_attrs(T,Attrs,RT)). | |
297 | ||
298 | % none is valid for arrowhead, arrowtail, ... and is different from default: | |
299 | none_valid(arrowhead). | |
300 | none_valid(arrowtail). | |
301 | ||
302 | :- dynamic custom_node_id/2, nodectr/1. | |
303 | nodectr(0). | |
304 | ||
305 | get_ctr(Res) :- retract(nodectr(C)),!, C1 is C+1, assertz(nodectr(C1)), Res=C. | |
306 | get_ctr(0) :- assertz(nodectr(1)). | |
307 | ||
308 | % generate or lookup ID for node | |
309 | gen_id(NodeVal,ID) :- | |
310 | (custom_node_id(NodeVal,ID) -> true | |
311 | ; get_ctr(C), | |
312 | assertz(custom_node_id(NodeVal,C)),ID=C). | |
313 | ||
314 | % TODO: hash NodeVal to improve performance for large graphs | |
315 | ||
316 | % lookup ID and generate message if it does not exist | |
317 | lookup_id(NodeVal,Kind,ID) :- | |
318 | (custom_node_id(NodeVal,ID) | |
319 | -> true | |
320 | ; get_as_string(NodeVal,VS), | |
321 | format(user_error,'The ~w node does not exist in CUSTOM_GRAPH_NODES: ~w~n',[Kind,VS]), | |
322 | %format('Internal value: ~w~n',[NodeVal]), portray_nodes, | |
323 | string_escape(VS,VSC), | |
324 | assertz(custom_node_id(NodeVal,VSC)), | |
325 | ID=VSC | |
326 | ). | |
327 | ||
328 | :- public portray_nodes/0. | |
329 | portray_nodes :- format(' ~w : ~w (~w)~n',['ID','Value','internal value']), | |
330 | custom_node_id(NodeVal,ID), | |
331 | translate_bvalue(NodeVal,NS), | |
332 | format(' ~w : ~w (~w)~n',[ID,NS,NodeVal]),fail. | |
333 | portray_nodes. | |
334 | ||
335 | :- dynamic custom_trans_label/2, trans_ctr/1. | |
336 | trans_ctr(1). | |
337 | gen_trans_color(Label,Col,_,IsColor) :- custom_trans_label(Label,C),!,Col=C,IsColor=false. | |
338 | gen_trans_color(_Label,Col,Infos,IsColor) :- member(color/C,Infos),!,Col=C,IsColor=false. | |
339 | gen_trans_color(Label,Col,_,IsColor) :- try_translate_bvalue_to_colour(Label,C),!,Col=C,IsColor=true. | |
340 | gen_trans_color(Label,Col,_,IsColor) :- retract(trans_ctr(Ctr)), C1 is Ctr+1, assertz(trans_ctr(C1)), | |
341 | translate_bvalue_to_colour(int(Ctr),C), | |
342 | assertz(custom_trans_label(Label,C)), Col=C,IsColor=false. | |
343 | ||
344 | :- public cg_trans_predicate/3. | |
345 | % Custom graph transition predicate for dot_graph_generator.pl | |
346 | cg_trans_predicate(NodeID,SuccID,DotAttributes) :- | |
347 | custom_edges(DefaultLabel,_,Infos,Edges), | |
348 | (member(color/DefaultCol,Infos) -> true ; DefaultCol=blue), | |
349 | (var(Edges) -> add_error(trans_predicate,'Variable custom_edges: ',Edges),fail ; true), | |
350 | member(Edge,Edges), | |
351 | cg_trans_aux(Edge,(DefaultLabel,DefaultCol),Infos,FromNode,ToNode,Attrs), | |
352 | add_default_attrs(Infos,Attrs,DotAttributes), | |
353 | lookup_id(FromNode,source,NodeID), | |
354 | lookup_id(ToNode,target,SuccID). | |
355 | ||
356 | cg_trans_aux(Pair,DefaultLabelCol,Infos, FromNode,ToNode,[label/Label, color/Colour]) :- | |
357 | get_pair(Pair,From1,To2),!, | |
358 | trans_pred_aux(From1,DefaultLabelCol,Infos,To2,FromNode,ToNode,Label,Colour). | |
359 | cg_trans_aux(Record,(DefaultLabel,DefaultCol),_Infos, FromNode,ToNode,Attrs) :- | |
360 | extract_record_fields(Record,_,DotAttrs,Vals), | |
361 | get_from_to(Vals,FromNode,ToNode), | |
362 | add_default_attrs([color/DefaultCol,label/DefaultLabel],DotAttrs,Attrs). | |
363 | ||
364 | :- use_module(probsrc(specfile), [animation_minor_mode/1]). | |
365 | :- use_module(probsrc(custom_explicit_sets),[singleton_set/2]). | |
366 | get_pair((From,To),From,To). | |
367 | get_pair(Set,From,To) :- % process optional values, e.g., in Alloy | |
368 | singleton_set(Set,El), !, El = (From,To). | |
369 | get_pair(avl_set(A),From,To) :- % process TLA+ tuples <<from,to>> translated to -> {(1,From),(2,To)} | |
370 | animation_minor_mode(tla), | |
371 | try_expand_custom_set_with_catch(avl_set(A), FunctionRes,get_pair), | |
372 | FunctionRes = [(int(1),From),(int(2),To)]. | |
373 | ||
374 | ||
375 | get_from_to(Vals,FromNode,ToNode) :- % either two field from:Fromnode, to:ToNode | |
376 | member(field(from,FromNode),Vals),!, | |
377 | member(field(to,ToNode),Vals). | |
378 | get_from_to(Vals,FromNode,ToNode) :- % or a single edge field which is a pair | |
379 | member(field(edge,(FromNode,ToNode)),Vals),!. | |
380 | ||
381 | ||
382 | % we have a transition where the colour is specified (e.g., CUSTOM_GRAPH_EDGES == {n1,col,n2 | ... } | |
383 | % we assume trans_predicate has been called first | |
384 | trans_pred_aux((From,To),(Label,_Col),_Infos,string(Colour),From,To,Label,Colour) :- | |
385 | To \= string(_), % we are not in one of the cases below where To is a label | |
386 | valid_rgb_color(Colour),!. | |
387 | % stems from something like CUSTOM_GRAPH_EDGES1 == graph*{"red"}; | |
388 | trans_pred_aux(FromValue,_Defaults,Infos,To,From,To,ELabel,Color) :- | |
389 | % format(user_output,'from: ~w~nto: ~w~n~n',[FromValue,To]), | |
390 | % ((From,LabelCol) |-> To) case | |
391 | get_trans_label_and_color(FromValue,Infos,From,Color,ELabel), % the From Value contains color and label | |
392 | !. | |
393 | trans_pred_aux(From,_Defaults,Infos,(LabelVal,ToVal),From,To,ELabel,Color) :- | |
394 | % (From |-> (LabelCol,To)) case | |
395 | get_trans_label_and_color((ToVal,LabelVal),Infos,To,Color,ELabel), % the To Value contains color and label | |
396 | !. | |
397 | trans_pred_aux(From,(Label,Col),_Infos,To,From,To,Label,Col). | |
398 | % no label or color specified in transition pair | |
399 | ||
400 | ||
401 | % try and decompose a from value, detecting color and label string ((From,"label"),"color") | |
402 | get_trans_label_and_color((FromVal,LabelVal),Infos,From,Color,ELabel) :- | |
403 | gen_trans_color(LabelVal,Color,Infos,IsColor), | |
404 | (IsColor | |
405 | -> get_trans_label(FromVal,From,ELabel) | |
406 | ; translate_value_and_escape(LabelVal,ELabel), | |
407 | From=FromVal | |
408 | ). | |
409 | ||
410 | get_trans_label((From,string(LabelVal)),From,ELabel) :- string_escape(LabelVal,ELabel). | |
411 | get_trans_label(From,From,''). % or should we use DefaultLabel | |
412 | ||
413 | translate_value_and_escape(string(S),ELabel) :- !, string_escape(S,ELabel). | |
414 | translate_value_and_escape(LabelVal,ELabel) :- | |
415 | translate:translate_bvalue(LabelVal,Label),string_escape(Label,ELabel). | |
416 | ||
417 | :- use_module(probsrc(b_interpreter),[b_compute_explicit_epression_no_wf/6]). | |
418 | :- use_module(probsrc(custom_explicit_sets),[try_expand_custom_set_with_catch/3]). | |
419 | :- use_module(probsrc(bsyntaxtree),[get_texpr_info/2]). | |
420 | ||
421 | % Kind = edges, nodes, graph | |
422 | eval_definition_fun(AnimFunction, Nr, Kind, BState, SInfos, FunctionRes) :- | |
423 | b_compute_explicit_epression_no_wf(AnimFunction,[],BState,FunctionResCl,'custom state graph',Nr), | |
424 | %nl, print('FunctionResult'(FunctionResCl)),nl, | |
425 | get_texpr_info(AnimFunction,Pos), | |
426 | extract_dot_function(FunctionResCl, Kind, Infos, FunctionRes,Pos), | |
427 | sort(Infos,SInfos). | |
428 | ||
429 | extract_dot_function(Value,graph,Attributes,FunctionRes,Pos) :- !, % for CUSTOM_GRAPH | |
430 | extract_dot_graph_function(Value,Attributes,OtherFields,Pos), | |
431 | FunctionRes=rec(OtherFields). % list of fields | |
432 | extract_dot_function((Label,Value),Kind,Info,FunctionRes,Pos) :- % treat e.g. == ("red","F",F) | |
433 | extract_dot_info(Label,Info,Info2),!, | |
434 | extract_dot_function(Value,Kind,Info2,FunctionRes,Pos). | |
435 | extract_dot_function((Value,Label),Kind,Info,FunctionRes,Pos) :- | |
436 | extract_dot_info(Label,Info,Info2),!, | |
437 | extract_dot_function(Value,Kind,Info2,FunctionRes,Pos). | |
438 | extract_dot_function(Record,Kind,DefaultDotAttributes,FunctionRes,Pos) :- | |
439 | % treat e.g. CUSTOM_GRAPH_NODES == rec(color:"blue", shape:"rect", nodes:e); | |
440 | % or CUSTOM_GRAPH_EDGES == rec(color:"red", style:"dotted", edges:e); | |
441 | % or CUSTOM_GRAPH_NODES == rec(color:"blue", label:"root", shape:"") | |
442 | extract_record_fields(Record,_,DotAttributes,Vals), | |
443 | !, | |
444 | ( select(field(ValAttr,Value),Vals,RestVals), | |
445 | member(ValAttr,[value, Kind]) % there is a value, edge, nodes field | |
446 | % this a record setting attributes for a set of nodes/edges | |
447 | -> DefaultDotAttributes = DotAttributes, | |
448 | try_expand_custom_set_with_catch(Value, FunctionRes,extract_dot_function), | |
449 | (RestVals=[] -> true ; add_message(state_custom_dot_graph,'Unrecognised DOT attributes: ',RestVals,Pos)) | |
450 | ; member(label/_,DotAttributes) % in case we have a label this represents a single record | |
451 | -> FunctionRes = [Record], DefaultDotAttributes=[] | |
452 | ; add_message(state_custom_graph,'CUSTOM_GRAPH record not ok (use fields color,shape,style,description and either label, edges or nodes): ',Vals,Pos), | |
453 | fail | |
454 | ). | |
455 | extract_dot_function(Value,_Kind,[],FunctionRes,_) :- | |
456 | % we try to see if it is a set of nodes (ideally as records) or edges | |
457 | try_expand_custom_set_with_catch(Value,FunctionRes,extract_dot_function),!. | |
458 | extract_dot_function(Value,_Kind,_,_,Pos) :- | |
459 | add_warning(state_custom_dot_graph,'Illegal CUSTOM_GRAPH value (use rec(label:L,shape:,...) record or set of records): ',Value,Pos), | |
460 | fail. | |
461 | ||
462 | % treat single CUSTOM_GRAPH record: | |
463 | extract_dot_graph_function(Record,Attributes,OtherFields,_) :- | |
464 | extract_record_fields(Record,_,Attributes,OtherFields),!. | |
465 | extract_dot_graph_function(Value,_,_,Pos) :- | |
466 | add_warning(state_custom_dot_graph,'Illegal CUSTOM_GRAPH value, use record',Value,Pos), | |
467 | fail. | |
468 | ||
469 | :- use_module(probsrc(translate), [translate_bvalue/2]). | |
470 | % extract dot information from a B value, if it looks like a color, shape, style or label | |
471 | extract_dot_info((A,B),I0,I2) :- !, extract_dot_info(A,I0,I1), extract_dot_info(B,I1,I2). | |
472 | extract_dot_info(string(Str),[Type/Str|T],T) :- | |
473 | (infer_string_type(Str,Type) -> true ; Type=label). | |
474 | extract_dot_info(Value,[label/Str|T],T) :- simple_label_value(Value), | |
475 | translate_bvalue(Value,Str). | |
476 | simple_label_value(fd(_,_)). | |
477 | ||
478 | infer_string_type(Str,color) :- valid_rgb_color(Str). | |
479 | infer_string_type(Str,shape) :- valid_dot_shape(Str). | |
480 | infer_string_type(Str,style) :- valid_dot_line_style(Str). | |
481 | infer_string_type(Str,style) :- valid_dot_node_style(Str). | |
482 | ||
483 | % get record fields from record or partial function STRING +-> STRING | |
484 | % and select dot attributes | |
485 | ||
486 | extract_record_fields(Record,Fields,DotAttributes,OtherFields) :- | |
487 | flexible_get_record_fields(Record,Fields), | |
488 | extract_info_from_fields(Fields,DotAttributes,OtherFields). | |
489 | ||
490 | :- use_module(library(lists),[maplist/3]). | |
491 | :- use_module(probsrc(custom_explicit_sets),[try_expand_custom_set_with_catch/3, is_set_value/2]). | |
492 | % similar to get_VISB_record_fields | |
493 | flexible_get_record_fields(rec(Fields),Res) :- !, Res=Fields. | |
494 | flexible_get_record_fields(StringFunction,Fields) :- | |
495 | is_set_value(StringFunction,flexible_get_record_fields), | |
496 | try_expand_custom_set_with_catch(StringFunction,Expanded,get_visb_DEFINITION_svg_object), | |
497 | % TODO: check we have no duplicates | |
498 | maplist(convert_to_field,Expanded,Fields). | |
499 | convert_to_field((string(FieldName),Value),field(FieldName,Value)). | |
500 | ||
501 | extract_info_from_fields([],[],[]). | |
502 | extract_info_from_fields([field(FName,FVAL)|TF],[Type/Str|TI],Val) :- | |
503 | dot_attribute_field(FName,Type),!, | |
504 | ( \+ checked_attribute(Type) -> get_as_string_for_attr(Type,FVAL,Str) | |
505 | ; get_label_value(Type,FVAL,Str) -> true | |
506 | ; add_message(state_custom_dot_graph,'Unexpected value for dot attribute: ',Type/FVAL), | |
507 | get_as_string(FVAL,Str) | |
508 | ), | |
509 | extract_info_from_fields(TF,TI,Val). | |
510 | extract_info_from_fields([field(FName,FVAL)|TF],[FName/EStr|TI],Val) :- | |
511 | \+ definitely_not_dot_attribute(FName), | |
512 | get_as_string(FVAL,Str), | |
513 | !, | |
514 | add_message(state_custom_dot_graph,'Assuming this is a dot attribute: ',FName/Str), | |
515 | string_escape(Str,EStr), | |
516 | extract_info_from_fields(TF,TI,Val). | |
517 | extract_info_from_fields([F|TF],Info,[F|TVal]) :- | |
518 | extract_info_from_fields(TF,Info,TVal). | |
519 | ||
520 | get_label_value(label,Val,Str) :- !, get_as_string(Val,Str). | |
521 | get_label_value(description,string(Str),Str). | |
522 | get_label_value(Type,string(Str),Str) :- infer_string_type(Str,Type). | |
523 | get_label_value(color,Val,Str) :- get_color(Val,Str). | |
524 | ||
525 | get_color(string(Str),Val) :- !, Val=Str. | |
526 | get_color(int(Nr),Val) :- !, Val=Nr. % numbers can be valid DOT colors when colorscheme provided | |
527 | get_color(Val,Col) :- | |
528 | try_translate_bvalue_to_colour(Val,Col). % from dot_graph_generator | |
529 | ||
530 | checked_attribute(description). | |
531 | checked_attribute(color). | |
532 | checked_attribute(shape). | |
533 | checked_attribute(style). | |
534 | ||
535 | definitely_not_dot_attribute(edge). | |
536 | definitely_not_dot_attribute(from). | |
537 | definitely_not_dot_attribute(nodes). | |
538 | definitely_not_dot_attribute(to). | |
539 | definitely_not_dot_attribute(value). | |
540 | definitely_not_dot_attribute(E) :- is_edges_field(E,_). | |
541 | definitely_not_dot_attribute(N) :- is_nodes_field(N,_). | |
542 | ||
543 | :- use_module(probsrc(kernel_strings),[to_b_string/2]). | |
544 | get_as_string(BValue,Str) :- to_b_string(BValue,string(Str)). | |
545 | ||
546 | % cf b_value_to_id_string in VisB; allow to use pairs to concatenate strings | |
547 | get_as_id_string(string(SValue),Res) :- !, Res=SValue. | |
548 | get_as_id_string((A,B),Res) :- !, | |
549 | get_as_id_string(A,VA), get_as_id_string(B,VB), atom_concat(VA,VB,Res). | |
550 | % TODO: maybe convert sequence of values using conc | |
551 | get_as_id_string(FValue,Res) :- get_as_string(FValue,Res). | |
552 | ||
553 | get_as_string_for_attr(id,Val,Str) :- !, get_as_id_string(Val,Str). % like SVG ids in VisB | |
554 | get_as_string_for_attr(_,Val,Str) :- !, get_as_string(Val,Str). | |
555 | ||
556 | :- use_module(probsrc(tools_matching),[is_dot_attribute/1]). | |
557 | dot_attribute_field(colour,color). | |
558 | dot_attribute_field(fontcolour,fontcolor). | |
559 | dot_attribute_field(description,description). % virtual attribute | |
560 | dot_attribute_field(stroke,style). % used in SVG | |
561 | dot_attribute_field(Name,Name) :- is_dot_attribute(Name). | |
562 | ||
563 |