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
6 :- module(state_permuter,[permute_state/2]).
7 /* File: state_permuter.pl */
8 /* Created: 8/6/06 by Michael Leuschel */
9
10
11 :- use_module(probsrc(module_information)).
12 :- module_info(group,symmetry).
13 :- module_info(description,'Computes all permutations of a B state; used by flooding symmetry.').
14
15
16 :- use_module(probsrc(error_manager)).
17
18 :- use_module(probsrc(b_global_sets),[b_global_set/1, is_unused_b_global_constant/2,
19 b_global_deferred_set/1,b_global_deferred_set_with_card_gt1/1,
20 all_elements_of_type/2,b_exists_global_set_with_potential_symmetry/0]).
21
22 :- use_module(library(lists)).
23
24 :- use_module(probsrc(store),[normalise_store/2]).
25
26 :- use_module(probsrc(self_check)).
27
28 :- assert_must_succeed(( I=[bind(x,int(1))], state_permuter:permute_state(I,R),
29 R==I )).
30 :- assert_must_succeed(( I=[bind(x,(pred_true,string(a)))],state_permuter:permute_state(I,R),
31 R==I )).
32 permute_state(X,NPX) :-
33 ( b_exists_global_set_with_potential_symmetry
34 -> permute_state2(X,NPX) ; NPX=X).
35
36 /* Note : it can happen that the same state is generated twice:
37
38 X={Name1,Name2} +--> will permute into itself twice
39
40 */
41
42 :- use_module(probsrc(specfile),[expand_const_and_vars_to_full_store/2]).
43
44 permute_state2(State,PermutedState) :-
45 (State = concrete_constants(BState)
46 -> PermutedState = concrete_constants(NPX)
47 ; (State = csp_and_b(CSPState,BState)
48 -> PermutedState = csp_and_b(CSPState,NPX)
49 ; (State=BState, PermutedState=NPX)
50 )
51 ),
52 expand_const_and_vars_to_full_store(BState,FullBState), /* TO DO: better treatment of ConstID in const_and_vars */
53 permute_state3(FullBState,[],PX),normalise_store(PX,NPX).
54
55
56 permute_state3([],Perm,[]) :- % print(labeling(Perm)),nl,
57 label_permutation(Perm).
58 permute_state3([bind(X,Val)|T],InPerm,[bind(X,PermVal)|PT]) :-
59 (permute_value(Val,InPerm,OutPerm,PermVal)
60 -> true
61 ; add_error(state_permuter,'permute_value failed: ',permute_value(Val,InPerm,OutPerm,PermVal)),
62 PermVal = Val
63 ),
64 %print(perm(Val,PermVal,OutPerm)),nl,
65 permute_state3(T,OutPerm,PT).
66
67
68 :- use_module(probsrc(custom_explicit_sets),[expand_custom_set_to_list/2]).
69
70 permute_value(pred_false /* bool_false */,P,P,pred_false /* bool_false */).
71 permute_value(pred_true /* bool_true */,P,P,pred_true /* bool_true */).
72 permute_value(fd(X,Set),InPerm,OutPerm,PX) :-
73 ((b_global_deferred_set_with_card_gt1(Set)
74 ; is_unused_b_global_constant(Set,X) /* TO DO: only makes sense if more than one unused global constant */
75 )
76 -> (member(perm(X,PX,Set),InPerm)
77 -> OutPerm = InPerm
78 ; OutPerm = [perm(X,PX,Set)|InPerm]
79 )
80 ; OutPerm=InPerm, PX=fd(X,Set)
81 ).
82 permute_value(global_set(X),P,P,global_set(X)).
83 permute_value(freetype(X),P,P,freetype(X)).
84 permute_value(avl_set(X),In,Out,PermutedList) :-
85 expand_custom_set_to_list(avl_set(X),Value),
86 % print(perm(X,Value)),nl,
87 permute_value(Value,In,Out,PermutedList).
88 permute_value([],P,P,[]).
89 permute_value(int(X),P,P,int(X)).
90 permute_value(term(X),P,P,term(X)).
91 permute_value(string(X),P,P,string(X)).
92 permute_value(rec(X),In,Out,rec(PX)) :-
93 permute_fields(X,In,Out,PX).
94 permute_value(freeval(I,C,X),In,Out,freeval(I,C,PX)) :-
95 permute_value(X,In,Out,PX).
96 permute_value([H|T],In,Out,[PH|PT]) :-
97 permute_value(H,In,In2,PH),
98 permute_value(T,In2,Out,PT).
99 % (PT = [PPH|_] -> check_normalised(PH,PPH) /* ensure that we generate normalised sets only;
100 % not all elements of set are either permuted or none;
101 % only works for simple sets !!*/
102 % ; true).
103 permute_value((H,T),In,Out,(PH,PT)) :-
104 permute_value(H,In,In2,PH),
105 permute_value(T,In2,Out,PT).
106 permute_value(closure(X,Y,Z),P,P,closure(X,Y,Z)).
107 permute_value(closure_x(X,Y,Z,E),P,P,closure_x(X,Y,Z,E)).
108 permute_value(abort(Err),P,P,abort(Err)) :- print(deprecated_abort_in_permute_value(Err)),nl.
109 /* to do: permute values inside closure; or disallow permutation generation for
110 states containing closures !!! */
111
112 permute_fields([],P,P,[]).
113 permute_fields([field(Name,Val)|T],In,Out,[field(Name,PVal)|PT]) :-
114 permute_value(Val,In,In2,PVal),
115 permute_fields(T,In2,Out,PT).
116
117
118 label_permutation(Perm) :-
119 findall(vals(Set,Vals), (b_global_set(Set),set_of_values(Set,Vals)), AV),
120 %print(label_perm(Perm,AV)),nl,
121 label_permutation(Perm,AV).
122
123
124 ?set_of_values(Set,Vals) :- b_global_deferred_set(Set),all_elements_of_type(Set,Vals).
125 set_of_values(Set,Vals) :-
126 findall(fd(X,Set),is_unused_b_global_constant(Set,X), Vals),
127 Vals \= [].
128
129 label_permutation([],_).
130 label_permutation([perm(X,PX,Set)|T], AV) :- % print(p(X,Set)),nl,
131 extract_value(AV,X,Set,PX,AV2), %print(val(X,PX,AV2)),nl,
132 label_permutation(T,AV2).
133
134 extract_value([vals(Set,Vals)|T],_X,Set,PX,AV2) :- !,
135 remove(Vals,PX,Vals2),
136 AV2 = [vals(Set,Vals2)|T].
137 extract_value([H|T],X,Set,PX,[H|T2]) :-
138 extract_value(T,X,Set,PX,T2).
139
140
141 remove([X|T],X,T).
142 remove([Y|T],X,[Y|DT]) :- remove(T,X,DT).
143
144
145 %check_normalised(PH,PPH) :- when((ground(PH),ground(PPH)), PH @< PPH).
146
147 /*
148
149 use_module(symsrc(state_permuter)), permute_state([ bind(x,[ fd(1,'Name'), fd(2,'Name')]) ], R).
150 R = [bind(x,[fd(2,'Name'),fd(1,'Name')])] ? ;
151 R = [bind(x,[fd(1,'Name'),fd(2,'Name')])] ? ;
152 no
153
154
155 Mottisfont, Dual 2.7 GHz figures:
156
157 scheduler, 6 PIDs
158 w/o perm reduction: 15.51 secs, 10498 states
159 with perm reduction: 2.03 secs, 10498 states
160
161 Volvo Cruise_finite1.mch (no deferred sets)
162 w/o: 54 secs, 1361 states
163 with: same
164
165 RussianPostalPuzzle, 4 keys
166 w/o: 15.73 secs, 2325 states
167 with: 3.06 secs, 5064 states (4816 permute states)
168
169 USB.mch, 2 TRANSFERS
170 w/o: 8.76 secs, 415 nodes
171 with: 5.53 secs, 415 nodes, 201 permute states
172 */