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