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 /* 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
86 expand_data_value(DataValue,S1) :-
87 (custom_explicit_sets:is_custom_explicit_set(DataValue,expand_data_value)
88 -> custom_explicit_sets:try_expand_custom_set(DataValue,S1)
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 grelation([],_,_,_,F,F).
110 grelation([(E0,E1,E2)|T],true,Parent,VariableName,F,Fi) :-
111 % interpret E0 as label for string; note: (E0,E1,E2) matches ((A,B),(C,D))
112 generate_state_for_dot,
113 simple_value(E0),
114 !,
115 translate_inner_node(E1,C1,E1_NewTransitions),
116 translate_inner_node(E2,C2,E2_NewTransitions),
117 translate_bvalue_for_dot(E0,E0String),
118 Label =.. [VariableName,E0String],
119 append([(C1,Label,C2)|E1_NewTransitions],F,F5),
120 append(E2_NewTransitions,F5,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([(C1,VariableName,C2)|E1_NewTransitions],F,F5),
126 append(E2_NewTransitions,F5,F6),
127 grelation(T,MatchTriples,Parent,VariableName,F6,Fi).
128
129
130
131 :- use_module(preferences,[get_preference/2]).
132
133 translate_inner_node(DataValue,NodeinGraph,NewTransitions) :- %% print(trans(DataValue)),nl,
134 % Input: DataValue
135 % Output: NodeinGraph representing DataValue + NewTransitions required to represent the structure
136 (get_preference(dot_state_graph_decompose,false) -> % treat as an atom
137 NewTransitions = [], NodeinGraph = DataValue
138 ; expand_data_value(DataValue,S1),
139 % check whether S1 is a atom/set
140 ( emptyset(S1) -> NodeinGraph = [], %'$Empty_Set',
141 NewTransitions=[]
142 ; cn_value(S1,NodeinGraph) -> NewTransitions=[]
143 ; simple_pair_value(S1),generate_state_for_dot -> NodeinGraph=S1, NewTransitions=[]
144 ; list_set(S1) ->
145 new_sg_node(S1,NodeinGraph),
146 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)
147 ; S1=(P1,P2)
148 -> % a complex pair
149 translate_inner_node(P1,Node1,NewTrans1),
150 translate_inner_node(P2,Node2,NewTrans2),
151 new_sg_node(S1,NodeinGraph),
152 append([(NodeinGraph,'$from',Node1),
153 (NodeinGraph,'$to_el',Node2)|NewTrans1],NewTrans2,NewTransitions)
154 ; % an atom
155 NewTransitions = [],
156 NodeinGraph = S1
157 )
158 ).
159
160 % simple values which can easily be rendered like a record
161 simple_pair_value((A,B)) :- !,simple_pair_value(A), simple_pair_value(B).
162 simple_pair_value(X) :- simple_value(X).
163
164 relation([(_,_)|_]).
165 relation([(X,_,_)|_]) :- generate_state_for_dot, simple_value(X). % TO DO: check if it is a function ?; maybe also support other nested ternary relations
166 emptyset([]).
167 list_set([]).
168 list_set([_|_]).
169 % what about AVL : supposed expanded before
170
171 is_set(avl_set(_)).
172 is_set(X) :- list_set(X).
173
174 simple_value(X) :- atomic(X).
175 simple_value(int(_)).
176 simple_value(fd(_,_)).
177 simple_value(string(_)).
178 simple_value(pred_false).
179 simple_value(pred_true).
180
181 :- dynamic cn/1, cn_value/2.
182
183 reset_n :-
184 retractall(cn(_)),retractall(cn_value(_,_)),asserta(cn(0)).
185
186 /* generate a new state graph node */
187 new_sg_node(Value,abs_cn(J,NestingCol)) :- retract(cn(I)), J is I+1,
188 asserta(cn(J)),
189 get_abstract_node_type_colour(Value,NestingCol),
190 assert(cn_value(Value,abs_cn(J,NestingCol))).
191
192 % for the moment: just compute the "depth/nesting" of the relation; we should do something more intelligent
193 get_abstract_node_type_colour([],C) :- !,C=1.
194 get_abstract_node_type_colour([H|_],C) :- !, get_abstract_node_type_colour(H,CH),
195 C is CH+1.
196 get_abstract_node_type_colour((A,_),C) :- !, get_abstract_node_type_colour(A,CH),
197 C is CH+1.
198 get_abstract_node_type_colour(_,0).
199
200
201 :- use_module(graph_iso_nauty).
202
203 :- use_module(state_space,[current_expression/2]).
204 print_cstate_graph(File) :-
205 current_expression(_,State),
206 print_cstate_graph(State,File).
207 print_cstate_graph(State,File) :-
208 state_graph_for_dot(State,GCE),
209 %print(state_graph(GCE)),nl,
210 (graph2dot(GCE,File) -> true
211 ; add_error(graph_canon,'Dot conversion failed: ',graph2dot(GCE,File))).
212 %,print_nauty_graph(GCE).
213
214 /* ---------------------------- */
215
216 initialise_nauty :- nauty_init.
217 clear_nauty :- nauty_clear.
218
219 add_state_graph_to_nauty(StateExpression,Exists) :-
220 (state_graph(StateExpression,SG)
221 -> add_nauty_graph(SG,Exists)
222 ; add_error(graph_canon,'Could not compute state_graph: ',StateExpression),fail).
223
224 /* ---------------------------- */
225
226
227 graph2dot(G,File) :- reset_dot,
228 tell(File),
229 print('digraph state {\n graph [fontsize=12]\nrankdir=TB;\n'),
230 %print('digraph state {\n graph [page=\"8.5, 11\",ratio=fill,size=\"7.5,10\"];\n'),
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 :- dynamic node_col/4.
287 add_node(X,_) :- node_col(X,_,_,_),!. % already processed
288 add_node(sg_root,Translation) :-
289 assert(node_col(sg_root,Translation,lightblue,diamond)).
290 add_node(fd(X,Type),Translation) :- !,
291 get_col_assoc(node,Type,Col),
292 assert(node_col(fd(X,Type),Translation,Col,box)).
293 add_node(int(X),Translation) :- !,
294 Col = 'wheat3', %get_col_assoc(node,integer,Col),
295 assert(node_col(int(X),Translation,Col,box)).
296 add_node(string(X),Translation) :- !,
297 Col = 'khaki1', %'lavender' 'burlywood', %get_col_assoc(node,integer,Col),
298 assert(node_col(string(X),Translation,Col,box)).
299 add_node(pred_true,T) :- !, assert(node_col(pred_true,T,'OliveDrab4',ellipse)).
300 add_node(pred_false,T) :- !, assert(node_col(pred_false,T,brown,ellipse)).
301 add_node(RecordOrPair,Translation) :- get_fields(RecordOrPair,Fields),!,
302 translate_fields(Fields,Atoms),
303 ajoin(['|{ ' | Atoms], RecTranslation),
304 assert(node_col(RecordOrPair,Translation,burlywood,record(RecTranslation))). % TO DO: maybe use dot record
305 add_node(Val,Translation) :- is_set(Val),!,
306 Col = 'LightSteelBlue1', %get_col_assoc(node,integer,Col),
307 assert(node_col(Val,Translation,Col,box)).
308 add_node(_Val,_Translation).
309
310 get_fields(rec(Fields),Fields).
311 get_fields((A,B),Fields) :- get_pair_fields((A,B),Fields,[]).
312
313 get_pair_fields((A,B)) --> !, get_pair_fields(A), get_pair_fields(B).
314 get_pair_fields(A) --> [field(prj,A)].
315
316 translate_fields([],[' }|']).
317 translate_fields([field(Name,Value)],Res) :- !,
318 trans_field(Name,VS,Res,[' }|']),
319 translate_bvalue_for_dot(Value,VS).
320 translate_fields([field(Name,Value)|T],Res) :-
321 trans_field(Name,VS,Res,['|' | Rest]),
322 translate_bvalue_for_dot(Value,VS),
323 translate_fields(T,Rest).
324
325 trans_field(prj,VS, [' { ', VS, ' } ' | Rest], Rest) :- !.
326 trans_field(Name,VS, [' { ',Name,' | ', VS, ' } ' | Rest], Rest).
327
328 :- dynamic col_association/3. % store colours used for types, edge labels,...
329 get_col_assoc(Domain,T,Col) :- col_association(Domain,T,Col),!.
330 get_col_assoc(Domain,T,Col) :- get_next_col(Domain,Col),
331 assert(col_association(Domain,T,Col)).
332
333 get_next_col(Type,Col) :- retract(cur_col(Type,N)),!, N1 is N+1,
334 (default_colours(N1,Col) -> NX=N1
335 ; NX = 1, default_colours(1,Col)),
336 assert(cur_col(Type,NX)).
337 get_next_col(_T,red).
338
339 :- dynamic cur_col/2.
340 cur_col(node,0).
341 cur_col(edge,99).
342 default_colours(1,'#efdf84').
343 default_colours(2,'#bdef6b').
344 default_colours(3,'#5863ee').
345 default_colours(4,'LightSteelBlue1').
346 default_colours(5,gray).
347
348 default_colours(100,firebrick).
349 default_colours(101,sienna).
350 default_colours(102,'SlateBlue4').
351 default_colours(103,black).
352
353 translate_abs_cn_node(AA,ColAA,Translation) :-
354 tools:string_concatenate('_',AA,AID1),
355 tools:string_concatenate(ColAA,AID1,AID2),
356 tools:string_concatenate('abs',AID2,Translation).
357
358 clusters2dot([]).
359 clusters2dot([cluster(Name,Elements)|T]) :-
360 format('subgraph \"cluster_~w\" {node [style=filled,color=white]; label=\"~w\"; style=filled;color=lightgrey; ',[Name,Name]),
361 nodes2dot(Elements),
362 clusters2dot(T).
363
364 nodes2dot([]) :- print('}'),nl.
365 nodes2dot([H|T]) :-
366 translate:translate_params_for_dot([H],HP),
367 %format('~w; ',[HP]),
368 tools:print_escaped(HP), print('; '),
369 nodes2dot(T).
370
371
372 /**********************************************/
373
374 /****** CANONICAL LABELLING USING LEXICOGRAPHIC AND AUTOMORHISM PRUNING: *******
375 ****** Makes use of Schreier-Sims data structure defined in Kreher's *******
376 ****** C.A.G.E.S book, and uses the techniques for pruning described in *******
377 ****** the chapter 7. *******/
378
379
380
381 /*******************************************************************
382 */
383 % schreiersims.pl implementation of the schreier sims representation of an
384 % automorphism group taken from Kreher's Combinatorial Algorithms book. Provides
385 % method for membership test of a permutation in the group that should run in O(n^2)
386 % time. Plans are not to spend time on implementing a method for listing all permutations
387 % represented in the group -- since this is not required at the time of writing.
388
389 % THIS IS NOT CURRENTLY USED, BUT WAS ONCE USED TO MORE CLOSELY FOLLOW NAUTY.
390 % HOWEVER, USING SCHREIERSIMS STRUCTURES IMPLEMENTATION IS VERY LIST INTENSIVE
391 % RESULTING IN A POOR PERFORMANCE -- HENCE NOT USED NOW. FUTURE WORK MAY WANT
392 % TO LOOK AT ITS USE BELOW..
393
394
395 /*** END OF CANONICAL LABELLING USING LEXICOGRAPHIC AND AUTOMORPHISM PRUNING ***/