1		% (c) 2014-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html
4
5		:- module(ltl_safety,[is_safety_property/2,ltl_mc_safety_property/3,
6		is_ltl2ba_tool_installed/0,
7		aut_transition/3, aut_finite_state/1, aut_initial_state/1,
8		tps_occurring/0]).
9
10		/* SICSTUS Libraries */
11		:- use_module(library(lists)).
12		:- use_module(library(codesio)).
13		:- use_module(library(terms)).
14		:- use_module(library(file_systems)).
15
16		/* ProB Libraries */
17		:- use_module(probsrc(tools),[ajoin/2,host_platform/1]).
18		:- use_module(probsrc(error_manager)).
19		%% :- use_module(probsrc(debug)).
20		:- use_module(probsrc(self_check)).
21		:- use_module(probsrc(preferences),[preference/2,set_preference/2,get_preference/2]).
22		%:- use_module(probsrc(system_call),[system_call/5]).
23		:- use_module(probsrc(debug),[debug_println/2,debug_mode/1]).
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_finite_state/1, aut_initial_state/1.
39
40		clear_automaton_facts :-
41		retractall(aut_transition(_,_,_)),
42		retractall(aut_initial_state(_)),
43		retractall(aut_finite_state(_)).
44
45		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
46		%%%%%%%%%%% Checking whether an LTL property represents a safety property %%%%%%%%%%
47		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
48		% The predicates check whether the parsed LTL property represents a safety property
49		% by checking the syntactical structure of the formula.
50		% The idea is borrowed from the following theorem from the paper
51		% "Safety, Liveness and Fairness in Temporal Logic" of A. Sistla:
52		%% THEOREM: Every propositional formula is a safety formula and if f,g are safety formulae,
53		%% then so are f & g, f or g, X f, f W g, and G f, where 'W' is the weak-until operator.
54		%
55		% Note that the checked formula should be a positive formula. An LTL formula is said to
56		% be a positive if none of the temporal operators appears in the scope of 'not'.
57
58		% Testing various properties for being safety or liveness. Some of
59		% the unit tests here represent examples from the paper mentioned above.
60		% Note that the first argument of is_safety_property/2 should be negated, as
61		% this is done after negating the original property that should be model checked (see select_ltl_mode/4 in ltl.pl)
62		:- assert_must_succeed((F = ap(p),
63		is_safety_property_test(not(F),_NF))).
64		:- assert_must_succeed((F = globally(deadlock),
65		is_safety_property_test(not(F),_NF))).
66		:- assert_must_succeed((F = weakuntil(not(ap(alloc)),ap(request)),
67		is_safety_property_test(not(F),_NF))).
68		:- assert_must_succeed((F = and(weakuntil(not(ap(alloc)),ap(request)),
69		globally(implies(ap(alloc),next(weakuntil(not(ap(alloc)),ap(request)))))),
70		is_safety_property_test(not(F),_NF))).
71		:- assert_must_succeed((F = globally(implies(not(ap(request)),or(ap(alloc),or(next(ap(alloc)),next(next(ap(alloc))))))),
72		is_safety_property_test(not(F),_NF))).
73		:- assert_must_succeed((F = globally(or(not(ap(p)),globally(not(ap(p))))),
74		is_safety_property_test(not(F),_NF))).
75		:- assert_must_succeed((F = not(until(ap(p1),until(ap(p2),ap(p3)))),
76		is_safety_property_test(not(F),_NF))).
77		:- assert_must_succeed((F = not(until(ap(p1),until(ap(p2),until(ap(p3),ap(p4))))),
78		is_safety_property_test(not(F),_NF))).
79		:- 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)))))))),
80		is_safety_property_test(not(F),_NF))).
81		:- assert_must_succeed((F = not(not(globally(deadlock))),
82		is_safety_property_test(not(F),_NF))).
83		:- assert_must_succeed((F = globally(or(ap(p),and(next(ap(q)),not(next(ap(q)))))),
84		is_safety_property_test(not(F),_NF))).
85		:- assert_must_succeed((F = and(globally(or(ap(p),next(globally(ap(q))))),globally(or(ap(p),next(globally(not(ap(q))))))),
86		is_safety_property_test(not(F),_NF))).
87		:- assert_must_fail((F = globally(implies(ap(request),finally(ap(alloc)))),
88		is_safety_property_test(not(F),_NF))).
89		:- assert_must_fail((F = globally(finally(ap(alloc))),
90		is_safety_property_test(not(F),_NF))).
91		:- assert_must_fail((F = globally(until(ap(request),finally(ap(alloc)))),
92		is_safety_property_test(not(F),_NF))).
93		:- assert_must_fail((F = implies(globally(finally(ap(send))),globally(finally(receive))),
94		is_safety_property_test(not(F),_NF))).
95		:- assert_must_fail((F = not(until(ap(p1),not(until(ap(p2),until(ap(p3),ap(p4)))))),
96		is_safety_property_test(not(F),_NF))).
97
98		is_safety_property_test(F,NF) :-
99		get_preference(use_safety_ltl_model_checker,Val),
100		set_preference(use_safety_ltl_model_checker,true),
101		is_safety_property(F,NF),
102		set_preference(use_safety_ltl_model_checker,Val).
103
104		is_safety_property(not(F),NF) :-
105		preference(use_safety_ltl_model_checker,true),
106		normalize_to_release_pnf(F,NF),
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(_)) :- !.
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		translate_to_ltl2ba_syntax(Ltl,Ltl1),
192		ltl2ba_init,
193		clear_automaton_facts,
194		(debug_mode(on) -> Verbose = true; Verbose = false),
195		c_call_ltl2ba(Ltl1,ltl_safety:assert_aut_initial_state,ltl_safety:assert_aut_finite_state,ltl_safety:assert_aut_transition,Verbose,ExitResult),
196		debug_print_ba_automaton,
197		(ExitResult = ok ->
198		load_and_check_safety_property(StartNodes,Result)
199		; ExitResult = error ->
200		add_error_fail(translating_ltl2ba,'An error appeared while translating LTL to BA for the following formula: ',Ltl1)
201		; otherwise ->
202		add_error_fail(translating_ltl2ba,'Unexpected error occurred while translating LTL to BA for the following formula: ',Ltl1)
203		).
204		ltl_mc_safety_property(_Ltl,_StarNodes,_Result) :-
205		add_error_fail(translating_ltl2ba,'Please ensure that ltl2ba is installed (see Help menu for ProB Tcl/Tk)','').
206
207		load_and_check_safety_property(StartNodes,Result) :-
208		%% start_mc_safety_property(random,StartNodes,Result).
209		start_mc_safety_property(breadth_first,StartNodes,Result).
210
211		is_ltl2ba_tool_installed :- is_ltl2ba_tool_installed(message).
212		is_ltl2ba_tool_installed(GenerateMsg) :-
213		host_platform(Platform),
214		get_platform_specifix_ltl2ba_library(Platform,File),
215		absolute_file_name(prob_lib(File),LTL2BALibrary),
216		(file_exists(LTL2BALibrary) ->
217		debug_println(9,'LTL2BA is installed.')
218		; GenerateMsg==message ->
219		add_message(translating_ltl2ba,
220		'ltl2ba-library archive could not be found in lib/ directory, install ltl2ba for faster model checking'),
221		fail
222		).
223
224		get_platform_specifix_ltl2ba_library(darwin,'ltl2ba.bundle'):- !.
225		get_platform_specifix_ltl2ba_library(linux,'ltl2ba.so') :- !.
226		get_platform_specifix_ltl2ba_library(windows,'ltl2ba.dll') :- !.
227		get_platform_specifix_ltl2ba_library(Unknown,_) :-
228		add_error_fail(translating_ltl2ba,'Unknown platform: ', Unknown).
229
230		:- public assert_aut_initial_state/1. % callback given to C
231		assert_aut_initial_state(StateDescription) :-
232		debug_println(9,asserting_initialstate(StateDescription)),
233		assert(aut_initial_state(StateDescription)).
234		:- public assert_aut_finite_state/1. % callback given to C
235		assert_aut_finite_state(StateDescription) :-
236		debug_println(9,asserting_finitestate(StateDescription)),
237		assert(aut_finite_state(StateDescription)).
238		:- public assert_aut_transition/3. % callback given to C
239		assert_aut_transition(Src,Atom,Dst) :-
240		atom_codes(Atom,Codes),
241		read_term_from_codes_exception(Codes,PrepRep,[]),
242		redefine_transition_label(PrepRep,Label),
243		debug_println(9,asserting_transition(aut_transition(Src,Label,Dst))),
244		assert(aut_transition(Src,Label,Dst)).
245
246		read_term_from_codes_exception(Codes,PrepRep,Options) :-
247		(read_term_from_codes(Codes,PrepRep,Options)
248		-> true
249		; atom_codes(Atom,Codes),
250		add_error(translating_ltl3ba_callback, 'Unexpected atom representation (does atom ends with fullstop?): ', Atom)
251		).
252
253		%redefine_automaton_facts :-
254		% aut_transition(Src,P,Dst),
255		% redefine_transition(Src,P,Dst),
256		% fail.
257		%redefine_automaton_facts.
258		%redefine_transition(Src,Predicate,Dst) :-
259		% retract(aut_transition(Src,Predicate,Dst)),
260		% redefine_transition_label(Predicate,Preposition),
261		% assert(aut_transition(Src,Preposition,Dst)).
262
263		redefine_transition_label(true,Res) :- !,
264		Res = true.
265		redefine_transition_label(false,Res) :- !,
266		Res = false.
267		redefine_transition_label(not(AP),Res) :-
268		ap_representation(AP,bpred(Pred)),!,
269		create_negation(Pred,NegPred),
270		create_atomic_b_predicate(NegPred,Res).
271		redefine_transition_label(AP,Res) :-
272		ap_representation(AP,Rep),!,
273		Res = ap(Rep).
274		redefine_transition_label(TP,Res) :-
275		tp_representation(TP,Rep),!,
276		Res = tp(Rep).
277		redefine_transition_label(F,Res) :-
278		F =.. [Functor|Args],
279		maplist(redefine_transition_label,Args,NewArgs),
280		Res =.. [Functor|NewArgs].
281
282		create_atomic_b_predicate(BPred,Res) :-
283		Res = ap(bpred(BPred)).
284
285		debug_print_ba_automaton :-
286		(debug_mode(on)
287		-> print_transitions_fail_loop
288		; true).
289
290		print_transitions_fail_loop :-
291		aut_transition(Src,Label,Dst),
292		print('Transition: '),print(Src),
293		translate_and_print_label(Label),
294		print(Dst),nl,fail.
295		print_transitions_fail_loop.
296
297		translate_and_print_label(Label) :-
298		pp_ba_label(Label,Atom,[]),
299		ajoin(Atom,Text),
300		print_label(Text).
301
302		%% pretty-printing predicate in Spin syntax (created just to test if ltl2ba produces the correct automaton)
303		pp_ba_label(true,['true'|S],S) :- !.
304		pp_ba_label(false,['false'|S],S) :- !.
305		pp_ba_label(ap(AP),[Atom|S],S) :- !,
306		pp_ap(AP,Atom).
307		pp_ba_label(tp(TP),[Atom|S],S) :- !,
308		pp_tp(TP,Atom).
309		pp_ba_label(not(Pred),['! ('|S],T) :- !,
310		pp_ba_label(Pred,S,[')'|T]).
311		pp_ba_label(and(Pred1,Pred2),['('|S],T) :- !,
312		pp_ba_label(Pred1,S,[' && '| S1]),
313		pp_ba_label(Pred2,S1,[')'|T]).
314		pp_ba_label(or(Pred1,Pred2),['('|S],T) :- !,
315		pp_ba_label(Pred1,S,[' || '| S1]),
316		pp_ba_label(Pred2,S1,[')'|T]).
317		pp_ba_label(Otherwise,['???'|S],S) :-
318		add_error(printing_ba_label_for_ltl2ba,'Non-expected label: ',Otherwise).
319
320		print_label(Label) :-
321		print(' --('),print(Label),print(')--> ').
322
323		translate_to_ltl2ba_syntax(Formula,Text) :-
324		retractall(ap_representation(_,_)),
325		retractall(tp_representation(_,_)),
326		retractall(tps_occurring),
327		pp_formula_to_ltl2ba_syntax(Formula,Text).
328
329		pp_formula_to_ltl2ba_syntax(Formula,Res) :-
330		pp_to_ltl2ba_syntax(Formula,Atoms,[]),
331		ajoin(Atoms,Res).
332
333		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
334		%%%%%%%%%%%%%%%%% Unit Tests %%%%%%%%%%%%%%%%%%%%%%
335		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
336
337		:- assert_must_succeed((F = and(or(true,false),true),
338		pp_formula_to_ltl2ba_syntax(F,Text),
339		Text = '((true || false) && true)')).
340		:- assert_must_succeed((F = implies(deadlock,not(true)),
341		pp_formula_to_ltl2ba_syntax(F,Text),
342		Text = '(deadlock -> ! true)')).
343		:- assert_must_succeed((F = not(until(true,next(implies(deadlock,not(true))))),
344		pp_formula_to_ltl2ba_syntax(F,Text),
345		Text = '! (true U X ((deadlock -> ! true)))')).
346		:- assert_must_succeed((F = weakuntil(true,false),
347		pp_formula_to_ltl2ba_syntax(F,Text),
348		Text = '((! true || false) V (true || false))')).
349		:- assert_must_succeed((F = globally(finally(true)),
350		pp_formula_to_ltl2ba_syntax(F,Text),
351		Text = '[] (<> (true))')).
352
353
354		pp_to_ltl2ba_syntax(true,['true'|S],S) :- !.
355		pp_to_ltl2ba_syntax(false,['false'|S],S) :- !.
356		pp_to_ltl2ba_syntax(deadlock,['deadlock'|S],S) :- !.
357		pp_to_ltl2ba_syntax(ap(X),[AP|S],S) :- !,
358		term_hash(X,Hash),
359		ajoin(['ap',Hash],AP),
360		(\+ap_representation(AP,_) -> assert(ap_representation(AP,X)); true).
361		pp_to_ltl2ba_syntax(action(X),[TP|S],S) :- !,
362		assert(tps_occurring),
363		term_hash(X,Hash),
364		ajoin(['tp',Hash],TP),
365		(\+tp_representation(TP,_) -> assert(tp_representation(TP,X)); true).
366		pp_to_ltl2ba_syntax(not(X),['! '|S],T) :- !,
367		pp_to_ltl2ba_syntax(X,S,T).
368		pp_to_ltl2ba_syntax(and(X,Y),['('|S],T) :- !,
369		pp_to_ltl2ba_syntax(X,S,[' && '|S1]),
370		pp_to_ltl2ba_syntax(Y,S1,[')'|T]).
371		pp_to_ltl2ba_syntax(or(X,Y),['('|S],T) :- !,
372		pp_to_ltl2ba_syntax(X,S,[' || '|S1]),
373		pp_to_ltl2ba_syntax(Y,S1,[')'|T]).
374		pp_to_ltl2ba_syntax(implies(X,Y),['('|S],T) :- !,
375		pp_to_ltl2ba_syntax(X,S,[' -> '|S1]),
376		pp_to_ltl2ba_syntax(Y,S1,[')'|T]).
377		pp_to_ltl2ba_syntax(next(X),['X ('|S],T) :- !,
378		pp_to_ltl2ba_syntax(X,S,[')'|T]).
379		pp_to_ltl2ba_syntax(globally(X),['[] ('|S],T) :- !,
380		pp_to_ltl2ba_syntax(X,S,[')'|T]).
381		pp_to_ltl2ba_syntax(finally(X),['<> ('|S],T) :- !,
382		pp_to_ltl2ba_syntax(X,S,[')'|T]).
383		pp_to_ltl2ba_syntax(until(X,Y),['('|S],T) :- !,
384		pp_to_ltl2ba_syntax(X,S,[' U '|S1]),
385		pp_to_ltl2ba_syntax(Y,S1,[')'|T]).
386		pp_to_ltl2ba_syntax(release(X,Y),['('|S],T) :- !,
387		pp_to_ltl2ba_syntax(X,S,[' V '|S1]),
388		pp_to_ltl2ba_syntax(Y,S1,[')'|T]).
389		pp_to_ltl2ba_syntax(weakuntil(X,Y),S,T) :- !,
390		pp_to_ltl2ba_syntax(release(or(not(X),Y),or(X,Y)),S,T).
391
392
393		%% Obsolete predicates (to be removed later)
394
395
396		%create_ba_pl_file(Text,Filename) :-
397		% write_string_to_file('prob_buchi_temp.pl',Filename,Text).
398		%
399		%write_string_to_file(BaseName,Filename,Machine) :-
400		% open(temp(BaseName),write,S,[if_exists(generate_unique_name),encoding('UTF-8')]),
401		% stream_property(S, file_name(Filename)),
402		% print_string(Machine,S),
403		% close(S).
404		%
405		%print_string([],_).
406		%print_string([C|Rest],S) :- put_code(S,C),print_string(Rest,S).
407
408