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).