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