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