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