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