1 | % (c) 2009-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_tools,[temporal_parser/3,temporal_parser_l/3, | |
6 | parse_ltlfile/2,check_csp_event/4, | |
7 | parse_and_pp_ltl_formula/2, | |
8 | typecheck_temporal_formula/3,extract_formulas/4, | |
9 | preprocess_formula/2, | |
10 | preprocess_tp/2]). | |
11 | ||
12 | /* SICSTUS Libraries */ | |
13 | :- use_module(library(lists)). | |
14 | ||
15 | /* ProB Libraries */ | |
16 | % B | |
17 | :- use_module(probsrc(bsyntaxtree), [predicate_identifiers/2, get_texpr_type/2]). | |
18 | :- use_module(probsrc(bmachine),[b_type_expression/5, b_get_machine_operation/4]). | |
19 | % CSP | |
20 | :- use_module(probcspsrc(haskell_csp),[channel/2, channel_type_list/2,parse_single_csp_expression/3]). | |
21 | % utility modules | |
22 | :- use_module(probsrc(error_manager)). | |
23 | :- use_module(probsrc(debug)). | |
24 | :- use_module(probsrc(self_check)). | |
25 | :- use_module(probsrc(tools),[split_atom/3, string_concatenate/3]). | |
26 | % state space modules | |
27 | :- use_module(probsrc(state_space),[current_state_id/1]). | |
28 | :- use_module(probsrc(specfile),[animation_mode/1,csp_mode/0, csp_with_bz_mode/0]). | |
29 | % other | |
30 | :- use_module(probsrc(parsercall),[call_ltl_parser/3, parse_expression/2,parse_predicate/2]). | |
31 | /* Promela Tools */ | |
32 | %:- use_module(probpromela(promela_tools),[parse_promela_strings/4]). | |
33 | /* ProB LTL modules */ | |
34 | :- use_module(probltlsrc(ltl_translate)). | |
35 | ||
36 | :- use_module(probsrc(module_information),[module_info/2]). | |
37 | :- module_info(group,ltl). | |
38 | :- module_info(description,'This module provides utility predicates for the LTL and CTL model checkers.'). | |
39 | ||
40 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
41 | % parse an LTL or CTL formula | |
42 | % Mode: ltl or ctl | |
43 | temporal_parser(Formula,Mode,Result) :- | |
44 | temporal_parser_l([Formula],Mode,[Result]). | |
45 | ||
46 | temporal_parser_l(Formulas,Mode,Result) :- | |
47 | % call the Java parser for LTL | |
48 | call_ltl_parser(Formulas,Mode,Res1), | |
49 | % check if everything was fine | |
50 | check_syntax_result_l(Res1,Parsed,ParseFlag,Mode), ParseFlag=ok, | |
51 | % typecheck atomic propositions and such things | |
52 | typecheck_temporal_formula_l(Parsed,Result,TypeFlag), TypeFlag=ok. | |
53 | ||
54 | check_syntax_result_l([],[],_,_). | |
55 | check_syntax_result_l([R|Rrest],[F|Frest],Res,Mode) :- | |
56 | check_syntax_result(R,F,Res,Mode), | |
57 | check_syntax_result_l(Rrest,Frest,Res,Mode). | |
58 | check_syntax_result(ltl(F),F,_,_Mode). | |
59 | check_syntax_result(syntax_error(E),_,error,Mode) :- | |
60 | add_error(Mode,'Syntax error: ',E). | |
61 | ||
62 | typecheck_temporal_formula_l([],[],_). | |
63 | typecheck_temporal_formula_l([F|Frest],[R|Rrest],Res) :- | |
64 | typecheck_temporal_formula(F,R,Res), | |
65 | typecheck_temporal_formula_l(Frest,Rrest,Res). | |
66 | typecheck_temporal_formula(ap(AP),ap(Typed),Res) :- | |
67 | !,typecheck_ap(AP,Typed,Res). | |
68 | typecheck_temporal_formula(action(TP),action(Typed),Res) :- | |
69 | !,typecheck_tp(TP,Typed,Res). | |
70 | typecheck_temporal_formula(ena(TP,F),ena(Typed,R),Res) :- % used in CTL only | |
71 | !,typecheck_tp(TP,Typed,Res), | |
72 | typecheck_temporal_formula(F,R,Res). | |
73 | typecheck_temporal_formula(F,R,Res) :- | |
74 | F =.. [Functor|InArgs], | |
75 | same_length(InArgs,OutArgs), | |
76 | R =.. [Functor|OutArgs], | |
77 | typecheck_temporal_formula_l(InArgs,OutArgs,Res). | |
78 | ||
79 | typecheck_ap(BasicAP,AP,_Res) :- is_basic_ap(BasicAP),!,AP=BasicAP. | |
80 | typecheck_ap(enabled(TP),enabled(R),Res) :- | |
81 | !,typecheck_tp(TP,R,Res). | |
82 | typecheck_ap(available(TP),available(R),Res) :- | |
83 | !,typecheck_tp(TP,R,Res). | |
84 | typecheck_ap(weak_fair(TP),weak_fair(R),Res) :- | |
85 | !,typecheck_tp(TP,R,Res). | |
86 | typecheck_ap(strong_fair(TP),strong_fair(R),Res) :- | |
87 | !,typecheck_tp(TP,R,Res). | |
88 | typecheck_ap(dlk(TPList),dlk(R),Res) :- | |
89 | !,typecheck_tp_l(TPList,R,Res). | |
90 | typecheck_ap(ctrl(TPList),ctrl(R),Res) :- | |
91 | !,typecheck_tp_l(TPList,R,Res). | |
92 | typecheck_ap(det(TPList),det(R),Res) :- | |
93 | !,typecheck_tp_l(TPList,R,Res). | |
94 | typecheck_ap(bpred(Raw),bpred(Typed),Res) :- | |
95 | b_type_expression(Raw,[variables],pred,Typed,Errors), | |
96 | add_all_perrors(Errors,[],typecheck_atomic_property), | |
97 | ( no_real_perror_occurred(Errors) -> true | |
98 | ; otherwise -> Res=error). | |
99 | typecheck_ap(unparsed_pred(Atom),xtl_predicate_check(Atom),ResultFlag) :- | |
100 | ( animation_mode(xtl) -> true | |
101 | ; otherwise -> ResultFlag=error). | |
102 | ||
103 | is_basic_ap(deadlock). | |
104 | is_basic_ap(sink). | |
105 | is_basic_ap(current). | |
106 | is_basic_ap(stateid(_)). | |
107 | ||
108 | typecheck_tp(unparsed_trans(Op),xtl(Opname,Arity,Args),ResultFlag) :- | |
109 | animation_mode(xtl), !, | |
110 | ( compound(Op) -> functor(Op,Opname,Arity), Op =.. [_|Args] | |
111 | ; split_atom(Op,['.'],[Opname|Args]) -> | |
112 | length(Args,Arity) | |
113 | ; otherwise -> | |
114 | add_error(ltl,'Failed to parse operation specification'), | |
115 | ResultFlag = error). | |
116 | typecheck_tp(unparsed_trans(Opname),csp(Channel,Arity,ResArgs),ResultFlag) :- | |
117 | csp_mode,!, | |
118 | ( Opname = tick | |
119 | -> Channel=Opname, Arity=0, ResArgs=[] % should we set Arity ?? | |
120 | ; Opname = tau | |
121 | -> Channel=Opname, Arity=0, ResArgs=[] % should we set Arity ?? | |
122 | ; (split_atom(Opname,['.','!'],[Channel|Args]), channel(Channel,_)) | |
123 | -> | |
124 | (channel_type_list(Channel, TypeList),length(TypeList,Arity),length(Args,Arity) | |
125 | -> (Arity = 0 | |
126 | -> ResArgs = [] | |
127 | ; (\+memberchk('_',Args) % we want to call the CSP-M parser only once when there is no '_' symbol in Args | |
128 | -> mergeArgsToDotTuple([Channel|Args],DotTupleEvent), | |
129 | parse_single_csp_expression(ltl,DotTupleEvent,ParsedEvent), | |
130 | splitToSingleArgs(ParsedEvent,[Channel|ResArgs],Arity) | |
131 | ; l_parse_single_csp_expression_undescore(ltl,Args,ResArgs) | |
132 | ) | |
133 | ) | |
134 | ; add_error(ltl,'Number of arguments not correct for: ', Opname), | |
135 | ResultFlag=error, ResArgs=[], Arity = 0 | |
136 | ) | |
137 | ; otherwise | |
138 | -> add_error(ltl,'Channel does not exist: ',Opname), | |
139 | ResultFlag = error, ResArgs=[], Arity = 0 | |
140 | ). | |
141 | typecheck_tp(bop(oppattern(_Pos,Name,Args)),Result,ResultFlag) :- | |
142 | ( b_get_machine_operation(Name,Results,Parameters,_) -> | |
143 | Result = bop(Name,NumberArgs,NumberResults,ArgPatterns,ResPatterns), | |
144 | length(Parameters,NumberArgs), length(Results,NumberResults), | |
145 | % Pattern matching for results is not yet supported | |
146 | ResPatterns = [], | |
147 | ( Args=[] -> | |
148 | ArgPatterns = [], | |
149 | ResPatterns = [] | |
150 | ; length(Args,NumberArgs) -> | |
151 | create_b_op_patterns(Args,Parameters,ArgPatterns,ResultFlag) | |
152 | ; otherwise -> | |
153 | add_error(ltl,'Number of arguments not correct for: ', Name),ResultFlag=error) | |
154 | ; csp_mode, Args=[] -> | |
155 | debug_println(9,unparsed_trans(Name)), | |
156 | typecheck_tp(unparsed_trans(Name),Result,ResultFlag) | |
157 | ; otherwise -> | |
158 | add_error(ltl,'Could not find operation: ', Name),ResultFlag=error). | |
159 | typecheck_tp(btrans(event(Name)),btrans(event(Name)),_ResultFlag) :- !. | |
160 | typecheck_tp(btrans(event(Name,RawPredicate)),btrans(event(Name,TPredicate,Poststate)),ResultFlag) :- | |
161 | ( b_get_machine_operation(Name,_,_Parameters,_) -> | |
162 | ( bmachine:type_with_errors(RawPredicate,[prepost,operation(Name)],pred,TPredicate) -> | |
163 | find_poststate_access(TPredicate,Poststate) | |
164 | ; otherwise -> ResultFlag=error) | |
165 | ; otherwise -> | |
166 | add_error(ltl,'Could not find operation: ', Name),ResultFlag=error). | |
167 | ||
168 | typecheck_tp_l([],[],_Res). | |
169 | typecheck_tp_l([TP|TPs],[TTP|TTPs],Res) :- | |
170 | typecheck_tp(TP,TTP,ResultFlag), | |
171 | (ResultFlag == error -> Res = error | |
172 | ; otherwise -> Res=Res1), | |
173 | typecheck_tp_l(TPs,TTPs,Res1). | |
174 | ||
175 | :- use_module(probsrc(bsyntaxtree),[syntaxtraversion/6]). | |
176 | find_poststate_access(TExpr,Poststate) :- | |
177 | find_poststate_access2(TExpr,P,[]), | |
178 | sort(P,Poststate). | |
179 | find_poststate_access2(TExpr) --> | |
180 | {syntaxtraversion(TExpr,Expr,_,Infos,Subs,_)}, | |
181 | find_poststate_access3(Expr,Infos), | |
182 | find_poststate_access_l(Subs). | |
183 | find_poststate_access3(identifier(Id),Infos) --> | |
184 | {memberchk(poststate,Infos),!,atom_concat(Orig,'\'',Id)}, | |
185 | [poststate(Orig,Id)]. | |
186 | find_poststate_access3(_,_) --> []. | |
187 | find_poststate_access_l([]) --> !. | |
188 | find_poststate_access_l([TExpr|Rest]) --> | |
189 | find_poststate_access2(TExpr), | |
190 | find_poststate_access_l(Rest). | |
191 | ||
192 | /* Parsing CSP expressions where '_' will be not parsed */ | |
193 | parse_single_csp_expression_undescore(Context,Expr,Res) :- | |
194 | (Expr=='_' -> Res = Expr; parse_single_csp_expression(Context,Expr,Res)). | |
195 | ||
196 | l_parse_single_csp_expression_undescore(Context,LExpr,LRes) :- | |
197 | maplist(parse_single_csp_expression_undescore(Context),LExpr,LRes). | |
198 | /*******************************************************/ | |
199 | ||
200 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
201 | % do some preprocessing on a formula: | |
202 | % - insert current state id | |
203 | % - rewrite CSP declarations in some cases | |
204 | ||
205 | preprocess_formula(In,Out) :- | |
206 | ( preprocess_formula2(In,Out) -> true | |
207 | ; otherwise -> | |
208 | add_error(ltl,'preprocessing formula failed: ',In),fail). | |
209 | ||
210 | :- assert_must_succeed(preprocess_formula2(globally(next(false)),false)). | |
211 | :- assert_must_succeed(preprocess_formula2(globally(next(next(true))),globally(true))). | |
212 | :- assert_must_succeed(preprocess_formula2(finally(next(true)),true)). | |
213 | :- assert_must_succeed(preprocess_formula2(finally(next(next(false))),finally(false))). | |
214 | ||
215 | % base cases | |
216 | preprocess_formula2(ap(A),ap(B)) :- !, | |
217 | (A=bpred(Pred) -> | |
218 | predicate_identifiers(Pred,Ids), | |
219 | debug_println(predicate_identifiers(A,Ids)) | |
220 | ; true), | |
221 | preprocess_ap(A,B). | |
222 | preprocess_formula2(action(A),action(B)) :- !,preprocess_tp(A,B). | |
223 | preprocess_formula2(ena(SpecA,FA),action(SpecB,FB)) :- | |
224 | !,preprocess_tp(SpecA,SpecB),preprocess_formula2(FA,FB). | |
225 | % (X true = true) and (X false = false) | |
226 | preprocess_formula2(next(F),PNextF) :- | |
227 | !,preprocess_formula2(F,PF), | |
228 | (PF = true -> PNextF = true | |
229 | ;PF = false -> PNextF = false | |
230 | ; otherwise -> PNextF = next(PF)). | |
231 | % idempotency laws | |
232 | preprocess_formula2(globally(globally(F)),globally(PF)) :- | |
233 | !,preprocess_formula2(F,PF). | |
234 | preprocess_formula2(finally(finally(F)),finally(PF)) :- | |
235 | !,preprocess_formula2(F,PF). | |
236 | preprocess_formula2(until(F,until(F,G)),until(PF,PG)) :- | |
237 | !,preprocess_formula2(F,PF), | |
238 | preprocess_formula2(G,PG). | |
239 | preprocess_formula2(until(until(F,G),G),until(PF,PG)) :- | |
240 | !,preprocess_formula2(F,PF), | |
241 | preprocess_formula2(G,PG). | |
242 | % absorption laws | |
243 | preprocess_formula2(finally(globally(finally(F))),globally(finally(PF))) :- | |
244 | !,preprocess_formula2(F,PF). | |
245 | preprocess_formula2(globally(finally(globally(F))),finally(globally(PF))) :- | |
246 | !,preprocess_formula2(F,PF). | |
247 | % F (f U g) == F g | |
248 | preprocess_formula2(finally(until(_F,G)),finally(PG)) :- | |
249 | !,preprocess_formula2(G,PG). | |
250 | % G (f R g) == G g | |
251 | preprocess_formula2(globally(release(_F,G)),globally(PG)) :- | |
252 | !,preprocess_formula2(G,PG). | |
253 | % F true = true | |
254 | preprocess_formula2(finally(F),PFinallyF) :- | |
255 | !,preprocess_formula2(F,PF), | |
256 | (PF = true -> PFinallyF = true | |
257 | ; otherwise -> PFinallyF = finally(PF)). | |
258 | % G false = false | |
259 | preprocess_formula2(globally(F),PGloballyF) :- | |
260 | !,preprocess_formula2(F,PF), | |
261 | (PF = false -> PGloballyF = false | |
262 | ; otherwise -> PGloballyF = globally(PF)). | |
263 | % otherwise | |
264 | preprocess_formula2(Term,NewTerm) :- | |
265 | functor(Term,Functor,Arity), | |
266 | functor(NewTerm,Functor,Arity), | |
267 | preprocess_formula_args(Arity,Term,NewTerm). | |
268 | ||
269 | preprocess_formula_args(0,_,_) :- !. | |
270 | preprocess_formula_args(N,Term,NewTerm) :- | |
271 | arg(N,Term,Arg), | |
272 | arg(N,NewTerm,NewArg), | |
273 | preprocess_formula2(Arg,NewArg), | |
274 | N2 is N-1, | |
275 | preprocess_formula_args(N2,Term,NewTerm). | |
276 | ||
277 | preprocess_ap(current,stateid(StateId)) :- !, | |
278 | current_state_id(StateId). | |
279 | preprocess_ap(enabled(A),enabled(B)) :- !, | |
280 | preprocess_tp(A,B). | |
281 | preprocess_ap(AP,AP). | |
282 | ||
283 | preprocess_tp(csp(Channel,Arity,CspArgs), | |
284 | bop(Channel,NumberArgs,NumberResults,ArgPatterns,ResPatterns)) :- | |
285 | csp_with_bz_mode, | |
286 | b_get_machine_operation(Channel,Results,Parameters,_Body), | |
287 | !, | |
288 | % check if more arguments are specified that allowed | |
289 | length(Parameters,NumberArgs), | |
290 | length(Results,NumberResults), | |
291 | MaxNumberAllowed is NumberArgs + NumberResults, | |
292 | ( Arity > MaxNumberAllowed -> | |
293 | add_error(ltl,'Too many arguments for LTL/CTL channel: ', Channel),fail | |
294 | ; Arity =< NumberResults -> | |
295 | ParamArgs = CspArgs,ResArgs = [] | |
296 | ; otherwise -> | |
297 | MinArgs is min(NumberArgs,Arity), | |
298 | append_length(ParamArgs,ResArgs,CspArgs,MinArgs)), | |
299 | csp_arguments(ParamArgs,1,Parameters,ArgPatterns,Exprs1), | |
300 | csp_arguments(ResArgs,1,Results,ResPatterns,Exprs2), | |
301 | append(Exprs1,Exprs2,Exprs), | |
302 | parse_preds_exprs(Exprs). | |
303 | preprocess_tp(TP,TP). | |
304 | ||
305 | csp_arguments([],_Index,_Parameters,[],[]). | |
306 | csp_arguments([P|ParamArgs],Index,[Param|ParamRest],ArgPatterns,Exprs) :- | |
307 | ( is_csp_placeholder(P) -> | |
308 | ArgPatterns = ArgPatternsRest, | |
309 | Exprs = ExprsRest | |
310 | ; otherwise -> | |
311 | ArgPatterns = [Index/ArgPattern|ArgPatternsRest], | |
312 | Exprs = [Expr|ExprsRest], | |
313 | csp_argument(P,Param,ArgPattern,Expr)), | |
314 | I2 is Index+1, | |
315 | csp_arguments(ParamArgs,I2,ParamRest,ArgPatternsRest,ExprsRest). | |
316 | csp_argument(Argument,Parameter,ParsedExpr,expr(ToParse,Type,ParsedExpr)) :- | |
317 | get_texpr_type(Parameter,Type), | |
318 | atom_codes(Argument,ToParse). | |
319 | ||
320 | is_csp_placeholder('_'). | |
321 | is_csp_placeholder('?'). | |
322 | ||
323 | % currently not called: nor is unparsed_ap called | |
324 | %translate_preds(In,Out) :- | |
325 | % unparsed_ap_l(In,Out,Translation,[]), | |
326 | % parse_preds_exprs(Translation). | |
327 | ||
328 | parse_preds_exprs([]) :- !. % nothing to parse | |
329 | parse_preds_exprs(Translation) :- | |
330 | split_preds(Translation,PredStrings,Preds,ExprStrings,Exprs), | |
331 | animation_mode(AnimMode), | |
332 | parse_preds_exprs2(AnimMode,PredStrings,Preds,ExprStrings,Exprs). | |
333 | ||
334 | % default: parse the predicates and expressions as B | |
335 | parse_preds_exprs2(_,PredStrings,Preds,ExprStringsWithTypes,Exprs) :- | |
336 | annotate_ap_type(Preds,bpred,BPreds), | |
337 | split_exprs_types(ExprStringsWithTypes,ExprStrings,Types), | |
338 | maplist(parse_expression,ExprStrings,UExprs), | |
339 | maplist(parse_predicate,PredStrings,UPreds), | |
340 | type_exprs(UExprs,Types,Exprs,EErrors), | |
341 | type_preds(UPreds,BPreds,PErrors), | |
342 | append(EErrors,PErrors,Errors), | |
343 | add_all_perrors(Errors,[],type_error). | |
344 | ||
345 | split_exprs_types([],[],[]). | |
346 | split_exprs_types([Expr/Type|ETRest],[Expr|ERest],[Type|TRest]) :- | |
347 | split_exprs_types(ETRest,ERest,TRest). | |
348 | ||
349 | type_exprs([],[],[],[]). | |
350 | type_exprs([Expr|Erest],[Type|TypeRest],[Typed|Trest],Errors) :- | |
351 | b_type_expression(Expr,[variables],Type,Typed,LErrors), | |
352 | append(LErrors,ErrorRest,Errors), | |
353 | type_exprs(Erest,TypeRest,Trest,ErrorRest). | |
354 | type_preds([],[],[]). | |
355 | type_preds([Pred|Prest],[Typed|Trest],Errors) :- | |
356 | b_type_expression(Pred,[variables],pred,Typed,LErrors), | |
357 | append(LErrors,ErrorRest,Errors), | |
358 | type_preds(Prest,Trest,ErrorRest). | |
359 | ||
360 | annotate_ap_type([],_,[]). | |
361 | annotate_ap_type([AP|APrest],Type,[R|Rrest]) :- | |
362 | functor(AP,Type,1),arg(1,AP,R), | |
363 | annotate_ap_type(APrest,Type,Rrest). | |
364 | ||
365 | ||
366 | ||
367 | split_preds([],[],[],[],[]). | |
368 | split_preds([pred(A,B)|Rest],[A|ARest],[B|BRest],X,Y) :- !, | |
369 | split_preds(Rest,ARest,BRest,X,Y). | |
370 | split_preds([expr(A,T,B)|Rest],X,Y,[A/T|ARest],[B|BRest]) :- | |
371 | split_preds(Rest,X,Y,ARest,BRest). | |
372 | ||
373 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
374 | % parse a file with several LTL formulas: | |
375 | ||
376 | parse_ltlfile(Filename, Formulas) :- | |
377 | ( parse_ltlfile2(Filename,Formulas) -> true | |
378 | ; otherwise -> | |
379 | add_error(ltl, 'Error while parsing the LTL formula file')). | |
380 | parse_ltlfile2(Filename, Formulas) :- | |
381 | read_file(Filename,Codes), | |
382 | parse_lines(Lines,Codes,[]), | |
383 | parse_sections(Raws,Lines,[]), | |
384 | parse_file_formulas(Raws,Formulas). | |
385 | parse_file_formulas(In,Out) :- | |
386 | extract_formulas(In,Strings,Parsed,Out), | |
387 | temporal_parser_l(Strings,ltl,Parsed). | |
388 | ||
389 | extract_formulas([],[],[],[]). | |
390 | extract_formulas([formula(Name,Raw)|Rin],[Raw|Rraw], | |
391 | [Parsed|Rparsed],[formula(Name,Parsed)|Rout]) :- | |
392 | extract_formulas(Rin,Rraw,Rparsed,Rout). | |
393 | ||
394 | /* | |
395 | parse_file2([]) --> []. | |
396 | parse_file2([F|Rest]) --> | |
397 | parse_section(F), | |
398 | parse_file2(Rest). */ | |
399 | ||
400 | parse_sections([formula(Name,F)|Rest]) --> | |
401 | munch_comments, | |
402 | [header(Name)], | |
403 | parse_section_formulas("",FCodes),!, | |
404 | { atom_codes(F,FCodes) }, | |
405 | parse_sections(Rest). | |
406 | parse_sections([]) --> []. | |
407 | ||
408 | munch_comments --> [comment(_)],!,munch_comments. | |
409 | munch_comments --> []. | |
410 | ||
411 | parse_section_formulas(Prev,F) --> | |
412 | munch_comments, | |
413 | [formula(Snippet)],!, | |
414 | {(Prev==[] -> S2=Snippet; append("\n",Snippet,S2) ),append(Prev,S2,F2)}, | |
415 | parse_section_formulas(F2,F). | |
416 | parse_section_formulas(F,F) --> munch_comments,[]. | |
417 | ||
418 | parse_lines([]) --> []. | |
419 | parse_lines([L|Rest]) --> | |
420 | parse_line(L), | |
421 | parse_lines(Rest). | |
422 | ||
423 | parse_line(comment(C)) --> | |
424 | pl_spaces, | |
425 | "#",!, | |
426 | pl_until_newline(C). | |
427 | parse_line(comment("")) --> | |
428 | pl_spaces, | |
429 | pl_newline,!. | |
430 | parse_line(header(Title)) --> | |
431 | pl_title(Title), | |
432 | pl_spaces, pl_newline, !. | |
433 | parse_line(formula([C|F])) --> | |
434 | % no empty formulas | |
435 | [C], | |
436 | pl_until_newline(F). | |
437 | ||
438 | pl_title(Title) --> | |
439 | "[", pl_spaces, pl_title2(T), {atom_codes(Title,T)}. | |
440 | pl_title2([]) --> pl_spaces,"]",!. | |
441 | pl_title2([]) --> pl_newline,!,{fail}. % maybe an exception? | |
442 | pl_title2([C|Rest]) --> [C],pl_title2(Rest). | |
443 | ||
444 | pl_spaces --> " ",!,pl_spaces. | |
445 | pl_spaces --> "\t",!,pl_spaces. | |
446 | pl_spaces --> []. | |
447 | ||
448 | pl_until_newline([]) --> pl_newline,!. | |
449 | pl_until_newline([C|Rest]) --> [C],!,pl_until_newline(Rest). | |
450 | pl_until_newline([]) --> []. | |
451 | ||
452 | pl_newline --> "\n\r",!. | |
453 | pl_newline --> "\n",!. | |
454 | pl_newline --> "\r". | |
455 | ||
456 | read_file(Filename,Codes) :- | |
457 | open(Filename,read,S,[encoding('UTF-8')]), | |
458 | read_codes(S,Codes), | |
459 | close(S). | |
460 | read_codes(S,Codes) :- | |
461 | get_code(S,Code), | |
462 | ( Code < 0 -> | |
463 | Codes = [] | |
464 | ; otherwise -> | |
465 | Codes = [Code|Rest], | |
466 | read_codes(S,Rest)). | |
467 | ||
468 | create_b_op_patterns(Args,Parameters,ArgPatterns,Res) :- | |
469 | create_b_op_patterns2(Args,Parameters,ArgPatterns,1,Res). | |
470 | create_b_op_patterns2([],[],[],_,_). | |
471 | create_b_op_patterns2([Arg|ARest],[Param|ParamRest],Patterns,Index,Res) :- | |
472 | create_b_op_pattern(Arg,Param,Pattern,Res), | |
473 | ( var(Pattern) -> Patterns = PRest | |
474 | ; otherwise -> Patterns = [Index/Pattern|PRest]), | |
475 | Index2 is Index+1, | |
476 | create_b_op_patterns2(ARest,ParamRest,PRest,Index2,Res). | |
477 | create_b_op_pattern(undef(_Pos),_,_,_). | |
478 | create_b_op_pattern(def(_Pos,Raw),TParam,Typed,Res) :- | |
479 | get_texpr_type(TParam,Type), | |
480 | b_type_expression(Raw,[variables],Type,Typed,Errors), | |
481 | add_all_perrors(Errors,[],typecheck_operation_argument), | |
482 | ( no_real_perror_occurred(Errors) -> true | |
483 | ; otherwise -> Res=error). | |
484 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
485 | ||
486 | parse_and_pp_ltl_formula(FormulaAsAtom,Text) :- | |
487 | temporal_parser(FormulaAsAtom,ltl,Ltl), | |
488 | ( pp_ltl_formula(Ltl,Text) | |
489 | -> true | |
490 | ; add_error_fail(ltl, 'Failed to pretty print LTL formula: ', Ltl) | |
491 | ). | |
492 | ||
493 | %%%%%%%% Other predicates %%%%%%%%%% | |
494 | ||
495 | :- assert_must_succeed((ltl_tools: mergeArgsToDotTuple([1,2,'<bob,alice>','{bob}'],Res), Res = '1.2.<bob,alice>.{bob}')). | |
496 | :- assert_must_succeed((ltl_tools: mergeArgsToDotTuple(['(bob,alice)'],Res), Res = '(bob,alice)')). | |
497 | :- assert_must_succeed(ltl_tools: mergeArgsToDotTuple([],'')). | |
498 | ||
499 | mergeArgsToDotTuple(List,Res) :- mergeArgsToDotTuple(List,'',Res). | |
500 | ||
501 | mergeArgsToDotTuple([],Str,Str). | |
502 | mergeArgsToDotTuple([H|T],Str,Res) :- | |
503 | (T\=[] -> string_concatenate(H,'.',HRes) ; HRes=H), | |
504 | string_concatenate(Str,HRes,StrRes),mergeArgsToDotTuple(T,StrRes,Res). | |
505 | ||
506 | splitToSingleArgs(dotTuple(List),List,Arity) :- | |
507 | N is Arity +1, | |
508 | length(List,N). | |
509 | splitToSingleArgs(X,[X],0). | |
510 | splitToSingleArgs(X,_L,N) :- | |
511 | add_internal_error('Internal Error: Arity does not match for channel: ',X/N). | |
512 | ||
513 | :- assert_must_succeed((check_csp_event(tick,0,[],R), R=tick(_))). | |
514 | :- assert_must_succeed((check_csp_event(tau,0,[],R), R=tau(_))). | |
515 | :- assert_must_fail(check_csp_arguments([setValue([alice,bob]),tupleExp([s,t,u])], [setValue([alice,bob]),in(na_tuple([s,t]))],some_event)). | |
516 | :- assert_must_succeed(check_csp_arguments([setValue([alice,bob]),tupleExp([s,t,u])], [setValue([alice,bob]),in(na_tuple([s,t,u]))],some_event)). | |
517 | :- assert_must_succeed(check_csp_arguments([setValue([bob,alice]),tupleExp([s,t,u])], [setValue([alice,bob]),in(na_tuple([s,t,u]))],some_event)). | |
518 | :- assert_must_succeed(check_csp_arguments([a,'_','_'],[in(a),in(int(10)),in(int(20))],true)). | |
519 | ||
520 | %% Predicate check csp event | |
521 | check_csp_event(tick,0,[],R) :- !, R=tick(_). | |
522 | check_csp_event(tau,0,[],R) :- !, R=tau(_). | |
523 | check_csp_event(Event,Arity,PatArgs,io(Vals,Event,_SrcSpan)) :- !, | |
524 | (channel(Event,_) -> | |
525 | ((channel_type_list(Event,List),length(List,Arity)) -> | |
526 | check_csp_arguments(PatArgs,Vals,Event) | |
527 | ; otherwise -> add_error(ltl,'Internal Error: Missing/extra arguments in CSP LTL/CTL pattern: ',Event:PatArgs),fail | |
528 | ) | |
529 | ; otherwise -> add_internal_error('Internal Error: Channel not defined: ',Event/Arity)). | |
530 | ||
531 | :- block check_csp_arguments(?,-,?). | |
532 | check_csp_arguments([],[],_). | |
533 | check_csp_arguments([],[H|T],Event) :- | |
534 | print('* Missing arguments in CSP LTL/CTL pattern (use .?): '),print(Event), | |
535 | print(' : '),print([H|T]),nl. | |
536 | check_csp_arguments([H|T],[],Event) :- | |
537 | add_error(ltl,'Extra arguments in CSP LTL/CTL pattern: ',Event:[H|T]),fail. | |
538 | check_csp_arguments([H|T],[PatH|PatT],Event) :- | |
539 | check_csp_arg(H,PatH),!, | |
540 | check_csp_arguments(T,PatT,Event). | |
541 | ||
542 | check_csp_arg(X,Y) :- | |
543 | var(Y),!, | |
544 | add_internal_error('Internal Error: Event argument was a variable, expected to be: ',X). | |
545 | check_csp_arg('_',_Y). % underscore should match any argument | |
546 | check_csp_arg(X,in(Y)) :- | |
547 | check_csp_arg(X,Y). | |
548 | check_csp_arg(X,out(Y)) :- | |
549 | check_csp_arg(X,Y). | |
550 | ||
551 | check_csp_arg(list(L),list(L1)) :- !, | |
552 | l_check_csp_arg(L,L1,list). | |
553 | check_csp_arg(setValue(L),setValue(L1)) :- !, | |
554 | sort(L,R), | |
555 | sort(L1,R1), | |
556 | l_check_csp_arg(R,R1,setValue). % elements order is not important within set expressions | |
557 | check_csp_arg(tupleExp(L),na_tuple(L1)) :- !, | |
558 | l_check_csp_arg(L,L1,na_tuple). | |
559 | check_csp_arg(X,Y) :- eq_csp_val(Y,X). | |
560 | ||
561 | eq_csp_val(int(X),int(Y)) :- !, Y=X. | |
562 | eq_csp_val(X,X). | |
563 | ||
564 | l_check_csp_arg([],[],_):- !. | |
565 | l_check_csp_arg([],[H|T],Functor) :- | |
566 | add_error_fail(ltl,'Missing elements in CSP LTL pattern: ',Functor:[H|T]). | |
567 | l_check_csp_arg([H|T],[H1|T1],Functor) :- | |
568 | check_csp_arg(H,H1),!, | |
569 | l_check_csp_arg(T,T1,Functor). |