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 ***/