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