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).