ltl_tools

annotate_ap_type([],_,[]).

annotate_ap_type([AP|APrest],Type,[R|Rrest]) :-
    functor(AP,Type,1),arg(1,AP,R),
    annotate_ap_type(APrest,Type,Rrest).

b_type_expression_for_ltl(Expr,Type,Typed,LErrors) :-
    (get_preference(symmetry_mode,off)
    -> Scope = [prob_ids(visible),variables]
    ; Scope = [variables] % we have to be careful with symmetry, TODO: better feedback
    ),
    % we would need to call add_prob_deferred_set_elements_to_store(State1,State2,visible)
    % should we also add external_library(all_available_libraries)
    b_type_expression(Expr,Scope,Type,Typed,LErrors).

check_csp_arg(X,Y) :-
    var(Y),!,
    add_internal_error('Internal Error: Event argument was a variable, expected to be: ',X).

check_csp_arg('_',_Y). % underscore should match any argument

check_csp_arg(X,in(Y)) :-
    check_csp_arg(X,Y).

check_csp_arg(X,out(Y)) :-
    check_csp_arg(X,Y).

check_csp_arg(list(L),list(L1)) :- !,
    l_check_csp_arg(L,L1,list).

check_csp_arg(setValue(L),setValue(L1)) :- !,
    sort(L,R),
    sort(L1,R1),
    l_check_csp_arg(R,R1,setValue). % elements order is not important within set expressions

check_csp_arg(tupleExp(L),na_tuple(L1)) :- !,
    l_check_csp_arg(L,L1,na_tuple).

check_csp_arg(X,Y) :- eq_csp_val(Y,X).

check_csp_arguments([],[],_).

check_csp_arguments([],[H|T],Event) :-
    print('* Missing arguments in CSP LTL/CTL pattern (use .?): '),print(Event),
    print(' : '),print([H|T]),nl.

check_csp_arguments([H|T],[],Event) :-
    add_error(ltl,'Extra arguments in CSP LTL/CTL pattern: ',Event:[H|T]),fail.

check_csp_arguments([H|T],[PatH|PatT],Event) :-
    check_csp_arg(H,PatH),!,
    check_csp_arguments(T,PatT,Event).

check_csp_event(tick,0,[],R) :- !, R=tick(_).

check_csp_event(tau,0,[],R) :- !, R=tau(_).

check_csp_event(Event,Arity,PatArgs,io(Vals,Event,_SrcSpan)) :- !,
    (channel(Event,_) ->
    ((channel_type_list(Event,List),length(List,Arity)) ->
    check_csp_arguments(PatArgs,Vals,Event)
    ; add_error(ltl,'Internal Error: Missing/extra arguments in CSP LTL/CTL pattern: ',Event:PatArgs),fail
    )
    ; add_internal_error('Internal Error: Channel not defined: ',Event/Arity)).

check_syntax_result(ltl(F),F,_,_Mode).

check_syntax_result(syntax_error(E),_,error,Mode) :-
    add_error(Mode,'Syntax error: ',E).

check_syntax_result_l([],[],_,_).

check_syntax_result_l([R|Rrest],[F|Frest],Res,Mode) :-
    check_syntax_result(R,F,Res,Mode),
    check_syntax_result_l(Rrest,Frest,Res,Mode).

create_b_op_pattern(undef(_Pos),_,_,_).

create_b_op_pattern(def(_Pos,Raw),TParam,Typed,Res) :-
    get_texpr_type(TParam,Type),
    b_type_expression_for_ltl(Raw,Type,Typed,Errors),
    add_all_perrors(Errors,[],typecheck_operation_argument),
    (no_real_perror_occurred(Errors) -> true ; Res=error).

create_b_op_patterns(Args,Parameters,ArgPatterns,Res) :-
    create_b_op_patterns2(Args,Parameters,ArgPatterns,1,Res).

create_b_op_patterns2([],[],[],_,_).

