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(ltl_translate,[pp_ltl_formula/2, pp_formulas/2, pp_ap/2, pp_tp/2, get_ltl_sub_formulas/3]).
6
7		/* SICSTUS Libraries */
8		:- use_module(library(lists)).
9		%% :- use_module(library(codesio)).
10		%% :- use_module(library(terms)).
11
12		/* ProB Libraries */
13		%% :- use_module(probsrc(error_manager)).
14		%% :- use_module(probsrc(debug)).
15		:- use_module(probsrc(self_check)).
16		:- use_module(probsrc(specfile),[csp_with_bz_mode/0]).
17		:- use_module(probsrc(tools),[ajoin/2]).
18		:- use_module(probsrc(translate), [translate_bexpression/2,translate_event/2]).
19		:- use_module(probsrc(state_space),[transition/4]).
20		:- use_module(library(codesio),[write_to_codes/2]).
21
22		:- use_module(probsrc(module_information),[module_info/2]).
23		:- module_info(group,ltl).
24		:- module_info(description,'This module provides utility predicates for pretty-printing LTL and CTL formulae.').
25
26		pp_ltl_formula(Formula,Text) :-
27		pp_ltl(Formula,Atoms,[]),
28		ajoin(Atoms,Text).
29
30		/* Pretty printer predicates */
31		:- public pp_op/2.
32		pp_op(Id,PP) :-
33		transition(_Src,Action,Id,_Dst),!,
34		translate_event(Action,PP).
35
36		pp_formulas([],[]).
37		pp_formulas([ApTp|Rest],[PP|PPrest]) :-
38		(pp_formula(ApTp,PP) -> true ; PP = '???'),
39		pp_formulas(Rest,PPrest).
40		pp_formula(ap(AP),ap(PP)) :-
41		pp_ap(AP,PP).
42		pp_formula(action(AP),tp(PP)) :-
43		pp_tp(AP,PP).
44
45		pp_ap(bpred(B),PP) :- !,
46		translate_bexpression(B,PP1),
47		ajoin(['{',PP1,'}'],PP).
48		pp_ap(xtl_predicate_check(P),PP) :- atom(P),!,
49		ajoin(['{',P,'}'],PP).
50		pp_ap(enabled(TP),PP) :- !,
51		pp_tp2(TP,TPP),
52		ajoin(['e(',TPP,')'],PP).
53		pp_ap(available(TP),PP) :- !, % TO DO: check_ap currently has no rule for Av(.) / available Operator !!
54		% Was introduced for David Williams.
55		% Only relevant for CSP and rewritten to [tau] U (e(tau) & not [tau]) or (e(a) & not e(tau))).
56		% This is done in the Prolog module with the C interface for LTL.
57		pp_tp2(TP,TPP),
58		ajoin(['Av(',TPP,')'],PP).
59		pp_ap(weak_fair(TP),PP) :- !,
60		pp_tp2(TP,TPP),
61		ajoin(['WF(',TPP,')'],PP).
62		pp_ap(strong_fair(TP),PP) :- !,
63		pp_tp2(TP,TPP),
64		ajoin(['SF(',TPP,')'],PP).
65		pp_ap(dlk(L),PP) :- !,
66		maplist(pp_tp2,L,S),
67		tools: ajoin_with_sep(S,',',SText),
68		ajoin(['deadlock(',SText,')'],PP).
69		pp_ap(ctrl(L),PP) :- !,
70		maplist(pp_tp2,L,S),
71		tools: ajoin_with_sep(S,',',SText),
72		ajoin(['controller(',SText,')'],PP).
73		pp_ap(det(L),PP) :- !,
74		maplist(pp_tp2,L,S),
75		tools: ajoin_with_sep(S,',',SText),
76		ajoin(['deterministic(',SText,')'],PP).
77		pp_ap(Expr,PP) :-
78		write_to_codes(Expr,Codes),
79		atom_codes(PP,Codes).
80
81		pp_tp(change_expr(Comparator,TE),PP) :-
82		pp_comp(Comparator,PPC), !,
83		translate_bexpression(TE,TPP),
84		ajoin([PPC,'({',TPP,'})'],PP).
85		pp_tp(before_after(TE),PP) :-
86		!,
87		translate_bexpression(TE,TPP),
88		ajoin(['BA({',TPP,'})'],PP).
89		pp_tp(T,PP) :-
90		pp_tp2(T,PP1),
91		ajoin(['[',PP1,']'],PP).
92		pp_tp2(btrans(event(Name)),Name) :- !.
93		pp_tp2(btrans(event(Name,Predicate,_)),PP) :- !,
94		translate_bexpression(Predicate,PP1),
95		ajoin([Name,' | ',PP1],PP).
96		pp_tp2(csp(tau,_Arity,[]),PP) :- !, PP = tau.
97		pp_tp2(csp(tick,_Arity,[]),PP) :- !, PP = tick.
98		pp_tp2(xtl(Op,0,[]),PP) :- !, PP = Op.
99		pp_tp2(xtl(Op,_Arity,PatternArgs),PP) :- !, Term =.. [Op|PatternArgs], pp_tp2(Term,PP).
100		pp_tp2(Action,PP) :-
101		translate_action(Action,PP),!.
102		pp_tp2(F,AF) :-
103		(translate: translate_event(F,AF) -> true; AF='???').
104
105		pp_comp(eq,unchanged).
106		pp_comp(neq,changed).
107		pp_comp(lt,increasing).
108		pp_comp(gt,decreasing).
109
110		translate_action(bop(Name,_NumberArgs,_NumberResults,ArgPatterns,_ResPatterns),Transition) :- !,
111		maplist(get_arg,ArgPatterns,ArgPatterns1),
112		maplist(translate_bexpression,ArgPatterns1,PPArgPatterns),
113		Op =.. [Name|PPArgPatterns],
114		Transition = Op.
115		/* ( NumberResults == 0 ->
116		Transition = Op
117		;
118		maplist(translate:translate_bexpression,ResPatterns,PPResPatterns),
119		Transition = '-->'(Op,PPResPatterns)
120		).
121		*/
122		translate_action(csp(Channel,_Arity,Args),PP) :-
123		(csp_with_bz_mode ->
124		% in this mode we need to remove 'CSP:'
125		translate: translate_event2(io(Args,Channel,_SPan),[_|S],[])
126		;
127		translate: translate_event2(io(Args,Channel,_SPan),S,[])
128		), ajoin(S,PP).
129
130		get_arg(N/Arg,Arg) :- nonvar(N),!.
131		get_arg(Arg,Arg).
132
133		/* Tests for pp_ltl_formula/2 */
134
135		:- assert_must_succeed((pp_ltl_formula(implies(globally(finally(until(true,false))),true),Text),
136		Text = '(G (F ((true U false))) => true)')).
137
138		:- assert_must_succeed((pp_ltl_formula(historically(not(release(yesterday(sink),next(deadlock)))),Text),
139		Text = 'H (not((Y (sink) R X (deadlock))))')).
140
141		:- assert_must_succeed((
142		pp_ltl_formula(implies(
143		ap(enabled(btrans(event('A')))),
144		or(weakuntil(
145		ap(bpred(equal(identifier(op('x')),integer(1)))),
146		ap(bpred(equal(identifier(op('x')),integer(2)))) ),
147		finally(action(btrans(event('A')))))),Text),
148		Text = '(e(A) => (({x = 1} W {x = 2}) or F ([A])))')).
149
150		:- assert_must_succeed((
151		pp_ltl_formula(implies(
152		current,
153		and(once(ap(bpred(equal(identifier(op('x')),integer(1))))),
154		action(btrans(event('A',equal(identifier(op('x')),integer(2)),_))))),Text),
155		Text = '(current => (O ({x = 1}) & [A | x = 2]))')).
156
157		:- assert_must_succeed((
158		pp_ltl_formula(fairnessimplication(
159		and(strongassumptions(and(ap(strong_fair(btrans(event('A')))),
160		ap(strong_fair(btrans(event('B')))))),
161		weakassumptions(or(ap(weak_fair(btrans(event('A')))),
162		ap(weak_fair(btrans(event('B'))))))),
163		true),Text),
164		Text = '(((SF(A) & SF(B))) & (WF(A) or WF(B)) => true)')).
165
166		:- assert_must_succeed((
167		pp_ltl_formula(fairnessimplication(
168		and(weakassumptions(and(ap(weak_fair(btrans(event('A')))),
169		ap(weak_fair(btrans(event('B')))))),
170		strongassumptions(or(ap(strong_fair(btrans(event('A')))),
171		ap(strong_fair(btrans(event('B'))))))),
172		true),Text),
173		Text = '(((WF(A) & WF(B))) & (SF(A) or SF(B)) => true)')).
174
175		:- assert_must_succeed((
176		pp_ltl_formula(globally(finally(ap(available(btrans(event('A')))))),Text),
177		Text = 'G (F (Av(A)))')).
178
179		/* Simple Pretty Printer for LTL/CTL Formulas */
180
181		pp_ltl(true,['true'|S],S).
182		pp_ltl(false,['false'|S],S).
183		pp_ltl(deadlock,['deadlock'|S],S).
184		pp_ltl(sink,['sink'|S],S).
185		pp_ltl(goal,['goal'|S],S).
186		pp_ltl(state_error,['error'|S],S).
187		pp_ltl(det_output,['det_output'|S],S).
188		pp_ltl(current,['current'|S],S).
189		pp_ltl(globally(F),['G ('| S],T) :- !, pp_ltl(F,S,[')'|T]).
190		pp_ltl(finally(F),['F ('| S],T) :- !, pp_ltl(F,S,[')'|T]).
191		pp_ltl(next(F),['X ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
192		pp_ltl(yesterday(F),['Y ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
193		pp_ltl(since(F,G),['('|S],T) :- !,
194		pp_ltl(F,S,[' S '| S1]),
195		pp_ltl(G,S1,[')'|T]).
196		pp_ltl(once(F),['O ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
197		pp_ltl(historically(F),['H ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
198		pp_ltl(until(F,G),['('|S],T) :- !,
199		pp_ltl(F,S,[' U '| S1]),
200		pp_ltl(G,S1,[')'|T]).
201		pp_ltl(weakuntil(F,G),['('|S],T) :- !,
202		pp_ltl(F,S,[' W '| S1]),
203		pp_ltl(G,S1,[')'|T]).
204		pp_ltl(release(F,G),['('|S],T) :- !,
205		pp_ltl(F,S,[' R '| S1]),
206		pp_ltl(G,S1,[')'|T]).
207		pp_ltl(implies(F,G),['('|S],T) :- !,
208		pp_ltl(F,S,[' => '| S1]),
209		pp_ltl(G,S1,[')'|T]).
210		pp_ltl(equivalent(F,G),['('|S],T) :- !,
211		pp_ltl(F,S,[' <=> '| S1]),
212		pp_ltl(G,S1,[')'|T]).
213		pp_ltl(fairnessimplication(FairAssump,Formula),['('|S],T) :- !,
214		pp_ltl_fairness(FairAssump,S,[' => '| S1]),
215		pp_ltl(Formula,S1,[')'|T]).
216		pp_ltl(or(F,G),['('|S],T) :- !,
217		pp_ltl(F,S,[' or '| S1]),
218		pp_ltl(G,S1,[')'|T]).
219		pp_ltl(and(F,G),['('|S],T) :- !,
220		pp_ltl(F,S,[' & '| S1]),
221		pp_ltl(G,S1,[')'|T]).
222		pp_ltl(not(F),['not('| S],T) :- !, pp_ltl(F,S,[')'|T]).
223		pp_ltl(ap(AP),[Pred|S],S) :- !, pp_ap(AP,Pred).
224		pp_ltl(action(A),[Action|S],S) :- !, pp_tp(A,Action).
225
226		/* Pretty Print CTL Part */
227		pp_ltl(ena(F),['EX ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
228		pp_ltl(en(F), ['EX ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
229		pp_ltl(an(F), ['AX ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
230		pp_ltl(eg(F), ['EG ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
231		pp_ltl(ef(F), ['EF ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
232		pp_ltl(ag(F), ['AG ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
233		pp_ltl(af(F), ['AF ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
234		pp_ltl(eu(F,G), ['( E '|S],T) :- !,
235		pp_ltl(F,S,[' U '|S1]),
236		pp_ltl(G,S1,[')'|T]).
237
238		/* Pretty Print Fairness Assumptions */
239		pp_ltl_fairness(strongassumptions(F),S1,T) :- !,
240		(F=all ->
241		S1 = ['SEF'|S], T = S
242		;
243		S1 = ['('|S], pp_ltl_fairness1(F,S,[')'|T])
244		).
245		pp_ltl_fairness(weakassumptions(F),S1,T) :- !,
246		(F=all ->
247		S1 = ['WEF'|S], T = S
248		;
249		S1 = ['('|S], pp_ltl_fairness1(F,S,[')'|T])
250		).
251		pp_ltl_fairness(and(F,G),S,T) :- !,
252		pp_ltl_fairness(F,S,[' & '|S1]),
253		pp_ltl_fairness(G,S1,T).
254
255		pp_ltl_fairness1(and(F,G),['('|S],T) :- !,
256		pp_ltl_fairness1(F,S,[' & '|S1]),
257		pp_ltl_fairness1(G,S1,[')'|T]).
258		pp_ltl_fairness1(or(F,G),S,T) :- !,
259		pp_ltl_fairness1(F,S,[' or '|S1]),
260		pp_ltl_fairness1(G,S1,T).
261		pp_ltl_fairness1(ap(AP),[Pred|S],S) :- !,
262		pp_ap(AP,Pred).
263
264
265
266
267		% TODO: extend and possibly use in pp_ltl above
268		get_ltl_sub_formulas(and(A,B),'&',[A,B]).
269		get_ltl_sub_formulas(or(A,B),'or',[A,B]).
270		get_ltl_sub_formulas(implies(A,B),'=>',[A,B]).
271		get_ltl_sub_formulas(equivalent(A,B),'<=>',[A,B]).
272		get_ltl_sub_formulas(until(A,B),'U',[A,B]).
273		get_ltl_sub_formulas(weakuntil(A,B),'W',[A,B]).
274		get_ltl_sub_formulas(release(A,B),'R',[A,B]).
275		get_ltl_sub_formulas(since(A,B),'S',[A,B]).
276		get_ltl_sub_formulas(globally(A),'G',[A]).
277		get_ltl_sub_formulas(finally(A),'F',[A]).
278		get_ltl_sub_formulas(not(A),'not',[A]).
279		get_ltl_sub_formulas(next(A),'X',[A]).
280		get_ltl_sub_formulas(yesterday(A),'Y',[A]).
281		get_ltl_sub_formulas(historically(A),'H',[A]).
282		get_ltl_sub_formulas(once(A),'O',[A]).