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