create_b_op_patterns2([Arg|ARest],[Param|ParamRest],Patterns,Index,Res) :-
    create_b_op_pattern(Arg,Param,Pattern,Res),
    (var(Pattern) -> Patterns = PRest ; Patterns = [Index/Pattern|PRest]),
    Index2 is Index+1,
    create_b_op_patterns2(ARest,ParamRest,PRest,Index2,Res).

csp_argument(Argument,Parameter,ParsedExpr,expr(ToParse,Type,ParsedExpr)) :-
    get_texpr_type(Parameter,Type),
    atom_codes(Argument,ToParse).

csp_arguments([],_Index,_Parameters,[],[]).

csp_arguments([P|ParamArgs],Index,[Param|ParamRest],ArgPatterns,Exprs) :-
    ( is_csp_placeholder(P) ->
    ArgPatterns = ArgPatternsRest,
    Exprs = ExprsRest
    ;
    ArgPatterns = [Index/ArgPattern|ArgPatternsRest],
    Exprs = [Expr|ExprsRest],
    csp_argument(P,Param,ArgPattern,Expr)),
    I2 is Index+1,
    csp_arguments(ParamArgs,I2,ParamRest,ArgPatternsRest,ExprsRest).

eq_csp_val(int(X),int(Y)) :- !, Y=X.

eq_csp_val(X,X).

find_poststate_access(TExpr,Poststate) :-
    find_poststate_access2(TExpr,P,[]),
    sort(P,Poststate).

find_poststate_access2(TExpr) -->
    {syntaxtraversion(TExpr,Expr,_,Infos,Subs,_)},
    find_poststate_access3(Expr,Infos),
    find_poststate_access_l(Subs).

find_poststate_access3(identifier(Id),Infos) -->
    {memberchk(poststate,Infos),!,atom_concat(Orig,'\'',Id)},
    [poststate(Orig,Id)].

find_poststate_access3(_,_) --> [].

find_poststate_access_l([]) --> !.

find_poststate_access_l([TExpr|Rest]) -->
    find_poststate_access2(TExpr),
    find_poststate_access_l(Rest).

get_line_counter(Val) :- (bb_get(ltl_line_counter,V) -> V=Val ; Val = -1).

inc_line_counter :- get_line_counter(L), L1 is L+1, bb_put(ltl_line_counter,L1).

is_basic_ap(deadlock).

is_basic_ap(det_output).

is_basic_ap(sink).

is_basic_ap(goal).

is_basic_ap(state_error).

is_basic_ap(current).

is_basic_ap(stateid(_)).

is_csp_placeholder('_').

is_csp_placeholder('?').

l_check_csp_arg([],[],_):- !.

l_check_csp_arg([],[H|T],Functor) :-
    add_error_fail(ltl,'Missing elements in CSP LTL pattern: ',Functor:[H|T]).

l_check_csp_arg([H|T],[H1|T1],Functor) :-
    check_csp_arg(H,H1),!,
    l_check_csp_arg(T,T1,Functor).

l_parse_single_csp_expression_undescore(Context,LExpr,LRes) :-
    maplist(parse_single_csp_expression_undescore(Context),LExpr,LRes).

mergeArgsToDotTuple(List,Res) :- mergeArgsToDotTuple(List,'',Res).

mergeArgsToDotTuple([],Str,Str).

mergeArgsToDotTuple([H|T],Str,Res) :-
    (T\=[] -> string_concatenate(H,'.',HRes) ; HRes=H),
    string_concatenate(Str,HRes,StrRes),mergeArgsToDotTuple(T,StrRes,Res).

parse_and_pp_ltl_formula(FormulaAsAtom,Text) :-
    temporal_parser(FormulaAsAtom,ltl,Ltl),
    ( pp_ltl_formula_classicb(Ltl,Text)
    -> true
    ; add_error_fail(ltl, 'Failed to pretty print LTL formula: ', Ltl)
).

