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 |