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