1		% (c) 2009-2024 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,
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, get_primed_machine_variables/1]).
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		:- use_module(probsrc(tools_files),[read_file_codes/2]).
27		:- use_module(probsrc(preferences),[get_preference/2]).
28		% state space modules
29		:- use_module(probsrc(state_space),[current_state_id/1]).
30		:- use_module(probsrc(specfile),[animation_mode/1,csp_mode/0, csp_with_bz_mode/0, b_or_z_mode/0, xtl_mode/0]).
31		% other
32		:- use_module(probsrc(parsercall),[call_ltl_parser/3, parse_expression/2,parse_predicate/2]).
33		/* Promela Tools */
34		%:- use_module(probpromela(promela_tools),[parse_promela_strings/4]).
35		/* ProB LTL modules */
36		:- use_module(probltlsrc(ltl_translate)).
37
38		:- use_module(probsrc(module_information),[module_info/2]).
39		:- module_info(group,ltl).
40		:- module_info(description,'This module provides utility predicates for the LTL and CTL model checkers.').
41
42		:- set_prolog_flag(double_quotes, codes).
43
44		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
45		% parse an LTL or CTL formula
46		% Mode: ltl or ctl
47		temporal_parser(Formula,Mode,Result) :-
48		temporal_parser_l([Formula],Mode,[Result]).
49
50		temporal_parser_l(Formulas,Mode,Result) :-
51		% call the Java parser for LTL
52		call_ltl_parser(Formulas,Mode,Res1),
53		% check if everything was fine
54		check_syntax_result_l(Res1,Parsed,ParseFlag,Mode), ParseFlag=ok,
55		% typecheck atomic propositions and such things
56		%tools_printing:nested_print_term(Parsed,10),
57		typecheck_temporal_formula_l(Parsed,Result,TypeFlag), TypeFlag=ok.
58
59		check_syntax_result_l([],[],_,_).
60		check_syntax_result_l([R|Rrest],[F|Frest],Res,Mode) :-
61		check_syntax_result(R,F,Res,Mode),
62		check_syntax_result_l(Rrest,Frest,Res,Mode).
63		check_syntax_result(ltl(F),F,_,_Mode).
64		check_syntax_result(syntax_error(E),_,error,Mode) :-
65		add_error(Mode,'Syntax error: ',E).
66
67		typecheck_temporal_formula_l([],[],_).
68		typecheck_temporal_formula_l([F|Frest],[R|Rrest],Res) :-
69		typecheck_temporal_formula(F,R,Res),
70		typecheck_temporal_formula_l(Frest,Rrest,Res).
71		typecheck_temporal_formula(ap(AP),ap(Typed),Res) :-
72		!,typecheck_ap(AP,Typed,Res).
73		typecheck_temporal_formula(action(TP),action(Typed),Res) :-
74		!,typecheck_tp(TP,Typed,Res).
75		typecheck_temporal_formula(ena(TP,F),ena(Typed,R),Res) :- % used in CTL only
76		!,typecheck_tp(TP,Typed,Res),
77		typecheck_temporal_formula(F,R,Res).
78		%typecheck_temporal_formula(forall(ID,LHSAP,RHS),forall(ID,LR,RR),Res) :-
79		% !, % TO DO: LHSAP is a B Predicate, add ID to the typing environment for LHS and RHS
80		% typecheck_temporal_formula(LHSAP,LR),
81		% typecheck_temporal_formula(RHS,RR).
82		typecheck_temporal_formula(F,R,Res) :-
83		F =.. [Functor|InArgs],
84		same_length(InArgs,OutArgs),
85		R =.. [Functor|OutArgs],
86		typecheck_temporal_formula_l(InArgs,OutArgs,Res).
87
88		typecheck_ap(BasicAP,AP,_Res) :- is_basic_ap(BasicAP),!,AP=BasicAP.
89		typecheck_ap(enabled(TP),enabled(R),Res) :-
90		!,typecheck_tp(TP,R,Res).
91		typecheck_ap(available(TP),available(R),Res) :-
92		!,typecheck_tp(TP,R,Res).
93		typecheck_ap(weak_fair(TP),weak_fair(R),Res) :-
94		!,typecheck_tp(TP,R,Res).
95		typecheck_ap(strong_fair(TP),strong_fair(R),Res) :-
96		!,typecheck_tp(TP,R,Res).
97		typecheck_ap(dlk(TPList),dlk(R),Res) :-
98		!,typecheck_tp_l(TPList,R,Res).
99		typecheck_ap(ctrl(TPList),ctrl(R),Res) :-
100		!,typecheck_tp_l(TPList,R,Res).
101		typecheck_ap(det(TPList),det(R),Res) :-
102		!,typecheck_tp_l(TPList,R,Res).
103		typecheck_ap(bpred(Raw),bpred(Typed),Res) :- !,
104		type_check_raw(Raw,pred,Typed,Res).
105		typecheck_ap(unparsed_pred(Atom),xtl_predicate_check(Atom),ResultFlag) :- !,
106		(animation_mode(xtl) -> true ; ResultFlag=error).
107		typecheck_ap(F,R,Res) :-
108		add_internal_error('Illegal LTL atomic proposition:',typecheck_ap(F,R,Res)),fail.
109
110		typecheck_expr(bexpr(E),TE,Type,Res) :- !,
111		type_check_raw(E,Type,TE,Res),
112		(Type=pred -> add_error(ltl,'Expression expected, but was predicate:',TE), Res=error
113		; true).
114		typecheck_expr(F,R,T,Res) :-
115		add_internal_error('Illegal LTL atomic expression:',typecheck_expr(F,R,T,Res)),fail.
116
117
118		%typecheck_pred(bpred(E),TE,Type,Res) :- !,
119		% type_check_raw(E,Type,TE,Res),
120		% (Type=pred -> true
121		% ; add_error(ltl,'Predicate expected, but was expression:',TE), Res=error
122		% ).
123		%typecheck_pred(F,R,T,Res) :-
124		% add_internal_error('Illegal LTL atomic predicate:',typecheck_pred(F,R,T,Res)),fail.
125
126
127		type_check_raw(Raw,Type,Typed,Res) :-
128		b_type_expression_for_ltl(Raw,Type,Typed0,Errors),
129		add_all_perrors(Errors,[],typecheck_atomic_property),
130		(no_real_perror_occurred(Errors)
131		-> inline_prob_deferred_set_elements_into_bexpr(Typed0,Typed)
132		; Typed=Typed0, Res=error).
133
134		is_basic_ap(deadlock).
135		is_basic_ap(det_output).
136		is_basic_ap(sink).
137		is_basic_ap(goal).
138		is_basic_ap(state_error).
139		is_basic_ap(current).
140		is_basic_ap(stateid(_)).
141
142		:- use_module(probsrc(b_global_sets),[inline_prob_deferred_set_elements_into_bexpr/2]).
143
144		typecheck_tp(unparsed_trans(Op),xtl(Opname,Arity,Args),ResultFlag) :-
145		animation_mode(xtl), !,
146		( compound(Op) -> functor(Op,Opname,Arity), Op =.. [_|Args]
147		; split_atom(Op,['.'],[Opname|Args]) ->
148		length(Args,Arity)
149		;
150		add_error(ltl,'Failed to parse operation specification'),
151		ResultFlag = error).
152		typecheck_tp(unparsed_trans(Opname),csp(Channel,Arity,ResArgs),ResultFlag) :-
153		csp_mode,!,
154		( Opname = tick
155		-> Channel=Opname, Arity=0, ResArgs=[] % should we set Arity ??
156		; Opname = tau
157		-> Channel=Opname, Arity=0, ResArgs=[] % should we set Arity ??
158		; (split_atom(Opname,['.','!'],[Channel|Args]), channel(Channel,_))
159		->
160		(channel_type_list(Channel, TypeList),length(TypeList,Arity),length(Args,Arity)
161		-> (Arity = 0
162		-> ResArgs = []
163		; (\+memberchk('_',Args)
164		% we want to call the CSP-M parser only once when there is no '_' symbol in Args
165		-> mergeArgsToDotTuple([Channel|Args],DotTupleEvent),
166		parse_single_csp_expression(ltl,DotTupleEvent,ParsedEvent),
167		splitToSingleArgs(ParsedEvent,[Channel|ResArgs],Arity)
168		; l_parse_single_csp_expression_undescore(ltl,Args,ResArgs)
169		)
170		)
171		; add_error(ltl,'Number of arguments not correct for: ', Opname),
172		ResultFlag=error, ResArgs=[], Arity = 0
173		)
174		;
175		add_error(ltl,'Channel does not exist: ',Opname),
176		ResultFlag = error, ResArgs=[], Arity = 0
177		).
178		typecheck_tp(bop(oppattern(_Pos,Name,Args)),Result,ResultFlag) :- !,
179		( b_or_z_mode, b_get_machine_operation(Name,Results,Parameters,_) ->
180		Result = bop(Name,NumberArgs,NumberResults,ArgPatterns,ResPatterns),
181		length(Parameters,NumberArgs), length(Results,NumberResults),
182		% Pattern matching for results is not yet supported
183		ResPatterns = [],
184		( Args=[] ->
185		ArgPatterns = [],
186		ResPatterns = []
187		; length(Args,NumberArgs) ->
188		create_b_op_patterns(Args,Parameters,ArgPatterns,ResultFlag)
189		;
190		add_error(ltl,'Number of arguments not correct for: ', Name),ResultFlag=error)
191		; (csp_mode ; xtl_mode), Args=[] ->
192		debug_println(9,unparsed_trans(Name)),
193		typecheck_tp(unparsed_trans(Name),Result,ResultFlag)
194		;
195		add_error(ltl,'Could not find operation: ', Name),ResultFlag=error).
196		typecheck_tp(btrans(event(Name)),btrans(event(Name)),_ResultFlag) :- !.
197		typecheck_tp(btrans(event(Name,RawPredicate)),btrans(event(Name,TPredicate,Poststate)),ResultFlag) :- !,
198		( b_get_machine_operation(Name,_,_Parameters,_) ->
199		( bmachine:type_with_errors(RawPredicate,[prepost,operation(Name)],pred,TPredicate) ->
200		find_poststate_access(TPredicate,Poststate)
201		; ResultFlag=error)
202		;
203		add_error(ltl,'Could not find operation: ', Name),ResultFlag=error).
204		typecheck_tp(before_after(bpred(RawPredicate)),before_after(TPred),ResultFlag) :- !,
205		get_primed_machine_variables(PV),
206		(get_preference(symmetry_mode,off) -> Scope = [prob_ids(visible),identifier(PV),variables]
207		; Scope = [identifier(PV),variables]
208		),
209		% in classical B x$0 refers to the value before a substitution
210		( bmachine:type_with_errors(RawPredicate,Scope,pred,TPred0)
211		-> % see prepost becomes_such b_parse_machine_operation_pre_post_predicate
212		inline_prob_deferred_set_elements_into_bexpr(TPred0,TPred) % TODO: we could compute the $0 variables
213		; ResultFlag=error).
214		typecheck_tp(change_expr(Comparator,Expr),change_expr(Comparator,TypedExpr),Res) :-
215		!, typecheck_expr(Expr,TypedExpr,_Type,Res).
216		typecheck_tp(F,R,Res) :-
217		add_internal_error('Illegal LTL transition predicate:',typecheck_tp(F,R,Res)),fail.
218
219		typecheck_tp_l([],[],_Res).
220		typecheck_tp_l([TP|TPs],[TTP|TTPs],Res) :-
221		typecheck_tp(TP,TTP,ResultFlag),
222		(ResultFlag == error -> Res = error ; Res=Res1),
223		typecheck_tp_l(TPs,TTPs,Res1).
224
225		:- use_module(probsrc(bsyntaxtree),[syntaxtraversion/6]).
226		find_poststate_access(TExpr,Poststate) :-
227		find_poststate_access2(TExpr,P,[]),
228		sort(P,Poststate).
229		find_poststate_access2(TExpr) -->
230		{syntaxtraversion(TExpr,Expr,_,Infos,Subs,_)},
231		find_poststate_access3(Expr,Infos),
232		find_poststate_access_l(Subs).
233		find_poststate_access3(identifier(Id),Infos) -->
234		{memberchk(poststate,Infos),!,atom_concat(Orig,'\'',Id)},
235		[poststate(Orig,Id)].
236		find_poststate_access3(_,_) --> [].
237		find_poststate_access_l([]) --> !.
238		find_poststate_access_l([TExpr|Rest]) -->
239		find_poststate_access2(TExpr),
240		find_poststate_access_l(Rest).
241
242		/* Parsing CSP expressions where '_' will be not parsed */
243		parse_single_csp_expression_undescore(Context,Expr,Res) :-
244		(Expr=='_' -> Res = Expr; parse_single_csp_expression(Context,Expr,Res)).
245
246		l_parse_single_csp_expression_undescore(Context,LExpr,LRes) :-
247		maplist(parse_single_csp_expression_undescore(Context),LExpr,LRes).
248		/*******************************************************/
249
250		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
251		% do some preprocessing on a formula:
252		% - insert current state id
253		% - rewrite CSP declarations in some cases
254
255		preprocess_formula(In,Out) :-
256		(preprocess_formula2(In,Out) -> true ; add_error(ltl,'preprocessing formula failed: ',In),fail).
257
258		:- assert_must_succeed(preprocess_formula2(globally(next(false)),false)).
259		:- assert_must_succeed(preprocess_formula2(globally(next(next(true))),globally(true))).
260		:- assert_must_succeed(preprocess_formula2(finally(next(true)),true)).
261		:- assert_must_succeed(preprocess_formula2(finally(next(next(false))),finally(false))).
262
263		% base cases
264		preprocess_formula2(ap(A),ap(B)) :- !,
265		(A=bpred(Pred) ->
266		predicate_identifiers(Pred,Ids),
267		debug_println(predicate_identifiers(A,Ids))
268		; true),
269		preprocess_ap(A,B).
270		preprocess_formula2(action(A),action(B)) :- !,preprocess_tp(A,B).
271		preprocess_formula2(ena(SpecA,FA),action(SpecB,FB)) :-
272		!,preprocess_tp(SpecA,SpecB),preprocess_formula2(FA,FB).
273		% (X true = true) and (X false = false)
274		preprocess_formula2(next(F),PNextF) :-
275		!,preprocess_formula2(F,PF),
276		(PF = true -> PNextF = true
277		;PF = false -> PNextF = false
278		; PNextF = next(PF)).
279		% idempotency laws
280		preprocess_formula2(globally(globally(F)),globally(PF)) :-
281		!,preprocess_formula2(F,PF).
282		preprocess_formula2(finally(finally(F)),finally(PF)) :-
283		!,preprocess_formula2(F,PF).
284		preprocess_formula2(until(F,until(F,G)),until(PF,PG)) :-
285		!,preprocess_formula2(F,PF),
286		preprocess_formula2(G,PG).
287		preprocess_formula2(until(until(F,G),G),until(PF,PG)) :-
288		!,preprocess_formula2(F,PF),
289		preprocess_formula2(G,PG).
290		% absorption laws
291		preprocess_formula2(finally(globally(finally(F))),globally(finally(PF))) :-
292		!,preprocess_formula2(F,PF).
293		preprocess_formula2(globally(finally(globally(F))),finally(globally(PF))) :-
294		!,preprocess_formula2(F,PF).
295		% F (f U g) == F g
296		preprocess_formula2(finally(until(_F,G)),finally(PG)) :-
297		!,preprocess_formula2(G,PG).
298		% G (f R g) == G g
299		preprocess_formula2(globally(release(_F,G)),globally(PG)) :-
300		!,preprocess_formula2(G,PG).
301		% F true = true
302		preprocess_formula2(finally(F),PFinallyF) :-
303		!,preprocess_formula2(F,PF),
304		(PF = true -> PFinallyF = true ; PFinallyF = finally(PF)).
305		% G false = false
306		preprocess_formula2(globally(F),PGloballyF) :-
307		!,preprocess_formula2(F,PF),
308		(PF = false -> PGloballyF = false ; PGloballyF = globally(PF)).
309		% otherwise
310		preprocess_formula2(Term,NewTerm) :-
311		functor(Term,Functor,Arity),
312		functor(NewTerm,Functor,Arity),
313		preprocess_formula_args(Arity,Term,NewTerm).
314
315		preprocess_formula_args(0,_,_) :- !.
316		preprocess_formula_args(N,Term,NewTerm) :-
317		arg(N,Term,Arg),
318		arg(N,NewTerm,NewArg),
319		preprocess_formula2(Arg,NewArg),
320		N2 is N-1,
321		preprocess_formula_args(N2,Term,NewTerm).
322
323		preprocess_ap(current,stateid(StateId)) :- !,
324		current_state_id(StateId).
325		preprocess_ap(enabled(A),enabled(B)) :- !,
326		preprocess_tp(A,B).
327		preprocess_ap(AP,AP).
328
329		preprocess_tp(csp(Channel,Arity,CspArgs),
330		bop(Channel,NumberArgs,NumberResults,ArgPatterns,ResPatterns)) :-
331		csp_with_bz_mode,
332		b_get_machine_operation(Channel,Results,Parameters,_Body),
333		!,
334		% check if more arguments are specified that allowed
335		length(Parameters,NumberArgs),
336		length(Results,NumberResults),
337		MaxNumberAllowed is NumberArgs + NumberResults,
338		( Arity > MaxNumberAllowed ->
339		add_error(ltl,'Too many arguments for LTL/CTL channel: ', Channel),fail
340		; Arity =< NumberResults ->
341		ParamArgs = CspArgs,ResArgs = []
342		;
343		MinArgs is min(NumberArgs,Arity),
344		append_length(ParamArgs,ResArgs,CspArgs,MinArgs)),
345		csp_arguments(ParamArgs,1,Parameters,ArgPatterns,Exprs1),
346		csp_arguments(ResArgs,1,Results,ResPatterns,Exprs2),
347		append(Exprs1,Exprs2,Exprs),
348		parse_preds_exprs(Exprs).
349		preprocess_tp(TP,TP).
350
351		csp_arguments([],_Index,_Parameters,[],[]).
352		csp_arguments([P|ParamArgs],Index,[Param|ParamRest],ArgPatterns,Exprs) :-
353		( is_csp_placeholder(P) ->
354		ArgPatterns = ArgPatternsRest,
355		Exprs = ExprsRest
356		;
357		ArgPatterns = [Index/ArgPattern|ArgPatternsRest],
358		Exprs = [Expr|ExprsRest],
359		csp_argument(P,Param,ArgPattern,Expr)),
360		I2 is Index+1,
361		csp_arguments(ParamArgs,I2,ParamRest,ArgPatternsRest,ExprsRest).
362		csp_argument(Argument,Parameter,ParsedExpr,expr(ToParse,Type,ParsedExpr)) :-
363		get_texpr_type(Parameter,Type),
364		atom_codes(Argument,ToParse).
365
366		is_csp_placeholder('_').
367		is_csp_placeholder('?').
368
369		% currently not called: nor is unparsed_ap called
370		%translate_preds(In,Out) :-
371		% unparsed_ap_l(In,Out,Translation,[]),
372		% parse_preds_exprs(Translation).
373
374		parse_preds_exprs([]) :- !. % nothing to parse
375		parse_preds_exprs(Translation) :-
376		split_preds(Translation,PredStrings,Preds,ExprStrings,Exprs),
377		animation_mode(AnimMode),
378		parse_preds_exprs2(AnimMode,PredStrings,Preds,ExprStrings,Exprs).
379
380		% default: parse the predicates and expressions as B
381		parse_preds_exprs2(_,PredStrings,Preds,ExprStringsWithTypes,Exprs) :-
382		annotate_ap_type(Preds,bpred,BPreds),
383		split_exprs_types(ExprStringsWithTypes,ExprStrings,Types),
384		maplist(parse_expression,ExprStrings,UExprs),
385		maplist(parse_predicate,PredStrings,UPreds),
386		type_exprs(UExprs,Types,Exprs,EErrors),
387		type_preds(UPreds,BPreds,PErrors),
388		append(EErrors,PErrors,Errors),
389		add_all_perrors(Errors,[],type_error).
390
391		split_exprs_types([],[],[]).
392		split_exprs_types([Expr/Type|ETRest],[Expr|ERest],[Type|TRest]) :-
393		split_exprs_types(ETRest,ERest,TRest).
394
395		type_exprs([],[],[],[]).
396		type_exprs([Expr|Erest],[Type|TypeRest],[Typed|Trest],Errors) :-
397		b_type_expression_for_ltl(Expr,Type,Typed,LErrors),
398		append(LErrors,ErrorRest,Errors),
399		type_exprs(Erest,TypeRest,Trest,ErrorRest).
400		type_preds([],[],[]).
401		type_preds([Pred|Prest],[Typed|Trest],Errors) :-
402		b_type_expression_for_ltl(Pred,pred,Typed,LErrors),
403		append(LErrors,ErrorRest,Errors),
404		type_preds(Prest,Trest,ErrorRest).
405
406		annotate_ap_type([],_,[]).
407		annotate_ap_type([AP|APrest],Type,[R|Rrest]) :-
408		functor(AP,Type,1),arg(1,AP,R),
409		annotate_ap_type(APrest,Type,Rrest).
410
411		b_type_expression_for_ltl(Expr,Type,Typed,LErrors) :-
412		(get_preference(symmetry_mode,off)
413		-> Scope = [prob_ids(visible),variables]
414		; Scope = [variables] % we have to be careful with symmetry, TODO: better feedback
415		),
416		% we would need to call add_prob_deferred_set_elements_to_store(State1,State2,visible)
417		% should we also add external_library(all_available_libraries)
418		b_type_expression(Expr,Scope,Type,Typed,LErrors).
419
420
421		split_preds([],[],[],[],[]).
422		split_preds([pred(A,B)|Rest],[A|ARest],[B|BRest],X,Y) :- !,
423		split_preds(Rest,ARest,BRest,X,Y).
424		split_preds([expr(A,T,B)|Rest],X,Y,[A/T|ARest],[B|BRest]) :-
425		split_preds(Rest,X,Y,ARest,BRest).
426
427		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
428		% parse a file with several LTL formulas:
429
430		% The format in Rodin and the format generated by the Tcl/Tk LTL viewer are different
431		% Rodin has formulas on one line, with comments starting with #
432		% Tcl/Tk generates sections with square brackets; within a section there is a single formula
433
434		parse_ltlfile(Filename, Formulas) :-
435		(parse_ltlfile2(Filename,Formulas) -> true ; add_error(ltl, 'Error while parsing the LTL formula file')).
436		parse_ltlfile2(Filename, Formulas) :-
437		read_file_codes(Filename,Codes),
438		reset_line_counter,
439		parse_lines(Lines,Codes,[]),
440		get_line_counter(LineCount), debug_format(19,'Read ~w lines from file ~w~n',[LineCount,Filename]),
441		parse_sections(Raws,Lines,[]),
442		maplist(parse_file_formula(Filename),Raws,Formulas).
443
444
445		:- use_module(probsrc(tools_strings),[ajoin/2]).
446		parse_file_formula(Filename,file_formula(StartLine,Name,Raw),formula(Name,Res)) :- !,
447		debug_format(19,'Parsing formula starting at line ~w in ~w~n',[StartLine,Filename]),
448		(temporal_parser(Raw,ltl,Parsed)
449		-> Res=Parsed
450		; ajoin(['Error parsing LTL formula ',Name,' starting at line ',StartLine,' in ',Filename],Msg),
451		add_error(ltl_tools,Msg,Raw),
452		Res = false).
453		parse_file_formula(_,X,Res) :-
454		add_internal_error('Illegal formula term:',X),!, Res=false.
455
456
457		/*
458		parse_file2([]) --> [].
459		parse_file2([F|Rest]) -->
460		parse_section(F),
461		parse_file2(Rest). */
462
463		parse_sections(Res) --> [comment(_)],!, parse_sections(Res).
464		parse_sections([file_formula(StartLine,Name,F)|Rest]) -->
465		[header(_,Name)],!,
466		parse_section_multi_line_formulas("",FCodes,StartLine),
467		{ atom_codes(F,FCodes) },
468		parse_sections(Rest).
469		parse_sections([file_formula(StartLine,FormulaName,F)|Rest]) -->
470		% no header section, this is Rodin Format and we expect one formula per line
471		[formula_line(StartLine,FCodes)],
472		!,
473		{ atom_codes(F,FCodes), ajoin(['ltl-formula-on-line-',StartLine],FormulaName) },
474		parse_sections(Rest).
475		parse_sections([]) --> [].
476
477
478		parse_section_multi_line_formulas(Prev,F,Line) --> [comment(_)],!, parse_section_multi_line_formulas(Prev,F,Line).
479		parse_section_multi_line_formulas(Prev,F,StartLine) -->
480		[formula_line(StartLine,Snippet)],!,
481		{(Prev==[] -> F2=Snippet
482		; append([Prev,"\n",Snippet],F2)
483		)},
484		parse_section_multi_line_formulas(F2,F,_).
485		parse_section_multi_line_formulas(F,F,-1) --> [].
486
487		parse_lines([]) --> [].
488		parse_lines([L|Rest]) -->
489		parse_line(L), %{get_line_counter(Line),print(parsed_line(Line,L)),nl},
490		parse_lines(Rest).
491
492		parse_line(Line) --> pl_spaces,!, parse_line(Line).
493		parse_line(comment(C)) -->
494		"#",!, % comment lines start with #
495		pl_until_newline(C).
496		parse_line(comment("")) -->
497		pl_newline,!.
498		parse_line(header(Line,Title)) -->
499		pl_title(Title), !,
500		{get_line_counter(Line)},
501		pl_opt_spaces, pl_newline, !.
502		parse_line(formula_line(Line,[C|F])) -->
503		% non empty formulas
504		[C], {get_line_counter(Line)},
505		pl_until_newline(F).
506
507		pl_title(Title) -->
508		"[", pl_opt_spaces, pl_title2(T), {atom_codes(Title,T)}.
509		pl_title2([]) --> pl_opt_spaces,"]",!.
510		pl_title2([]) --> pl_newline,!,{fail}. % maybe an exception?
511		pl_title2([C|Rest]) --> [C],pl_title2(Rest).
512
513		pl_spaces --> " ",!,pl_spaces.
514		pl_spaces --> "\t",!,pl_spaces.
515
516		pl_opt_spaces --> " ",!,pl_opt_spaces.
517		pl_opt_spaces --> "\t",!,pl_opt_spaces.
518		pl_opt_spaces --> [].
519
520		pl_until_newline([]) --> pl_newline,!.
521		pl_until_newline([C|Rest]) --> [C],!,pl_until_newline(Rest).
522		pl_until_newline([]) --> []. % end of string/file
523
524		pl_newline --> "\n\r",!, {inc_line_counter}.
525		pl_newline --> "\n",!,{inc_line_counter}.
526		pl_newline --> "\r",{inc_line_counter}.
527
528		inc_line_counter :- get_line_counter(L), L1 is L+1, bb_put(ltl_line_counter,L1).
529		get_line_counter(Val) :- (bb_get(ltl_line_counter,V) -> V=Val ; Val = -1).
530		reset_line_counter :- bb_put(ltl_line_counter,1).
531
532
533		create_b_op_patterns(Args,Parameters,ArgPatterns,Res) :-
534		create_b_op_patterns2(Args,Parameters,ArgPatterns,1,Res).
535		create_b_op_patterns2([],[],[],_,_).
536		create_b_op_patterns2([Arg|ARest],[Param|ParamRest],Patterns,Index,Res) :-
537		create_b_op_pattern(Arg,Param,Pattern,Res),
538		(var(Pattern) -> Patterns = PRest ; Patterns = [Index/Pattern|PRest]),
539		Index2 is Index+1,
540		create_b_op_patterns2(ARest,ParamRest,PRest,Index2,Res).
541		create_b_op_pattern(undef(_Pos),_,_,_).
542		create_b_op_pattern(def(_Pos,Raw),TParam,Typed,Res) :-
543		get_texpr_type(TParam,Type),
544		b_type_expression_for_ltl(Raw,Type,Typed,Errors),
545		add_all_perrors(Errors,[],typecheck_operation_argument),
546		(no_real_perror_occurred(Errors) -> true ; Res=error).
547		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
548
549
550		parse_and_pp_ltl_formula(FormulaAsAtom,Text) :-
551		temporal_parser(FormulaAsAtom,ltl,Ltl),
552		( pp_ltl_formula_classicb(Ltl,Text)
553		-> true
554		; add_error_fail(ltl, 'Failed to pretty print LTL formula: ', Ltl)
555		).
556
557		:- use_module(probsrc(specfile),[unset_animation_minor_modes/1,reset_animation_minor_modes/1]).
558		:- use_module(probsrc(translate),[set_unicode_mode/0, unset_unicode_mode/0]).
559		pp_ltl_formula_classicb(Ltl,Text) :-
560		unset_animation_minor_modes(L), % unset eventb mode, as we will later parse the LTL formula in classic mode!
561		% TO DO: improve and ensure things like finite(.) from Event-B work in atomic propositions
562		set_unicode_mode,
563		call_cleanup(pp_ltl_formula(Ltl,Text),
564		(reset_animation_minor_modes(L),unset_unicode_mode)).
565
566		%%%%%%%% Other predicates %%%%%%%%%%
567
568		:- assert_must_succeed((ltl_tools: mergeArgsToDotTuple([1,2,'<bob,alice>','{bob}'],Res), Res = '1.2.<bob,alice>.{bob}')).
569		:- assert_must_succeed((ltl_tools: mergeArgsToDotTuple(['(bob,alice)'],Res), Res = '(bob,alice)')).
570		:- assert_must_succeed(ltl_tools: mergeArgsToDotTuple([],'')).
571
572		mergeArgsToDotTuple(List,Res) :- mergeArgsToDotTuple(List,'',Res).
573
574		mergeArgsToDotTuple([],Str,Str).
575		mergeArgsToDotTuple([H|T],Str,Res) :-
576		(T\=[] -> string_concatenate(H,'.',HRes) ; HRes=H),
577		string_concatenate(Str,HRes,StrRes),mergeArgsToDotTuple(T,StrRes,Res).
578
579		splitToSingleArgs(dotTuple(List),List,Arity) :-
580		N is Arity +1, length(List,N),!.
581		splitToSingleArgs(X,[X],0) :- !.
582		splitToSingleArgs(ParsedEvent,_,N) :-
583		ajoin(['Expected arity ',N,' for channel: '],Msg),
584		add_internal_error(Msg,ParsedEvent).
585
586		:- assert_must_succeed((check_csp_event(tick,0,[],R), R=tick(_))).
587		:- assert_must_succeed((check_csp_event(tau,0,[],R), R=tau(_))).
588		:- assert_must_fail(check_csp_arguments([setValue([alice,bob]),tupleExp([s,t,u])], [setValue([alice,bob]),in(na_tuple([s,t]))],some_event)).
589		:- assert_must_succeed(check_csp_arguments([setValue([alice,bob]),tupleExp([s,t,u])], [setValue([alice,bob]),in(na_tuple([s,t,u]))],some_event)).
590		:- assert_must_succeed(check_csp_arguments([setValue([bob,alice]),tupleExp([s,t,u])], [setValue([alice,bob]),in(na_tuple([s,t,u]))],some_event)).
591		:- assert_must_succeed(check_csp_arguments([a,'_','_'],[in(a),in(int(10)),in(int(20))],true)).
592
593		%% Predicate check csp event
594		check_csp_event(tick,0,[],R) :- !, R=tick(_).
595		check_csp_event(tau,0,[],R) :- !, R=tau(_).
596		check_csp_event(Event,Arity,PatArgs,io(Vals,Event,_SrcSpan)) :- !,
597		(channel(Event,_) ->
598		((channel_type_list(Event,List),length(List,Arity)) ->
599		check_csp_arguments(PatArgs,Vals,Event)
600		; add_error(ltl,'Internal Error: Missing/extra arguments in CSP LTL/CTL pattern: ',Event:PatArgs),fail
601		)
602		; add_internal_error('Internal Error: Channel not defined: ',Event/Arity)).
603
604		:- block check_csp_arguments(?,-,?).
605		check_csp_arguments([],[],_).
606		check_csp_arguments([],[H|T],Event) :-
607		print('* Missing arguments in CSP LTL/CTL pattern (use .?): '),print(Event),
608		print(' : '),print([H|T]),nl.
609		check_csp_arguments([H|T],[],Event) :-
610		add_error(ltl,'Extra arguments in CSP LTL/CTL pattern: ',Event:[H|T]),fail.
611		check_csp_arguments([H|T],[PatH|PatT],Event) :-
612	?	check_csp_arg(H,PatH),!,
613	?	check_csp_arguments(T,PatT,Event).
614
615		check_csp_arg(X,Y) :-
616		var(Y),!,
617		add_internal_error('Internal Error: Event argument was a variable, expected to be: ',X).
618		check_csp_arg('_',_Y). % underscore should match any argument
619		check_csp_arg(X,in(Y)) :-
620		check_csp_arg(X,Y).
621		check_csp_arg(X,out(Y)) :-
622		check_csp_arg(X,Y).
623
624		check_csp_arg(list(L),list(L1)) :- !,
625		l_check_csp_arg(L,L1,list).
626		check_csp_arg(setValue(L),setValue(L1)) :- !,
627		sort(L,R),
628		sort(L1,R1),
629		l_check_csp_arg(R,R1,setValue). % elements order is not important within set expressions
630		check_csp_arg(tupleExp(L),na_tuple(L1)) :- !,
631		l_check_csp_arg(L,L1,na_tuple).
632		check_csp_arg(X,Y) :- eq_csp_val(Y,X).
633
634		eq_csp_val(int(X),int(Y)) :- !, Y=X.
635		eq_csp_val(X,X).
636
637		l_check_csp_arg([],[],_):- !.
638		l_check_csp_arg([],[H|T],Functor) :-
639		add_error_fail(ltl,'Missing elements in CSP LTL pattern: ',Functor:[H|T]).
640		l_check_csp_arg([H|T],[H1|T1],Functor) :-
641		check_csp_arg(H,H1),!,
642		l_check_csp_arg(T,T1,Functor).