parse_file_formula(Filename,file_formula(StartLine,Name,Raw),formula(Name,Res)) :- !,
    debug_format(19,'Parsing formula starting at line ~w in ~w~n',[StartLine,Filename]),
    (temporal_parser(Raw,ltl,Parsed)
    -> Res=Parsed
    ; ajoin(['Error parsing LTL formula ',Name,' starting at line ',StartLine,' in ',Filename],Msg),
    add_error(ltl_tools,Msg,Raw),
    Res = false).

parse_file_formula(_,X,Res) :-
    add_internal_error('Illegal formula term:',X),!, Res=false.

parse_line(Line) --> pl_spaces,!, parse_line(Line).

parse_line(comment(C)) -->
    "#",!, % comment lines start with #
    pl_until_newline(C).

parse_line(comment("")) -->
    pl_newline,!.

parse_line(header(Line,Title)) -->
    pl_title(Title), !,
    {get_line_counter(Line)},
    pl_opt_spaces, pl_newline, !.

parse_line(formula_line(Line,[C|F])) -->
    % non empty formulas
    [C], {get_line_counter(Line)},
    pl_until_newline(F).

parse_lines([]) --> [].

parse_lines([L|Rest]) -->
    parse_line(L), %{get_line_counter(Line),print(parsed_line(Line,L)),nl},
    parse_lines(Rest).

parse_ltlfile(Filename, Formulas) :-
    (parse_ltlfile2(Filename,Formulas) -> true ; add_error(ltl, 'Error while parsing the LTL formula file')).

parse_ltlfile2(Filename, Formulas) :-
    read_file_codes(Filename,Codes),
    reset_line_counter,
    parse_lines(Lines,Codes,[]),
    get_line_counter(LineCount), debug_format(19,'Read ~w lines from file ~w~n',[LineCount,Filename]),
    parse_sections(Raws,Lines,[]),
    maplist(parse_file_formula(Filename),Raws,Formulas).

parse_preds_exprs([]) :- !. % nothing to parse

parse_preds_exprs(Translation) :-
    split_preds(Translation,PredStrings,Preds,ExprStrings,Exprs),
    animation_mode(AnimMode),
    parse_preds_exprs2(AnimMode,PredStrings,Preds,ExprStrings,Exprs).

parse_preds_exprs2(_,PredStrings,Preds,ExprStringsWithTypes,Exprs) :-
    annotate_ap_type(Preds,bpred,BPreds),
    split_exprs_types(ExprStringsWithTypes,ExprStrings,Types),
    maplist(parse_expression,ExprStrings,UExprs),
    maplist(parse_predicate,PredStrings,UPreds),
    type_exprs(UExprs,Types,Exprs,EErrors),
    type_preds(UPreds,BPreds,PErrors),
    append(EErrors,PErrors,Errors),
    add_all_perrors(Errors,[],type_error).

parse_section_multi_line_formulas(Prev,F,Line) --> [comment(_)],!, parse_section_multi_line_formulas(Prev,F,Line).

parse_section_multi_line_formulas(Prev,F,StartLine) -->
    [formula_line(StartLine,Snippet)],!,
    {(Prev==[] -> F2=Snippet
    ; append([Prev,"\n",Snippet],F2)
    )},
    parse_section_multi_line_formulas(F2,F,_).

parse_section_multi_line_formulas(F,F,-1) --> [].

parse_sections(Res) --> [comment(_)],!, parse_sections(Res).

parse_sections([file_formula(StartLine,Name,F)|Rest]) -->
    [header(_,Name)],!,
    parse_section_multi_line_formulas("",FCodes,StartLine),
    { atom_codes(F,FCodes) },
    parse_sections(Rest).

parse_sections([file_formula(StartLine,FormulaName,F)|Rest]) -->
    % no header section, this is Rodin Format and we expect one formula per line
    [formula_line(StartLine,FCodes)],
    !,
    { atom_codes(F,FCodes), ajoin(['ltl-formula-on-line-',StartLine],FormulaName) },
    parse_sections(Rest).

parse_sections([]) --> [].

parse_single_csp_expression_undescore(Context,Expr,Res) :-
    (Expr=='_' -> Res = Expr; parse_single_csp_expression(Context,Expr,Res)).

