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