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