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