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