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,
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,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		* Result: 'fair' if the sequence is fair, or unfair(Ids) if the sequence is unfair where
245		* Ids is the list of FairId that are enabled (permanently in the case of weak fairness)
246		* in the loop but never executed.
247		*/
248		:- meta_predicate evaluate_ltl_fairness(+,+,+,3,2,-).
249		:- meta_predicate find_enabled_fairids_for_state(3,-,-).
250		:- meta_predicate find_enabled_fairids(-,3,-,-).
251		:- meta_predicate eval_fairness(-,-,3,2,-).
252		:- meta_predicate is_executed(2,-,-).
253		:- meta_predicate is_executed2(2,-,-).
254
255		evaluate_ltl_fairness(WeakStrong,StateTransitions,loop(ReEntry),FairCallEnabled,FairCallExecuted,Result) :-
256		!,append_length(Loop,StateTransitions,ReEntry),
257	?	eval_fairness(WeakStrong,Loop,FairCallEnabled,FairCallExecuted,Result).
258		evaluate_ltl_fairness(_WeakStrong,_ST,_Type,_FairCallEn,_FairCallEx,fair). % Fairness is only relevant for loops
259		eval_fairness(Type,Loop,FairCallEnabled,FairCallExecuted,Result) :-
260		maplist(strans_state,Loop,States),
261	?	find_enabled_fairids(Type,FairCallEnabled,States,RelevantIds),
262		exclude(is_executed(FairCallExecuted,Loop),RelevantIds,NotExecuted),
263		(NotExecuted = [] -> Result=fair ; Result=unfair(NotExecuted)).
264		strans_state(strans(StateId,_TransId),StateId).
265
266		find_enabled_fairids(weak,FairCall,[StateId|RLoop],Ids) :-
267		find_enabled_fairids_for_state(FairCall,StateId,Unsorted),
268		sort(Unsorted,InitialIds),
269	?	find_enabled_fairids_weak(RLoop,FairCall,InitialIds,Ids).
270		find_enabled_fairids(strong,FairCall,Loop,Ids) :-
271		maplist(find_enabled_fairids_for_state(FairCall),Loop,LEnabled),
272		append(LEnabled,Unsorted),
273		sort(Unsorted,Ids).
274
275		find_enabled_fairids_weak([],_FairCall,Ids,Ids).
276		find_enabled_fairids_weak(_Loop,_FairCall,[],[]) :- !.
277		find_enabled_fairids_weak([StateId|RLoop],FairCall,InitialIds,Ids) :-
278		find_enabled_fairids_for_state(FairCall,StateId,LocalIds),
279		% we use intersect here, only those actions should be tested
280		% for "executed in loop" that are enabled in each state of the loop
281		ord_intersection(InitialIds,LocalIds,Ids1),
282	?	find_enabled_fairids_weak(RLoop,FairCall,Ids1,Ids).
283
284		find_enabled_fairids_for_state(FairCall,StateId,Enabled) :-
285		findall(FairId,call(FairCall,StateId,_TransId,FairId),Unsorted),
286		sort(Unsorted,Enabled).
287
288
289		is_executed(FairCall,Loop,FairId) :-
290		somechk(is_executed2(FairCall,FairId),Loop).
291		is_executed2(FairCall,FairId,strans(StateId,_TransId)) :-
292		call(FairCall,StateId,FairId),!.
293
294		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
295		% determine unknown values by giving rules for known values
296
297		compute_unknown(CorePred,Arity,TargetPred) :-
298	?	enumerate_true_false_unknown(Arity,InputArgs),
299	?	compute_unknown_values(CorePred,InputArgs,Result),
300		ToStore =.. [TargetPred | Result],
301		% print( assertz(ToStore) ),nl,
302		assertz( ToStore ),
303		fail.
304		compute_unknown(_CorePred,_Arity,_TargetPred).
305
306		enumerate_true_false_unknown(0,[]).
307		enumerate_true_false_unknown(Arity,[Value|Rest]) :-
308	?	Arity > 0, member(Value,[true,false,unknown]),
309	?	A2 is Arity-1, enumerate_true_false_unknown(A2,Rest).
310
311		compute_unknown_values(CorePred,InputArgs,Result) :-
312		length(InputArgs,N), N1 is N+1,
313		length(Args,N1),
314		append(IArgs,[R],Args),
315		Call =.. [CorePred | Args],
316		findall( R, (maplist(enumerate_unknown,InputArgs,IArgs),
317		call(Call)),
318		Outputs),
319		sort(Outputs,SOutputs),
320		( SOutputs = [O] -> true
321		; SOutputs = [_|_] -> O=unknown),
322		append(InputArgs,[O],Result).
323
324		enumerate_unknown(true,true).
325		enumerate_unknown(false,false).
326	?	enumerate_unknown(unknown,V) :- member(V,[true,false]).
327
328		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
329		% basic rules
330
331		:- public ltl_eval_not_base/2, ltl_eval_and_base/3, ltl_eval_or_base/3, ltl_eval_equivalent_base/3.
332		:- public ltl_eval_implies_base/3, ltl_eval_until_base/4.
333
334		ltl_eval_not_base(true, false).
335		ltl_eval_not_base(false,true).
336
337		ltl_eval_and_base(false,_, false).
338		ltl_eval_and_base(true, false,false).
339		ltl_eval_and_base(true, true, true).
340
341		ltl_eval_or_base(true, _, true).
342		ltl_eval_or_base(false,true, true).
343		ltl_eval_or_base(false,false,false).
344
345		ltl_eval_implies_base(false,_, true).
346		ltl_eval_implies_base(true, true, true).
347		ltl_eval_implies_base(true, false,false).
348
349		ltl_eval_equivalent_base(false, false,true).
350		ltl_eval_equivalent_base(true, true,true).
351		ltl_eval_equivalent_base(true, false,false).
352		ltl_eval_equivalent_base(false,true,false).
353
354		ltl_eval_until_base(_, true, _,true).
355		ltl_eval_until_base(false,false,_,false).
356		ltl_eval_until_base(true, false,N,N).
357
358		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
359		% lifted to unknown values
360
361		:- dynamic ltl_eval_not/2, ltl_eval_and/3, ltl_eval_or/3, ltl_eval_implies/3, ltl_eval_equivalent/3.
362		:- dynamic ltl_eval_until/4.
363		:- compute_unknown(ltl_eval_not_base,1,ltl_eval_not).
364		:- compute_unknown(ltl_eval_and_base,2,ltl_eval_and).
365		:- compute_unknown(ltl_eval_or_base,2,ltl_eval_or).
366		:- compute_unknown(ltl_eval_implies_base,2,ltl_eval_implies).
367		:- compute_unknown(ltl_eval_equivalent_base,2,ltl_eval_equivalent).
368		:- compute_unknown(ltl_eval_until_base,3,ltl_eval_until).