1 % (c) 2009-2026 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 /* originally graph_canon.pl - graph isomorphism module 1/11/2005 */
6
7 :- module(state_graph_canon, [
8 state_graph/2,
9 state_graph_for_dot/2
10 ]).
11
12
13 :- use_module(probsrc(error_manager)).
14
15 %:- compile(sp4_compatibility).
16 :- use_module(probsrc(tools)).
17
18 :- use_module(probsrc(module_information),[module_info/2]).
19 :- module_info(group,symmetry).
20 :- module_info(description,'Compute canonical forms of state as graphs.').
21
22
23 /* given the properties clause of the bmachine, extract the names of the
24 known constants, in the order of their declaration */
25 % currently works only for machines that do not use inheritance
26
27 % removed
28
29 % ------------------------------------------------------------------------------
30
31 /* Assert all the elements of the sets used by this machine, for this session of ProB,
32 and also those that are symmetric or not */
33 % assert_global_set_info :- better use b_global_sets now
34
35 /******************************************************************************/
36
37
38
39 /******** STATE AS SINGLE GRAPH ***************/
40 :- use_module(probsrc(specfile),[expand_const_and_vars/3]).
41
42 :- dynamic generate_state_for_dot/0.
43
44 state_graph_for_dot(State,R) :-
45 assertz(generate_state_for_dot),
46 call_cleanup(state_graph(State,R), retract(generate_state_for_dot)),
47 !.
48 state_graph_for_dot(State,R) :-
49 add_error(state_graph,'Computing state graph failed for :',State),
50 R=[].
51
52 state_graph(root,R) :- !,R=[].
53 state_graph(concrete_constants(C),SG) :- !, state_graph(C,SG).
54 state_graph(const_and_vars(ConstID,S),SG) :- !,
55 expand_const_and_vars(ConstID,S,Full),
56 reset_n,
57 state_graph(Full,[],SG).
58 state_graph(csp_and_b(_,S),SG) :- !, state_graph(S,SG).
59 state_graph(S,SG) :-
60 reset_n,
61 state_graph(S,[],SG).
62 state_graph([],Final,Final).
63 state_graph([bind(VarName,Value)|T],C,F) :-
64 tools:string_escape(VarName,EscVarName),
65 (top_level_translate_node(Value,EscVarName,PG) -> true
66 %print(translate(Value,VarName,PG)),nl
67 ; add_error(state_graph,'Call failed: ',top_level_translate_node(Value,VarName,PG))),
68 append(PG,C,C2),
69 state_graph(T,C2,F).
70
71 top_level_translate_node(DataValue,VariableName,NewTransitions) :-
72 % Input: DataValue
73 % Output: NewTransitions required to represent the structure
74 % In contrast to translate_inner_node, we do not generate new inner artificial nodes;
75 % VariableName is used as an arc-label to encode the top-level information
76 expand_data_value(DataValue,S1),
77 % check whether S1 is a relation/atom/set
78 ( relation(S1) -> gen_relation(S1,VariableName,NewTransitions)
79 ; emptyset(S1) -> NewTransitions = [(sg_root,VariableName,sg_root)]
80 %% [('$Empty_Set',VariableName,sg_root)] has problems as we cannot distinguish between v={} and v={{}}
81 %% [] has problems when we have set_up_constants and variables which are all initialised with
82 %% the empty set: then we get confused between set_up_constants & initialise_machine
83 ; list_set(S1) -> gset(S1,sg_root,VariableName,[],NewTransitions)
84 ; S1=(P1,P2) -> % a pair
85 translate_inner_node(P1,Node1,NewTrans1),
86 translate_inner_node(P2,Node2,NewTrans2),
87 append([(Node1,VariableName,Node2)|NewTrans1],NewTrans2,NewTransitions)
88 ; % an atom
89 NewTransitions = [(DataValue,VariableName,sg_root)]
90 ).
91
92 :- use_module(probsrc(custom_explicit_sets),[is_custom_explicit_set/2, try_expand_custom_set_with_catch/3]).
93 expand_data_value(DataValue,S1) :-
94 (is_custom_explicit_set(DataValue,expand_data_value)
95 -> try_expand_custom_set_with_catch(DataValue,S1,expand_data_value)
96 ; DataValue=S1
97 ).
98 % TO DO: convert to Difference-List to get rid of all the appends below
99
100
101 gset([],_,_,F,F).
102 gset([S1|T],Parent,TransitionLabel,F,Fi) :-
103 translate_inner_node(S1,C1,S1_NewTransitions),
104 append([(C1,TransitionLabel,Parent)|S1_NewTransitions],F,F4),
105 gset(T,Parent,TransitionLabel,F4,Fi).
106
107 gen_relation(S1,VariableName,NewTransitions) :-
108 (S1=[H|_],is_pair_to_pair(H) -> MatchTriples=false ; MatchTriples=true),
109 grelation(S1,MatchTriples,sg_root,VariableName,[],NewTransitions).
110
111 :- use_module(probsrc(kernel_objects),[infer_value_type/2]).
112 is_pair_to_pair(((A,B),(C,D))) :-
113 infer_value_type(A,T1), infer_value_type(C,T1),
114 infer_value_type(B,T2), infer_value_type(D,T2).
115
116 :- use_module(library(lists),[append/2]).
117 :- use_module(probsrc(translate),[translate_bvalue_for_dot/2]).
118 grelation([],_,_,_,F,F).
119 grelation([(E0,E1,E2)|T],true,Parent,VariableName,F,Fi) :-
120 % interpret E0 as label for string; note: (E0,E1,E2) matches ((A,B),(C,D))
121 generate_state_for_dot,
122 simple_value(E0),
123 !,
124 translate_inner_node(E1,C1,E1_NewTransitions),
125 translate_inner_node(E2,C2,E2_NewTransitions),
126 translate_bvalue_for_dot(E0,E0String),
127 Label =.. [VariableName,E0String],
128 append([E2_NewTransitions,[(C1,Label,C2)|E1_NewTransitions],F],F6),
129 grelation(T,true,Parent,VariableName,F6,Fi).
130 grelation([(E1,E2)|T],MatchTriples,Parent,VariableName,F,Fi) :-
131 translate_inner_node(E1,C1,E1_NewTransitions),
132 translate_inner_node(E2,C2,E2_NewTransitions),
133 append([E2_NewTransitions,[(C1,VariableName,C2)|E1_NewTransitions],F],F6),
134 grelation(T,MatchTriples,Parent,VariableName,F6,Fi).
135
136
137
138 :- use_module(probsrc(preferences),[get_preference/2]).
139
140 translate_inner_node(DataValue,NodeinGraph,NewTransitions) :- %% print(trans(DataValue)),nl,
141 % Input: DataValue
142 % Output: NodeinGraph representing DataValue + NewTransitions required to represent the structure
143 (get_preference(dot_state_graph_decompose,false) -> % treat as an atom
144 NewTransitions = [], NodeinGraph = DataValue
145 ; expand_data_value(DataValue,S1),
146 % check whether S1 is a atom/set
147 ( emptyset(S1) -> NodeinGraph = [], %'$Empty_Set',
148 NewTransitions=[]
149 ; cn_value(S1,NodeinGraph) -> NewTransitions=[]
150 ; simple_pair_value(S1),generate_state_for_dot -> NodeinGraph=S1, NewTransitions=[]
151 ; list_set(S1) ->
152 new_sg_node(S1,NodeinGraph),
153 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)
154 ; S1=(P1,P2)
155 -> % a complex pair
156 translate_inner_node(P1,Node1,NewTrans1),
157 translate_inner_node(P2,Node2,NewTrans2),
158 new_sg_node(S1,NodeinGraph),
159 append([(NodeinGraph,'$from',Node1),
160 (NodeinGraph,'$to_el',Node2)|NewTrans1],NewTrans2,NewTransitions)
161 ; % an atom
162 NewTransitions = [],
163 NodeinGraph = S1
164 )
165 ).
166
167 % simple values which can easily be rendered like a record
168 simple_pair_value((A,B)) :- !,simple_pair_value(A), simple_pair_value(B).
169 simple_pair_value(X) :- simple_value(X).
170
171 relation([(_,_)|_]).
172 relation([(X,_,_)|_]) :- generate_state_for_dot, simple_value(X). % TO DO: check if it is a function ?; maybe also support other nested ternary relations
173 emptyset([]).
174 list_set([]).
175 list_set([_|_]).
176 % what about AVL : supposed expanded before
177
178
179 simple_value(X) :- atomic(X).
180 simple_value(int(_)).
181 simple_value(fd(_,_)).
182 simple_value(string(_)).
183 simple_value(pred_false).
184 simple_value(pred_true).
185
186 :- dynamic cn/1, cn_value/2.
187
188 reset_n :-
189 retractall(cn(_)),retractall(cn_value(_,_)),asserta(cn(0)).
190
191 /* generate a new state graph node */
192 new_sg_node(Value,abs_cn(J,NestingCol)) :- retract(cn(I)), J is I+1,
193 asserta(cn(J)),
194 get_abstract_node_type_colour(Value,NestingCol),
195 assertz(cn_value(Value,abs_cn(J,NestingCol))).
196
197 % for the moment: just compute the "depth/nesting" of the relation; we should do something more intelligent
198 get_abstract_node_type_colour([],C) :- !,C=1.
199 get_abstract_node_type_colour([H|_],C) :- !, get_abstract_node_type_colour(H,CH),
200 C is CH+1.
201 get_abstract_node_type_colour((A,_),C) :- !, get_abstract_node_type_colour(A,CH),
202 C is CH+1.
203 get_abstract_node_type_colour(_,0).
204
205
206
207 /**********************************************/
208
209 /****** CANONICAL LABELLING USING LEXICOGRAPHIC AND AUTOMORHISM PRUNING: *******
210 ****** Makes use of Schreier-Sims data structure defined in Kreher's *******
211 ****** C.A.G.E.S book, and uses the techniques for pruning described in *******
212 ****** the chapter 7. *******/
213
214
215
216 /*******************************************************************
217 */
218 % schreiersims.pl implementation of the schreier sims representation of an
219 % automorphism group taken from Kreher's Combinatorial Algorithms book. Provides
220 % method for membership test of a permutation in the group that should run in O(n^2)
221 % time. Plans are not to spend time on implementing a method for listing all permutations
222 % represented in the group -- since this is not required at the time of writing.
223
224 % THIS IS NOT CURRENTLY USED, BUT WAS ONCE USED TO MORE CLOSELY FOLLOW NAUTY.
225 % HOWEVER, USING SCHREIERSIMS STRUCTURES IMPLEMENTATION IS VERY LIST INTENSIVE
226 % RESULTING IN A POOR PERFORMANCE -- HENCE NOT USED NOW. FUTURE WORK MAY WANT
227 % TO LOOK AT ITS USE BELOW..
228
229
230 /*** END OF CANONICAL LABELLING USING LEXICOGRAPHIC AND AUTOMORPHISM PRUNING ***/