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 */