1		% (c) 2006-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
5
6		:- module(symmetry_marker,[precompile_marker_typing_info/0,
7		compute_marker_for_state/2,
8		type_allows_for_precise_marker/1,
9		hash_model_checking_imprecise/2,
10		non_symmetric_type/1]).
11		/* File: symmetry_marker.pl */
12		/* Created: 28/9/06 */
13
14
15		:- use_module(module_information).
16		:- module_info(group,symmetry).
17		:- module_info(description,'This module computes symmetry hash markers for B states (used for hash symmetry).').
18
19		:- use_module(debug).
20
21		:- use_module(library(lists)).
22
23		/* marker(Object, Type, ValueAsTerm) */
24
25
26		:- use_module(b_global_sets,[is_unused_b_global_constant/3,
27		b_global_deferred_set_with_card_gt1/1, b_global_set_with_potential_symmetry/1]).
28
29		:- use_module(error_manager).
30
31		type_allows_for_precise_marker(integer).
32		type_allows_for_precise_marker(string).
33		type_allows_for_precise_marker(boolean).
34		type_allows_for_precise_marker(set(global(_))) :- !. % ok, whether global set deferred or not
35		type_allows_for_precise_marker(set(couple(X,Y))) :- !,
36		((Y=global(_),non_symmetric_type(X)) % type_allows_for_precise_marker(Y) not ok; unless we are guaranteed to have a function
37		-> true
38		; (X=global(_),non_symmetric_type(Y)) % see comment above
39		-> true
40		; (non_symmetric_type(X), non_symmetric_type(Y)) -> true
41		; print_fail(set(couple(X,Y)))).
42		type_allows_for_precise_marker(set(X)) :-
43		(non_symmetric_type(X) -> true
44		; print_fail(set(X))).
45		type_allows_for_precise_marker(seq(X)) :- !, type_allows_for_precise_marker(set(couple(integer,X))).
46		type_allows_for_precise_marker(global(_)).
47		type_allows_for_precise_marker(couple(X,Y)) :- !,type_allows_for_precise_marker(X),
48		type_allows_for_precise_marker(Y).
49		type_allows_for_precise_marker(record(F)) :- !, fields_allows_for_precise_marker(F).
50
51		fields_allows_for_precise_marker([]).
52		fields_allows_for_precise_marker([field(_Name,Type)|T]) :-
53		type_allows_for_precise_marker(Type),
54		fields_allows_for_precise_marker(T).
55
56		:- use_module(preferences,[get_preference/2]).
57		hash_model_checking_imprecise(ID,BasicType) :- %print(check),nl,
58		get_preference(symmetry_mode,hash),
59		(b_get_machine_constants(TL) ; b_get_machine_variables(TL)),
60		member(b(identifier(ID),BasicType,_),TL),
61		\+ type_allows_for_precise_marker(BasicType).
62
63
64		%:- use_module(translate,[pretty_type/2]).
65		print_fail(_T) :-
66		%print('*** type may lead to imprecise hash marker:'),
67		%translate:pretty_type(T,S),print(S),nl,
68		fail.
69		% a type which does not contain any deferred set elements
70		non_symmetric_type(integer) :- !.
71		non_symmetric_type(boolean) :- !.
72		non_symmetric_type(string) :- !.
73		non_symmetric_type(set(X)) :- !, non_symmetric_type(X).
74		non_symmetric_type(couple(X,Y)) :- !,non_symmetric_type(X), non_symmetric_type(Y).
75	?	non_symmetric_type(global(X)) :- !, \+ b_global_set_with_potential_symmetry(X).
76		non_symmetric_type(seq(X)) :- !, non_symmetric_type(X).
77		non_symmetric_type(record(F)) :- !, non_symmetric_fields(F).
78		non_symmetric_type(freetype(_)) :- !.
79		non_symmetric_type(X) :- add_error_fail(non_symmetric_type,'Unknown type: ',X).
80
81		non_symmetric_fields([]).
82		non_symmetric_fields([field(_Name,Type)|T]) :- non_symmetric_type(Type),
83		non_symmetric_fields(T).
84
85		/* first a predicate to count the occurrences of anonymous set elements */
86
87		/* possible improvement: count nr of occurences for each variable */
88
89		:- use_module(bmachine,[b_get_machine_constants/1, b_get_machine_variables/1]).
90		:- volatile non_symmetric_var/2.
91		:- dynamic non_symmetric_var/2.
92		precompile_marker_typing_info :-
93		retractall(non_symmetric_var(_,_)),
94		bmachine:b_get_machine_variables(TypedVarList),
95		bmachine:b_get_machine_constants(TypedCstList),
96		append(TypedCstList,TypedVarList,List),
97		analyse_typed_varlist(List).
98
99		analyse_typed_varlist([]).
100		analyse_typed_varlist([b(identifier(ID),Type,_)|T]) :-
101		(non_symmetric_type(Type)
102		-> assert(non_symmetric_var(ID,Type))
103		%% ,print(non_sym(ID,Type)),nl
104		; true),
105		analyse_typed_varlist(T).
106
107
108		%:- dynamic count/4.
109
110
111		count_state(State) :- empty_avl(E),
112		%nl,translate:print_bstate(State),nl,
113		count_env(State,E,Out),
114		%portray_avl(Out),nl,
115		compute_deferred_set_el_markers(Out).
116
117		count_env([],I,O) :- !, O=I.
118		count_env([bind(Var,Val)|T],In,Out) :- !,
119		(non_symmetric_var(Var,_) -> In=I1
120		; %print(counting(Var)),nl,
121		count_obj(Val,Var,In,I1)),
122		count_env(T,I1,Out).
123		count_env(E,I,O) :- add_error(symmetry_marker,'Illegal env: ',E), O=I.
124
125		:- use_module(library(avl)).
126		/* IDEA: instead of just storing variable Var, store entire path to
127		occurrence of fd(Nr,T) */
128		count_obj(fd(Nr,T),PathToObject,In,Out) :- !, %print(fd(Nr,T)),
129		((b_global_deferred_set_with_card_gt1(T) ;
130		is_unused_b_global_constant(T,Nr,_) /* TO DO: only makes sense if more than one unused global constant */
131		)
132		-> %add_count(PathToObject,Nr,T,In,Out)
133		add_avl_count(In,usage_count(Nr,T,PathToObject),Out)
134		; Out=In
135		).
136		count_obj((X,Y),PathToObject,In,Out) :- !, count_pair(X,Y,PathToObject,In,Out).
137		count_obj([X|Y],PathToObject,In,Out) :- !,
138		(could_contain_deferred_set_elements(X)
139		-> count_obj_list([X|Y],PathToObject,In,Out) /* only count set if there are deferred set elements inside */
140		; Out=In
141		).
142		count_obj(avl_set(A),PathToObject,In,Out) :- !,
143		(avl_could_contain_deferred_set_element(A)
144		-> count_avl(A,el(PathToObject),In,Out)
145		; Out=In
146		).
147		%count_obj([],_,O,O).
148		count_obj(_,_,O,O).
149		% no need to have base case for empty avl; as empty set represented by []
150
151
152		count_avl(empty,_PathToObject) --> [].
153		count_avl(node(Key,_True,_,L,R),PathToObject) -->
154		count_avl(L,PathToObject), count_obj(Key,PathToObject),
155		count_avl(R,PathToObject).
156
157		count_pair(X,Y,PathToObject,In,Out) :- not_symmetric(Y),!,
158		count_obj(X,mapped_to(PathToObject,Y),In,Out).
159		count_pair(X,Y,PathToObject,In,Out) :- not_symmetric(X),!,
160		count_obj(Y,mapped_from(X,PathToObject),In,Out).
161		count_pair(X,X,PathToObject,In,Out) :- !, /* is this correct ??
162		should we only do it for simple X, what about sets: should
163		work if normalised ?? */
164		count_obj(X,leftright(PathToObject),In,Out).
165		count_pair(X,Y,PathToObject,In,Out) :- !,
166		count_obj(X,left(PathToObject),In,I1),
167		count_obj(Y,right(PathToObject),I1,Out).
168
169
170		could_contain_deferred_set_elements([]).
171		could_contain_deferred_set_elements([H|_]) :- could_contain_deferred_set_elements(H).
172		could_contain_deferred_set_elements(fd(_Nr,_T)).
173		%b_global_deferred_set_with_card_gt1(T) ; b_global_sets:is_unused_b_global_constant(T,Nr,_).
174		could_contain_deferred_set_elements((A,B)) :-
175		(could_contain_deferred_set_elements(A) -> true ; could_contain_deferred_set_elements(B)).
176		could_contain_deferred_set_elements(avl_set(A)) :- avl_could_contain_deferred_set_element(A).
177
178		avl_could_contain_deferred_set_element(node(X,_,_,_L,_R)) :- /* first underscore should be true */
179		could_contain_deferred_set_elements(X).
180		%an_avl_element(node(X,_,_,_L,_R),X). /* first underscore should be true */
181
182		count_obj_list([],_,O,O).
183		count_obj_list([X|Y],PathToObject,In,Out) :-
184		count_obj(X,el(PathToObject),In,I1),
185		count_obj(Y,PathToObject,I1,Out).
186
187		/* not_symmetric: check if object has symmetric permutations */
188		not_symmetric([]).
189		not_symmetric((X,Y)) :- not_symmetric(X), not_symmetric(Y).
190		not_symmetric(pred_false /* bool_false */).
191		not_symmetric(pred_true /* bool_true */).
192		not_symmetric(string(_)).
193		not_symmetric(fd(Nr,T)) :-
194		\+ b_global_deferred_set_with_card_gt1(T),
195		\+ is_unused_b_global_constant(T,Nr,_). /* TO DO: only makes sense if more than one unused global constant */
196		not_symmetric(int(_)).
197		/* add same for sets ?? */
198
199
200		% add_avl_count(usage_count(Nr,T,PathToObject),In,Out)
201		add_avl_count(AVL,Key,NewAVL) :- %print(add_count(Key)),nl,
202		(avl_fetch(Key,AVL,OldCount)
203		-> NewCount is OldCount+1,
204		avl_change(Key,AVL,_,NewAVL,NewCount)
205		; avl_store(Key,AVL,1,NewAVL)
206		). %, print(ok(NewCount)),nl.
207
208
209		/*
210		add_count(Var,Nr,T) :-
211		(retract(count(Nr,T,Var,C1))
212		-> (C is C1+1, assert(count(Nr,T,Var,C)))
213		; assert(count(Nr,T,Var,1))
214		). */
215
216		:- volatile deferred_set_el_marker/3.
217		:- dynamic deferred_set_el_marker/3.
218
219		/* compute individual markers for deferred set elements by hashing
220		classical path information using sha */
221
222		/*
223		compute_deferred_set_el_markers(CountAVL) :-
224		retractall(deferred_set_el_marker(_,_,_)),
225		avl_generate_el_markers(CountAVL,'$DUMMY',-1,[],OutType,OutNr,OutCount),
226		%% print(last_marker(OutType,OutNr,OutCount)),nl, %%
227		assert_def_marker(OutType,OutNr,OutCount).
228
229		avl_generate_el_markers(empty,CurType,CurElNr,CurCount,CurType,CurElNr,CurCount).
230		avl_generate_el_markers(node(usage_count(Nr,T,Path),Count,_,L,R),CurType,CurElNr,CurCount,
231		OutT,OutNr,OutCount) :-
232		avl_generate_el_markers(L,CurType,CurElNr,CurCount,T1,N1,C1),
233		((N1=Nr,T1=T) % we are still treating the same deferred set element fd(T,Nr)
234		-> C2=[count(Path,Count)|C1] % add cur path to list of paths for fd(T,Nr)
235		; assert_def_marker(T1,N1,C1), % assert cur paths for fd(T1,N1)
236		% We could use instead: avl_store(fd(T1,N1),AVL,el(T1,C1),NewAVL)
237		%print(marker(T1,N1,C1)),nl, %%
238		C2 = [count(Path,Count)] % start fresh; collecting paths for fd(T,Nr)
239		), avl_generate_el_markers(R,T,Nr,C2,OutT,OutNr,OutCount).
240
241		:- use_module(extension('probhash/probhash')).
242		assert_def_marker(T1,N1,C1) :- raw_sha_hash(el(T1,C1),MHash),
243		assert(deferred_set_el_marker(T1,N1,MHash)).
244		*/
245
246		/*
247		an attempt at not storing paths but just sort the fd-elements according to path
248		information and assign them a number: without adding id_couple below in marker/3 we get collisions, e.g, for
249		./probcli examples/B/SymmetryReduction/PhilRing.mch -mc 1000 -p DEFAULT_SETSIZE 3 -p SYMMETRY_MODE hash -cc 13 47
250		*/
251
252		compute_deferred_set_el_markers(CountAVL) :-
253		avl_to_list(CountAVL,AList),
254		%print(AList),nl,
255		merge_paths(AList,BList),
256		sort(BList,SBList),
257		%print(merged(SBList)),nl,
258		retractall(deferred_set_el_marker(_,_,_)),
259		assert_markers(SBList,0),!.
260
261		% merge all the information for same deferred set elements (Nr,Type)
262		merge_paths([],[]).
263		merge_paths([usage_count(Nr,Type,Path)-Count|Tail],Res) :-
264		merge_paths(Tail,Nr,Type,[count(Path,Count)],Res).
265
266		merge_paths([],Nr,Type,MarkerPaths,[marker(Type,MarkerPaths,Nr)]). % :- print(marker(Type,MarkerPaths,Nr)),nl.
267		merge_paths([usage_count(Nr,Type,Path)-Count|Tail],Nr,Type,M,Res) :- !,
268		merge_paths(Tail,Nr,Type,[count(Path,Count)|M],Res).
269		merge_paths([usage_count(Nr,Type,Path)-Count|Tail],Nr2,T2,M,[marker(T2,M,Nr2)|Res]) :-
270		% print(marker(T2,Nr2,M)),nl,
271		merge_paths(Tail,Nr,Type,[count(Path,Count)],Res).
272
273		:- use_module(extension('probhash/probhash')).
274		assert_markers([],_).
275		assert_markers([marker(Type,Paths,Nr)|T],ID) :-
276		get_same_markers(T,Type,Paths,Same,TT,NrSame), % get all other elements with same Paths information
277		ID1 is ID+1,
278		(NrSame=0 -> assert(deferred_set_el_marker(Type,Nr,fdunique(ID1,Type)))
279		; assert_same_markers([Nr|Same],Type,ID1,NrSame)),
280		assert_markers(TT,ID1).
281
282		get_same_markers([marker(Type,Paths,Nr)|T],Type,Paths,[Nr|SM],TT,ResNr) :- !,
283		get_same_markers(T,Type,Paths,SM,TT,SNr), ResNr is SNr+1.
284		get_same_markers(T,_,_,[],T,0).
285
286
287		assert_same_markers([],_,_,_).
288		assert_same_markers([Nr|T],Type,ID,NrSame) :-
289		assert(deferred_set_el_marker(Type,Nr,fdsame(ID,Type,NrSame))),
290		assert_same_markers(T,Type,ID,NrSame).
291
292
293		/* */
294
295
296		% -------------------------------------------------------
297
298
299		/* marker(+ProBOBject, -TypeOfObject, -HashTerm) */
300
301
302		%:- use_module(b_global_sets,[all_elements_of_type/2]).
303		:- use_module(custom_explicit_sets).
304
305		/* missing: closure, records,... */
306		marker(closure(P,T,B),set(any),closure(P,T,B)).
307		marker(global_set(GS),set(Type),Local) :-
308		marker_explicit_set(global_set(GS),set(Type),Local).
309		marker(avl_set(S),set(Type),SLocal) :- % marker_explicit_set(avl_set(S),set(Type),Val,Local).
310		(avl_marker(S, Type,Local) -> true ; print(failed_avl_marker(S)),nl,fail),
311		sort_markers(Local,SLocal).
312		marker(closure_x(P,T,B,E),set(Type),Local) :-
313		marker_explicit_set(closure_x(P,T,B,E),set(Type),Local).
314		marker(int(N), integer, N). % int(N)
315		marker(string(S), string, S). % string(S)).
316		marker(fd(Nr,T), global(T), Term) :-
317		(deferred_set_el_marker(T,Nr,Term)
318		-> true
319		; (b_global_deferred_set_with_card_gt1(T)
320		-> print(not_counted(Nr,T)),nl ; true),
321		Term=fd(Nr,T) /*should not happen for deferred sets */
322		).
323		marker(pred_false /* bool_false */, boolean, pred_false).
324		marker(pred_true /* bool_true */, boolean, pred_true).
325		marker((X,Y), couple(T1,T2), Mark) :-
326		(X==Y -> Mark = id_couple(L1), marker(X,T1,L1) % added 7/9/2011 by leuschel
327		; Mark = couple(L1,L2), marker(X,T1,L1),marker(Y,T2,L2)).
328		marker([], set(_), []).
329		marker([H|T], set(Type), Local) :-
330		l_marker([H|T],Type,LL),
331		sort_markers(LL,Local).
332
333
334		marker_explicit_set(ES,set(Type),Local) :-
335		expand_custom_set_to_list_now(ES,Res),
336		l_marker(Res,Type,LL),
337		sort_markers(LL,Local).
338
339
340		l_marker([], _Type, []).
341		l_marker([H|T], Type, [LH|LT]) :-
342		marker(H,Type,LH),
343		l_marker(T,Type,LT).
344
345		avl_marker(Avl, Type,Local) :- avl_domain(Avl,List),
346		l_marker(List,Type,Local).
347
348
349
350		/* example queries:
351		use_module(symmetry_marker),
352		symmetry_marker:compute_marker_for_state([bind(tr,[(fd(1,'Session'),fd(1,'Session')),(fd(1,'Session'),fd(2,'Session'))]),
353		bind(inv,[fd(1,'Session')]),bind(i,fd(1,'Session')),
354		bind(reach,[fd(1,'Session'),fd(2,'Session')]),bind(rac,[fd(1,'Session')])],M).
355
356		symmetry_marker:nodes_in_graph([(fd(1,'Session'),fd(1,'Session')),(fd(1,'Session'),fd(2,'Session'))],N).
357
358		use_module(symmetry_marker),symmetry_marker:cm.
359
360		use_module(symmetry_marker),
361		symmetry_marker:count_state([bind(tr,[(fd(1,'Session'),fd(1,'Session')),(fd(1,'Session'),fd(2,'Session'))]),
362		bind(inv,[fd(1,'Session')]),bind(i,fd(1,'Session')),
363		bind(reach,[fd(1,'Session'),fd(2,'Session')]),bind(rac,[fd(1,'Session')])]),
364		symmetry_marker:count(X,Y,Z).
365		*/
366
367
368		:- use_module(library(samsort)).
369
370		sort_markers(X,SX) :- samsort(X,SX). % sort without duplicate removal
371
372
373
374		:- use_module(specfile,[expand_const_and_vars_to_full_store/2]).
375
376		:- use_module(self_check).
377		:- assert_must_succeed((symmetry_marker:compute_marker_for_state([bind(x,fd(1,'Name')),bind(y,fd(2,'Name'))],R1),
378		symmetry_marker:compute_marker_for_state([bind(x,fd(2,'Name')),bind(y,fd(1,'Name'))],R2),R1==R2)).
379
380		compute_marker_for_state(State,Marker) :-
381		(State = concrete_constants(BState)
382		-> Marker = concrete_constants(BMarker)
383		; (State = csp_and_b(CSPState,BState)
384		-> Marker = csp_and_b(CSPState,BMarker)
385		; (State=[] ; State = [_|_] ; State = const_and_vars(_,_) ),
386		State=BState, Marker=BMarker
387		)
388		),
389		expand_const_and_vars_to_full_store(BState,FullBState),
390		count_state(FullBState), /* first count the number of occurrences
391		of every symmetric element in the State; this number will
392		be used as the marker for that element */
393		marker_for_state(FullBState,BMarker).
394		% ,raw_sha_hash(BMarker0,BMarker). % , print(marker_for_state(FullBState,BMarker)),nl,nl.
395
396		/* compute a marker for a given state */
397		marker_for_state([],[]).
398		marker_for_state([bind(Var,Val)|T],[M|TM]) :-
399		(non_symmetric_var(Var,_) -> TermMarker=Val
400		; marker(Val, _Type,TermMarker)),
401		M=mark(Var,TermMarker),
402		marker_for_state(T,TM).
403
404
405		% TESTING CODE
406
407		/*
408		:- dynamic marker/2.
409		% symmetry_marker:cm.
410		% symmetry_marker:marker(10,M1), symmetry_marker:marker(18,M2), M1=M2.
411
412		:- public cm/0.
413		cm :-
414		print('Computing markers for state space'),nl,
415		retractall(marker(_,_)),
416		cms(ID, M),
417		assert(marker(ID,M)),
418		fail.
419		cm :-
420		marker(ID,Marker),
421		marker(ID2,Marker), ID2 > ID,
422		print(same_marker(ID,ID2)),nl,
423		fail.
424		cm :- print('Finished'),nl.
425
426		:- use_module(state_space,[visited_expression/2]).
427		cms(ID, M) :-
428		state_space:visited_expression(ID,State),
429		compute_marker_for_state(State,M),
430		print(marker(ID,State,M)),nl.
431
432
433		:- public test_sym/0.
434		test_sym :- state_space:visited_expression(ID,State),
435		print(ID), print(' : '),
436		sym_mark_for_state(State).
437
438		sym_mark_for_state(State) :-print(State),nl,
439		member(bind(Var,Val),State),
440		print(Var), print(' = '),
441		marker(Val, T,L),
442		print(marker(Val,T,L)),
443		print(' '),
444		nl,
445		fail.
446		sym_mark_for_state(_) :- nl.
447		*/