1 | | % (c) 2014-2022 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_safety,[is_safety_property/2, safety_property_can_be_encoded_directly/1, |
6 | | ltl_mc_safety_property/3, |
7 | | is_ltl2ba_tool_installed/0, |
8 | | aut_transition/3, aut_final_state/1, aut_initial_state/1, |
9 | | tps_occurring/0, ltl_formula_uses_tps/1]). |
10 | | |
11 | | /* SICSTUS Libraries */ |
12 | | :- use_module(library(lists)). |
13 | | :- use_module(library(codesio)). |
14 | | :- use_module(library(terms)). |
15 | | :- use_module(library(file_systems)). |
16 | | |
17 | | /* ProB Libraries */ |
18 | | :- use_module(probsrc(tools),[ajoin/2,host_platform/1]). |
19 | | :- use_module(probsrc(error_manager)). |
20 | | %% :- use_module(probsrc(debug)). |
21 | | :- use_module(probsrc(self_check)). |
22 | | %:- use_module(probsrc(system_call),[system_call/5]). |
23 | | :- use_module(probsrc(debug),[debug_println/2,debug_mode/1, debug_format/3]). |
24 | | :- use_module(probsrc(bsyntaxtree),[create_negation/2]). |
25 | | |
26 | | :- use_module(extension('ltl2ba/ltl2ba')). |
27 | | |
28 | | /* ProB LTL Model Checker Modules */ |
29 | | :- use_module(probltlsrc(safety_mc),[start_mc_safety_property/3]). |
30 | | :- use_module(probltlsrc(ltl_translate),[pp_ap/2,pp_tp/2]). |
31 | | |
32 | | :- use_module(probsrc(module_information),[module_info/2]). |
33 | | :- module_info(group,ltl). |
34 | | :- module_info(description,'This module provides predicates for checking whether an LTL formula is a safety property.'). |
35 | | |
36 | | :- dynamic ap_representation/2, tp_representation/2, tps_occurring/0. |
37 | | |
38 | | :- dynamic aut_transition/3, aut_final_state/1, aut_initial_state/1. |
39 | | |
40 | | clear_automaton_facts :- |
41 | | retractall(aut_transition(_,_,_)), |
42 | | retractall(aut_initial_state(_)), |
43 | | retractall(aut_final_state(_)). |
44 | | |
45 | | aut_state(S) :- aut_initial_state(S). |
46 | | aut_state(S) :- aut_final_state(S). |
47 | | % Note : these are not all the states !! |
48 | | |
49 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
50 | | %%%%%%%%%%% Checking whether an LTL property represents a safety property %%%%%%%%%% |
51 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
52 | | % The predicates check whether the parsed LTL property represents a safety property |
53 | | % by checking the syntactical structure of the formula. |
54 | | % The idea is borrowed from the following theorem from the paper |
55 | | % "Safety, Liveness and Fairness in Temporal Logic" of A. Sistla: |
56 | | %% THEOREM: Every propositional formula is a safety formula and if f,g are safety formulae, |
57 | | %% then so are f & g, f or g, X f, f W g, and G f, where 'W' is the weak-until operator. |
58 | | % |
59 | | % Note that the checked formula should be a positive formula. An LTL formula is said to |
60 | | % be a positive if none of the temporal operators appears in the scope of 'not'. |
61 | | |
62 | | % Testing various properties for being safety or liveness. Some of |
63 | | % the unit tests here represent examples from the paper mentioned above. |
64 | | % Note that the first argument of is_safety_property/2 should be negated, as |
65 | | % this is done after negating the original property that should be model checked (see select_ltl_mode/4 in ltl.pl) |
66 | | :- assert_must_succeed((F = ap(p), |
67 | | is_safety_property(not(F),_NF))). |
68 | | :- assert_must_succeed((F = globally(deadlock), |
69 | | is_safety_property(not(F),_NF))). |
70 | | :- assert_must_succeed((F = weakuntil(not(ap(alloc)),ap(request)), |
71 | | is_safety_property(not(F),_NF))). |
72 | | :- assert_must_succeed((F = and(weakuntil(not(ap(alloc)),ap(request)), |
73 | | globally(implies(ap(alloc),next(weakuntil(not(ap(alloc)),ap(request)))))), |
74 | | is_safety_property(not(F),_NF))). |
75 | | :- assert_must_succeed((F = globally(implies(not(ap(request)),or(ap(alloc),or(next(ap(alloc)),next(next(ap(alloc))))))), |
76 | | is_safety_property(not(F),_NF))). |
77 | | :- assert_must_succeed((F = globally(or(not(ap(p)),globally(not(ap(p))))), |
78 | | is_safety_property(not(F),_NF))). |
79 | | :- assert_must_succeed((F = not(until(ap(p1),until(ap(p2),ap(p3)))), |
80 | | is_safety_property(not(F),_NF))). |
81 | | :- assert_must_succeed((F = not(until(ap(p1),until(ap(p2),until(ap(p3),ap(p4))))), |
82 | | is_safety_property(not(F),_NF))). |
83 | | :- assert_must_succeed((F = not(until(ap(p1),until(ap(p2),until(ap(p3),until(ap(p4),until(ap(p5),until(ap(p6),ap(p7)))))))), |
84 | | is_safety_property(not(F),_NF))). |
85 | | :- assert_must_succeed((F = not(not(globally(deadlock))), |
86 | | is_safety_property(not(F),_NF))). |
87 | | :- assert_must_succeed((F = globally(or(ap(p),and(next(ap(q)),not(next(ap(q)))))), |
88 | | is_safety_property(not(F),_NF))). |
89 | | :- assert_must_succeed((F = and(globally(or(ap(p),next(globally(ap(q))))),globally(or(ap(p),next(globally(not(ap(q))))))), |
90 | | is_safety_property(not(F),_NF))). |
91 | | :- assert_must_fail((F = globally(implies(ap(request),finally(ap(alloc)))), |
92 | | is_safety_property(not(F),_NF))). |
93 | | :- assert_must_fail((F = globally(finally(ap(alloc))), |
94 | | is_safety_property(not(F),_NF))). |
95 | | :- assert_must_fail((F = globally(until(ap(request),finally(ap(alloc)))), |
96 | | is_safety_property(not(F),_NF))). |
97 | | :- assert_must_fail((F = implies(globally(finally(ap(send))),globally(finally(receive))), |
98 | | is_safety_property(not(F),_NF))). |
99 | | :- assert_must_fail((F = not(until(ap(p1),not(until(ap(p2),until(ap(p3),ap(p4)))))), |
100 | | is_safety_property(not(F),_NF))). |
101 | | |
102 | | |
103 | | is_safety_property(not(F),NF) :- |
104 | | normalize_to_release_pnf(F,NF), |
105 | | F \= true, % not(true) corresponds to G true which is also a liveness property and |
106 | | % will lead to a warning later that there is no accept_all state |
107 | | is_syntactically_safe(NF). |
108 | | |
109 | | is_syntactically_safe(deadlock) :- !. |
110 | | is_syntactically_safe(false) :- !. |
111 | | is_syntactically_safe(true) :- !. |
112 | | is_syntactically_safe(ap(F)) :- F \= available(_), !. % Gavin Lowe's available operator is only treated in ltlc.pl |
113 | | is_syntactically_safe(action(_)) :- !. |
114 | | is_syntactically_safe(and(F,G)) :- !, |
115 | | is_syntactically_safe(F), |
116 | | is_syntactically_safe(G). |
117 | | is_syntactically_safe(or(F,G)) :- !, |
118 | | is_syntactically_safe(F), |
119 | | is_syntactically_safe(G). |
120 | | is_syntactically_safe(next(F)) :- !, |
121 | | is_syntactically_safe(F). |
122 | | is_syntactically_safe(weakuntil(F,G)) :- !, |
123 | | is_syntactically_safe(F), |
124 | | is_syntactically_safe(G). |
125 | | is_syntactically_safe(release(F,G)) :- !, |
126 | | is_syntactically_safe(F), |
127 | | is_syntactically_safe(G). |
128 | | is_syntactically_safe(not(F)) :- !, |
129 | | is_atomic_proposition(F). |
130 | | |
131 | | is_atomic_proposition(F) :- |
132 | | F =.. [Functor|_Args], |
133 | | memberchk(Functor,[true,false,ap,action]). |
134 | | |
135 | | % Release PNF (the Release PNF does not imply exponential blow-up of the origin LTL formula) |
136 | | % f = true | false | a | not a | f1 & f2 | f1 or f2 | X f | f1 U f2 | f1 R f2 |
137 | | normalize_to_release_pnf(deadlock,deadlock) :- !. |
138 | | normalize_to_release_pnf(false,false) :- !. |
139 | | normalize_to_release_pnf(true,true) :- !. |
140 | | normalize_to_release_pnf(ap(P),ap(P)) :- !. |
141 | | normalize_to_release_pnf(action(P),action(P)) :- !. |
142 | | normalize_to_release_pnf(and(F,G),and(NF,NG)) :- !, |
143 | | normalize_to_release_pnf(F,NF), |
144 | | normalize_to_release_pnf(G,NG). |
145 | | normalize_to_release_pnf(or(F,G),or(NF,NG)) :- !, |
146 | | normalize_to_release_pnf(F,NF), |
147 | | normalize_to_release_pnf(G,NG). |
148 | | normalize_to_release_pnf(implies(F,G),NImplies) :- !, |
149 | | normalize_to_release_pnf(or(not(F),G),NImplies). |
150 | | normalize_to_release_pnf(next(F),next(NF)) :- !, |
151 | | normalize_to_release_pnf(F,NF). |
152 | | normalize_to_release_pnf(globally(F),release(false,NF)) :- !, |
153 | | normalize_to_release_pnf(F,NF). |
154 | | normalize_to_release_pnf(finally(F),until(true,NF)) :- !, |
155 | | normalize_to_release_pnf(F,NF). |
156 | | normalize_to_release_pnf(weakuntil(F,G),weakuntil(NF,NG)) :- !, |
157 | | normalize_to_release_pnf(F,NF), |
158 | | normalize_to_release_pnf(G,NG). |
159 | | normalize_to_release_pnf(release(F,G),release(NF,NG)) :- !, |
160 | | normalize_to_release_pnf(F,NF), |
161 | | normalize_to_release_pnf(G,NG). |
162 | | normalize_to_release_pnf(until(F,G),until(NF,NG)) :- !, |
163 | | normalize_to_release_pnf(F,NF), |
164 | | normalize_to_release_pnf(G,NG). |
165 | | % not rules |
166 | | normalize_to_release_pnf(not(true),false) :- !. |
167 | | normalize_to_release_pnf(not(false),true) :- !. |
168 | | normalize_to_release_pnf(not(and(F,G)),NOr) :- !, |
169 | | normalize_to_release_pnf(or(not(F),not(G)),NOr). |
170 | | normalize_to_release_pnf(not(or(F,G)),NAnd) :- !, |
171 | | normalize_to_release_pnf(and(not(F),not(G)),NAnd). |
172 | | normalize_to_release_pnf(not(next(F)),NNext) :- !, |
173 | | normalize_to_release_pnf(next(not(F)),NNext). |
174 | | normalize_to_release_pnf(not(finally(F)),NGlobally) :- !, |
175 | | normalize_to_release_pnf(release(false,not(F)),NGlobally). |
176 | | normalize_to_release_pnf(not(globally(F)),NUntil) :- !, |
177 | | normalize_to_release_pnf(until(true,not(F)),NUntil). |
178 | | normalize_to_release_pnf(not(until(F,G)),NRelease) :- !, |
179 | | normalize_to_release_pnf(release(not(F),not(G)),NRelease). |
180 | | normalize_to_release_pnf(not(F),NF) :- !, |
181 | | (F = not(F1) -> |
182 | | normalize_to_release_pnf(F1,NF) |
183 | | ; normalize_to_release_pnf(F,NF1), |
184 | | NF=not(NF1)). |
185 | | |
186 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
187 | | %%%%%%%%%%%%%%%%% Predicates for using the LTL2BA Tool %%%%%%%%%%%%%%%%%%%%%%%%%%%% |
188 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
189 | | |
190 | | ltl_mc_safety_property(Ltl,StartNodes,Result) :- |
191 | | encode_ltl_formula_as_ba(Ltl,Ltl1,ExitResult), |
192 | | debug_print_ba_automaton, |
193 | | (ExitResult = ok -> |
194 | | SMode = breadth_first, % can also be random |
195 | ? | start_mc_safety_property(SMode,StartNodes,Result) % uses aut_transition/3, aut_final_state/1, aut_initial_state/1 from this module |
196 | | ; ExitResult = error -> |
197 | | add_error_fail(translating_ltl2ba,'An error appeared while translating LTL to BA for the following formula: ',Ltl1) |
198 | | ; |
199 | | add_error_fail(translating_ltl2ba,'Unexpected error occurred while translating LTL to BA for the following formula: ',Ltl1) |
200 | | ). |
201 | | ltl_mc_safety_property(_Ltl,_StarNodes,_Result) :- |
202 | | add_error_fail(translating_ltl2ba,'Please ensure that ltl2ba is installed (see Help menu in ProB Tcl/Tk)',''). |
203 | | |
204 | | |
205 | | % -------------------------- |
206 | | % some direct encodings for a few common LTL patterns |
207 | | |
208 | ? | safety_property_can_be_encoded_directly(F) :- direct_encode_ltl_as_ba(F,false). |
209 | | %safety_property_can_be_encoded_directly(F) :- format('Cannot encode LTL safety property without ltl2ba:~n ~w~n',[F]),fail. |
210 | | |
211 | | % custom rules to translate formulas without ltl2ba |
212 | | direct_encode_ltl_as_ba(not(false),GenAutomata) :- encode_not_globally(false,GenAutomata). |
213 | ? | direct_encode_ltl_as_ba(not(globally(F)),GenAutomata) :- encode_not_globally(F,GenAutomata). |
214 | | |
215 | | encode_not_globally(implies(AP,next(NextAP)),GenAutomata) :- % formulas like G([Loop] => XX{x=0}) |
216 | | translate_ap(AP,TAP), |
217 | | negate_ap(AP,NegTAP), |
218 | | negate_ap(NextAP,NegAP), |
219 | | (GenAutomata=false -> true |
220 | | ; clear_automaton_facts, |
221 | | assertz(aut_initial_state('T0_init')), |
222 | | %assertz(aut_final_state(accept_S12)), % ?? useful |
223 | | assertz(aut_final_state(accept_all)), |
224 | | assertz(aut_transition('T0_init', TAP, accept_S12)), |
225 | | assertz(aut_transition('T0_init', NegTAP, 'T0_init')), |
226 | | assertz(aut_transition('accept_S12', NegAP, accept_all)), |
227 | | assertz(aut_transition('accept_S12', NegTAP, 'T0_init')), |
228 | | assertz(aut_transition('accept_S12', TAP, accept_S12)) |
229 | | ). |
230 | | /* We could also encode it non-deterministically, as LTL2BA does: G( [Action] => PROP ) |
231 | | Transition: T0_init --(true)--> T0_init |
232 | | Transition: T0_init --([Action])--> accept_S2 |
233 | | Transition: accept_S2 --(! (PROP))--> accept_all |
234 | | */ |
235 | | encode_not_globally(AP,GenAutomata) :- % special translation for checking LTL formula G{Pred} |
236 | | negate_ap(AP,NegAP), |
237 | | (GenAutomata=false -> true |
238 | | ; clear_automaton_facts, |
239 | | assertz(aut_initial_state('T0_init')), |
240 | | assertz(aut_final_state(accept_all)), |
241 | | assertz(aut_transition('T0_init', NegAP, accept_all)), |
242 | | assertz(aut_transition('T0_init', true, 'T0_init')) |
243 | | ). |
244 | | |
245 | | translate_ap(action(BOP),tp(BOP)). |
246 | | translate_ap(ap(Pred),ap(Pred)). |
247 | | translate_ap(not(AP),NAP) :- negate_ap(AP,NAP). |
248 | | translate_ap(false,false). |
249 | | translate_ap(true,true). |
250 | | translate_ap(implies(A,B),implies(TA,TB)) :- translate_ap(A,TA), translate_ap(B,TB). |
251 | | translate_ap(equivalent(A,B),equivalent(TA,TB)) :- translate_ap(A,TA), translate_ap(B,TB). |
252 | | translate_ap(and(A,B),and(TA,TB)) :- translate_ap(A,TA), translate_ap(B,TB). |
253 | | translate_ap(or(A,B),or(TA,TB)) :- translate_ap(A,TA), translate_ap(B,TB). |
254 | | |
255 | | negate_ap(implies(A,B),and(TA,NB)) :- translate_ap(A,TA), negate_ap(B,NB). |
256 | | negate_ap(equivalent(A,B),equivalent(TA,NB)) :- translate_ap(A,TA), negate_ap(B,NB). |
257 | | negate_ap(or(A,B),and(NA,NB)) :- negate_ap(A,NA), negate_ap(B,NB). |
258 | | negate_ap(and(A,B),or(NA,NB)) :- negate_ap(A,NA), negate_ap(B,NB). |
259 | | negate_ap(ap(Pred),not(ap(Pred))). |
260 | | negate_ap(action(BOP),not(tp(BOP))). |
261 | | negate_ap(not(AP),TAP) :- translate_ap(AP,TAP). |
262 | | %negate_ap(true,false). |
263 | | negate_ap(false,true). |
264 | | |
265 | | % check if an LTL formula uses transition informations of the form [Action] |
266 | | ltl_formula_uses_tps(globally(A)) :- !, ltl_formula_uses_tps(A). |
267 | | ltl_formula_uses_tps(finally(A)) :- !, ltl_formula_uses_tps(A). |
268 | | ltl_formula_uses_tps(next(A)) :- !, ltl_formula_uses_tps(A). |
269 | | ltl_formula_uses_tps(until(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)). |
270 | | ltl_formula_uses_tps(weakuntil(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)). |
271 | | ltl_formula_uses_tps(release(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)). |
272 | | ltl_formula_uses_tps(action(_)) :- !. |
273 | | ltl_formula_uses_tps(AP) :- basic_ap(AP),!, fail. |
274 | | ltl_formula_uses_tps(not(AP)) :- !, ltl_formula_uses_tps(AP). |
275 | | ltl_formula_uses_tps(and(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)). |
276 | | ltl_formula_uses_tps(or(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)). |
277 | | ltl_formula_uses_tps(implies(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)). |
278 | | ltl_formula_uses_tps(equivalent(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)). |
279 | | ltl_formula_uses_tps(A) :- add_internal_error('Unknown LTL property:',ltl_formula_uses_tps(A)). |
280 | | |
281 | | basic_ap(ap(_)). |
282 | | basic_ap(true). |
283 | | basic_ap(false). |
284 | | %basic_ap(deadlock). % are wrapped in ap(...) |
285 | | %basic_ap(sink). % ditto |
286 | | |
287 | | |
288 | | % -------------------------- |
289 | | |
290 | | encode_ltl_formula_as_ba(Ltl,Ltl1,ExitResult) :- |
291 | ? | GenAutomata=true,direct_encode_ltl_as_ba(Ltl,GenAutomata),!, |
292 | | (ltl_formula_uses_tps(Ltl) |
293 | | -> debug_format(19,'LTL (safety) formula uses transition informations~n',[]), |
294 | | assertz(tps_occurring) % influences the way the safety mc needs to run |
295 | | ; true), |
296 | | debug_format(19,'Encoding LTL formula directly without ltl2ba~n',[]), |
297 | | Ltl1=Ltl, ExitResult=ok. |
298 | | encode_ltl_formula_as_ba(Ltl,Ltl1,ExitResult) :- |
299 | | clear_automaton_facts, |
300 | | %format('LTL formula: ~w~n',[Ltl]), |
301 | | translate_to_ltl2ba_syntax(Ltl,Ltl1), % this has a side-effect of asserting tps_occurring, ... !!!! |
302 | | safe_ltl2ba_init, |
303 | | (debug_mode(on) -> Verbose = true; Verbose = false), |
304 | | c_call_ltl2ba(Ltl1,ltl_safety:assert_aut_initial_state, |
305 | | ltl_safety:assert_aut_final_state, |
306 | | ltl_safety:assert_aut_transition,Verbose,ExitResult). |
307 | | |
308 | | |
309 | | safe_ltl2ba_init :- |
310 | | catch(ltl2ba_init,Exc, |
311 | | (add_error(translating_ltl2ba,'Exception when initialising LTL2BA (possibly wrong architecture, try reinstalling with probcli -install ltl2ba):',Exc),fail)). |
312 | | |
313 | | is_ltl2ba_tool_installed :- is_ltl2ba_tool_installed(message). |
314 | | is_ltl2ba_tool_installed(GenerateMsg) :- |
315 | | host_platform(Platform), |
316 | | get_platform_specifix_ltl2ba_library(Platform,File), |
317 | | absolute_file_name(prob_lib(File),LTL2BALibrary), |
318 | | (file_exists(LTL2BALibrary) -> |
319 | | debug_println(9,'LTL2BA is installed.'), |
320 | | safe_ltl2ba_init |
321 | | ; GenerateMsg==message -> |
322 | | add_message(translating_ltl2ba, |
323 | | 'ltl2ba library could not be found in lib/ directory of ProB, install ltl2ba for faster model checking (see Help menu in ProB Tcl/Tk): ',LTL2BALibrary), |
324 | | fail |
325 | | ). |
326 | | |
327 | | get_platform_specifix_ltl2ba_library(darwin,'ltl2ba.bundle'):- !. |
328 | | get_platform_specifix_ltl2ba_library(linux,'ltl2ba.so') :- !. |
329 | | get_platform_specifix_ltl2ba_library(windows,'ltl2ba.dll') :- !. |
330 | | get_platform_specifix_ltl2ba_library(Unknown,_) :- |
331 | | add_error_fail(translating_ltl2ba,'Unknown platform: ', Unknown). |
332 | | |
333 | | :- public assert_aut_initial_state/1. % callback given to C |
334 | | assert_aut_initial_state(StateDescription) :- |
335 | | debug_println(9,asserting_initialstate(StateDescription)), |
336 | | assertz(aut_initial_state(StateDescription)). |
337 | | :- public assert_aut_final_state/1. % callback given to C |
338 | | assert_aut_final_state(StateDescription) :- |
339 | | debug_println(9,asserting_finitestate(StateDescription)), |
340 | | assertz(aut_final_state(StateDescription)). |
341 | | :- public assert_aut_transition/3. % callback given to C |
342 | | assert_aut_transition(Src,Atom,Dst) :- |
343 | | atom_codes(Atom,Codes), |
344 | | read_term_from_codes_exception(Codes,PrepRep,[]), |
345 | | redefine_transition_label(PrepRep,Label), |
346 | | debug_println(9,asserting_transition(aut_transition(Src,Label,Dst))), |
347 | | assertz(aut_transition(Src,Label,Dst)). |
348 | | |
349 | | read_term_from_codes_exception(Codes,PrepRep,Options) :- |
350 | | (read_term_from_codes(Codes,PrepRep,Options) |
351 | | -> true |
352 | | ; atom_codes(Atom,Codes), |
353 | | add_error(translating_ltl3ba_callback, 'Unexpected atom representation (does atom ends with fullstop?): ', Atom) |
354 | | ). |
355 | | |
356 | | %redefine_automaton_facts :- |
357 | | % aut_transition(Src,P,Dst), |
358 | | % redefine_transition(Src,P,Dst), |
359 | | % fail. |
360 | | %redefine_automaton_facts. |
361 | | %redefine_transition(Src,Predicate,Dst) :- |
362 | | % retract(aut_transition(Src,Predicate,Dst)), |
363 | | % redefine_transition_label(Predicate,Preposition), |
364 | | % assertz(aut_transition(Src,Preposition,Dst)). |
365 | | |
366 | | redefine_transition_label(true,Res) :- !, |
367 | | Res = true. |
368 | | redefine_transition_label(false,Res) :- !, |
369 | | Res = false. |
370 | | redefine_transition_label(not(AP),Res) :- |
371 | | ap_representation(AP,bpred(Pred)),!, |
372 | | create_negation(Pred,NegPred), |
373 | | create_atomic_b_predicate(NegPred,Res). |
374 | | redefine_transition_label(AP,Res) :- |
375 | | ap_representation(AP,Rep),!, |
376 | | Res = ap(Rep). |
377 | | redefine_transition_label(TP,Res) :- |
378 | | tp_representation(TP,Rep),!, |
379 | | Res = tp(Rep). |
380 | | redefine_transition_label(F,Res) :- |
381 | | F =.. [Functor|Args], |
382 | | maplist(redefine_transition_label,Args,NewArgs), |
383 | | Res =.. [Functor|NewArgs]. |
384 | | |
385 | | create_atomic_b_predicate(BPred,Res) :- |
386 | | Res = ap(bpred(BPred)). |
387 | | |
388 | | debug_print_ba_automaton :- |
389 | | %listing(aut_initial_state/1), listing(aut_final_state/1), listing(aut_transition/3), |
390 | | (debug_mode(on) |
391 | | -> print_transitions_fail_loop |
392 | | ; true). |
393 | | |
394 | | print_transitions_fail_loop :- |
395 | | aut_transition(Src,Label,Dst), |
396 | | print('Transition: '),print(Src), |
397 | | translate_and_print_label(Label), |
398 | | print(Dst),nl,fail. |
399 | | print_transitions_fail_loop. |
400 | | |
401 | | translate_and_print_label(Label) :- |
402 | | pp_ba_label(Label,Atom,[]), |
403 | | ajoin(Atom,Text), |
404 | | print_label(Text). |
405 | | |
406 | | %% pretty-printing predicate in Spin syntax (created just to test if ltl2ba produces the correct automaton) |
407 | | pp_ba_label(true,['true'|S],S) :- !. |
408 | | pp_ba_label(false,['false'|S],S) :- !. |
409 | | pp_ba_label(ap(AP),[Atom|S],S) :- !, |
410 | | pp_ap(AP,Atom). |
411 | | pp_ba_label(tp(TP),[Atom|S],S) :- !, |
412 | | pp_tp(TP,Atom). |
413 | | pp_ba_label(not(Pred),['! ('|S],T) :- !, |
414 | | pp_ba_label(Pred,S,[')'|T]). |
415 | | pp_ba_label(and(Pred1,Pred2),['('|S],T) :- !, |
416 | | pp_ba_label(Pred1,S,[' && '| S1]), |
417 | | pp_ba_label(Pred2,S1,[')'|T]). |
418 | | pp_ba_label(or(Pred1,Pred2),['('|S],T) :- !, |
419 | | pp_ba_label(Pred1,S,[' || '| S1]), |
420 | | pp_ba_label(Pred2,S1,[')'|T]). |
421 | | pp_ba_label(Otherwise,['???'|S],S) :- |
422 | | add_error(printing_ba_label_for_ltl2ba,'Non-expected label: ',Otherwise). |
423 | | |
424 | | print_label(Label) :- |
425 | | print(' --('),print(Label),print(')--> '). |
426 | | |
427 | | translate_to_ltl2ba_syntax(Formula,Text) :- |
428 | | retractall(ap_representation(_,_)), |
429 | | retractall(tp_representation(_,_)), |
430 | | retractall(tps_occurring), |
431 | | pp_formula_to_ltl2ba_syntax(Formula,Text). |
432 | | |
433 | | pp_formula_to_ltl2ba_syntax(Formula,Res) :- |
434 | | pp_to_ltl2ba_syntax(Formula,Atoms,[]), |
435 | | ajoin(Atoms,Res). |
436 | | |
437 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
438 | | %%%%%%%%%%%%%%%%% Unit Tests %%%%%%%%%%%%%%%%%%%%%% |
439 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
440 | | |
441 | | :- assert_must_succeed((F = and(or(true,false),true), |
442 | | pp_formula_to_ltl2ba_syntax(F,Text), |
443 | | Text = '((true || false) && true)')). |
444 | | :- assert_must_succeed((F = implies(deadlock,not(true)), |
445 | | pp_formula_to_ltl2ba_syntax(F,Text), |
446 | | Text = '(deadlock -> ! true)')). |
447 | | :- assert_must_succeed((F = not(until(true,next(implies(deadlock,not(true))))), |
448 | | pp_formula_to_ltl2ba_syntax(F,Text), |
449 | | Text = '! (true U X ((deadlock -> ! true)))')). |
450 | | :- assert_must_succeed((F = weakuntil(true,false), |
451 | | pp_formula_to_ltl2ba_syntax(F,Text), |
452 | | Text = '((! true || false) V (true || false))')). |
453 | | :- assert_must_succeed((F = globally(finally(true)), |
454 | | pp_formula_to_ltl2ba_syntax(F,Text), |
455 | | Text = '[] (<> (true))')). |
456 | | |
457 | | |
458 | | pp_to_ltl2ba_syntax(true,['true'|S],S) :- !. |
459 | | pp_to_ltl2ba_syntax(false,['false'|S],S) :- !. |
460 | | pp_to_ltl2ba_syntax(deadlock,['deadlock'|S],S) :- !. |
461 | | pp_to_ltl2ba_syntax(ap(X),[AP|S],S) :- !, |
462 | | term_hash(X,Hash), |
463 | | ajoin(['ap',Hash],AP), |
464 | | (\+ap_representation(AP,_) -> assertz(ap_representation(AP,X)); true). |
465 | | pp_to_ltl2ba_syntax(action(X),[TP|S],S) :- !, |
466 | | assertz(tps_occurring), |
467 | | term_hash(X,Hash), |
468 | | ajoin(['tp',Hash],TP), |
469 | | (\+tp_representation(TP,_) -> assertz(tp_representation(TP,X)); true). |
470 | | pp_to_ltl2ba_syntax(not(X),['! '|S],T) :- !, |
471 | | pp_to_ltl2ba_syntax(X,S,T). |
472 | | pp_to_ltl2ba_syntax(and(X,Y),['('|S],T) :- !, |
473 | | pp_to_ltl2ba_syntax(X,S,[' && '|S1]), |
474 | | pp_to_ltl2ba_syntax(Y,S1,[')'|T]). |
475 | | pp_to_ltl2ba_syntax(or(X,Y),['('|S],T) :- !, |
476 | | pp_to_ltl2ba_syntax(X,S,[' || '|S1]), |
477 | | pp_to_ltl2ba_syntax(Y,S1,[')'|T]). |
478 | | pp_to_ltl2ba_syntax(implies(X,Y),['('|S],T) :- !, |
479 | | pp_to_ltl2ba_syntax(X,S,[' -> '|S1]), |
480 | | pp_to_ltl2ba_syntax(Y,S1,[')'|T]). |
481 | | pp_to_ltl2ba_syntax(equivalent(X,Y),['('|S],T) :- !, |
482 | | pp_to_ltl2ba_syntax(X,S,[' <-> '|S1]), |
483 | | pp_to_ltl2ba_syntax(Y,S1,[')'|T]). |
484 | | pp_to_ltl2ba_syntax(next(X),['X ('|S],T) :- !, |
485 | | pp_to_ltl2ba_syntax(X,S,[')'|T]). |
486 | | pp_to_ltl2ba_syntax(globally(X),['[] ('|S],T) :- !, |
487 | | pp_to_ltl2ba_syntax(X,S,[')'|T]). |
488 | | pp_to_ltl2ba_syntax(finally(X),['<> ('|S],T) :- !, |
489 | | pp_to_ltl2ba_syntax(X,S,[')'|T]). |
490 | | pp_to_ltl2ba_syntax(until(X,Y),['('|S],T) :- !, |
491 | | pp_to_ltl2ba_syntax(X,S,[' U '|S1]), |
492 | | pp_to_ltl2ba_syntax(Y,S1,[')'|T]). |
493 | | pp_to_ltl2ba_syntax(release(X,Y),['('|S],T) :- !, |
494 | | pp_to_ltl2ba_syntax(X,S,[' V '|S1]), |
495 | | pp_to_ltl2ba_syntax(Y,S1,[')'|T]). |
496 | | pp_to_ltl2ba_syntax(weakuntil(X,Y),S,T) :- !, |
497 | | pp_to_ltl2ba_syntax(release(or(not(X),Y),or(X,Y)),S,T). |