1 | | % (c) 2009-2020 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 | | /* graph_canon.pl - graph isomorphism module 1/11/2005 */ |
5 | | |
6 | | :- module(graph_canon, [ |
7 | | print_cstate_graph/2, print_cstate_graph/1, |
8 | | initialise_nauty/0, clear_nauty/0, |
9 | | add_state_graph_to_nauty/2 |
10 | | ]). |
11 | | |
12 | | |
13 | | :- use_module(error_manager). |
14 | | |
15 | | %:- compile(sp4_compatibility). |
16 | | :- use_module(tools). |
17 | | |
18 | | :- use_module(module_information,[module_info/2]). |
19 | | :- module_info(group,symmetry). |
20 | | :- module_info(description,'Compute canonical forms of state graphs and store them using nauty C interface.'). |
21 | | |
22 | | |
23 | | |
24 | | /* given the properties clause of the bmachine, extract the names of the |
25 | | known constants, in the order of their declaration */ |
26 | | % currently works only for machines that do not use inheritance |
27 | | |
28 | | % removed |
29 | | |
30 | | % ------------------------------------------------------------------------------ |
31 | | |
32 | | /* Assert all the elements of the sets used by this machine, for this session of ProB, |
33 | | and also those that are symmetric or not */ |
34 | | % assert_global_set_info :- better use b_global_sets now |
35 | | |
36 | | /******************************************************************************/ |
37 | | |
38 | | /******** STATE AS SINGLE GRAPH ***************/ |
39 | | :- use_module(specfile,[expand_const_and_vars/3]). |
40 | | |
41 | | :- dynamic generate_state_for_dot/0. |
42 | | state_graph_for_dot(State,R) :- |
43 | | assert(generate_state_for_dot), |
44 | | call_cleanup(state_graph(State,R), retract(generate_state_for_dot)). |
45 | | |
46 | | state_graph(root,R) :- !,R=[]. |
47 | | state_graph(concrete_constants(C),SG) :- !, state_graph(C,SG). |
48 | | state_graph(const_and_vars(ConstID,S),SG) :- !, |
49 | | expand_const_and_vars(ConstID,S,Full), |
50 | | reset_n, |
51 | | state_graph(Full,[],SG). |
52 | | state_graph(S,SG) :- |
53 | | reset_n, |
54 | | state_graph(S,[],SG). |
55 | | state_graph([],Final,Final). |
56 | | state_graph([bind(VarName,Value)|T],C,F) :- |
57 | | tools:string_escape(VarName,EscVarName), |
58 | | (top_level_translate_node(Value,EscVarName,PG) -> true |
59 | | %print(translate(Value,VarName,PG)),nl |
60 | | ; add_error(state_graph,'Call failed: ',top_level_translate_node(Value,VarName,PG))), |
61 | | append(PG,C,C2), |
62 | | state_graph(T,C2,F). |
63 | | |
64 | | top_level_translate_node(DataValue,VariableName,NewTransitions) :- |
65 | | % Input: DataValue |
66 | | % Output: NewTransitions required to represent the structure |
67 | | % In contrast to translate_inner_node, we do not generate new inner artificial nodes; |
68 | | % VariableName is used as an arc-label to encode the top-level information |
69 | | expand_data_value(DataValue,S1), |
70 | | % check whether S1 is a relation/atom/set |
71 | ? | ( relation(S1) -> gen_relation(S1,VariableName,NewTransitions) |
72 | | ; emptyset(S1) -> NewTransitions = [(sg_root,VariableName,sg_root)] |
73 | | %% [('$Empty_Set',VariableName,sg_root)] has problems as we cannot distinguish between v={} and v={{}} |
74 | | %% [] has problems when we have set_up_constants and variables which are all initialised with |
75 | | %% the empty set: then we get confused between set_up_constants & initialise_machine |
76 | | ; list_set(S1) -> gset(S1,sg_root,VariableName,[],NewTransitions) |
77 | | ; S1=(P1,P2) -> % a pair |
78 | | translate_inner_node(P1,Node1,NewTrans1), |
79 | | translate_inner_node(P2,Node2,NewTrans2), |
80 | | append([(Node1,VariableName,Node2)|NewTrans1],NewTrans2,NewTransitions) |
81 | | ; % an atom |
82 | | NewTransitions = [(DataValue,VariableName,sg_root)] |
83 | | ). |
84 | | |
85 | | :- use_module(custom_explicit_sets,[is_custom_explicit_set/2, try_expand_custom_set_with_catch/3]). |
86 | | expand_data_value(DataValue,S1) :- |
87 | | (is_custom_explicit_set(DataValue,expand_data_value) |
88 | | -> try_expand_custom_set_with_catch(DataValue,S1,expand_data_value) |
89 | | ; DataValue=S1 |
90 | | ). |
91 | | % TO DO: convert to Difference-List to get rid of all the appends below |
92 | | |
93 | | |
94 | | gset([],_,_,F,F). |
95 | | gset([S1|T],Parent,TransitionLabel,F,Fi) :- |
96 | | translate_inner_node(S1,C1,S1_NewTransitions), |
97 | | append([(C1,TransitionLabel,Parent)|S1_NewTransitions],F,F4), |
98 | | gset(T,Parent,TransitionLabel,F4,Fi). |
99 | | |
100 | | gen_relation(S1,VariableName,NewTransitions) :- |
101 | | (S1=[H|_],is_pair_to_pair(H) -> MatchTriples=false ; MatchTriples=true), |
102 | | grelation(S1,MatchTriples,sg_root,VariableName,[],NewTransitions). |
103 | | |
104 | | :- use_module(kernel_objects,[infer_value_type/2]). |
105 | | is_pair_to_pair(((A,B),(C,D))) :- |
106 | | infer_value_type(A,T1), infer_value_type(C,T1), |
107 | | infer_value_type(B,T2), infer_value_type(D,T2). |
108 | | |
109 | | :- use_module(library(lists),[append/2]). |
110 | | grelation([],_,_,_,F,F). |
111 | | grelation([(E0,E1,E2)|T],true,Parent,VariableName,F,Fi) :- |
112 | | % interpret E0 as label for string; note: (E0,E1,E2) matches ((A,B),(C,D)) |
113 | | generate_state_for_dot, |
114 | | simple_value(E0), |
115 | | !, |
116 | | translate_inner_node(E1,C1,E1_NewTransitions), |
117 | | translate_inner_node(E2,C2,E2_NewTransitions), |
118 | | translate_bvalue_for_dot(E0,E0String), |
119 | | Label =.. [VariableName,E0String], |
120 | | append([E2_NewTransitions,[(C1,Label,C2)|E1_NewTransitions],F],F6), |
121 | | grelation(T,true,Parent,VariableName,F6,Fi). |
122 | | grelation([(E1,E2)|T],MatchTriples,Parent,VariableName,F,Fi) :- |
123 | | translate_inner_node(E1,C1,E1_NewTransitions), |
124 | | translate_inner_node(E2,C2,E2_NewTransitions), |
125 | | append([E2_NewTransitions,[(C1,VariableName,C2)|E1_NewTransitions],F],F6), |
126 | | grelation(T,MatchTriples,Parent,VariableName,F6,Fi). |
127 | | |
128 | | |
129 | | |
130 | | :- use_module(preferences,[get_preference/2]). |
131 | | |
132 | | translate_inner_node(DataValue,NodeinGraph,NewTransitions) :- %% print(trans(DataValue)),nl, |
133 | | % Input: DataValue |
134 | | % Output: NodeinGraph representing DataValue + NewTransitions required to represent the structure |
135 | | (get_preference(dot_state_graph_decompose,false) -> % treat as an atom |
136 | | NewTransitions = [], NodeinGraph = DataValue |
137 | | ; expand_data_value(DataValue,S1), |
138 | | % check whether S1 is a atom/set |
139 | | ( emptyset(S1) -> NodeinGraph = [], %'$Empty_Set', |
140 | | NewTransitions=[] |
141 | ? | ; cn_value(S1,NodeinGraph) -> NewTransitions=[] |
142 | ? | ; simple_pair_value(S1),generate_state_for_dot -> NodeinGraph=S1, NewTransitions=[] |
143 | | ; list_set(S1) -> |
144 | | new_sg_node(S1,NodeinGraph), |
145 | | gset(S1,NodeinGraph,'$to_el',[],NewTransitions) % use the $to_el label to encode membership, using ':' would be more readable; but less efficient for symmetry (extra layers required) |
146 | | ; S1=(P1,P2) |
147 | | -> % a complex pair |
148 | | translate_inner_node(P1,Node1,NewTrans1), |
149 | | translate_inner_node(P2,Node2,NewTrans2), |
150 | | new_sg_node(S1,NodeinGraph), |
151 | | append([(NodeinGraph,'$from',Node1), |
152 | | (NodeinGraph,'$to_el',Node2)|NewTrans1],NewTrans2,NewTransitions) |
153 | | ; % an atom |
154 | | NewTransitions = [], |
155 | | NodeinGraph = S1 |
156 | | ) |
157 | | ). |
158 | | |
159 | | % simple values which can easily be rendered like a record |
160 | | simple_pair_value((A,B)) :- !,simple_pair_value(A), simple_pair_value(B). |
161 | ? | simple_pair_value(X) :- simple_value(X). |
162 | | |
163 | | relation([(_,_)|_]). |
164 | | relation([(X,_,_)|_]) :- generate_state_for_dot, simple_value(X). % TO DO: check if it is a function ?; maybe also support other nested ternary relations |
165 | | emptyset([]). |
166 | | list_set([]). |
167 | | list_set([_|_]). |
168 | | % what about AVL : supposed expanded before |
169 | | |
170 | | is_set(avl_set(_)). |
171 | | is_set(X) :- list_set(X). |
172 | | |
173 | | simple_value(X) :- atomic(X). |
174 | | simple_value(int(_)). |
175 | | simple_value(fd(_,_)). |
176 | | simple_value(string(_)). |
177 | | simple_value(pred_false). |
178 | | simple_value(pred_true). |
179 | | |
180 | | :- dynamic cn/1, cn_value/2. |
181 | | |
182 | | reset_n :- |
183 | | retractall(cn(_)),retractall(cn_value(_,_)),asserta(cn(0)). |
184 | | |
185 | | /* generate a new state graph node */ |
186 | | new_sg_node(Value,abs_cn(J,NestingCol)) :- retract(cn(I)), J is I+1, |
187 | | asserta(cn(J)), |
188 | | get_abstract_node_type_colour(Value,NestingCol), |
189 | | assert(cn_value(Value,abs_cn(J,NestingCol))). |
190 | | |
191 | | % for the moment: just compute the "depth/nesting" of the relation; we should do something more intelligent |
192 | | get_abstract_node_type_colour([],C) :- !,C=1. |
193 | | get_abstract_node_type_colour([H|_],C) :- !, get_abstract_node_type_colour(H,CH), |
194 | | C is CH+1. |
195 | | get_abstract_node_type_colour((A,_),C) :- !, get_abstract_node_type_colour(A,CH), |
196 | | C is CH+1. |
197 | | get_abstract_node_type_colour(_,0). |
198 | | |
199 | | |
200 | | :- use_module(graph_iso_nauty). |
201 | | |
202 | | :- use_module(state_space,[current_expression/2]). |
203 | | print_cstate_graph(File) :- |
204 | | current_expression(_,State), |
205 | | print_cstate_graph(State,File). |
206 | | print_cstate_graph(State,File) :- |
207 | | state_graph_for_dot(State,GCE), |
208 | | %print(state_graph(GCE)),nl, |
209 | | (graph2dot(GCE,File) -> true |
210 | | ; add_error(graph_canon,'Dot conversion failed: ',graph2dot(GCE,File))). |
211 | | %,print_nauty_graph(GCE). |
212 | | |
213 | | /* ---------------------------- */ |
214 | | |
215 | | initialise_nauty :- nauty_init. |
216 | | clear_nauty :- nauty_clear. |
217 | | |
218 | | add_state_graph_to_nauty(StateExpression,Exists) :- |
219 | | (state_graph(StateExpression,SG) |
220 | | -> add_nauty_graph(SG,Exists) |
221 | | ; add_error(graph_canon,'Could not compute state_graph: ',StateExpression),fail). |
222 | | |
223 | | /* ---------------------------- */ |
224 | | |
225 | | |
226 | | graph2dot(G,File) :- reset_dot, |
227 | | (get_preference(dot_horizontal_layout,true) -> RDir='LR'; RDir='TB'), |
228 | | PSize='', %(get_preference(dot_with_page_size,true) -> PSize='page="8.5, 11",ratio=fill,size="7.5,10",' ; PSize=''), |
229 | | tell(File), |
230 | | format('digraph state {\n graph [~wfontsize=12]\nrankdir=~w;~n',[PSize,RDir]), |
231 | | edges2dot(G), |
232 | | nodes2dot, |
233 | | findall(cluster(Ty,El),cluster(Ty,El),T), |
234 | | clusters2dot(T), |
235 | | print('}'), |
236 | | told. |
237 | | :- use_module(b_global_sets). |
238 | ? | cluster(Type,Elements) :- b_global_set(Type), |
239 | | % compute all elements of global sets which are used in current state graph |
240 | | findall(Translation, (enum_global_type(El,Type), node_col(El,Translation,_,_)),Elements). |
241 | | % maybe add boolean ?? |
242 | | edges2dot([]). |
243 | | edges2dot([(A,B,C)|T]) :- /* edge from A -> C with label B */ |
244 | | translate_node_value(A,AID), |
245 | | (B = abs_cn(BB,ColBB) |
246 | | -> translate_abs_cn_node(BB,ColBB,EdgeLabel) |
247 | | ; EdgeLabel = B), |
248 | | translate_node_value(C,CID), |
249 | | get_col_assoc(edge,EdgeLabel,EdgCol), |
250 | | format('\"~w\" -> \"~w\" [label = \"~w\", color = \"~w\"];\n', |
251 | | [AID,CID,EdgeLabel,EdgCol]), |
252 | | edges2dot(T). |
253 | | |
254 | | reset_dot :- retractall(col_association(_,_,_)), |
255 | | retractall(node_col(_,_,_,_)), |
256 | | retractall(cur_col(_,_)), |
257 | | assert(cur_col(node,0)), assert(cur_col(edge,99)). |
258 | | |
259 | | translate_node_value(abs_cn(AA,ColAA), Translation) :- !, |
260 | | translate_abs_cn_node(AA,ColAA,Translation). |
261 | | translate_node_value(sg_root,Translation) :- !, |
262 | | Translation = 'ROOT-NODE', add_node(sg_root,Translation). |
263 | | translate_node_value(Val,Translation) :- |
264 | | translate_bvalue_for_dot(Val,Translation), |
265 | | add_node(Val,Translation). |
266 | | |
267 | | translate_bvalue_for_dot(string(S),Translation) :- !, |
268 | | % normal quotes confuse dot |
269 | | %ajoin(['''''',S,''''''],Translation). |
270 | | tools:string_escape(S,ES), |
271 | | ajoin(['\\"',ES,'\\"'],Translation). |
272 | | translate_bvalue_for_dot(Val,ETranslation) :- |
273 | | translate:translate_bvalue(Val,Translation), |
274 | | tools:string_escape(Translation,ETranslation). |
275 | | |
276 | ? | nodes2dot :- node_col(_,Translation,Col,Shape), |
277 | | (Shape=record(Label) |
278 | | -> |
279 | | format('\"~w\" [shape=record, label=\"~w\", color = \"~w\", style = \"filled, solid\"]\n',[Translation,Label,Col]) |
280 | | ; |
281 | | format('\"~w\" [color = \"~w\", style = \"filled, solid\", shape = \"~w\"]\n',[Translation,Col,Shape]) |
282 | | ), |
283 | | fail. |
284 | | nodes2dot. |
285 | | |
286 | | :- use_module(kernel_reals,[is_real/2]). |
287 | | :- dynamic node_col/4. |
288 | ? | add_node(X,_) :- node_col(X,_,_,_),!. % already processed |
289 | | add_node(sg_root,Translation) :- |
290 | | assert(node_col(sg_root,Translation,lightblue,diamond)). |
291 | | add_node(fd(X,Type),Translation) :- !, |
292 | | get_col_assoc(node,Type,Col), |
293 | | get_preference(dot_normal_node_shape,Shape), |
294 | | assert(node_col(fd(X,Type),Translation,Col,Shape)). |
295 | | add_node(int(X),Translation) :- !, |
296 | | Col = 'wheat3', %get_col_assoc(node,integer,Col), |
297 | | get_preference(dot_normal_node_shape,Shape), |
298 | | assert(node_col(int(X),Translation,Col,Shape)). |
299 | | add_node(string(X),Translation) :- !, |
300 | | Col = 'khaki1', %'lavender' 'burlywood', %get_col_assoc(node,integer,Col), |
301 | | get_preference(dot_normal_node_shape,Shape), |
302 | | assert(node_col(string(X),Translation,Col,Shape)). |
303 | | add_node(pred_true,T) :- !, assert(node_col(pred_true,T,'OliveDrab4',ellipse)). |
304 | | add_node(pred_false,T) :- !, assert(node_col(pred_false,T,brown,ellipse)). |
305 | | add_node(RecordOrPair,Translation) :- get_fields(RecordOrPair,Fields),!, |
306 | | translate_fields(Fields,Atoms), |
307 | | ajoin(['|{ ' | Atoms], RecTranslation), |
308 | | assert(node_col(RecordOrPair,Translation,burlywood,record(RecTranslation))). % TO DO: maybe use dot record |
309 | | add_node(Val,Translation) :- is_set(Val),!, |
310 | | Col = 'LightSteelBlue1', %get_col_assoc(node,integer,Col), |
311 | | get_preference(dot_normal_node_shape,Shape), |
312 | | assert(node_col(Val,Translation,Col,Shape)). |
313 | | add_node(Term,Translation) :- is_real(Term,_),!, |
314 | | Col = 'wheat2', %get_col_assoc(node,integer,Col), |
315 | | get_preference(dot_normal_node_shape,Shape), |
316 | | assert(node_col(Term,Translation,Col,Shape)). |
317 | | add_node(_Val,_Translation). |
318 | | |
319 | | get_fields(rec(Fields),Fields). |
320 | | get_fields((A,B),Fields) :- get_pair_fields((A,B),Fields,[]). |
321 | | |
322 | | get_pair_fields((A,B)) --> !, get_pair_fields(A), get_pair_fields(B). |
323 | | get_pair_fields(A) --> [field(prj,A)]. |
324 | | |
325 | | translate_fields([],[' }|']). |
326 | | translate_fields([field(Name,Value)],Res) :- !, |
327 | | trans_field(Name,VS,Res,[' }|']), |
328 | | translate_bvalue_for_dot(Value,VS). |
329 | | translate_fields([field(Name,Value)|T],Res) :- |
330 | | trans_field(Name,VS,Res,['|' | Rest]), |
331 | | translate_bvalue_for_dot(Value,VS), |
332 | | translate_fields(T,Rest). |
333 | | |
334 | | trans_field(prj,VS, [' { ', VS, ' } ' | Rest], Rest) :- !. |
335 | | trans_field(Name,VS, [' { ',Name,' | ', VS, ' } ' | Rest], Rest). |
336 | | |
337 | | :- dynamic col_association/3. % store colours used for types, edge labels,... |
338 | | get_col_assoc(Domain,T,Col) :- col_association(Domain,T,Col),!. |
339 | | get_col_assoc(Domain,T,Col) :- get_next_col(Domain,Col), |
340 | | assert(col_association(Domain,T,Col)). |
341 | | |
342 | | get_next_col(Type,Col) :- retract(cur_col(Type,N)),!, N1 is N+1, |
343 | | (default_colours(N1,Col) -> NX=N1 |
344 | | ; NX = 1, default_colours(1,Col)), |
345 | | assert(cur_col(Type,NX)). |
346 | | get_next_col(_T,red). |
347 | | |
348 | | :- dynamic cur_col/2. |
349 | | cur_col(node,0). |
350 | | cur_col(edge,99). |
351 | | default_colours(1,'#efdf84'). |
352 | | default_colours(2,'#bdef6b'). |
353 | | default_colours(3,'#5863ee'). |
354 | | default_colours(4,'LightSteelBlue1'). |
355 | | default_colours(5,gray). |
356 | | |
357 | | default_colours(100,firebrick). |
358 | | default_colours(101,sienna). |
359 | | default_colours(102,'SlateBlue4'). |
360 | | default_colours(103,black). |
361 | | |
362 | | translate_abs_cn_node(AA,ColAA,Translation) :- |
363 | | tools:string_concatenate('_',AA,AID1), |
364 | | tools:string_concatenate(ColAA,AID1,AID2), |
365 | | tools:string_concatenate('abs',AID2,Translation). |
366 | | |
367 | | clusters2dot([]). |
368 | | clusters2dot([cluster(Name,Elements)|T]) :- |
369 | | tools:string_escape(Name,EscName), |
370 | | format('subgraph \"cluster_~w\" {node [style=filled,color=white]; label=\"~w\"; style=filled;color=lightgrey; ',[EscName,EscName]), |
371 | | nodes2dot(Elements), |
372 | | clusters2dot(T). |
373 | | |
374 | | nodes2dot([]) :- print('}'),nl. |
375 | | nodes2dot([H|T]) :- |
376 | | translate:translate_params_for_dot([H],HP), |
377 | | %format('~w; ',[HP]), |
378 | | tools:print_escaped(HP), print('; '), |
379 | | nodes2dot(T). |
380 | | |
381 | | |
382 | | /**********************************************/ |
383 | | |
384 | | /****** CANONICAL LABELLING USING LEXICOGRAPHIC AND AUTOMORHISM PRUNING: ******* |
385 | | ****** Makes use of Schreier-Sims data structure defined in Kreher's ******* |
386 | | ****** C.A.G.E.S book, and uses the techniques for pruning described in ******* |
387 | | ****** the chapter 7. *******/ |
388 | | |
389 | | |
390 | | |
391 | | /******************************************************************* |
392 | | */ |
393 | | % schreiersims.pl implementation of the schreier sims representation of an |
394 | | % automorphism group taken from Kreher's Combinatorial Algorithms book. Provides |
395 | | % method for membership test of a permutation in the group that should run in O(n^2) |
396 | | % time. Plans are not to spend time on implementing a method for listing all permutations |
397 | | % represented in the group -- since this is not required at the time of writing. |
398 | | |
399 | | % THIS IS NOT CURRENTLY USED, BUT WAS ONCE USED TO MORE CLOSELY FOLLOW NAUTY. |
400 | | % HOWEVER, USING SCHREIERSIMS STRUCTURES IMPLEMENTATION IS VERY LIST INTENSIVE |
401 | | % RESULTING IN A POOR PERFORMANCE -- HENCE NOT USED NOW. FUTURE WORK MAY WANT |
402 | | % TO LOOK AT ITS USE BELOW.. |
403 | | |
404 | | |
405 | | /*** END OF CANONICAL LABELLING USING LEXICOGRAPHIC AND AUTOMORPHISM PRUNING ***/ |