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