pl_newline --> "\n\r",!, {inc_line_counter}.

pl_newline --> "\n",!,{inc_line_counter}.

pl_newline --> "\r",{inc_line_counter}.

pl_opt_spaces --> " ",!,pl_opt_spaces.

pl_opt_spaces --> "\t",!,pl_opt_spaces.

pl_opt_spaces --> [].

pl_spaces --> " ",!,pl_spaces.

pl_spaces --> "\t",!,pl_spaces.

pl_title(Title) -->
    "[", pl_opt_spaces, pl_title2(T), {atom_codes(Title,T)}.

pl_title2([]) --> pl_opt_spaces,"]",!.

pl_title2([]) --> pl_newline,!,{fail}. % maybe an exception?

pl_title2([C|Rest]) --> [C],pl_title2(Rest).

pl_until_newline([]) --> pl_newline,!.

pl_until_newline([C|Rest]) --> [C],!,pl_until_newline(Rest).

pl_until_newline([]) --> []. % end of string/file

pp_ltl_formula_classicb(Ltl,Text) :-
    unset_animation_minor_modes(L), % unset eventb mode, as we will later parse the LTL formula in classic mode!
    % TO DO: improve and ensure things like finite(.) from Event-B work in atomic propositions
    set_unicode_mode,
    call_cleanup(pp_ltl_formula(Ltl,Text),
    (reset_animation_minor_modes(L),unset_unicode_mode)).

preprocess_ap(current,stateid(StateId)) :- !,
    current_state_id(StateId).

preprocess_ap(enabled(A),enabled(B)) :- !,
    preprocess_tp(A,B).

preprocess_ap(AP,AP).

preprocess_formula(In,Out) :-
    (preprocess_formula2(In,Out) -> true ; add_error(ltl,'preprocessing formula failed: ',In),fail).

preprocess_formula2(ap(A),ap(B)) :- !,
    (A=bpred(Pred) ->
    predicate_identifiers(Pred,Ids),
    debug_println(predicate_identifiers(A,Ids))
    ; true),
    preprocess_ap(A,B).

preprocess_formula2(action(A),action(B)) :- !,preprocess_tp(A,B).

preprocess_formula2(ena(SpecA,FA),action(SpecB,FB)) :-
    !,preprocess_tp(SpecA,SpecB),preprocess_formula2(FA,FB).

preprocess_formula2(next(F),PNextF) :-
    !,preprocess_formula2(F,PF),
    (PF = true -> PNextF = true
    ;PF = false -> PNextF = false
    ; PNextF = next(PF)).

preprocess_formula2(globally(globally(F)),globally(PF)) :-
    !,preprocess_formula2(F,PF).

preprocess_formula2(finally(finally(F)),finally(PF)) :-
    !,preprocess_formula2(F,PF).

preprocess_formula2(until(F,until(F,G)),until(PF,PG)) :-
    !,preprocess_formula2(F,PF),
    preprocess_formula2(G,PG).

preprocess_formula2(until(until(F,G),G),until(PF,PG)) :-
    !,preprocess_formula2(F,PF),
    preprocess_formula2(G,PG).

preprocess_formula2(finally(globally(finally(F))),globally(finally(PF))) :-
    !,preprocess_formula2(F,PF).

preprocess_formula2(globally(finally(globally(F))),finally(globally(PF))) :-
    !,preprocess_formula2(F,PF).

preprocess_formula2(finally(until(_F,G)),finally(PG)) :-
    !,preprocess_formula2(G,PG).

preprocess_formula2(globally(release(_F,G)),globally(PG)) :-
    !,preprocess_formula2(G,PG).

preprocess_formula2(finally(F),PFinallyF) :-
    !,preprocess_formula2(F,PF),
    (PF = true -> PFinallyF = true ; PFinallyF = finally(PF)).

preprocess_formula2(globally(F),PGloballyF) :-
    !,preprocess_formula2(F,PF),
    (PF = false -> PGloballyF = false ; PGloballyF = globally(PF)).

