1 | | % (c) 2009-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(ltlc, [ltlc_init/0,c_ltl_modelcheck/4,c_ltl_modelcheck/9,c_ltl_aptp/2]). |
6 | | |
7 | | :- use_module(library(lists)). |
8 | | :- use_module('../../src/module_information.pl'). |
9 | | :- use_module('../../src/debug.pl'). |
10 | | :- use_module('../../src/error_manager.pl'). |
11 | | |
12 | | :- module_info(group,ltl). |
13 | | :- module_info(description,'This is the interface to the LTL model checker\'s C code.'). |
14 | | |
15 | | :- meta_predicate c_ltl_modelcheck(-,-,-,5). |
16 | | |
17 | | /* the C interface */ |
18 | | foreign_resource(ltlc, [ltlc_modelcheck]). |
19 | | foreign(ltlc_modelcheck,ltlc_modelcheck(+term,+term,+term,+term,+term,+term,+term,+term,+term,-term)). |
20 | | |
21 | | |
22 | | :- dynamic loaded/0. |
23 | | |
24 | | ltlc_init :- loadfr. |
25 | | |
26 | | loadfr :- (loaded -> true |
27 | | ; (assertz(loaded), |
28 | | load_foreign_resource(library(ltlc))) |
29 | | ). |
30 | | |
31 | | |
32 | | /* The central predicate */ |
33 | | c_ltl_modelcheck(Formula, Startnodes, Result, CModule:Callback) :- |
34 | ? | c_ltl_modelcheck(Formula, Startnodes, Result, CModule:Callback, none, none, none, [], []). |
35 | | |
36 | | c_ltl_modelcheck(Formula, Startnodes, Result, Callback, |
37 | | Update, GetTransIdsPred, GetEnabledActionsPred, WeakFairnessArgs, StrongFairnessArgs) :- |
38 | ? | c_ltl_closure(Formula,Closure,Main,_), |
39 | | debug_println(9,closure(Formula,Closure,Main)), |
40 | | debug_println(9,fairness(GetTransIdsPred, WeakFairnessArgs, StrongFairnessArgs)), |
41 | | ltlc_modelcheck(Closure, Startnodes, Callback, |
42 | | Update, GetTransIdsPred, GetEnabledActionsPred, WeakFairnessArgs, StrongFairnessArgs, Main, Result). |
43 | | |
44 | | % Return the list of atomic propositions and transition propositions |
45 | | % of a formula. c_ltl_modelcheck returns counter-examples, where the |
46 | | % evaluation part of the atoms begins with the evaluation of the |
47 | | % formulas corresponding to ApTp. |
48 | | c_ltl_aptp(Formula,ApTp) :- |
49 | | c_ltl_closure(Formula,_,_,ApTp). |
50 | | |
51 | | /* Take a formula (with all supported operators), normalise it |
52 | | * (rewrite to basic operators) and convert it into a list of |
53 | | * atomic propositions (APs), transition propositions (TPs), |
54 | | * and basic operators with references to other parts of the |
55 | | * closure. |
56 | | * Additionally a reference to the original formula is given |
57 | | * Each reference has the form pos(N) or neg(N) where N is |
58 | | * the position of the subformula in the closure (starting with 0). |
59 | | * The position -1 refers to "true". |
60 | | * The closure always start with the APs and TPs. |
61 | | * Example: |
62 | | * Formula: not(globally(ap(AP))) |
63 | | * Closure: [ap(AP),next(3),nextnot(3),until(pos(-1),neg(0),1) |
64 | | * Main: pos(3) |
65 | | */ |
66 | | c_ltl_closure(Formula,Closure,Main,Atomics) :- |
67 | | %ltl_translate:pp_ltl_formula(Formula,FTxt), format('Normalising: ~w~n',[FTxt]), |
68 | | ( ltl_norm(Formula, Normalised) -> |
69 | | debug_println(normal_form(Normalised)) |
70 | | ; atom(Formula) -> |
71 | | add_internal_error('ltl_norm failed for formula, be sure to pass it as term and not as atom: ',Formula), |
72 | | fail |
73 | | ; |
74 | | add_internal_error('ltl_norm failed for formula: ',Formula), |
75 | | fail), |
76 | | %ltl_translate:pp_ltl_formula(Normalised,NTxt), format('Normalised = ~w~n',[NTxt]), |
77 | | positive_closure(Normalised, PClosure), |
78 | ? | stripClosure(PClosure, Normalised, Main, Closure, Atomics). |
79 | | |
80 | | stripClosure(Unsorted, MainIn, MainOut, Result, Atomics) :- |
81 | | filter_parts(Ap,Tp,Next,Nextnot,Yest,Yestnot,Unsorted,Generic), |
82 | | append([Ap,Tp,Next,Nextnot,Yest,Yestnot,Generic], Sorted), |
83 | | append(Ap,Tp,Atomics), |
84 | ? | findref(MainIn,Sorted,MainOut), |
85 | ? | numeric_refs(Sorted,Sorted,Result). |
86 | | |
87 | | filter_parts(Ap,Tp,Next,Nextnot,Yest,Yestnot) --> |
88 | | filter_terms(Ap, ap(_)), |
89 | | filter_terms(Tp, action(_)), |
90 | | filter_terms(Nextnot, next(not(_))), |
91 | | filter_terms(Next, next(_)), |
92 | | filter_terms(Yestnot, yesterday(not(_))), |
93 | | filter_terms(Yest, yesterday(_)). |
94 | | |
95 | | filter_terms(Filtered,Pattern,In,Out) :- filter_terms2(In,Pattern,Filtered,Out). |
96 | | |
97 | | filter_terms2([],_,[],[]). |
98 | | filter_terms2([E|Rest],Term,A,B) :- |
99 | | ( copy_term(Term, E) -> |
100 | | A=[E|ARest],B=BRest |
101 | | ; |
102 | | A=ARest,B=[E|BRest]), |
103 | | filter_terms2(Rest,Term,ARest,BRest). |
104 | | |
105 | | numeric_refs([],_,[]). |
106 | | numeric_refs([F|Rest],L,[R|RRest]) :- |
107 | ? | xconv(F,L,R),numeric_refs(Rest,L,RRest). |
108 | | |
109 | | xconv(ap(AP),_,ap(AP)). |
110 | | xconv(action(TP),_,tp(TP)). |
111 | ? | xconv(next(not(X)),L,nextnot(R)) :- !,finduref(X,L,R),!. |
112 | ? | xconv(next(X),L,next(R)) :- finduref(X,L,R),!. |
113 | ? | xconv(yesterday(not(X)),L,yesterdaynot(R)) :- !,finduref(X,L,R),!. |
114 | ? | xconv(yesterday(X),L,yesterday(R)) :- finduref(X,L,R),!. |
115 | ? | xconv(or(A,B),L,or(RA,RB)) :- findref(A,L,RA),findref(B,L,RB). |
116 | | xconv(until(A,B),L,until(RA,RB,RN)) :- |
117 | ? | findref(A,L,RA), |
118 | ? | findref(B,L,RB), |
119 | ? | findref(next(until(A,B)),L,pos(RN)). |
120 | | xconv(since(A,B),L,since(RA,RB,RY)) :- |
121 | | findref(A,L,RA), |
122 | ? | findref(B,L,RB), |
123 | ? | findref(yesterday(since(A,B)),L,pos(RY)). |
124 | ? | findref(not(F),L,neg(N)) :- !,finduref(F,L,N). |
125 | ? | findref(F,L,pos(N)) :- finduref(F,L,N). |
126 | | |
127 | | finduref(true,_,-1) :- !. |
128 | ? | finduref(F,L,N) :- nth0(N,L,F). |
129 | | |
130 | | |
131 | | %******************************************************************************* |
132 | | % Closure of a formula |
133 | | |
134 | | % the positive closure has only the positive (without leading nots) |
135 | | % formulas of the closure. |
136 | | % Also its elements are sorted |
137 | | positive_closure(F,NDPositive) :- |
138 | | closure(F,Closure), |
139 | | sort_closure(Closure,Sorted), |
140 | | remove_negatives(Sorted,Positive), |
141 | | remove_duplicates(Positive,NDPositive). |
142 | | |
143 | | remove_duplicates(In,Out) :- remove_duplicates2(In,[],Out). |
144 | | remove_duplicates2([],_,[]). |
145 | | remove_duplicates2([E|Rest],Before,Out) :- |
146 | | ( member(E,Before) -> |
147 | | !,remove_duplicates2(Rest,Before,Out) |
148 | | ; |
149 | | Out=[E|DRest],remove_duplicates2(Rest,[E|Before],DRest)). |
150 | | |
151 | | closure(F,C) :- closure([F],[],C). |
152 | | |
153 | | closure([],Acc,Acc). |
154 | | closure([true|Rest],Acc,Closure) :- |
155 | | !,closure(Rest,Acc,Closure). |
156 | | closure([F|Rest],Acc,Closure) :- |
157 | | findall(G,dclosure(F,G),Gen), |
158 | | filternew(Gen,Acc,Rest,New), |
159 | | append(Rest,New,Next), |
160 | | closure(Next,[F|Acc],Closure). |
161 | | |
162 | | dclosure(F,Neg) :- negate(F,Neg). |
163 | | dclosure(or(F,_),F). |
164 | | dclosure(or(_,F),F). |
165 | | dclosure(next(F),F). |
166 | | dclosure(yesterday(F),F). |
167 | | dclosure(not(next(F)),next(Neg)) :- negate(F,Neg). |
168 | | dclosure(not(yesterday(F)),yesterday(Neg)) :- negate(F,Neg). |
169 | | dclosure(until(F,_),F). |
170 | | dclosure(until(_,F),F). |
171 | | dclosure(until(A,B),next(until(A,B))). |
172 | | dclosure(since(F,_),F). |
173 | | dclosure(since(_,F),F). |
174 | | dclosure(since(A,B),yesterday(since(A,B))). |
175 | | |
176 | | negate(not(F),F) :- !. |
177 | | negate(F,not(F)). |
178 | | |
179 | | filternew([],_,_,[]). |
180 | | filternew([F|Rest],Ex1,Ex2,Result) :- |
181 | ? | (\+ member(F,Ex1), \+ member(F,Ex2) |
182 | | -> Result = [F|FRest] |
183 | | ; Result = FRest), |
184 | | filternew(Rest,Ex1,Ex2,FRest). |
185 | | |
186 | | remove_negatives([],[]). |
187 | | remove_negatives([F|Rest],Positive) :- |
188 | | (F = not(_) |
189 | | -> !,Positive = PRest |
190 | | ; Positive = [F|PRest]), |
191 | | remove_negatives(Rest,PRest). |
192 | | |
193 | | sort_closure(In,Out) :- sort_closure2(In,[],Out). |
194 | | sort_closure2([],_,[]) :- !. |
195 | | sort_closure2(Unsorted,Sorted,[F|RestSorted]) :- |
196 | | select_formula(Unsorted,Sorted,F,URest), |
197 | | sort_closure2(URest,[F|Sorted],RestSorted). |
198 | | |
199 | | select_formula([F|FRest],Sorted,F,FRest) :- |
200 | | deps(F,Deps), |
201 | | subset(Deps,Sorted),!. |
202 | | select_formula([F|FRest],Sorted,S,[F|Rest]) :- |
203 | | select_formula(FRest,Sorted,S,Rest). |
204 | | |
205 | | deps(true,[]). |
206 | | deps(not(F),[F]). |
207 | | deps(ap(_),[]). |
208 | | deps(or(A,B),[A,B]). |
209 | | deps(next(F),D) :- (F=not(N) -> D=[next(N)]; D=[]). |
210 | | deps(yesterday(F),D) :- (F=not(N) -> D=[yesterday(N)]; D=[]). |
211 | | deps(until(A,B),[A,B,next(until(A,B))]). |
212 | | deps(since(A,B),[A,B,yesterday(since(A,B))]). |
213 | | deps(action(_),[]). |
214 | | |
215 | | % subset(A,B): A is a subset of B |
216 | | subset([],_). |
217 | | subset([F|Rest],Superset) :- |
218 | ? | (F=true;member(F,Superset)),!,subset(Rest,Superset). |
219 | | |
220 | | %******************************************************************************* |
221 | | % normalise a formula (LTL) |
222 | | |
223 | | % part I: translating syntatic sugar |
224 | | ltl_norm(false,not(true)). |
225 | | ltl_norm(and(A,B),N) :- ltl_norm(not(or(not(A),not(B))),N). |
226 | | ltl_norm(implies(A,B),N) :- ltl_norm(or(not(A),B),N). |
227 | | ltl_norm(equivalent(A,B),N) :- ltl_norm(and(implies(A,B),implies(B,A)),N). |
228 | | ltl_norm(finally(F),N) :- ltl_norm(until(true,F),N). |
229 | | ltl_norm(globally(F),N) :- ltl_norm(not(finally(not(F))),N). |
230 | | ltl_norm(weakuntil(A,B),N) :- ltl_norm(or(globally(A),until(A,B)),N). |
231 | | ltl_norm(release(A,B),N) :- ltl_norm(not(until(not(A),not(B))),N). |
232 | | ltl_norm(once(F),N) :- ltl_norm(since(true,F),N). |
233 | | ltl_norm(historically(F),N) :- ltl_norm(not(once(not(F))),N). |
234 | | ltl_norm(trigger(A,B),N) :- ltl_norm(not(since(not(A),not(B))),N). |
235 | | %ltl_norm(forall(ID,LHS,N),N) :- ... |
236 | | %ltl_norm(exists(ID,LHS,N),N) :- ... |
237 | | |
238 | | % part II: mostly normalising arguments recursivly, removing not(not(...)) |
239 | | ltl_norm(true,true). |
240 | | ltl_norm(next(F),next(NF)) :- ltl_norm(F,NF). |
241 | | ltl_norm(yesterday(F),yesterday(NF)) :- ltl_norm(F,NF). |
242 | | ltl_norm(or(A,B),or(NA,NB)) :- |
243 | | ltl_norm(A,NA),ltl_norm(B,NB). |
244 | | ltl_norm(not(F),N) :- ltl_norm(F,N1), (N1=not(P) -> N=P; N=not(N1)). |
245 | | ltl_norm(ap(X),N) :- |
246 | | (X=available(F) -> |
247 | | ltl_norm(available(F),N) |
248 | | ; N = ap(X) |
249 | | ). |
250 | | ltl_norm(until(A,B),until(NA,NB)) :- |
251 | | ltl_norm(A,NA),ltl_norm(B,NB). |
252 | | ltl_norm(since(A,B),since(NA,NB)) :- |
253 | | ltl_norm(A,NA),ltl_norm(B,NB). |
254 | | ltl_norm(action(Op),action(Op)). |
255 | | |
256 | | % part III (fairness) |
257 | | % ignore fairness assumptions, they will be given later as an additional argument to the ltlc_modelcheck function |
258 | | ltl_norm(fairnessimplication(_Assumptions,F),NF) :- |
259 | | ltl_norm(F,NF). |
260 | | |
261 | | % Normalising Gavin Lowe's available operator |
262 | | % available a ----> [tau] U ((e(tau) & not [tau]) or (e(a) & not e(tau))) |
263 | | % Note: It works only for CSP !!! |
264 | | ltl_norm(available(F),N) :- |
265 | | ltl_norm( |
266 | | until( action(csp(tau,_,[])), |
267 | | or(and(ap(enabled(csp(tau,_,[]))),not(action(csp(tau,_,[])))), |
268 | | and(ap(enabled(F)),not(ap(enabled(csp(tau,_,[]))))) |
269 | | ) |
270 | | ),N). |