1 | | % (c) 2009-2024 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(root,R) :- !,R=[]. |
49 | | state_graph(concrete_constants(C),SG) :- !, state_graph(C,SG). |
50 | | state_graph(const_and_vars(ConstID,S),SG) :- !, |
51 | | expand_const_and_vars(ConstID,S,Full), |
52 | | reset_n, |
53 | | state_graph(Full,[],SG). |
54 | | state_graph(S,SG) :- |
55 | | reset_n, |
56 | | state_graph(S,[],SG). |
57 | | state_graph([],Final,Final). |
58 | | state_graph([bind(VarName,Value)|T],C,F) :- |
59 | | tools:string_escape(VarName,EscVarName), |
60 | | (top_level_translate_node(Value,EscVarName,PG) -> true |
61 | | %print(translate(Value,VarName,PG)),nl |
62 | | ; add_error(state_graph,'Call failed: ',top_level_translate_node(Value,VarName,PG))), |
63 | | append(PG,C,C2), |
64 | | state_graph(T,C2,F). |
65 | | |
66 | | top_level_translate_node(DataValue,VariableName,NewTransitions) :- |
67 | | % Input: DataValue |
68 | | % Output: NewTransitions required to represent the structure |
69 | | % In contrast to translate_inner_node, we do not generate new inner artificial nodes; |
70 | | % VariableName is used as an arc-label to encode the top-level information |
71 | | expand_data_value(DataValue,S1), |
72 | | % check whether S1 is a relation/atom/set |
73 | ? | ( relation(S1) -> gen_relation(S1,VariableName,NewTransitions) |
74 | | ; emptyset(S1) -> NewTransitions = [(sg_root,VariableName,sg_root)] |
75 | | %% [('$Empty_Set',VariableName,sg_root)] has problems as we cannot distinguish between v={} and v={{}} |
76 | | %% [] has problems when we have set_up_constants and variables which are all initialised with |
77 | | %% the empty set: then we get confused between set_up_constants & initialise_machine |
78 | | ; list_set(S1) -> gset(S1,sg_root,VariableName,[],NewTransitions) |
79 | | ; S1=(P1,P2) -> % a pair |
80 | | translate_inner_node(P1,Node1,NewTrans1), |
81 | | translate_inner_node(P2,Node2,NewTrans2), |
82 | | append([(Node1,VariableName,Node2)|NewTrans1],NewTrans2,NewTransitions) |
83 | | ; % an atom |
84 | | NewTransitions = [(DataValue,VariableName,sg_root)] |
85 | | ). |
86 | | |
87 | | :- use_module(probsrc(custom_explicit_sets),[is_custom_explicit_set/2, try_expand_custom_set_with_catch/3]). |
88 | | expand_data_value(DataValue,S1) :- |
89 | | (is_custom_explicit_set(DataValue,expand_data_value) |
90 | | -> try_expand_custom_set_with_catch(DataValue,S1,expand_data_value) |
91 | | ; DataValue=S1 |
92 | | ). |
93 | | % TO DO: convert to Difference-List to get rid of all the appends below |
94 | | |
95 | | |
96 | | gset([],_,_,F,F). |
97 | | gset([S1|T],Parent,TransitionLabel,F,Fi) :- |
98 | | translate_inner_node(S1,C1,S1_NewTransitions), |
99 | | append([(C1,TransitionLabel,Parent)|S1_NewTransitions],F,F4), |
100 | | gset(T,Parent,TransitionLabel,F4,Fi). |
101 | | |
102 | | gen_relation(S1,VariableName,NewTransitions) :- |
103 | | (S1=[H|_],is_pair_to_pair(H) -> MatchTriples=false ; MatchTriples=true), |
104 | | grelation(S1,MatchTriples,sg_root,VariableName,[],NewTransitions). |
105 | | |
106 | | :- use_module(probsrc(kernel_objects),[infer_value_type/2]). |
107 | | is_pair_to_pair(((A,B),(C,D))) :- |
108 | | infer_value_type(A,T1), infer_value_type(C,T1), |
109 | | infer_value_type(B,T2), infer_value_type(D,T2). |
110 | | |
111 | | :- use_module(library(lists),[append/2]). |
112 | | :- use_module(probsrc(translate),[translate_bvalue_for_dot/2]). |
113 | | grelation([],_,_,_,F,F). |
114 | | grelation([(E0,E1,E2)|T],true,Parent,VariableName,F,Fi) :- |
115 | | % interpret E0 as label for string; note: (E0,E1,E2) matches ((A,B),(C,D)) |
116 | | generate_state_for_dot, |
117 | | simple_value(E0), |
118 | | !, |
119 | | translate_inner_node(E1,C1,E1_NewTransitions), |
120 | | translate_inner_node(E2,C2,E2_NewTransitions), |
121 | | translate_bvalue_for_dot(E0,E0String), |
122 | | Label =.. [VariableName,E0String], |
123 | | append([E2_NewTransitions,[(C1,Label,C2)|E1_NewTransitions],F],F6), |
124 | | grelation(T,true,Parent,VariableName,F6,Fi). |
125 | | grelation([(E1,E2)|T],MatchTriples,Parent,VariableName,F,Fi) :- |
126 | | translate_inner_node(E1,C1,E1_NewTransitions), |
127 | | translate_inner_node(E2,C2,E2_NewTransitions), |
128 | | append([E2_NewTransitions,[(C1,VariableName,C2)|E1_NewTransitions],F],F6), |
129 | | grelation(T,MatchTriples,Parent,VariableName,F6,Fi). |
130 | | |
131 | | |
132 | | |
133 | | :- use_module(probsrc(preferences),[get_preference/2]). |
134 | | |
135 | | translate_inner_node(DataValue,NodeinGraph,NewTransitions) :- %% print(trans(DataValue)),nl, |
136 | | % Input: DataValue |
137 | | % Output: NodeinGraph representing DataValue + NewTransitions required to represent the structure |
138 | | (get_preference(dot_state_graph_decompose,false) -> % treat as an atom |
139 | | NewTransitions = [], NodeinGraph = DataValue |
140 | | ; expand_data_value(DataValue,S1), |
141 | | % check whether S1 is a atom/set |
142 | | ( emptyset(S1) -> NodeinGraph = [], %'$Empty_Set', |
143 | | NewTransitions=[] |
144 | ? | ; cn_value(S1,NodeinGraph) -> NewTransitions=[] |
145 | ? | ; simple_pair_value(S1),generate_state_for_dot -> NodeinGraph=S1, NewTransitions=[] |
146 | | ; list_set(S1) -> |
147 | | new_sg_node(S1,NodeinGraph), |
148 | | 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) |
149 | | ; S1=(P1,P2) |
150 | | -> % a complex pair |
151 | | translate_inner_node(P1,Node1,NewTrans1), |
152 | | translate_inner_node(P2,Node2,NewTrans2), |
153 | | new_sg_node(S1,NodeinGraph), |
154 | | append([(NodeinGraph,'$from',Node1), |
155 | | (NodeinGraph,'$to_el',Node2)|NewTrans1],NewTrans2,NewTransitions) |
156 | | ; % an atom |
157 | | NewTransitions = [], |
158 | | NodeinGraph = S1 |
159 | | ) |
160 | | ). |
161 | | |
162 | | % simple values which can easily be rendered like a record |
163 | | simple_pair_value((A,B)) :- !,simple_pair_value(A), simple_pair_value(B). |
164 | ? | simple_pair_value(X) :- simple_value(X). |
165 | | |
166 | | relation([(_,_)|_]). |
167 | | relation([(X,_,_)|_]) :- generate_state_for_dot, simple_value(X). % TO DO: check if it is a function ?; maybe also support other nested ternary relations |
168 | | emptyset([]). |
169 | | list_set([]). |
170 | | list_set([_|_]). |
171 | | % what about AVL : supposed expanded before |
172 | | |
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 | | assertz(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 | | |
202 | | /**********************************************/ |
203 | | |
204 | | /****** CANONICAL LABELLING USING LEXICOGRAPHIC AND AUTOMORHISM PRUNING: ******* |
205 | | ****** Makes use of Schreier-Sims data structure defined in Kreher's ******* |
206 | | ****** C.A.G.E.S book, and uses the techniques for pruning described in ******* |
207 | | ****** the chapter 7. *******/ |
208 | | |
209 | | |
210 | | |
211 | | /******************************************************************* |
212 | | */ |
213 | | % schreiersims.pl implementation of the schreier sims representation of an |
214 | | % automorphism group taken from Kreher's Combinatorial Algorithms book. Provides |
215 | | % method for membership test of a permutation in the group that should run in O(n^2) |
216 | | % time. Plans are not to spend time on implementing a method for listing all permutations |
217 | | % represented in the group -- since this is not required at the time of writing. |
218 | | |
219 | | % THIS IS NOT CURRENTLY USED, BUT WAS ONCE USED TO MORE CLOSELY FOLLOW NAUTY. |
220 | | % HOWEVER, USING SCHREIERSIMS STRUCTURES IMPLEMENTATION IS VERY LIST INTENSIVE |
221 | | % RESULTING IN A POOR PERFORMANCE -- HENCE NOT USED NOW. FUTURE WORK MAY WANT |
222 | | % TO LOOK AT ITS USE BELOW.. |
223 | | |
224 | | |
225 | | /*** END OF CANONICAL LABELLING USING LEXICOGRAPHIC AND AUTOMORPHISM PRUNING ***/ |