preprocess_formula2(Term,NewTerm) :-
    functor(Term,Functor,Arity),
    functor(NewTerm,Functor,Arity),
    preprocess_formula_args(Arity,Term,NewTerm).

preprocess_formula_args(0,_,_) :- !.

preprocess_formula_args(N,Term,NewTerm) :-
    arg(N,Term,Arg),
    arg(N,NewTerm,NewArg),
    preprocess_formula2(Arg,NewArg),
    N2 is N-1,
    preprocess_formula_args(N2,Term,NewTerm).

preprocess_tp(csp(Channel,Arity,CspArgs),
    bop(Channel,NumberArgs,NumberResults,ArgPatterns,ResPatterns)) :-
    csp_with_bz_mode,
    b_get_machine_operation(Channel,Results,Parameters,_Body),
    !,
    % check if more arguments are specified that allowed
    length(Parameters,NumberArgs),
    length(Results,NumberResults),
    MaxNumberAllowed is NumberArgs + NumberResults,
    ( Arity > MaxNumberAllowed ->
    add_error(ltl,'Too many arguments for LTL/CTL channel: ', Channel),fail
    ; Arity =< NumberResults ->
    ParamArgs = CspArgs,ResArgs = []
    ;
    MinArgs is min(NumberArgs,Arity),
    append_length(ParamArgs,ResArgs,CspArgs,MinArgs)),
    csp_arguments(ParamArgs,1,Parameters,ArgPatterns,Exprs1),
    csp_arguments(ResArgs,1,Results,ResPatterns,Exprs2),
    append(Exprs1,Exprs2,Exprs),
    parse_preds_exprs(Exprs).

preprocess_tp(TP,TP).

reset_line_counter :- bb_put(ltl_line_counter,1).

splitToSingleArgs(dotTuple(List),List,Arity) :-
    N is Arity +1, length(List,N),!.

splitToSingleArgs(X,[X],0) :- !.

splitToSingleArgs(ParsedEvent,_,N) :-
    ajoin(['Expected arity ',N,' for channel: '],Msg),
    add_internal_error(Msg,ParsedEvent).

split_exprs_types([],[],[]).

split_exprs_types([Expr/Type|ETRest],[Expr|ERest],[Type|TRest]) :-
    split_exprs_types(ETRest,ERest,TRest).

split_preds([],[],[],[],[]).

split_preds([pred(A,B)|Rest],[A|ARest],[B|BRest],X,Y) :- !,
    split_preds(Rest,ARest,BRest,X,Y).

split_preds([expr(A,T,B)|Rest],X,Y,[A/T|ARest],[B|BRest]) :-
    split_preds(Rest,X,Y,ARest,BRest).

temporal_parser(Formula,Mode,Result) :-
    temporal_parser_l([Formula],Mode,[Result]).

temporal_parser_l(Formulas,Mode,Result) :-
    % call the Java parser for LTL
    call_ltl_parser(Formulas,Mode,Res1),
    % check if everything was fine
    check_syntax_result_l(Res1,Parsed,ParseFlag,Mode), ParseFlag=ok,
    % typecheck atomic propositions and such things
    %tools_printing:nested_print_term(Parsed,10),
    typecheck_temporal_formula_l(Parsed,Result,TypeFlag), TypeFlag=ok.

type_check_raw(Raw,Type,Typed,Res) :-
    b_type_expression_for_ltl(Raw,Type,Typed0,Errors),
    add_all_perrors(Errors,[],typecheck_atomic_property),
    (no_real_perror_occurred(Errors)
    -> inline_prob_deferred_set_elements_into_bexpr(Typed0,Typed)
    ; Typed=Typed0, Res=error).

type_exprs([],[],[],[]).

type_exprs([Expr|Erest],[Type|TypeRest],[Typed|Trest],Errors) :-
    b_type_expression_for_ltl(Expr,Type,Typed,LErrors),
    append(LErrors,ErrorRest,Errors),
    type_exprs(Erest,TypeRest,Trest,ErrorRest).

