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