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 | | % check an LTL formula on a concrete path |
7 | | |
8 | | :- module(ltl_verification, [evaluate_ltl_formula/6,evaluate_ltl_fairness/6]). |
9 | | |
10 | | /* SICSTUS libraries */ |
11 | | :- use_module(library(lists)). |
12 | | :- use_module(library(between),[numlist/3]). |
13 | | :- use_module(library(ordsets),[ord_intersection/3]). |
14 | | |
15 | | /* ProB standard modules */ |
16 | | :- use_module(probsrc(error_manager),[add_error/3]). |
17 | | |
18 | | :- use_module(probsrc(module_information),[module_info/2]). |
19 | | :- module_info(group,ltl). |
20 | | :- module_info(description,'This module provides predicates for checking an LTL formula on a concrete path.'). |
21 | | |
22 | | /* |
23 | | * evaluate_ltl_formula(Formula,StateTransitions,Type,CallbackAP,CallbackTP,Result): |
24 | | * Formula: AST of the LTL formula |
25 | | * StateTransitions: List of the form [strans(StateId,TransId)] which describes the |
26 | | * sequence of states and transitions between them. If there is no next state in |
27 | | * the sequence, TransId can be 'none' |
28 | | * Type: form of the counter-example. If it's a lasso-like form, Type should be |
29 | | * loop(ReEntry) where ReEntry is the offset of the first state of the loop |
30 | | * in the sequence, starting with 0. |
31 | | * If Type is not loop(_), the sequence is regarded as finite |
32 | | * CallbackAP: Callback predicate to check an atomic proposition. Callbacks are of |
33 | | * the form CallbackAP(AP,StateId) where AP is the specification of an atomic |
34 | | * proposition ap(AP) in the AST of the formula and StateId the the ID of the |
35 | | * state in which it should be evaluated. |
36 | | * If the call succeeds, the proposition is regarded as true, if not as false. |
37 | | * CallbackTP: Like CallbackAP, CallbackTP is a predicate to check a proposition |
38 | | * TP on a transition as it appears as action(TP) in the LTL formula. |
39 | | * The call is of the form CallbackTP(TP,StateId,TransID). |
40 | | * Result: true, false or unknown |
41 | | * A formula can only be unknown if the sequence is finite (without a loop). |
42 | | */ |
43 | | :- meta_predicate evaluate_ltl_formula(+,+,+,2,3,-). |
44 | | evaluate_ltl_formula(Formula,StateTransitions,Type,CallbackAP,CallbackTP,Result) :- |
45 | | check_sequence(StateTransitions,Type), |
46 | | length(StateTransitions,N), |
47 | | Path = path(StateTransitions,N,Type,CallbackAP,CallbackTP), |
48 | | eval_ltl_formula(Formula,0,Path,Result), |
49 | | % In case of an unknown result, check if the sequence if finite |
50 | | check_result(Type,Result,Formula). |
51 | | |
52 | | check_sequence(StateTransitions,Type) :- |
53 | | ( Type=loop(_),last(StateTransitions,strans(_,none)) -> |
54 | | add_error(ltl_verification,'last element of lasso sequence has no transition id', |
55 | | StateTransitions) |
56 | | ; true). |
57 | | |
58 | | check_result(loop(_),unknown,Formula) :- |
59 | | !,add_error(ltl_verification, |
60 | | 'evaluate_ltl_formula computed unknown result for infinite sequence', |
61 | | Formula). |
62 | | check_result(loop(_),deadlock,Formula) :- |
63 | | !,add_error(ltl_verification, |
64 | | 'evaluate_ltl_formula computed unknown result for dead locking sequence', |
65 | | Formula). |
66 | | check_result(_Type,_Result,_Formula). |
67 | | |
68 | | eval_ltl_formula(false,_Index,_Path,false). |
69 | | eval_ltl_formula(true,_Index,_Path,true). |
70 | | eval_ltl_formula(ap(AP),Index,Path,Value) :- |
71 | | access_index_in_path(Index,Path,State,_Trans), |
72 | | path_ap(Path,Call), |
73 | | (call(Call,AP,State) -> Value=true ; Value=false). |
74 | | eval_ltl_formula(action(TP),Index,Path,Value) :- |
75 | | access_index_in_path(Index,Path,State,Trans), |
76 | | ( Trans=none -> |
77 | | (eval_ltl_is_deadlock(Index,Path) -> Value=false ; Value=unknown) |
78 | | ; |
79 | | path_tp(Path,Call), |
80 | | (call(Call,TP,State,Trans) -> Value=true ; Value=false)). |
81 | | eval_ltl_formula(not(A),Index,Path,Value) :- |
82 | | eval_ltl_formula(A,Index,Path,VA), |
83 | | ltl_eval_not(VA,Value),!. |
84 | | eval_ltl_formula(and(A,B),Index,Path,Value) :- |
85 | | eval_ltl_formula(A,Index,Path,VA), |
86 | | eval_ltl_formula(B,Index,Path,VB), |
87 | | ltl_eval_and(VA,VB,Value),!. |
88 | | eval_ltl_formula(or(A,B),Index,Path,Value) :- |
89 | | eval_ltl_formula(A,Index,Path,VA), |
90 | | eval_ltl_formula(B,Index,Path,VB), |
91 | | ltl_eval_or(VA,VB,Value),!. |
92 | | eval_ltl_formula(implies(A,B),Index,Path,Value) :- |
93 | | eval_ltl_formula(A,Index,Path,VA), |
94 | | eval_ltl_formula(B,Index,Path,VB), |
95 | | ltl_eval_implies(VA,VB,Value),!. |
96 | | eval_ltl_formula(equivalent(A,B),Index,Path,Value) :- |
97 | | eval_ltl_formula(A,Index,Path,VA), |
98 | | eval_ltl_formula(B,Index,Path,VB), |
99 | | ltl_eval_equivalent(VA,VB,Value),!. |
100 | | eval_ltl_formula(finally(A),Index,Path,Value) :- |
101 | | eval_ltl_formula(until(true,A),Index,Path,Value). % TODO: Do not use normalisation |
102 | | eval_ltl_formula(globally(A),Index,Path,Value) :- |
103 | | eval_ltl_formula(not(finally(not(A))),Index,Path,Value). % TODO: Do not use normalisation |
104 | | eval_ltl_formula(weakuntil(A,B),Index,Path,Value) :- |
105 | | eval_ltl_formula(or(globally(A),until(A,B)),Index,Path,Value). % TODO: Do not use normalisation |
106 | | eval_ltl_formula(release(A,B),Index,Path,Value) :- |
107 | | eval_ltl_formula(not(until(not(A),not(B))),Index,Path,Value). % TODO: Do not use normalisation |
108 | | eval_ltl_formula(once(A),Index,Path,Value) :- |
109 | | eval_ltl_formula(since(true,A),Index,Path,Value). % TODO: Do not use normalisation |
110 | | eval_ltl_formula(historically(A),Index,Path,Value) :- |
111 | | eval_ltl_formula(not(once(not(A))),Index,Path,Value). % TODO: Do not use normalisation |
112 | | eval_ltl_formula(trigger(A,B),Index,Path,Value) :- |
113 | | eval_ltl_formula(not(since(not(A),not(B))),Index,Path,Value). % TODO: Do not use normalisation |
114 | | eval_ltl_formula(next(A),Index,Path,Value) :- |
115 | | last_index_in_path(Path,Last), |
116 | | ( Index<Last -> % we're are somewhere in the path, |
117 | | Next is Index+1,eval_ltl_formula(A,Next,Path,Value) % just use the next position |
118 | | ; path_type(Path,loop(ReEntry)) -> % End of the path: If it's a loop, |
119 | | eval_ltl_formula(A,ReEntry,Path,Value) % use the start of the lasso as next |
120 | | ; eval_ltl_is_deadlock(Index,Path) -> % End of the path (no loop): In a |
121 | | Value=false % deadlock X(...) is always false |
122 | | ; % End of the path: We don't know the |
123 | | Value=unknown). % next state |
124 | | eval_ltl_formula(yesterday(A),Index,Path,Value) :- |
125 | | ( Index > 0 -> |
126 | | Y is Index-1,eval_ltl_formula(A,Y,Path,Value) |
127 | | ; % Y(...) is always false in the |
128 | | Value=false). % initial state. |
129 | | eval_ltl_formula(until(Inv,Goal),Index,Path,Value) :- |
130 | | future_indices(Index,Path,Indices), |
131 | | eval_until(Indices,Inv,Goal,Path,Value). |
132 | | eval_ltl_formula(since(Inv,Goal),Index,Path,Value) :- |
133 | | eval_since(Index,Inv,Goal,Path,Value). |
134 | | eval_ltl_is_deadlock(Index,Path) :- |
135 | | eval_ltl_formula(ap(deadlock),Index,Path,true). |
136 | | |
137 | | access_index_in_path(Index,Path,State,Transition) :- |
138 | | path_statetransitions(Path,StateTransitions), |
139 | | nth0(Index,StateTransitions,strans(State,Transition)). |
140 | | last_index_in_path(Path,Last) :- |
141 | | path_length(Path,N),Last is N-1. |
142 | | |
143 | | path_statetransitions(path(StateTransitions,_N,_Type,_AP,_TP),StateTransitions). |
144 | | path_type(path(_ST,_N,Type,_AP,_TP),Type). |
145 | | path_length(path(_ST,N,_Type,_AP,_TP),N). |
146 | | path_ap(path(_ST,_N,_Type,AP,_TP),AP). |
147 | | path_tp(path(_ST,_N,_Type,_AP,TP),TP). |
148 | | |
149 | | eval_until([],_,_,Path,Result) :- |
150 | | last_index_in_path(Path,Last), |
151 | | ( path_type(Path,loop(_)) -> Result=false |
152 | | ; eval_ltl_is_deadlock(Last,Path) -> Result=false |
153 | | ; Result=unknown). |
154 | | eval_until([H|T],Inv,Goal,Path,Result) :- |
155 | | eval_ltl_formula(Goal,H,Path,GValue), |
156 | | ( GValue = true -> Result=true |
157 | | ; |
158 | | eval_ltl_formula(Inv,H,Path,IValue), |
159 | | eval_until(T,Inv,Goal,Path,NValue), |
160 | | ltl_eval_until(IValue,GValue,NValue,Result),!). |
161 | | |
162 | | future_indices(Index,Path,Result) :- |
163 | | last_index_in_path(Path,Last), |
164 | | numlist(Index,Last,Rest), |
165 | | ( path_type(Path,loop(ReEntry)), Index>ReEntry -> |
166 | | I2 is Index-1, |
167 | | numlist(ReEntry,I2,Before), |
168 | | append(Rest,Before,Result) |
169 | | ; |
170 | | Result = Rest). |
171 | | |
172 | | eval_since(Index,Inv,Goal,Path,Result) :- |
173 | | eval_ltl_formula(Goal,Index,Path,GValue), |
174 | | ( Index = 0 -> Result=GValue |
175 | | ; GValue = true -> Result=true |
176 | | ; |
177 | | eval_ltl_formula(Inv,Index,Path,IValue), |
178 | | ( GValue=false,IValue=false -> Result=false |
179 | | ; |
180 | | Y is Index-1, |
181 | | eval_since(Y,Inv,Goal,Path,NValue), |
182 | | ltl_eval_until(IValue,GValue,NValue,Result),! % same logic as until |
183 | | ) |
184 | | ). |
185 | | |
186 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
187 | | % evalute a fairness condition on a given path |
188 | | |
189 | | /* |
190 | | * evaluate_ltl_fairness(WeakStrong,StateTransitions,Type,FairCall,Result): |
191 | | * WeakStrong: weak or strong: Which fairness type should be checked |
192 | | * StateTransitions: [strans(StateId,TransId)] like in evaluate_ltl_formula/6 |
193 | | * Type: like in evaluate_ltl_formula/6, for all types but loop(_) the is result always fair |
194 | | * FairCall: Callback predicate to check which transitions occur that match the Spec. |
195 | | * The call has the form FairCall(+StateId,TransId,FairId). |
196 | | * StateId is an ID of a state and TransId the ID of a transition starting from that |
197 | | * state. If the predicate fails, it is assumed that the transition is not subject to |
198 | | * fairness. It it succeeds, the predicate should return a term that is used to |
199 | | * destinguish between actions. |
200 | | * E.g. it could return 'op' for both op(1) and op(2) such that all op(...) transitions |
201 | | * are treated as equal. |
202 | | * The call can be used to enumerate all transition IDs with their fairness ID that |
203 | | * start in the state and match the fairness criteria. |
204 | | * Result: 'fair' if the sequence is fair, or unfair(Ids) if the sequence is unfair where |
205 | | * Ids is the list of FairId that are enabled (permanently in the case of weak fairness) |
206 | | * in the loop but never executed. |
207 | | */ |
208 | | :- meta_predicate evaluate_ltl_fairness(+,+,+,3,2,-). |
209 | | :- meta_predicate find_enabled_fairids_for_state(3,-,-). |
210 | | :- meta_predicate find_enabled_fairids(-,3,-,-). |
211 | | :- meta_predicate eval_fairness(-,-,3,2,-). |
212 | | :- meta_predicate is_executed(2,-,-). |
213 | | :- meta_predicate is_executed2(2,-,-). |
214 | | |
215 | | evaluate_ltl_fairness(WeakStrong,StateTransitions,loop(ReEntry),FairCallEnabled,FairCallExecuted,Result) :- |
216 | | !,append_length(Loop,StateTransitions,ReEntry), |
217 | | eval_fairness(WeakStrong,Loop,FairCallEnabled,FairCallExecuted,Result). |
218 | | evaluate_ltl_fairness(_WeakStrong,_ST,_Type,_FairCallEn,_FairCallEx,fair). % Fairness is only relevant for loops |
219 | | eval_fairness(Type,Loop,FairCallEnabled,FairCallExecuted,Result) :- |
220 | | maplist(strans_state,Loop,States), |
221 | | find_enabled_fairids(Type,FairCallEnabled,States,RelevantIds), |
222 | | exclude(is_executed(FairCallExecuted,Loop),RelevantIds,NotExecuted), |
223 | | (NotExecuted = [] -> Result=fair ; Result=unfair(NotExecuted)). |
224 | | strans_state(strans(StateId,_TransId),StateId). |
225 | | |
226 | | find_enabled_fairids(weak,FairCall,[StateId|RLoop],Ids) :- |
227 | | find_enabled_fairids_for_state(FairCall,StateId,Unsorted), |
228 | | sort(Unsorted,InitialIds), |
229 | | find_enabled_fairids_weak(RLoop,FairCall,InitialIds,Ids). |
230 | | find_enabled_fairids(strong,FairCall,Loop,Ids) :- |
231 | | maplist(find_enabled_fairids_for_state(FairCall),Loop,LEnabled), |
232 | | append(LEnabled,Unsorted), |
233 | | sort(Unsorted,Ids). |
234 | | |
235 | | find_enabled_fairids_weak([],_FairCall,Ids,Ids). |
236 | | find_enabled_fairids_weak(_Loop,_FairCall,[],[]) :- !. |
237 | | find_enabled_fairids_weak([StateId|RLoop],FairCall,InitialIds,Ids) :- |
238 | | find_enabled_fairids_for_state(FairCall,StateId,LocalIds), |
239 | | % we use intersect here, only those actions should be tested |
240 | | % for "executed in loop" that are enabled in each state of the loop |
241 | | ord_intersection(InitialIds,LocalIds,Ids1), |
242 | | find_enabled_fairids_weak(RLoop,FairCall,Ids1,Ids). |
243 | | |
244 | | find_enabled_fairids_for_state(FairCall,StateId,Enabled) :- |
245 | | findall(FairId,call(FairCall,StateId,_TransId,FairId),Unsorted), |
246 | | sort(Unsorted,Enabled). |
247 | | |
248 | | |
249 | | is_executed(FairCall,Loop,FairId) :- |
250 | | somechk(is_executed2(FairCall,FairId),Loop). |
251 | | is_executed2(FairCall,FairId,strans(StateId,_TransId)) :- |
252 | | call(FairCall,StateId,FairId),!. |
253 | | |
254 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
255 | | % determine unknown values by giving rules for known values |
256 | | |
257 | | compute_unknown(CorePred,Arity,TargetPred) :- |
258 | ? | enumerate_true_false_unknown(Arity,InputArgs), |
259 | ? | compute_unknown_values(CorePred,InputArgs,Result), |
260 | | ToStore =.. [TargetPred | Result], |
261 | | % print( assertz(ToStore) ),nl, |
262 | | assertz( ToStore ), |
263 | | fail. |
264 | | compute_unknown(_CorePred,_Arity,_TargetPred). |
265 | | |
266 | | enumerate_true_false_unknown(0,[]). |
267 | | enumerate_true_false_unknown(Arity,[Value|Rest]) :- |
268 | ? | Arity > 0, member(Value,[true,false,unknown]), |
269 | ? | A2 is Arity-1, enumerate_true_false_unknown(A2,Rest). |
270 | | |
271 | | compute_unknown_values(CorePred,InputArgs,Result) :- |
272 | | length(InputArgs,N), N1 is N+1, |
273 | | length(Args,N1), |
274 | | append(IArgs,[R],Args), |
275 | | Call =.. [CorePred | Args], |
276 | | findall( R, (maplist(enumerate_unknown,InputArgs,IArgs), |
277 | | call(Call)), |
278 | | Outputs), |
279 | | sort(Outputs,SOutputs), |
280 | | ( SOutputs = [O] -> true |
281 | | ; SOutputs = [_|_] -> O=unknown), |
282 | | append(InputArgs,[O],Result). |
283 | | |
284 | | enumerate_unknown(true,true). |
285 | | enumerate_unknown(false,false). |
286 | ? | enumerate_unknown(unknown,V) :- member(V,[true,false]). |
287 | | |
288 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
289 | | % basic rules |
290 | | |
291 | | :- public ltl_eval_not_base/2, ltl_eval_and_base/3, ltl_eval_or_base/3, ltl_eval_equivalent_base/3. |
292 | | :- public ltl_eval_implies_base/3, ltl_eval_until_base/4. |
293 | | |
294 | | ltl_eval_not_base(true, false). |
295 | | ltl_eval_not_base(false,true). |
296 | | |
297 | | ltl_eval_and_base(false,_, false). |
298 | | ltl_eval_and_base(true, false,false). |
299 | | ltl_eval_and_base(true, true, true). |
300 | | |
301 | | ltl_eval_or_base(true, _, true). |
302 | | ltl_eval_or_base(false,true, true). |
303 | | ltl_eval_or_base(false,false,false). |
304 | | |
305 | | ltl_eval_implies_base(false,_, true). |
306 | | ltl_eval_implies_base(true, true, true). |
307 | | ltl_eval_implies_base(true, false,false). |
308 | | |
309 | | ltl_eval_equivalent_base(false, false,true). |
310 | | ltl_eval_equivalent_base(true, true,true). |
311 | | ltl_eval_equivalent_base(true, false,false). |
312 | | ltl_eval_equivalent_base(false,true,false). |
313 | | |
314 | | ltl_eval_until_base(_, true, _,true). |
315 | | ltl_eval_until_base(false,false,_,false). |
316 | | ltl_eval_until_base(true, false,N,N). |
317 | | |
318 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
319 | | % lifted to unknown values |
320 | | |
321 | | :- dynamic ltl_eval_not/2, ltl_eval_and/3, ltl_eval_or/3, ltl_eval_implies/3, ltl_eval_equivalent/3. |
322 | | :- dynamic ltl_eval_until/4. |
323 | | :- compute_unknown(ltl_eval_not_base,1,ltl_eval_not). |
324 | | :- compute_unknown(ltl_eval_and_base,2,ltl_eval_and). |
325 | | :- compute_unknown(ltl_eval_or_base,2,ltl_eval_or). |
326 | | :- compute_unknown(ltl_eval_implies_base,2,ltl_eval_implies). |
327 | | :- compute_unknown(ltl_eval_equivalent_base,2,ltl_eval_equivalent). |
328 | | :- compute_unknown(ltl_eval_until_base,3,ltl_eval_until). |