type_preds([],[],[]).

type_preds([Pred|Prest],[Typed|Trest],Errors) :-
    b_type_expression_for_ltl(Pred,pred,Typed,LErrors),
    append(LErrors,ErrorRest,Errors),
    type_preds(Prest,Trest,ErrorRest).

typecheck_ap(BasicAP,AP,_Res) :- is_basic_ap(BasicAP),!,AP=BasicAP.

typecheck_ap(enabled(TP),enabled(R),Res) :-
    !,typecheck_tp(TP,R,Res).

typecheck_ap(available(TP),available(R),Res) :-
    !,typecheck_tp(TP,R,Res).

typecheck_ap(weak_fair(TP),weak_fair(R),Res) :-
    !,typecheck_tp(TP,R,Res).

typecheck_ap(strong_fair(TP),strong_fair(R),Res) :-
    !,typecheck_tp(TP,R,Res).

typecheck_ap(dlk(TPList),dlk(R),Res) :-
    !,typecheck_tp_l(TPList,R,Res).

typecheck_ap(ctrl(TPList),ctrl(R),Res) :-
    !,typecheck_tp_l(TPList,R,Res).

typecheck_ap(det(TPList),det(R),Res) :-
    !,typecheck_tp_l(TPList,R,Res).

typecheck_ap(bpred(Raw),bpred(Typed),Res) :- !,
    type_check_raw(Raw,pred,Typed,Res).

typecheck_ap(unparsed_pred(Atom),xtl_predicate_check(Atom),ResultFlag) :- !,
    (animation_mode(xtl) -> true ; ResultFlag=error).

typecheck_ap(F,R,Res) :-
    add_internal_error('Illegal LTL atomic proposition:',typecheck_ap(F,R,Res)),fail.

typecheck_expr(bexpr(E),TE,Type,Res) :- !,
    type_check_raw(E,Type,TE,Res),
    (Type=pred -> add_error(ltl,'Expression expected, but was predicate:',TE), Res=error
    ; true).

typecheck_expr(F,R,T,Res) :-
    add_internal_error('Illegal LTL atomic expression:',typecheck_expr(F,R,T,Res)),fail.

typecheck_temporal_formula(ap(AP),ap(Typed),Res) :-
    !,typecheck_ap(AP,Typed,Res).

typecheck_temporal_formula(action(TP),action(Typed),Res) :-
    !,typecheck_tp(TP,Typed,Res).

typecheck_temporal_formula(ena(TP,F),ena(Typed,R),Res) :- % used in CTL only
    !,typecheck_tp(TP,Typed,Res),
    typecheck_temporal_formula(F,R,Res).

typecheck_temporal_formula(F,R,Res) :-
    F =.. [Functor|InArgs],
    same_length(InArgs,OutArgs),
    R =.. [Functor|OutArgs],
    typecheck_temporal_formula_l(InArgs,OutArgs,Res).

typecheck_temporal_formula_l([],[],_).

typecheck_temporal_formula_l([F|Frest],[R|Rrest],Res) :-
    typecheck_temporal_formula(F,R,Res),
    typecheck_temporal_formula_l(Frest,Rrest,Res).

typecheck_tp(unparsed_trans(Op),xtl(Opname,Arity,Args),ResultFlag) :-
    animation_mode(xtl), !,
    ( compound(Op) -> functor(Op,Opname,Arity), Op =.. [_|Args]
    ; split_atom(Op,['.'],[Opname|Args]) ->
    length(Args,Arity)
    ;
    add_error(ltl,'Failed to parse operation specification'),
    ResultFlag = error).

