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