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(operation_call(Action),OpCall) :-
93		translate_action(Action,PP),!, ajoin(['calls(',PP,')'],OpCall).
94		pp_tp2(btrans(event(Name)),Name) :- !.
95		pp_tp2(btrans(event(Name,Predicate,_)),PP) :- !,
96		translate_bexpression(Predicate,PP1),
97		ajoin([Name,' | ',PP1],PP).
98		pp_tp2(csp(tau,_Arity,[]),PP) :- !, PP = tau.
99		pp_tp2(csp(tick,_Arity,[]),PP) :- !, PP = tick.
100		pp_tp2(xtl(Op,0,[]),PP) :- !, PP = Op.
101		pp_tp2(xtl(Op,_Arity,PatternArgs),PP) :- !, Term =.. [Op|PatternArgs], pp_tp2(Term,PP).
102		pp_tp2(Action,PP) :-
103		translate_action(Action,PP),!.
104		pp_tp2(F,AF) :-
105		(translate: translate_event(F,AF) -> true; AF='???').
106
107		pp_comp(eq,unchanged).
108		pp_comp(neq,changed).
109		pp_comp(lt,increasing).
110		pp_comp(gt,decreasing).
111
112		translate_action(bop(Name,_NumberArgs,_NumberResults,ArgPatterns,_ResPatterns),Transition) :- !,
113		maplist(get_arg,ArgPatterns,ArgPatterns1),
114		maplist(translate_bexpression,ArgPatterns1,PPArgPatterns),
115		Op =.. [Name|PPArgPatterns],
116		Transition = Op.
117		/* ( NumberResults == 0 ->
118		Transition = Op
119		;
120		maplist(translate:translate_bexpression,ResPatterns,PPResPatterns),
121		Transition = '-->'(Op,PPResPatterns)
122		).
123		*/
124		translate_action(csp(Channel,_Arity,Args),PP) :-
125		(csp_with_bz_mode ->
126		% in this mode we need to remove 'CSP:'
127		translate: translate_event2(io(Args,Channel,_SPan),[_|S],[])
128		;
129		translate: translate_event2(io(Args,Channel,_SPan),S,[])
130		), ajoin(S,PP).
131
132		get_arg(N/Arg,Arg) :- nonvar(N),!.
133		get_arg(Arg,Arg).
134
135		/* Tests for pp_ltl_formula/2 */
136
137		:- assert_must_succeed((pp_ltl_formula(implies(globally(finally(until(true,false))),true),Text),
138		Text = '(G (F ((true U false))) => true)')).
139
140		:- assert_must_succeed((pp_ltl_formula(historically(not(release(yesterday(sink),next(deadlock)))),Text),
141		Text = 'H (not((Y (sink) R X (deadlock))))')).
142
143		:- assert_must_succeed((
144		pp_ltl_formula(implies(
145		ap(enabled(btrans(event('A')))),
146		or(weakuntil(
147		ap(bpred(equal(identifier(op('x')),integer(1)))),
148		ap(bpred(equal(identifier(op('x')),integer(2)))) ),
149		finally(action(btrans(event('A')))))),Text),
150		Text = '(e(A) => (({x = 1} W {x = 2}) or F ([A])))')).
151
152		:- assert_must_succeed((
153		pp_ltl_formula(implies(
154		current,
155		and(once(ap(bpred(equal(identifier(op('x')),integer(1))))),
156		action(btrans(event('A',equal(identifier(op('x')),integer(2)),_))))),Text),
157		Text = '(current => (O ({x = 1}) & [A | x = 2]))')).
158
159		:- assert_must_succeed((
160		pp_ltl_formula(fairnessimplication(
161		and(strongassumptions(and(ap(strong_fair(btrans(event('A')))),
162		ap(strong_fair(btrans(event('B')))))),
163		weakassumptions(or(ap(weak_fair(btrans(event('A')))),
164		ap(weak_fair(btrans(event('B'))))))),
165		true),Text),
166		Text = '(((SF(A) & SF(B))) & (WF(A) or WF(B)) => true)')).
167
168		:- assert_must_succeed((
169		pp_ltl_formula(fairnessimplication(
170		and(weakassumptions(and(ap(weak_fair(btrans(event('A')))),
171		ap(weak_fair(btrans(event('B')))))),
172		strongassumptions(or(ap(strong_fair(btrans(event('A')))),
173		ap(strong_fair(btrans(event('B'))))))),
174		true),Text),
175		Text = '(((WF(A) & WF(B))) & (SF(A) or SF(B)) => true)')).
176
177		:- assert_must_succeed((
178		pp_ltl_formula(globally(finally(ap(available(btrans(event('A')))))),Text),
179		Text = 'G (F (Av(A)))')).
180
181		/* Simple Pretty Printer for LTL/CTL Formulas */
182
183		pp_ltl(true,['true'|S],S).
184		pp_ltl(false,['false'|S],S).
185		pp_ltl(deadlock,['deadlock'|S],S).
186		pp_ltl(sink,['sink'|S],S).
187		pp_ltl(goal,['goal'|S],S).
188		pp_ltl(state_error,['error'|S],S).
189		pp_ltl(det_output,['det_output'|S],S).
190		pp_ltl(current,['current'|S],S).
191		pp_ltl(globally(F),['G ('| S],T) :- !, pp_ltl(F,S,[')'|T]).
192		pp_ltl(finally(F),['F ('| S],T) :- !, pp_ltl(F,S,[')'|T]).
193		pp_ltl(next(F),['X ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
194		pp_ltl(yesterday(F),['Y ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
195		pp_ltl(since(F,G),['('|S],T) :- !,
196		pp_ltl(F,S,[' S '| S1]),
197		pp_ltl(G,S1,[')'|T]).
198		pp_ltl(once(F),['O ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
199		pp_ltl(historically(F),['H ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
200		pp_ltl(until(F,G),['('|S],T) :- !,
201		pp_ltl(F,S,[' U '| S1]),
202		pp_ltl(G,S1,[')'|T]).
203		pp_ltl(weakuntil(F,G),['('|S],T) :- !,
204		pp_ltl(F,S,[' W '| S1]),
205		pp_ltl(G,S1,[')'|T]).
206		pp_ltl(release(F,G),['('|S],T) :- !,
207		pp_ltl(F,S,[' R '| S1]),
208		pp_ltl(G,S1,[')'|T]).
209		pp_ltl(implies(F,G),['('|S],T) :- !,
210		pp_ltl(F,S,[' => '| S1]),
211		pp_ltl(G,S1,[')'|T]).
212		pp_ltl(equivalent(F,G),['('|S],T) :- !,
213		pp_ltl(F,S,[' <=> '| S1]),
214		pp_ltl(G,S1,[')'|T]).
215		pp_ltl(fairnessimplication(FairAssump,Formula),['('|S],T) :- !,
216		pp_ltl_fairness(FairAssump,S,[' => '| S1]),
217		pp_ltl(Formula,S1,[')'|T]).
218		pp_ltl(or(F,G),['('|S],T) :- !,
219		pp_ltl(F,S,[' or '| S1]),
220		pp_ltl(G,S1,[')'|T]).
221		pp_ltl(and(F,G),['('|S],T) :- !,
222		pp_ltl(F,S,[' & '| S1]),
223		pp_ltl(G,S1,[')'|T]).
224		pp_ltl(not(F),['not('| S],T) :- !, pp_ltl(F,S,[')'|T]).
225		pp_ltl(ap(AP),[Pred|S],S) :- !, pp_ap(AP,Pred).
226		pp_ltl(action(A),[Action|S],S) :- !, pp_tp(A,Action).
227
228		/* Pretty Print CTL Part */
229		pp_ltl(ena(F),['EX ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
230		pp_ltl(en(F), ['EX ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
231		pp_ltl(an(F), ['AX ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
232		pp_ltl(eg(F), ['EG ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
233		pp_ltl(ef(F), ['EF ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
234		pp_ltl(ag(F), ['AG ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
235		pp_ltl(af(F), ['AF ('|S],T) :- !, pp_ltl(F,S,[')'|T]).
236		pp_ltl(eu(F,G), ['( E '|S],T) :- !,
237		pp_ltl(F,S,[' U '|S1]),
238		pp_ltl(G,S1,[')'|T]).
239
240		/* Pretty Print Fairness Assumptions */
241		pp_ltl_fairness(strongassumptions(F),S1,T) :- !,
242		(F=all ->
243		S1 = ['SEF'|S], T = S
244		;
245		S1 = ['('|S], pp_ltl_fairness1(F,S,[')'|T])
246		).
247		pp_ltl_fairness(weakassumptions(F),S1,T) :- !,
248		(F=all ->
249		S1 = ['WEF'|S], T = S
250		;
251		S1 = ['('|S], pp_ltl_fairness1(F,S,[')'|T])
252		).
253		pp_ltl_fairness(and(F,G),S,T) :- !,
254		pp_ltl_fairness(F,S,[' & '|S1]),
255		pp_ltl_fairness(G,S1,T).
256
257		pp_ltl_fairness1(and(F,G),['('|S],T) :- !,
258		pp_ltl_fairness1(F,S,[' & '|S1]),
259		pp_ltl_fairness1(G,S1,[')'|T]).
260		pp_ltl_fairness1(or(F,G),S,T) :- !,
261		pp_ltl_fairness1(F,S,[' or '|S1]),
262		pp_ltl_fairness1(G,S1,T).
263		pp_ltl_fairness1(ap(AP),[Pred|S],S) :- !,
264		pp_ap(AP,Pred).
265
266
267
268
269		% TODO: extend and possibly use in pp_ltl above
270		get_ltl_sub_formulas(and(A,B),'&',[A,B]).
271		get_ltl_sub_formulas(or(A,B),'or',[A,B]).
272		get_ltl_sub_formulas(implies(A,B),'=>',[A,B]).
273		get_ltl_sub_formulas(equivalent(A,B),'<=>',[A,B]).
274		get_ltl_sub_formulas(until(A,B),'U',[A,B]).
275		get_ltl_sub_formulas(weakuntil(A,B),'W',[A,B]).
276		get_ltl_sub_formulas(release(A,B),'R',[A,B]).
277		get_ltl_sub_formulas(since(A,B),'S',[A,B]).
278		get_ltl_sub_formulas(globally(A),'G',[A]).
279		get_ltl_sub_formulas(finally(A),'F',[A]).
280		get_ltl_sub_formulas(not(A),'not',[A]).
281		get_ltl_sub_formulas(next(A),'X',[A]).
282		get_ltl_sub_formulas(yesterday(A),'Y',[A]).
283		get_ltl_sub_formulas(historically(A),'H',[A]).
284		get_ltl_sub_formulas(once(A),'O',[A]).