| 1 | % (c) 2014-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 | :- module(ltl_fairness,[initialise_fairness_assumptions/4, | |
| 6 | fairness_check_on/2, | |
| 7 | ev_fairness_id/3, | |
| 8 | ev_fairness_id/4, | |
| 9 | get_fairness_specification/3, | |
| 10 | check_scc_ce/2]). | |
| 11 | ||
| 12 | :- use_module(probsrc(module_information)). | |
| 13 | :- module_info(group,ltl). | |
| 14 | :- module_info(description,'This module provides LTL fairness checking on models.'). | |
| 15 | ||
| 16 | % SICSTUS libraries | |
| 17 | :- use_module(library(lists)). | |
| 18 | :- use_module(library(ordsets)). | |
| 19 | :- use_module(library(codesio)). % for read_from_codes/2 | |
| 20 | ||
| 21 | % ProB libraries | |
| 22 | :- use_module(probsrc(specfile),[animation_mode/1]). | |
| 23 | :- use_module(probsrc(self_check)). | |
| 24 | :- use_module(probsrc(error_manager)). | |
| 25 | :- use_module(probsrc(debug)). | |
| 26 | :- use_module(probsrc(state_space),[transition/4]). | |
| 27 | ||
| 28 | :- use_module(probltlsrc(ltl_tools), [preprocess_tp/2]). | |
| 29 | :- use_module(probltlsrc(ltl_propositions), [check_transition/4]). | |
| 30 | ||
| 31 | % import the low-level C-library wrapper | |
| 32 | :- use_module(extension('ltlc/ltlc')). | |
| 33 | ||
| 34 | % We allow that more than one action can be given in a single LTL formula | |
| 35 | % for checking the found SCC component for fairness in regard to those actions. | |
| 36 | % There are two types of fairness which we want to support for the LTL Model Checker: strong and weak fairness. | |
| 37 | ||
| 38 | % We use the operators SF(-) and WF(-) for picking actions for the fairness assumption. If we want to check | |
| 39 | % an LTL formula "f" by setting strong fairness constraints for the action a, we write then "SF(a) => f". | |
| 40 | % It is also possible to express fairness constraints for more than one actions by using the boolean operators | |
| 41 | % & and or. | |
| 42 | ||
| 43 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 44 | ||
| 45 | ||
| 46 | %%%%%%%%%%%%%%%%%%%% Initialising the fairness assumptions (begin) %%%%%%%%%%%%%%%%%%%%% | |
| 47 | % temporary implemented prediates for testing the fairness check implementation. | |
| 48 | ||
| 49 | % if you want to check if a trace is strongly fair w.r.t. multiple actions (e.g. Req2 and Req1) | |
| 50 | % then conjugate these with the & operator and place every action between two braces | |
| 51 | ||
| 52 | % in case fairness should be ignored, just give an empty atom ''. | |
| 53 | ||
| 54 | fairness_check_on(all,_StrongFairnessAssumption). | |
| 55 | fairness_check_on([_|_],_StrongFairnessAssumption). | |
| 56 | fairness_check_on(_WeakFairnessAssumption,all). | |
| 57 | fairness_check_on(_WeakFairnessAssumption,[_|_]). | |
| 58 | ||
| 59 | initialise_fairness_assumptions(Ltl,WeakFairnessArgs,StrongFairnessArgs,LtlFormula) :- | |
| 60 | (Ltl = fairnessimplication(FairnessFormula,LtlFormula) -> | |
| 61 | get_strong_weak_fairness_arguments(FairnessFormula,WeakFairnessArgs,StrongFairnessArgs), | |
| 62 | debug_println(9,get_strong_weak_fairness_arguments(FairnessFormula,WeakFairnessArgs,StrongFairnessArgs)) | |
| 63 | ; | |
| 64 | WeakFairnessArgs = [], StrongFairnessArgs = [], LtlFormula = Ltl). | |
| 65 | ||
| 66 | get_strong_weak_fairness_arguments(FairnessFormula,WeakFairnessArgs,StrongFairnessArgs) :- | |
| 67 | (FairnessFormula = and(strongassumptions(SAssumptions),weakassumptions(WAssumptions)) | |
| 68 | -> get_fairness_assumption_actions(SAssumptions,StrongFairnessArgs), | |
| 69 | get_fairness_assumption_actions(WAssumptions,WeakFairnessArgs) | |
| 70 | ; FairnessFormula = and(weakassumptions(WAssumptions),strongassumptions(SAssumptions)) | |
| 71 | -> get_fairness_assumption_actions(SAssumptions,StrongFairnessArgs), | |
| 72 | get_fairness_assumption_actions(WAssumptions,WeakFairnessArgs) | |
| 73 | ; FairnessFormula = weakassumptions(F) | |
| 74 | -> StrongFairnessArgs =[], get_fairness_assumption_actions(F,WeakFairnessArgs) | |
| 75 | ; FairnessFormula = strongassumptions(F) | |
| 76 | -> WeakFairnessArgs = [], get_fairness_assumption_actions(F,StrongFairnessArgs) | |
| 77 | ; | |
| 78 | add_internal_error('Unrecognised fairness assumption: ', get_strong_weak_fairness_arguments(FairnessFormula,WeakFairnessArgs,StrongFairnessArgs)) | |
| 79 | ). | |
| 80 | ||
| 81 | get_fairness_assumption_actions(F,Res) :- | |
| 82 | (F=all -> | |
| 83 | Res = all | |
| 84 | ; | |
| 85 | normalise_to_dnf(F,DNF), | |
| 86 | (debug:debug_mode(on) -> | |
| 87 | ltl_translate: pp_ltl_formula(DNF,Text), | |
| 88 | print('Disjunctive Normal Form for Fairness Forlmula: '), | |
| 89 | print(Text),nl | |
| 90 | ; true), | |
| 91 | get_or_args(DNF,R), | |
| 92 | list_to_ord_set(R,Res) | |
| 93 | ). | |
| 94 | ||
| 95 | :- assert_must_succeed((normalise_to_dnf(and(or(ap(a),ap(b)),ap(c)),R), R == or(and(ap(a),ap(c)),and(ap(b),ap(c))))). | |
| 96 | :- assert_must_succeed((normalise_to_dnf(and(ap(a),ap(b)),R), R == and(ap(a),ap(b)))). | |
| 97 | :- assert_must_succeed((normalise_to_dnf(or(ap(a),ap(b)),R), R == or(ap(a),ap(b)))). | |
| 98 | :- assert_must_succeed((normalise_to_dnf(ap(a),R), R == ap(a))). | |
| 99 | :- assert_must_succeed((normalise_to_dnf(and(or(ap(a),ap(b)),or(ap(c),ap(d))),R), | |
| 100 | R == or(or(and(ap(a),ap(c)),and(ap(a),ap(d))),or(and(ap(b),ap(c)),and(ap(b),ap(d)))) )). | |
| 101 | ||
| 102 | normalise_to_dnf(F,DNF) :- | |
| 103 | ex2disj(F,DNF). | |
| 104 | ||
| 105 | ex2disj(or(A,B),or(AR,BR)) :- !, | |
| 106 | ex2disj(A,AR), | |
| 107 | ex2disj(B,BR). | |
| 108 | ex2disj(and(A,B),R) :- !, | |
| 109 | ex2disj(A,AR), | |
| 110 | ex2disj(B,BR), | |
| 111 | join(AR,BR,R). | |
| 112 | ex2disj(ap(X),ap(X)) :- !. | |
| 113 | ||
| 114 | join(or(A,B),C,or(AC,BC)) :- !, | |
| 115 | join(A,C,AC), | |
| 116 | join(B,C,BC). | |
| 117 | join(C,or(A,B),or(AC,BC)) :- | |
| 118 | C\=or(_,_),!, | |
| 119 | join(C,A,AC), | |
| 120 | join(C,B,BC). | |
| 121 | join(A,B,and(A,B)) :- | |
| 122 | A\=or(_,_),B\=or(_,_),!. | |
| 123 | ||
| 124 | % left argument of get_and_args/2 is a boolean formula in DNF without any not(-) operators | |
| 125 | get_or_args(ap(strong_fair(A)),[[R]]) :- !, | |
| 126 | preprocess_tp(A,R). | |
| 127 | get_or_args(ap(weak_fair(A)),[[R]]) :- !, | |
| 128 | preprocess_tp(A,R). | |
| 129 | %get_or_args(ap(A),[[A]]) :- atom(A),!. | |
| 130 | get_or_args(and(A,B),Args) :- !, | |
| 131 | get_and_args(and(A,B),Res), | |
| 132 | list_to_ord_set(Res,Res1), | |
| 133 | Args = [Res1]. | |
| 134 | get_or_args(or(A,B),Res) :- !, | |
| 135 | get_or_args(A,R1), | |
| 136 | get_or_args(B,R2), | |
| 137 | append(R1,R2,Res). | |
| 138 | ||
| 139 | get_and_args(ap(strong_fair(A)),[R]) :- !, preprocess_tp(A,R). | |
| 140 | get_and_args(ap(weak_fair(A)),[R]) :- !, preprocess_tp(A,R). | |
| 141 | %get_and_args(ap(A),[A]) :- atom(A),!. | |
| 142 | get_and_args(and(A,B),Res) :- !, | |
| 143 | get_and_args(A,R1), | |
| 144 | get_and_args(B,R2), | |
| 145 | append(R1,R2,Res). | |
| 146 | %%%%%%%%%%%%%%%%%%%% Initialising the fairness assumptions (end) %%%%%%%%%%%%%%%%%%%%% | |
| 147 | ||
| 148 | ||
| 149 | %%%%%%%%%%%%%%%%%%%% Callback predicates (begin) %%%%%%%%%%%%%%%%%%%%% | |
| 150 | % Callback from LTLc (fairness): | |
| 151 | ||
| 152 | % check_fairness(FairnessAssumption,[anode(AtomId,Nodeid,[trans(NextAtomId,NextNodeId,[TransitionId])])]) | |
| 153 | % FairnessAssumtion is the Fairness Condition of the LTL formula. | |
| 154 | % For instance, if we have the LTL formula "SF ([a] & [b]) => Phi" then FairnessAssumption consists of the actions [a,b] | |
| 155 | ||
| 156 | % Tested only for B and CSP models | |
| 157 | %% :- use_module(library(timeout)). | |
| 158 | ||
| 159 | %get_transition_ids(Arg,StateIds,LTransIds) :- | |
| 160 | % time_out(get_transition_ids_1(Arg,StateIds,LTransIds1),5000,R), | |
| 161 | % (R = time_out -> LTransIds = []; LTransIds = LTransIds1). | |
| 162 | ||
| 163 | :- public cltl_get_transition_ids_callback/3. | |
| 164 | %%% infolog-analysis: call-back predicate from C | |
| 165 | cltl_get_transition_ids_callback(Arg,StateIds,LTransIds) :- | |
| 166 | (var(Arg) -> | |
| 167 | add_internal_error('Action argument is a variable!',cltl_get_transition_ids_callback(Arg,StateIds,LTransIds)) | |
| 168 | ; var(StateIds) -> | |
| 169 | % if StateIds is a variable it can cause endless loop (memory use increases rapidly) | |
| 170 | add_internal_error('Unexpected argument for state ids. Expected a list of state ids, but got a variable!',cltl_get_transition_ids_callback(Arg,StateIds,LTransIds)) | |
| 171 | ; | |
| 172 | get_transition_ids(Arg,StateIds,LTransIds), | |
| 173 | length(StateIds,NStates),length(LTransIds,NTransitions), | |
| 174 | debug_println(9,get_transition_ids(fainress_argument(Arg),state_ids(NStates,StateIds),transition_ids(NTransitions,LTransIds))) | |
| 175 | ). | |
| 176 | ||
| 177 | get_transition_ids(Arg,StateIds,LTransIds) :- | |
| 178 | findall(TransId,(member(NodeId,StateIds),match_transition(NodeId,Arg,TransId)),LTransIds). | |
| 179 | ||
| 180 | match_transition(NodeId,Arg,TransId) :- | |
| 181 | %% print(match_transition(NodeId,Arg,TransId)),nl, | |
| 182 | ? | transition(NodeId,OpName,TransId,Dst), |
| 183 | ? | match_transition_with_argument(Arg,OpName,NodeId,Dst). |
| 184 | %% check_transition(Arg,OpName,NodeId,_Dst). | |
| 185 | ||
| 186 | match_transition_with_argument(bop(Name,NumberArgs,NumberResults,ArgPatterns,ResPatterns),Transition,_NodeId,_Dst) :- !, | |
| 187 | functor(Op,Name,NumberArgs), | |
| 188 | ( NumberResults == 0 -> | |
| 189 | Transition = Op | |
| 190 | ; | |
| 191 | Transition = '-->'(Op,ReturnValues), | |
| 192 | length(ReturnValues,NumberResults), | |
| 193 | (ReturnValues=ResPatterns -> true | |
| 194 | ; ltl_propositions: check_bop_res_patterns(ResPatterns,SrcNode,State,ReturnValues)) | |
| 195 | ), | |
| 196 | (Op =.. [_Name|ArgPatterns]; ltl_propositions: check_bop_arg_patterns(ArgPatterns,SrcNode,State,Op)). | |
| 197 | match_transition_with_argument(Op,Transition,NodeId,DstId) :- | |
| 198 | ? | check_transition(Op,Transition,NodeId,DstId). |
| 199 | ||
| 200 | :- public cltl_get_enabled_actions_callback/2. | |
| 201 | % In case we have general fairness checking for all actions of the model | |
| 202 | %%% infolog-analysis: call-back predicate from C | |
| 203 | cltl_get_enabled_actions_callback(StateIds,ActionsSet) :- | |
| 204 | % is it possible to get an empty list? | |
| 205 | findall(Action,(member(StateId,StateIds),get_enabled_action(StateId,Action)),Actions), | |
| 206 | list_to_ord_set(Actions,ActionsSet), | |
| 207 | debug_println(9,enabled_actions(StateIds,ActionsSet)). | |
| 208 | ||
| 209 | get_enabled_action(StateId,Action):- | |
| 210 | ? | transition(StateId,A,_AId,_DstId), |
| 211 | create_action_argument(A,Action). | |
| 212 | ||
| 213 | create_action_argument(A,Action) :- | |
| 214 | animation_mode(Mode), | |
| 215 | (Mode == cspm -> | |
| 216 | get_tp_specification_for_csp(A,Action) | |
| 217 | ; Mode == b -> | |
| 218 | get_tp_specification_for_b(A,Action) | |
| 219 | ; Mode == csp_and_b -> | |
| 220 | get_tp_specification_for_csp_and_b(A,Action) | |
| 221 | ; Mode == xtl -> %TO DO: review wether ok | |
| 222 | create_xtl_action_argument(A,Action) | |
| 223 | ; % TODO: implement general fairness check support also for the other formalisms | |
| 224 | animation_mode(Mode), | |
| 225 | add_error(ltl_wrap_action,'Fairness not supported for ',action(A,Mode)) | |
| 226 | ). | |
| 227 | ||
| 228 | create_xtl_action_argument(Op,xtl(OpName,Arity,Args)) :- | |
| 229 | functor(Op,OpName,Arity), Op =.. [_|Args]. | |
| 230 | ||
| 231 | get_tp_specification_for_csp_and_b(A,Action) :- | |
| 232 | % plain CSP event | |
| 233 | functor(A,F,_), | |
| 234 | member(F,[tau,io]),!, | |
| 235 | get_tp_specification_for_csp(A,Action). | |
| 236 | get_tp_specification_for_csp_and_b(A,Action) :- | |
| 237 | get_tp_specification_for_b(A,Action). | |
| 238 | ||
| 239 | :- public get_transition_id/4. % used by C Callback ?? | |
| 240 | get_transition_id(Arg,NodeId,TransId,DstId) :- | |
| 241 | ? | transition(NodeId,Op,TransId,DstId), |
| 242 | ? | match_transition_with_argument(Arg,Op,NodeId,DstId). |
| 243 | % %% check_transition(Arg,Op,NodeId,DstId). | |
| 244 | ||
| 245 | %%%%%%%%%%%%%%%%%%%% Callback predicates (end) %%%%%%%%%%%%%%%%%%%%% | |
| 246 | ||
| 247 | %%%%%%%%%%%%%%%%% Predicates for checking whether the given SCC is a possible counter example for a checked Ltl formula %%%%%%%%%%%%%%%% | |
| 248 | ||
| 249 | :- use_module(probltlsrc(ltl_tools),[temporal_parser/3]). | |
| 250 | :- use_module(probltlsrc(ltl),[ltl_model_check_ast/5]). | |
| 251 | ||
| 252 | check_scc_ce(LtlFormula,SCC) :- | |
| 253 | Max = 10000, Mode = init, | |
| 254 | (temporal_parser(LtlFormula,ltl,Ltl) -> true ; add_error_fail(ltl,'LTL Parser failed: ',LtlFormula)), | |
| 255 | ltl_model_check_ast(Ltl,Max,Mode,_,Status), % TO DO: why do we call this internal predicate ?? | |
| 256 | clean_scc(Status,Result), | |
| 257 | atom_codes(SCC,Codes), | |
| 258 | read_from_codes(Codes,SCCTerm), | |
| 259 | (match_ce_result(SCCTerm,Result) -> | |
| 260 | true | |
| 261 | ; | |
| 262 | print(result_was(Result)),nl, | |
| 263 | add_error(ltl_scc_check,'No one of the SCCs could be reproduced as counter example: ',SCC) | |
| 264 | ). | |
| 265 | ||
| 266 | % predicates for removing all unnecessary information like atomids and ap/tp evaluations | |
| 267 | clean_scc(model(Trace,Entry),Result) :- | |
| 268 | maplist(get_nodeid,Trace,CleanedTrace), | |
| 269 | Result = model(CleanedTrace,Entry). | |
| 270 | ||
| 271 | get_nodeid(atom(StateId,_Evaluation,_AtomId),StateId). | |
| 272 | get_nodeid(El,StateId) :- add_internal_error('Unrecognised trace element: ', get_nodeid(El,StateId)). | |
| 273 | ||
| 274 | match_ce_result([],_) :- !,fail. | |
| 275 | match_ce_result([H|T],Result) :- | |
| 276 | (H = Result -> true; match_ce_result(T,Result)). | |
| 277 | ||
| 278 | %%%%%%%%%%%%%%% To get fairness specifications for the particular loop %%%%%%%%%%%%%%% | |
| 279 | get_fairness_specification(loop(ReEntry),StateTransitions,Assumption) :- !, | |
| 280 | append_length(Loop,StateTransitions,ReEntry), | |
| 281 | maplist(get_specifications,Loop,ListsofSpecs), | |
| 282 | append(ListsofSpecs,Specs), | |
| 283 | list_to_ord_set(Specs,OrdSet), | |
| 284 | Assumption = [OrdSet]. | |
| 285 | get_fairness_specification(_,_,[[]]). | |
| 286 | ||
| 287 | get_specifications(strans(StateId,_),Specs) :- | |
| 288 | findall(Spec, | |
| 289 | (transition(StateId,Transition,_TransId,_DstId),get_tp_specification(Transition,Spec)), | |
| 290 | Specs). | |
| 291 | ||
| 292 | get_tp_specification(Transition,Spec) :- animation_mode(Mode), | |
| 293 | get_tp_specification(Mode,Transition,Spec). | |
| 294 | ||
| 295 | get_tp_specification(b,Transition,Spec) :- !, | |
| 296 | get_tp_specification_for_b(Transition,Spec). | |
| 297 | get_tp_specification(csp_and_b,Transition,Spec) :- !, | |
| 298 | get_tp_specification_for_csp_and_b(Transition,Spec). | |
| 299 | get_tp_specification(cspm,Transition,Spec) :- !, | |
| 300 | get_tp_specification_for_csp(Transition,Spec). | |
| 301 | get_tp_specification(xtl, Transition,Spec) :- !, % TO DO: review wether ok | |
| 302 | create_xtl_action_argument(Transition,Spec). | |
| 303 | get_tp_specification(Mode,Transition,_Spec) :- | |
| 304 | add_error_fail(ltl_verification, 'Fairness not implemented for formalism yet ',Mode:Transition). | |
| 305 | ||
| 306 | /* B transition specification */ | |
| 307 | get_tp_specification_for_b('-->'(Op,ReturnValues),Spec) :- !, | |
| 308 | Op =.. [OpName|Args], | |
| 309 | length(Args,NumberArgs), | |
| 310 | length(ReturnValues,NumberResults), | |
| 311 | Spec=bop(OpName,NumberArgs,NumberResults,Args,ReturnValues). | |
| 312 | get_tp_specification_for_b(Transition,Spec) :- | |
| 313 | Transition =.. [OpName|Args], | |
| 314 | length(Args,NumberArgs), | |
| 315 | Spec=bop(OpName,NumberArgs,0,Args,[]). | |
| 316 | ||
| 317 | /* CSP transition specification */ | |
| 318 | get_tp_specification_for_csp(tick(_),Res) :- !, Res = csp(tick,0,[]). | |
| 319 | get_tp_specification_for_csp(tau(_),Res) :- !, Res=csp(tau,0,[]). | |
| 320 | get_tp_specification_for_csp(io(Vals,Channel,_Span),Res) :- !, | |
| 321 | length(Vals,N), | |
| 322 | Res = csp(Channel,N,Vals). | |
| 323 | get_tp_specification_for_csp(A,Action) :- | |
| 324 | add_internal_error('Unknown CSP event: ',get_tp_specification_for_csp(A,Action)), | |
| 325 | Action=csp(unknown(A),0,[]). | |
| 326 | ||
| 327 | ev_fairness_id(Spec,StateId,Op) :- | |
| 328 | ? | check_transition(Spec,Op,StateId,_DstId). |
| 329 | ev_fairness_id(Spec,StateId,TransId,Op) :- | |
| 330 | ? | transition(StateId,Op,TransId,DstId), |
| 331 | ? | check_transition(Spec,Op,StateId,DstId). |