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