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