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