1 | % (c) 2014-2019 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 | :- module(predicate_handling,[prime_predicate/2, | |
6 | create_state_predicate/2, | |
7 | create_succ_state_predicate/2, | |
8 | create_constants_state_predicate/2, | |
9 | get_initial_state_predicate/1, | |
10 | get_transition_predicate/1, | |
11 | get_single_transition_predicate/2, | |
12 | create_negation_and_cleanup/2, | |
13 | create_primary_inputs_predicate/2, | |
14 | deprime_state/2, | |
15 | prime_n_times/3, | |
16 | unprimed/1]). | |
17 | ||
18 | :- use_module(probsrc(module_information)). | |
19 | :- module_info(group,symbolic_model_checker). | |
20 | :- module_info(description,'Handling and creation of predicates used in the symbolic model checker.'). | |
21 | ||
22 | :- use_module(library(lists)). | |
23 | ||
24 | :- use_module(probsrc(b_global_sets), [b_global_set/1, | |
25 | is_b_global_constant/3]). | |
26 | :- use_module(probsrc(bmachine),[b_get_machine_operation/4, | |
27 | b_get_machine_constants/1, | |
28 | b_get_machine_variables/1, | |
29 | b_get_initialisation_from_machine/2, | |
30 | b_get_properties_from_machine/1, | |
31 | get_proven_invariant/2]). | |
32 | :- use_module(probsrc(before_after_predicates),[before_after_predicate_with_equalities/3, | |
33 | before_after_predicate_list_disjunct_with_equalities/3, | |
34 | before_after_predicate_for_operation/2]). | |
35 | :- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2, | |
36 | disjunct_predicates/2, | |
37 | disjunction_to_list/2, | |
38 | transform_bexpr/3, | |
39 | syntaxtransformation/5, | |
40 | create_texpr/4, | |
41 | safe_create_texpr/3, | |
42 | create_negation/2, | |
43 | get_texpr_expr/2, | |
44 | get_texpr_type/2, | |
45 | unique_typed_id/3]). | |
46 | ||
47 | :- use_module(probsrc(preferences), [get_preference/2]). | |
48 | ||
49 | get_initial_state_predicate(Init) :- | |
50 | % the initial state contains both the constants defined by the properties | |
51 | % and the variables set by the initialisation | |
52 | b_get_properties_from_machine(Properties), | |
53 | b_get_initialisation_from_machine(Initialisation,_), | |
54 | before_after_predicate_with_equalities(Initialisation,[],InitialisationPred), | |
55 | conjunct_predicates([Properties,InitialisationPred],PredWithPrimes), | |
56 | transform_bexpr(predicate_handling:remove_prime_from_expression,PredWithPrimes,Init). | |
57 | ||
58 | get_transition_predicate(TransitionPredicate) :- | |
59 | get_preference(use_po,false), !, | |
60 | findall(Body,b_get_machine_operation(_Name,_Results,_Parameters,Body),ListOfBodies), | |
61 | b_get_machine_variables(Variables), | |
62 | b_get_machine_constants(Constants), | |
63 | append(Variables,Constants,VarsAndConsts), | |
64 | before_after_predicate_list_disjunct_with_equalities(ListOfBodies,VarsAndConsts,TransitionPredicateNoInputs), | |
65 | add_primary_inputs(TransitionPredicateNoInputs,TransitionPredicate). | |
66 | get_transition_predicate(TransitionPredicate) :- | |
67 | get_preference(use_po,true), !, | |
68 | findall(op(OpName,Pred),(before_after_predicate_for_operation(OpName,Pred)),Ops), | |
69 | maplist(op_to_transition,Ops,SingleSteps), | |
70 | disjunct_predicates(SingleSteps,TransitionPredicateNoInputs), | |
71 | add_primary_inputs(TransitionPredicateNoInputs,TransitionPredicate). | |
72 | ||
73 | op_to_transition(op(OpName,BaPred),StepConstraint) :- | |
74 | (get_proven_invariant(OpName,ProvenInvariant) | |
75 | -> true ; ProvenInvariant = b(truth,pred,[])), | |
76 | prime_predicate(ProvenInvariant,PrimedProvenInvariant), | |
77 | conjunct_predicates([BaPred,PrimedProvenInvariant],StepConstraint). | |
78 | ||
79 | get_single_transition_predicate(OpName,TP) :- | |
80 | b_get_machine_operation(OpName,_Results,_Parameters,Body), | |
81 | b_get_machine_variables(Variables), | |
82 | b_get_machine_constants(Constants), | |
83 | append(Variables,Constants,VarsAndConsts), | |
84 | before_after_predicate_with_equalities(Body,VarsAndConsts,TransitionPredicateNoInputs), | |
85 | add_primary_inputs(TransitionPredicateNoInputs,TP). | |
86 | ||
87 | :- meta_predicate maplist(4,-,-,-,-). | |
88 | maplist(Pred, As, Bs, Cs, Ds) :- | |
89 | (foreach(A,As), | |
90 | foreach(B,Bs), | |
91 | foreach(C,Cs), | |
92 | foreach(D,Ds), | |
93 | param(Pred) | |
94 | do call(Pred, A, B, C, D) | |
95 | ). | |
96 | ||
97 | add_primary_inputs(TIn,TOut) :- | |
98 | % transition is a disjunction | |
99 | % as a first step add an integer variable to each disjunct | |
100 | % + a constraint stating that the sum is 1 | |
101 | disjunction_to_list(TIn,Disjuncts), | |
102 | maplist(add_input_to_op,Disjuncts,TopLevelIdentifiers,_InnerIdentifiers,DisjunctsOut), | |
103 | sum_is_one(TopLevelIdentifiers,Constraint), | |
104 | disjunct_predicates(DisjunctsOut,Disjunction), | |
105 | conjunct_predicates([Disjunction,Constraint],TOut). | |
106 | ||
107 | add_input_to_op(Op,IId,InnerIIds,OpOut) :- | |
108 | unique_typed_id("_ic3_pi",integer,IId), | |
109 | safe_create_texpr(integer(1),integer,Int1), | |
110 | safe_create_texpr(equal(IId,Int1),pred,EqualToOne), | |
111 | add_inner_inputs_to_op(Op,InnerIIds,Op2), | |
112 | conjunct_predicates([Op2,EqualToOne],OpOut). | |
113 | ||
114 | % add variables to substitutions like ANY, etc. | |
115 | % these variables should make the substitution deterministic | |
116 | % once they are fixed to a value | |
117 | add_inner_inputs_to_op(Subst,Ids,SubstOut) :- | |
118 | get_texpr_expr(Subst,Expr), | |
119 | add_inner_inputs_to_op_aux(Expr,Ids,ExprOut), !, | |
120 | safe_create_texpr(ExprOut,pred,SubstOut). | |
121 | %add_inner_inputs_to_op(Subst,[],Subst) :- | |
122 | % translate:translate_bexpression(Subst,PPSubst), | |
123 | % format('not implemented in add_inner_inputs_to_op: ~w~n',[PPSubst]). | |
124 | add_inner_inputs_to_op(Subst,[],Subst). | |
125 | % these might contain a non-deterministic choice somewhere | |
126 | add_inner_inputs_to_op_aux(conjunct(A,B),Ids,conjunct(NA,NB)) :- !, | |
127 | add_inner_inputs_to_op(A,AIds,NA), | |
128 | add_inner_inputs_to_op(B,BIds,NB), | |
129 | append(AIds,BIds,Ids). | |
130 | add_inner_inputs_to_op_aux(disjunct(A,B),Ids,disjunct(NA,NB)) :- !, | |
131 | add_inner_inputs_to_op(A,AIds,NA), | |
132 | add_inner_inputs_to_op(B,BIds,NB), | |
133 | append(AIds,BIds,Ids). | |
134 | % these have a non-deterministic choice. add a variable. | |
135 | add_inner_inputs_to_op_aux(member(A,B),[InputId],conjunct(b(member(A,B),pred,[]),Eq)) :- !, | |
136 | get_texpr_type(A,Type), | |
137 | unique_typed_id("_ic3_pi",Type,InputId), | |
138 | safe_create_texpr(equal(A,InputId),pred,Eq). | |
139 | % these should always be deterministic | |
140 | add_inner_inputs_to_op_aux(equal(A,B),[],equal(A,B)) :- !. | |
141 | ||
142 | sum_is_one(Identifiers,Constraint) :- | |
143 | build_sum(Identifiers,Sum), | |
144 | safe_create_texpr(integer(1),integer,Int1), | |
145 | safe_create_texpr(equal(Sum,Int1),pred,Constraint). | |
146 | ||
147 | build_sum([Id],Id). | |
148 | build_sum([Id|Ids],Sum) :- | |
149 | build_sum(Ids,SubSum), | |
150 | safe_create_texpr(add(Id,SubSum),integer,Sum). | |
151 | ||
152 | remove_prime_from_binding(binding(Id,Res,PP),binding(NId,Res,PP)) :- | |
153 | remove_prime(Id,NId). | |
154 | ||
155 | remove_prime_from_expression(b(identifier(Id),Type,Infos),b(identifier(NId),Type,Infos)) :- !, | |
156 | remove_prime(Id,NId). | |
157 | remove_prime_from_expression(Expr,Expr). | |
158 | ||
159 | remove_prime(Id,NoPrimeId) :- | |
160 | atom_codes(Id,Codes), | |
161 | append(NoPrimeIdCodes,[39],Codes), !, % last character is 39 = prime | |
162 | atom_codes(NoPrimeId,NoPrimeIdCodes). | |
163 | remove_prime(Id,Id). | |
164 | ||
165 | create_state_predicate(Solution,StatePredicate) :- | |
166 | include(unprimed,Solution,UPSolution), | |
167 | create_state_predicate_aux(UPSolution,StatePredicate). | |
168 | ||
169 | create_succ_state_predicate(Solution,SStatePredicate) :- | |
170 | deprime_state(Solution,DePrimedState), | |
171 | create_state_predicate_aux(DePrimedState,SStatePredicate). | |
172 | ||
173 | deprime_state(State,DeprimedState) :- | |
174 | include(primed,State,PSolution), | |
175 | maplist(remove_prime_from_binding,PSolution,DeprimedState). | |
176 | ||
177 | create_constants_state_predicate(Solution,ConstantsStatePred) :- | |
178 | include(unprimed,Solution,UPSolution), | |
179 | b_get_machine_constants(Csts), | |
180 | include(filter_vars_and_constants(Csts),UPSolution,UPSolutionOnlyConstants), | |
181 | UPSolutionOnlyConstants \= [], | |
182 | create_state_predicate_aux(UPSolutionOnlyConstants,ConstantsStatePred). | |
183 | ||
184 | create_primary_inputs_predicate(Solution,InputsPred) :- | |
185 | exclude(primed,Solution,NoPrimes), | |
186 | include(primary_input,NoPrimes,NoPrimesNoState), | |
187 | maplist(create_single_assignment_predicate(NoPrimesNoState),NoPrimesNoState,SolutionPreds), | |
188 | conjunct_predicates(SolutionPreds,InputsPred). | |
189 | ||
190 | create_state_predicate_aux(Solution,StatePredicate) :- | |
191 | b_get_machine_variables(Vars), b_get_machine_constants(Csts), | |
192 | append(Vars,Csts,VandC), | |
193 | include(filter_vars_and_constants(VandC),Solution,SolutionOnlyStateVars), | |
194 | maplist(create_single_assignment_predicate(VandC),SolutionOnlyStateVars,SolutionPreds), | |
195 | conjunct_predicates(SolutionPreds,StatePredicate). | |
196 | ||
197 | create_single_assignment_predicate(VandC,binding(Name,Value,_PP),Pred) :- | |
198 | % fetch the type for the particular variable / constant | |
199 | member(b(identifier(Name),Type,Infos),VandC), | |
200 | Pred = b(equal(b(identifier(Name),Type,Infos),b(value(Value),Type,[])),pred,[]). | |
201 | ||
202 | filter_vars_and_constants(VandC,binding(Id,_,_)) :- | |
203 | member(b(identifier(Id),_,_),VandC). | |
204 | ||
205 | unprimed(binding(Id,_,_)) :- atom_codes(Id,Codes), \+last(Codes,39). | |
206 | primed(binding(Id,_,_)) :- atom_codes(Id,Codes), last(Codes,39). | |
207 | ||
208 | primary_input(binding(Id,_,_)) :- atom_codes(Id,Codes), prefix("_ic3_pi", Codes). | |
209 | ||
210 | prime_predicate(A,B) :- | |
211 | create_texpr(OExpr,Type,Info,A), | |
212 | create_texpr(NExpr,Type,Info,B), | |
213 | prime_texpr(OExpr,Type,NExpr). | |
214 | ||
215 | % certain identifiers should not be primed | |
216 | % global sets | |
217 | do_not_prime_identifier(Id,set(global(Id))) :- | |
218 | b_global_set(Id). | |
219 | % members of global sets | |
220 | do_not_prime_identifier(MId,global(SId)) :- | |
221 | is_b_global_constant(SId,_,MId). | |
222 | ||
223 | prime_texpr(identifier(Old),Type,identifier(New)) :- | |
224 | % write(pt(Old,Type)), nl, | |
225 | do_not_prime_identifier(Old,Type), !, | |
226 | Old = New. | |
227 | prime_texpr(identifier(Old),_Type,identifier(New)) :- !, | |
228 | atom_concat(Old,'\'',New). | |
229 | prime_texpr(lazy_lookup_expr(Old),_,lazy_lookup_expr(New)) :- | |
230 | !, atom_concat(Old,'\'',New). | |
231 | prime_texpr(lazy_lookup_pred(Old),_,lazy_lookup_pred(New)) :- | |
232 | !, atom_concat(Old,'\'',New). | |
233 | prime_texpr(OExpr,_,NExpr) :- | |
234 | syntaxtransformation(OExpr,Subs,_TNames,NSubs,NExpr), | |
235 | prime_texpr_l(Subs,NSubs). | |
236 | prime_texpr_l([],[]). | |
237 | ||
238 | prime_texpr_l([Old|ORest],[New|NRest]) :- | |
239 | prime_predicate(Old,New), | |
240 | prime_texpr_l(ORest,NRest). | |
241 | ||
242 | % involves specialised cleanup rules for atb provers | |
243 | create_negation_and_cleanup(P,NP) :- | |
244 | get_texpr_expr(P,implication(A,B)), !, | |
245 | create_negation_and_cleanup(B,NegB), | |
246 | safe_create_texpr(conjunct(A,NegB),pred,NP). | |
247 | create_negation_and_cleanup(P,NP) :- | |
248 | create_negation(P,NP). | |
249 | ||
250 | prime_n_times(0,P,P) :- !. | |
251 | prime_n_times(N,P,Primed) :- | |
252 | prime_predicate(P,T), | |
253 | N2 is N - 1, | |
254 | prime_n_times(N2,T,Primed). |