typecheck_tp(unparsed_trans(Opname),csp(Channel,Arity,ResArgs),ResultFlag) :-
    csp_mode,!,
    ( Opname = tick
    -> Channel=Opname, Arity=0, ResArgs=[] % should we set Arity ??
    ; Opname = tau
    -> Channel=Opname, Arity=0, ResArgs=[] % should we set Arity ??
    ; (split_atom(Opname,['.','!'],[Channel|Args]), channel(Channel,_))
    ->
    (channel_type_list(Channel, TypeList),length(TypeList,Arity),length(Args,Arity)
    -> (Arity = 0
    -> ResArgs = []
    ; (\+memberchk('_',Args)
    % we want to call the CSP-M parser only once when there is no '_' symbol in Args
    -> mergeArgsToDotTuple([Channel|Args],DotTupleEvent),
    parse_single_csp_expression(ltl,DotTupleEvent,ParsedEvent),
    splitToSingleArgs(ParsedEvent,[Channel|ResArgs],Arity)
    ; l_parse_single_csp_expression_undescore(ltl,Args,ResArgs)
    )
    )
    ; add_error(ltl,'Number of arguments not correct for: ', Opname),
    ResultFlag=error, ResArgs=[], Arity = 0
    )
    ;
    add_error(ltl,'Channel does not exist: ',Opname),
    ResultFlag = error, ResArgs=[], Arity = 0
).

typecheck_tp(bop(oppattern(_Pos,Name,Args)),Result,ResultFlag) :- !,
    ( b_or_z_mode, b_get_machine_operation(Name,Results,Parameters,_) ->
    Result = bop(Name,NumberArgs,NumberResults,ArgPatterns,ResPatterns),
    length(Parameters,NumberArgs), length(Results,NumberResults),
    % Pattern matching for results is not yet supported
    ResPatterns = [],
    ( Args=[] ->
    ArgPatterns = [],
    ResPatterns = []
    ; length(Args,NumberArgs) ->
    create_b_op_patterns(Args,Parameters,ArgPatterns,ResultFlag)
    ;
    add_error(ltl,'Number of arguments not correct for: ', Name),ResultFlag=error)
    ; (csp_mode ; xtl_mode), Args=[] ->
    debug_println(9,unparsed_trans(Name)),
    typecheck_tp(unparsed_trans(Name),Result,ResultFlag)
    ;
    add_error(ltl,'Could not find operation: ', Name),ResultFlag=error).

typecheck_tp(btrans(event(Name)),btrans(event(Name)),_ResultFlag) :- !.

typecheck_tp(btrans(event(Name,RawPredicate)),btrans(event(Name,TPredicate,Poststate)),ResultFlag) :- !,
    ( b_get_machine_operation(Name,_,_Parameters,_) ->
    ( bmachine:type_with_errors(RawPredicate,[prepost,operation(Name)],pred,TPredicate) ->
    find_poststate_access(TPredicate,Poststate)
    ; ResultFlag=error)
    ;
    add_error(ltl,'Could not find operation: ', Name),ResultFlag=error).

typecheck_tp(before_after(bpred(RawPredicate)),before_after(TPred),ResultFlag) :- !,
    get_primed_machine_variables(PV),
    (get_preference(symmetry_mode,off) -> Scope = [prob_ids(visible),identifier(PV),variables]
    ; Scope = [identifier(PV),variables]
    ),
    % in classical B x$0 refers to the value before a substitution
    ( bmachine:type_with_errors(RawPredicate,Scope,pred,TPred0)
    -> % see prepost becomes_such b_parse_machine_operation_pre_post_predicate
    inline_prob_deferred_set_elements_into_bexpr(TPred0,TPred) % TODO: we could compute the $0 variables
    ; ResultFlag=error).

typecheck_tp(change_expr(Comparator,Expr),change_expr(Comparator,TypedExpr),Res) :-
    !, typecheck_expr(Expr,TypedExpr,_Type,Res).

typecheck_tp(F,R,Res) :-
    add_internal_error('Illegal LTL transition predicate:',typecheck_tp(F,R,Res)),fail.

typecheck_tp_l([],[],_Res).

typecheck_tp_l([TP|TPs],[TTP|TTPs],Res) :-
    typecheck_tp(TP,TTP,ResultFlag),
    (ResultFlag == error -> Res = error ; Res=Res1),
    typecheck_tp_l(TPs,TTPs,Res1).