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