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		!,
194		(ExitResult = ok ->
195		SMode = breadth_first, % can also be random
196		start_mc_safety_property(SMode,StartNodes,Result) % uses aut_transition/3, aut_final_state/1, aut_initial_state/1 from this module
197		; ExitResult = error ->
198		add_error_fail(translating_ltl2ba,'An error appeared while translating LTL to BA for the following formula: ',Ltl1)
199		;
200		add_error_fail(translating_ltl2ba,'Unexpected error occurred while translating LTL to BA for the following formula: ',Ltl1)
201		).
202		ltl_mc_safety_property(_Ltl,_StarNodes,_Result) :-
203		add_error_fail(translating_ltl2ba,'Please ensure that ltl2ba is installed (see Help menu in ProB Tcl/Tk)','').
204
205
206		% --------------------------
207		% some direct encodings for a few common LTL patterns
208
209		safety_property_can_be_encoded_directly(F) :- direct_encode_ltl_as_ba(F,false).
210		%safety_property_can_be_encoded_directly(F) :- format('Cannot encode LTL safety property without ltl2ba:~n ~w~n',[F]),fail.
211
212		% custom rules to translate formulas without ltl2ba
213		direct_encode_ltl_as_ba(not(false),GenAutomata) :- encode_not_globally(false,GenAutomata).
214		direct_encode_ltl_as_ba(not(globally(F)),GenAutomata) :- encode_not_globally(F,GenAutomata).
215
216		encode_not_globally(implies(AP,next(NextAP)),GenAutomata) :- % formulas like G([Loop] => XX{x=0})
217		translate_ap(AP,TAP),
218		negate_ap(AP,NegTAP),
219		negate_ap(NextAP,NegAP),
220		(GenAutomata=false -> true
221		; clear_automaton_facts,
222		assertz(aut_initial_state('T0_init')),
223		%assertz(aut_final_state(accept_S12)), % ?? useful
224		assertz(aut_final_state(accept_all)),
225		assertz(aut_transition('T0_init', TAP, accept_S12)),
226		assertz(aut_transition('T0_init', NegTAP, 'T0_init')),
227		assertz(aut_transition('accept_S12', NegAP, accept_all)),
228		assertz(aut_transition('accept_S12', NegTAP, 'T0_init')),
229		assertz(aut_transition('accept_S12', TAP, accept_S12))
230		).
231		/* We could also encode it non-deterministically, as LTL2BA does: G( [Action] => PROP )
232		Transition: T0_init --(true)--> T0_init
233		Transition: T0_init --([Action])--> accept_S2
234		Transition: accept_S2 --(! (PROP))--> accept_all
235		*/
236		encode_not_globally(AP,GenAutomata) :- % special translation for checking LTL formula G{Pred}
237		negate_ap(AP,NegAP),
238		(GenAutomata=false -> true
239		; clear_automaton_facts,
240		assertz(aut_initial_state('T0_init')),
241		assertz(aut_final_state(accept_all)),
242		assertz(aut_transition('T0_init', NegAP, accept_all)),
243		assertz(aut_transition('T0_init', true, 'T0_init'))
244		).
245
246		translate_ap(action(BOP),tp(BOP)).
247		translate_ap(ap(Pred),ap(Pred)).
248		translate_ap(not(AP),NAP) :- negate_ap(AP,NAP).
249		translate_ap(false,false).
250		translate_ap(true,true).
251		translate_ap(implies(A,B),implies(TA,TB)) :- translate_ap(A,TA), translate_ap(B,TB).
252		translate_ap(equivalent(A,B),equivalent(TA,TB)) :- translate_ap(A,TA), translate_ap(B,TB).
253		translate_ap(and(A,B),and(TA,TB)) :- translate_ap(A,TA), translate_ap(B,TB).
254		translate_ap(or(A,B),or(TA,TB)) :- translate_ap(A,TA), translate_ap(B,TB).
255
256		negate_ap(implies(A,B),and(TA,NB)) :- translate_ap(A,TA), negate_ap(B,NB).
257		negate_ap(equivalent(A,B),equivalent(TA,NB)) :- translate_ap(A,TA), negate_ap(B,NB).
258		negate_ap(or(A,B),and(NA,NB)) :- negate_ap(A,NA), negate_ap(B,NB).
259		negate_ap(and(A,B),or(NA,NB)) :- negate_ap(A,NA), negate_ap(B,NB).
260		negate_ap(ap(Pred),not(ap(Pred))).
261		negate_ap(action(BOP),not(tp(BOP))).
262		negate_ap(not(AP),TAP) :- translate_ap(AP,TAP).
263		%negate_ap(true,false).
264		negate_ap(false,true).
265
266		% check if an LTL formula uses transition informations of the form [Action]
267		ltl_formula_uses_tps(globally(A)) :- !, ltl_formula_uses_tps(A).
268		ltl_formula_uses_tps(finally(A)) :- !, ltl_formula_uses_tps(A).
269		ltl_formula_uses_tps(next(A)) :- !, ltl_formula_uses_tps(A).
270		ltl_formula_uses_tps(until(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)).
271		ltl_formula_uses_tps(weakuntil(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)).
272		ltl_formula_uses_tps(release(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)).
273		ltl_formula_uses_tps(action(_)) :- !.
274		ltl_formula_uses_tps(AP) :- basic_ap(AP),!, fail.
275		ltl_formula_uses_tps(not(AP)) :- !, ltl_formula_uses_tps(AP).
276		ltl_formula_uses_tps(and(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)).
277		ltl_formula_uses_tps(or(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)).
278		ltl_formula_uses_tps(implies(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)).
279		ltl_formula_uses_tps(equivalent(A,B)) :- !, (ltl_formula_uses_tps(A) -> true ; ltl_formula_uses_tps(B)).
280		ltl_formula_uses_tps(A) :- add_internal_error('Unknown LTL property:',ltl_formula_uses_tps(A)).
281
282		basic_ap(ap(_)).
283		basic_ap(true).
284		basic_ap(false).
285		%basic_ap(deadlock). % are wrapped in ap(...)
286		%basic_ap(sink). % ditto
287
288
289		% --------------------------
290
291		encode_ltl_formula_as_ba(Ltl,Ltl1,ExitResult) :-
292		GenAutomata=true,direct_encode_ltl_as_ba(Ltl,GenAutomata),!,
293		(ltl_formula_uses_tps(Ltl)
294		-> debug_format(19,'LTL (safety) formula uses transition informations~n',[]),
295		assertz(tps_occurring) % influences the way the safety mc needs to run
296		; true),
297		debug_format(19,'Encoding LTL formula directly without ltl2ba~n',[]),
298		Ltl1=Ltl, ExitResult=ok.
299		encode_ltl_formula_as_ba(Ltl,Ltl1,ExitResult) :-
300		clear_automaton_facts,
301		%format('LTL formula: ~w~n',[Ltl]),
302		translate_to_ltl2ba_syntax(Ltl,Ltl1), % this has a side-effect of asserting tps_occurring, ... !!!!
303		safe_ltl2ba_init,
304		(debug_mode(on) -> Verbose = true; Verbose = false),
305		c_call_ltl2ba(Ltl1,ltl_safety:assert_aut_initial_state,
306		ltl_safety:assert_aut_final_state,
307		ltl_safety:assert_aut_transition,Verbose,ExitResult).
308
309
310		safe_ltl2ba_init :-
311		catch(ltl2ba_init,Exc,
312		(add_error(translating_ltl2ba,'Exception when initialising LTL2BA (possibly wrong architecture, try reinstalling with probcli -install ltl2ba):',Exc),fail)).
313
314		is_ltl2ba_tool_installed :- is_ltl2ba_tool_installed(message).
315		is_ltl2ba_tool_installed(GenerateMsg) :-
316		host_platform(Platform),
317		get_platform_specifix_ltl2ba_library(Platform,File),
318		absolute_file_name(prob_lib(File),LTL2BALibrary),
319		(file_exists(LTL2BALibrary) ->
320		debug_println(9,'LTL2BA is installed.'),
321		safe_ltl2ba_init
322		; GenerateMsg==message ->
323		add_message(translating_ltl2ba,
324		'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),
325		fail
326		).
327
328		get_platform_specifix_ltl2ba_library(darwin,'ltl2ba.bundle'):- !.
329		get_platform_specifix_ltl2ba_library(linux,'ltl2ba.so') :- !.
330		get_platform_specifix_ltl2ba_library(windows,'ltl2ba.dll') :- !.
331		get_platform_specifix_ltl2ba_library(Unknown,_) :-
332		add_error_fail(translating_ltl2ba,'Unknown platform: ', Unknown).
333
334		:- public assert_aut_initial_state/1. % callback given to C
335		assert_aut_initial_state(StateDescription) :-
336		debug_println(9,asserting_initialstate(StateDescription)),
337		assertz(aut_initial_state(StateDescription)).
338		:- public assert_aut_final_state/1. % callback given to C
339		assert_aut_final_state(StateDescription) :-
340		debug_println(9,asserting_finitestate(StateDescription)),
341		assertz(aut_final_state(StateDescription)).
342		:- public assert_aut_transition/3. % callback given to C
343		assert_aut_transition(Src,Atom,Dst) :-
344		atom_codes(Atom,Codes),
345		read_term_from_codes_exception(Codes,PrepRep,[]),
346		redefine_transition_label(PrepRep,Label),
347		debug_println(9,asserting_transition(aut_transition(Src,Label,Dst))),
348		assertz(aut_transition(Src,Label,Dst)).
349
350		read_term_from_codes_exception(Codes,PrepRep,Options) :-
351		(read_term_from_codes(Codes,PrepRep,Options)
352		-> true
353		; atom_codes(Atom,Codes),
354		add_error(translating_ltl3ba_callback, 'Unexpected atom representation (does atom ends with fullstop?): ', Atom)
355		).
356
357		%redefine_automaton_facts :-
358		% aut_transition(Src,P,Dst),
359		% redefine_transition(Src,P,Dst),
360		% fail.
361		%redefine_automaton_facts.
362		%redefine_transition(Src,Predicate,Dst) :-
363		% retract(aut_transition(Src,Predicate,Dst)),
364		% redefine_transition_label(Predicate,Preposition),
365		% assertz(aut_transition(Src,Preposition,Dst)).
366
367		redefine_transition_label(true,Res) :- !,
368		Res = true.
369		redefine_transition_label(false,Res) :- !,
370		Res = false.
371		redefine_transition_label(not(AP),Res) :-
372		ap_representation(AP,bpred(Pred)),!,
373		create_negation(Pred,NegPred),
374		create_atomic_b_predicate(NegPred,Res).
375		redefine_transition_label(AP,Res) :-
376		ap_representation(AP,Rep),!,
377		Res = ap(Rep).
378		redefine_transition_label(TP,Res) :-
379		tp_representation(TP,Rep),!,
380		Res = tp(Rep).
381		redefine_transition_label(F,Res) :-
382		F =.. [Functor|Args],
383		maplist(redefine_transition_label,Args,NewArgs),
384		Res =.. [Functor|NewArgs].
385
386		create_atomic_b_predicate(BPred,Res) :-
387		Res = ap(bpred(BPred)).
388
389		debug_print_ba_automaton :-
390		%listing(aut_initial_state/1), listing(aut_final_state/1), listing(aut_transition/3),
391		(debug_mode(on)
392		-> print_transitions_fail_loop
393		; true).
394
395		print_transitions_fail_loop :-
396		aut_transition(Src,Label,Dst),
397		print('Transition: '),print(Src),
398		translate_and_print_label(Label),
399		print(Dst),nl,fail.
400		print_transitions_fail_loop.
401
402		translate_and_print_label(Label) :-
403		pp_ba_label(Label,Atom,[]),
404		ajoin(Atom,Text),
405		print_label(Text).
406
407		%% pretty-printing predicate in Spin syntax (created just to test if ltl2ba produces the correct automaton)
408		pp_ba_label(true,['true'|S],S) :- !.
409		pp_ba_label(false,['false'|S],S) :- !.
410		pp_ba_label(ap(AP),[Atom|S],S) :- !,
411		pp_ap(AP,Atom).
412		pp_ba_label(tp(TP),[Atom|S],S) :- !,
413		pp_tp(TP,Atom).
414		pp_ba_label(not(Pred),['! ('|S],T) :- !,
415		pp_ba_label(Pred,S,[')'|T]).
416		pp_ba_label(and(Pred1,Pred2),['('|S],T) :- !,
417		pp_ba_label(Pred1,S,[' && '| S1]),
418		pp_ba_label(Pred2,S1,[')'|T]).
419		pp_ba_label(or(Pred1,Pred2),['('|S],T) :- !,
420		pp_ba_label(Pred1,S,[' || '| S1]),
421		pp_ba_label(Pred2,S1,[')'|T]).
422		pp_ba_label(Otherwise,['???'|S],S) :-
423		add_error(printing_ba_label_for_ltl2ba,'Non-expected label: ',Otherwise).
424
425		print_label(Label) :-
426		print(' --('),print(Label),print(')--> ').
427
428		translate_to_ltl2ba_syntax(Formula,Text) :-
429		retractall(ap_representation(_,_)),
430		retractall(tp_representation(_,_)),
431		retractall(tps_occurring),
432		pp_formula_to_ltl2ba_syntax(Formula,Text).
433
434		pp_formula_to_ltl2ba_syntax(Formula,Res) :-
435		pp_to_ltl2ba_syntax(Formula,Atoms,[]),
436		ajoin(Atoms,Res).
437
438		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
439		%%%%%%%%%%%%%%%%% Unit Tests %%%%%%%%%%%%%%%%%%%%%%
440		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
441
442		:- assert_must_succeed((F = and(or(true,false),true),
443		pp_formula_to_ltl2ba_syntax(F,Text),
444		Text = '((true || false) && true)')).
445		:- assert_must_succeed((F = implies(deadlock,not(true)),
446		pp_formula_to_ltl2ba_syntax(F,Text),
447		Text = '(deadlock -> ! true)')).
448		:- assert_must_succeed((F = not(until(true,next(implies(deadlock,not(true))))),
449		pp_formula_to_ltl2ba_syntax(F,Text),
450		Text = '! (true U X ((deadlock -> ! true)))')).
451		:- assert_must_succeed((F = weakuntil(true,false),
452		pp_formula_to_ltl2ba_syntax(F,Text),
453		Text = '((! true || false) V (true || false))')).
454		:- assert_must_succeed((F = globally(finally(true)),
455		pp_formula_to_ltl2ba_syntax(F,Text),
456		Text = '[] (<> (true))')).
457
458
459		pp_to_ltl2ba_syntax(true,['true'|S],S) :- !.
460		pp_to_ltl2ba_syntax(false,['false'|S],S) :- !.
461		pp_to_ltl2ba_syntax(deadlock,['deadlock'|S],S) :- !.
462		pp_to_ltl2ba_syntax(ap(X),[AP|S],S) :- !,
463		term_hash(X,Hash),
464		ajoin(['ap',Hash],AP),
465		(\+ap_representation(AP,_) -> assertz(ap_representation(AP,X)); true).
466		pp_to_ltl2ba_syntax(action(X),[TP|S],S) :- !,
467		assertz(tps_occurring),
468		term_hash(X,Hash),
469		ajoin(['tp',Hash],TP),
470		(\+tp_representation(TP,_) -> assertz(tp_representation(TP,X)); true).
471		pp_to_ltl2ba_syntax(not(X),['! '|S],T) :- !,
472		pp_to_ltl2ba_syntax(X,S,T).
473		pp_to_ltl2ba_syntax(and(X,Y),['('|S],T) :- !,
474		pp_to_ltl2ba_syntax(X,S,[' && '|S1]),
475		pp_to_ltl2ba_syntax(Y,S1,[')'|T]).
476		pp_to_ltl2ba_syntax(or(X,Y),['('|S],T) :- !,
477		pp_to_ltl2ba_syntax(X,S,[' || '|S1]),
478		pp_to_ltl2ba_syntax(Y,S1,[')'|T]).
479		pp_to_ltl2ba_syntax(implies(X,Y),['('|S],T) :- !,
480		pp_to_ltl2ba_syntax(X,S,[' -> '|S1]),
481		pp_to_ltl2ba_syntax(Y,S1,[')'|T]).
482		pp_to_ltl2ba_syntax(equivalent(X,Y),['('|S],T) :- !,
483		pp_to_ltl2ba_syntax(X,S,[' <-> '|S1]),
484		pp_to_ltl2ba_syntax(Y,S1,[')'|T]).
485		pp_to_ltl2ba_syntax(next(X),['X ('|S],T) :- !,
486		pp_to_ltl2ba_syntax(X,S,[')'|T]).
487		pp_to_ltl2ba_syntax(globally(X),['[] ('|S],T) :- !,
488		pp_to_ltl2ba_syntax(X,S,[')'|T]).
489		pp_to_ltl2ba_syntax(finally(X),['<> ('|S],T) :- !,
490		pp_to_ltl2ba_syntax(X,S,[')'|T]).
491		pp_to_ltl2ba_syntax(until(X,Y),['('|S],T) :- !,
492		pp_to_ltl2ba_syntax(X,S,[' U '|S1]),
493		pp_to_ltl2ba_syntax(Y,S1,[')'|T]).
494		pp_to_ltl2ba_syntax(release(X,Y),['('|S],T) :- !,
495		pp_to_ltl2ba_syntax(X,S,[' V '|S1]),
496		pp_to_ltl2ba_syntax(Y,S1,[')'|T]).
497		pp_to_ltl2ba_syntax(weakuntil(X,Y),S,T) :- !,
498		pp_to_ltl2ba_syntax(release(or(not(X),Y),or(X,Y)),S,T).