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