b_trace_checking

changed_binding(FromId,ToId,Bind) :-
    visited_expression(FromId,FromState),
    visited_expression(ToId,ToState),
    get_id_binding(ToState,Bind),
    \+ get_id_binding(FromState,Bind).

check_default_trace_for_specfile(File) :- get_default_trace_file(File,TFile),
    tcltk_check_sequence_from_file(prolog,TFile,default_trace_replay).

check_non_det_bind(State,bind(Var,Val)) :- member(bind(Var,StoredVal),State), unify(StoredVal,Val).

check_non_det_vars(NewID,NonDetVars) :-
    visited_expression(NewID,State),
    get_state(State,VarState),
    maplist(check_non_det_bind(VarState),NonDetVars).

convert_action(V,R) :- var(V),!,R=V.

convert_action(io(V,Ch),R) :- !, strip_dots(V,SV),R=io(SV,Ch,_SRCSPAN).

convert_action(io(V,Ch,_),R) :- !, strip_dots(V,SV),R=io(SV,Ch,_SRCSPAN).

convert_action(tick(_SRCSPAN),R) :- !, R = tick(_).

convert_action(X,Res) :- nonvar(X),X=..[F|Args],!,
    l_convert_term(Args,CArgs),Res=..[F|CArgs].

convert_action(X,X).

convert_term(V,R) :- var(V),!,R=V.

convert_term(closure(A,B,C),R) :- !, R=closure(A,B,C). % we may mess with identifiers; see test 1575

convert_term(term(bool(0)),R) :- !, R=pred_false /* bool_false */.

convert_term(term(bool(1)),R) :- !, R=pred_true /* bool_true */.

convert_term(bool_true,pred_true /* bool_true */) :- !.

convert_term(bool_false,pred_false /* bool_false */) :- !.

convert_term(string(S),R) :- !, R=string(S).

convert_term(X,Representation) :- atomic(X), lookup_global_constant(X,Representation),!.

convert_term(X,Res) :- nonvar(X),X=..[F|Args],!,
    l_convert_term(Args,CArgs),Res=..[F|CArgs].

convert_term(X,X).

decompose_binding(bind(ID,Val),ID,Val).

expand_explicit_set([H|T],AA) :- !, custom_explicit_sets:convert_to_avl([H|T],AA).

expand_explicit_set(A,AA) :-
    on_enumeration_warning(custom_explicit_sets:try_expand_and_convert_to_avl_if_smaller_than(A,AA,200), fail).

find_action_in_options(ActionAsTerm,Options,State, Action,ActionOpAsTerm,NewID) :-
    member( (_Id,Action,ActionOpAsTerm,NewID), Options),
    unify_action_as_term(ActionAsTerm,ActionOpAsTerm,State).

find_successor_state(ID,Pred,NewID,_) :-
    % transition(ID,ActionOpAsTerm,OpID,SuccID),
    tcltk_get_options(_),
    current_options(Options), % print(Options),nl,
    member( (_,Action,ActionOpAsTerm,NewID), Options),
    state_space:visited_expression(NewID,State),
    expand_const_and_vars_to_full_store(State,EState),
    % print(try(NewID,State)),nl,
    add_prob_deferred_set_elements_to_store(EState,DEState,all),
    announce_event(start_solving),
    b_interpreter:b_test_boolean_expression_cs(Pred,[],DEState,'find successor state',ID), % deferred
    announce_event(end_solving),
    debug_println(19,successor_found(NewID)),
    print(' --> '),my_print_event(ActionOpAsTerm,_),nl,nl,
    my_perform_action_as_string(Action,ActionOpAsTerm,NewID),
    !.

find_successor_state(ID,Pred,NewID,_LineNr) :-
    max_reached_or_timeout_for_node(ID), % we have not computed all options
    get_op_name_for_state(ID,OpName), print(try_providing_custom_predicate(OpName)),nl,
    tcltk_add_user_executed_operation_typed(OpName,_,Pred,NewID), % The Pred can only talk about parameters and the state before; thus this only works for setup_constants and initialise_machine
    (silent_mode(on) -> true
    ; print_green(successor_found(NewID)),nl,
    print(' --> '),print(OpName),nl),
    !.

find_successor_state(ID,Pred,_,LineNr) :-
    % we could try and execute operation by predicate here; in case max_reached_for_node(ID) or time_out_for_node(ID)
    format('State ID = ~w; line number = ~w~n',[ID,LineNr]),
    (max_reached_for_node(ID)
    -> format_to_codes('Try increasing the MAX_OPERATIONS preference. No successor found satisfying predicate at step ~w of replay: ',[LineNr],Codes)
    ; time_out_for_node(ID) -> format_to_codes('TIME-OUT occurred. No successor found satisfying predicate at step ~w of replay: ',[LineNr],Codes)
    ; format_to_codes('No successor found satisfying predicate at step ~w of replay: ',[LineNr],Codes)
    ),
    atom_codes(Msg,Codes),
    translate:translate_bexpression(Pred,TP),
    add_error(tcltk_check_state_sequence_from_file,Msg,TP),
    fail.

generate_predicate(ArgVal,TypedPara,b(equal(TypedPara,TVal),pred,[])) :-
    get_texpr_type(TypedPara,Type),
    TVal = b(value(ArgVal),Type,[]).

get_change_list(FromId,ToId,ChangedVarNames,ChangedValues) :-
    findall(Bind,changed_binding(FromId,ToId,Bind),List),
    maplist(decompose_binding,List,ChangedVarNames,ChangedValues).

get_default_trace_file(File,TraceFile) :-
    get_default_trace_file(File,'.trace',TraceFile).

get_default_trace_file(File,Ext,TraceFile) :-
    split_filename(File,FN,_MchExt),
    string_concatenate(FN,Ext,TraceFile).

get_id_binding(const_and_vars(_,List),Bind) :- !, member(Bind,List).

get_id_binding(concrete_constants(List),Bind) :- !, member(Bind,List).

get_id_binding(List,Bind) :- !, member(Bind,List).

get_mode_value(deterministic_trace_replay,true,Msg) :-
    Msg = 'Performing deterministic replay (lower memory usage, but no backtracking in case replay fails) for file: ~w~n'.

get_mode_value(backtracking_trace_replay,false,Msg) :-
    Msg = 'Performing replay with backtracking for file: ~w~n'.

get_mode_value(Other,_,_) :- Other \= default_trace_replay,
    add_error(b_trace_checking,'Illegal replay mode: ',Other),fail.

get_op_name_for_state(root,OP) :- !,
    (b_machine_has_constants_or_properties -> OP='$setup_constants' ; OP='$initialise_machine').

get_op_name_for_state(ID,'$initialise_machine') :-
    visited_expression(ID,concrete_constants(_)),!.

get_parameters(RestPair,Paras) :- member('='(params,json(Paras)),RestPair),!.

get_parameters(_,[]). % e.g., for initialise machine

get_state(concrete_constants(X),R) :- !, R=X.

get_state(const_and_vars(_,X),R) :- !, R=X.

get_state(X,X).

get_unchanged_list(FromId,ToId,UnChangedVarNames) :-
    findall(Bind,unchanged_binding(FromId,ToId,Bind),List),
    maplist(decompose_binding,List,UnChangedVarNames,_).

ident(0).

ident(N) :- N > 40, !, N1 is N mod 40, ident(N1).

ident(N) :- N>0, print('- '), N1 is N-1, ident(N1).

insert_nl_prefix(N,Acc,Acc) :- N =< 1,!.

insert_nl_prefix(N,Acc,[10,13|Res]) :- N1 is N-1, insert_nl_prefix(N1,Acc,Res).

is_a_reset_operation(start_cspm_MAIN).

is_a_reset_operation(start_csp_MAIN).

is_a_reset_operation(Op) :- functor(Op,'$setup_constants',_).

is_a_reset_operation(Op) :- functor(Op,Functor,_),
    unify_functor(Functor,'$initialise_machine',root),
    b_or_z_mode, \+ b_machine_has_constants_or_properties.

is_a_set(closure(_,_,_)).

is_a_set([]).

is_a_set([_|_]).

is_a_set(global_set(_)).

is_a_set(avl_set(_)).

l_convert_term([],[]).

l_convert_term([H|T],[CH|CT]) :- convert_term(H,CH), l_convert_term(T,CT).

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

l_generate_predicate([],_,Op,[]) :- !, add_warning(b_trace_checking,'Trace file contains too few parameters for: ',Op).

l_generate_predicate(_,[],Op,[]) :- !, add_warning(b_trace_checking,'Trace file contains too many parameters for: ',Op).

l_generate_predicate([ArgVal|TArg],[TypedPara|TPar],OpName,[Pred|TPred]) :-
    generate_predicate(ArgVal,TypedPara,Pred),
    l_generate_predicate(TArg,TPar,OpName,TPred).

l_unify([],[]).

l_unify([H|T],[I|S]) :- unify(H,I), l_unify(T,S).

my_perform_action_as_string(ActionStr,ActionOpAsTerm,NewID) :-
    tcltk_interface:tcltk_perform_action_string(ActionStr,ActionOpAsTerm,NewID).

my_print_event(Op,OpStrTA) :-
    temporary_set_preference(expand_avl_upto,4,CHNG),
    translate_event(Op,OpStr),
    truncate_atom(OpStr,100,OpStrTA),
    reset_temporary_preference(expand_avl_upto,CHNG),
    write(OpStrTA).

my_see(File) :-
    catch(see(File),
    error(existence_error(_,_),_),
    add_error_fail(my_see,'File does not exist: ',File)).

mytranslate(H,ES) :-
    % should we use unicode mode to avoid more ambiguities?
    translate_bvalue_to_parseable_classicalb(H,S),
    b_escape_json_string_atom(S,ES).

order_paras([],OpName,Rest,[]) :- (Rest=[] -> true ; format('*** Unknown parameters for ~w: ~w~n',[OpName,Rest])).

order_paras([ID|T],OpName,Env,[Val|TVal]) :-
    (select(bind(ID,Val),Env,Env2) -> order_paras(T,OpName,Env2,TVal)
    ; %add_error(translate_json_operation,'Parameter not specified: ',ID:Env), % keep Val a variable
    format('*** Parameter not specified for ~w: ~w~n',[OpName,ID]),
    order_paras(T,OpName,Env,TVal)
).

parse_trace_file(MName,Trace) :-
    safe_read(Term),!,
    (Term = end_of_file -> (Trace = [])
    ; (Term = machine(MName)
    -> Trace = T
    ; Trace = [Term|T]
    ),
    parse_trace_file(MName,T)
).

perform_action_tclk(Action,ActionOpAsTerm,NewID,_Ident) :-
    my_perform_action_as_string(Action,ActionOpAsTerm,NewID),
    tcltk_get_options(_).

perform_action_tclk(_Action,_ActionOpAsTerm,_NewID,Ident) :- % undo action
    state_space:current_state_id(FromID),
    tcltk_interface:tcltk_backtrack,
    tcltk_get_options(_),
    state_space:current_state_id(ToID),
    silent_mode(off),
    ident(Ident),
    print(backtrack_from_to(FromID,ToID)),nl,
    fail.

perform_alternative_op_with_same_functor(Options,Functors,ActionMsg,AltMsg,ActionAsTerm,Action,NewID) :-
    \+ member( (_,_,ActionAsTerm,_), Options),
    (silent_mode(on) -> true
    ; ajoin(['Could not ', ActionMsg, ' with parameters from trace file.'], Msg1),
    ajoin(['Will attempt any possible ', AltMsg, '.'], Msg2),
    print_message(Msg1), print_message(Msg2)
    ),
    %print(ActionAsTerm),nl, print(Options),nl,nl,
    member( (_,ActionStr,MachineActionAsTerm,NewID), Options),
    functor(MachineActionAsTerm,Functor,_),
    member(Functor,Functors),
    (Action=ActionStr -> true ; print(cannot_match(Action,ActionStr)),nl,fail).

perform_custom_operation_retry(OpName,NewID) :-
    (OpName = '$initialise_machine' ; OpName = '$setup_constants'),
    !,
    state_space:current_state_id(CurID),
    (max_reached_for_node(CurID) ; not_all_transitions_added(CurID)),
    preferences:get_preference(maxNrOfInitialisations,0),
    tcltk_add_user_executed_operation_typed(OpName,_,b(truth,pred,[]),NewID),
    (get_preference(deterministic_trace_replay,true) -> ! ; true),
    print_green(init_found(NewID)),nl.

perform_custom_operation_retry(ActionAsTerm,NewID) :-
    (ActionAsTerm = '-->'(_,_) % for operations with return types we cannot provide a predicate to solve yet
    -> preferences:get_preference(maxNrOfEnablingsPerOperation,0)
    ; true),
    state_space:current_state_id(CurID),
    get_operation_name(ActionAsTerm,OpName),
    (max_reached_for_node(CurID) ; time_out_for_node(CurID,OpName,_) ; not_all_transitions_added(CurID)),
    debug_println(9,try_custom(CurID,ActionAsTerm)), % Execute operation by predicate
    % (state_space:transition(CurID,AA,BB,CC),format('Successor of ~w: ~w --~w--> ~w~n',[CurID,AA,BB,CC]),fail ; true),
    get_operation_return_values_and_arguments(ActionAsTerm,ExpectedResults,OpArgs),
    % TO DO: optionally check return values
    (OpArgs = [] -> Pred = b(truth,pred,[])
    ; \+ b_is_operation_name(OpName)
    -> add_error(trace_checking_fails,'Operation does not exist in loaded specification:',OpName),fail
    ; b_get_machine_operation_typed_parameters(OpName,TArgParas),
    l_generate_predicate(OpArgs,TArgParas,OpName,Conjuncts),
    conjunct_predicates(Conjuncts,Pred)
    ),
    !,
    %print('PRED: '),translate:print_bexpr(Pred),nl,
    start_ms_timer(Timer),
    profile_single_call(OpName,CurID,
    tcltk_interface:tcltk_add_user_executed_operation_typed(OpName,OpTerm,Pred,NewID) % The Pred can only talk about parameters and the state before; thus this only works for setup_constants and initialise_machine
    ),
    (get_preference(deterministic_trace_replay,true) -> ! ; true), % by preventing backtracking we can reduce memory consumption
    print_green(successor_found(NewID, OpName)),nl,
    get_operation_return_values_and_arguments(OpTerm,ActualResults,_),
    (l_unify(ExpectedResults,ActualResults) -> true
    ; ajoin(['Result values for ',OpName,' do not match for transition from ',CurID,' to ',NewID,':'],Msg),
    translate_bvalue(ExpectedResults,ER),
    translate_bvalue(ActualResults,AR),
    add_warning(b_trace_checking,Msg,[expected(ER),actual(AR)])
    ),
    (debug_mode(on) -> stop_ms_timer_with_msg(Timer,'Custom: ') ; true),
    garbage_collect, % important to keep memory consumption down for long traces e.g. for Innotrans VBF traces
    (debug_mode(on) -> print_memory_used_wo_gc,nl ; true),
    tcltk_get_options(_).

perform_initialisation :- b_or_z_mode, b_machine_has_constants_or_properties,!,
    perform_sequence_of_operations(['$setup_constants','$initialise_machine']).

perform_initialisation :- perform_sequence_of_operations(['$initialise_machine']).

perform_one_operation_in_sequence('$non_det_modified_vars'(ActionAsTerm,NonDetVars),Ident) :- !,
    current_expression(_CurID,State),
    current_options(Options),
    member( (_Id,Action,ActionOpAsTerm,NewID), Options),
    unify_action_as_term(ActionAsTerm,ActionOpAsTerm,State),
    %ident(Ident), format('checking non_det_modified_vars for ~w in ~w~n',[ActionAsTerm,NewID]),nl,
    check_non_det_vars(NewID,NonDetVars),
    !,
    perform_action_tclk(Action,ActionOpAsTerm,NewID,Ident).

perform_one_operation_in_sequence('$non_det_modified_vars'(Op,_),Ident) :- !,
    ident(Ident), format('ignoring non_det_modified_vars for ~w~n',[Op]), % TO DO: use constraint-based finding of successor
    perform_one_operation_in_sequence(Op,Ident).

perform_one_operation_in_sequence('$check_value'(ID,VAL),Ident) :- !,
    ident(Ident), format('checking value of ~w ',[ID]),
    state_space:current_expression(_,State),
    expand_const_and_vars_to_full_store(State,EState),
    lookup_value_for_existing_id(ID,EState,StoredVal),
    translate:print_bvalue(StoredVal),
    (unify(StoredVal,VAL) -> print_green(' ok'),nl
    ; print_red(' failed'),nl, %print(StoredVal),nl, print(VAL),nl,
    fail).

perform_one_operation_in_sequence(Op,Ident) :-
    (silent_mode(on) -> true
    ; ident(Ident),print('<- '),print(Ident), print(': '), my_print_event(Op,OpStr),
    print(' :: '),
    state_space:current_state_id(CurID), print(CurID),nl
    ),
    (is_a_reset_operation(Op)
    -> tcltk_reset, %tcltk_goto_state(reset,root), % reset animation history
    tcltk_get_options(_)
    ; true),
    convert_action(Op,COp),
    if(perform_single_operation(COp,Ident),true,
    (silent_mode(off),
    ident(Ident), print_red(' **** FAIL ****'),nl,
    fail)),
    (get_preference(deterministic_trace_replay,true) -> ! ; true),
    (silent_mode(on) -> true
    ; ident(Ident), print(' | '), print(Ident), print(': '), print(OpStr),
    %functor(Op,OpName,_), print(OpName),
    %((OpName = '-->', arg(1,Op,A1), functor(A1,RealOpName,_)) -> print(RealOpName) ; true),
    print_green(' success -->'),
    state_space:current_state_id(NewCurID),
    statistics(walltime,[Tot,Delta]),
    format('~w [~w (Delta ~w) ms]~n',[NewCurID,Tot,Delta])
).

perform_sequence_of_operations(Trace) :-
    retractall(max_nr_replayed(_)),
    assertz(max_nr_replayed(0)),
    perform_sequence_of_operations2(Trace,0).

perform_sequence_of_operations2([],Ident) :-
    (silent_mode(on) -> true ; ident(Ident),print('SUCCESS'),nl).

perform_sequence_of_operations2([Op|T],Ident) :-
    get_error_context(Context),
    state_space:current_state_id(ID),get_operation_name(Op,FOP),
    set_error_context(operation(FOP,ID)),
    perform_one_operation_in_sequence(Op,Ident),
    update_max_nr_replayed(Ident),
    restore_error_context(Context),
    Ident1 is Ident+1,
    (get_preference(deterministic_trace_replay,true) -> ! ; true),
    perform_sequence_of_operations2(T,Ident1).

perform_single_operation('$jump'(TO,FROM),Ident) :- !,
    current_state_id(ID),
    print_red('Warning: trace file contains JUMP!'),nl,
    (ID=FROM -> true ; ident(Ident),format('Cannot perform jump from ~w (to ~w)~n',[FROM,TO])),
    (visited_expression_id(TO) -> tcltk_interface:tcltk_goto_state(jump,TO)
    ; add_error(trace_checking_fails,'State ID does not exist for jump:',TO),fail
).

perform_single_operation(ActionAsTerm,Ident) :-
    % tools_printing:print_term_summary(perform_single_op(ActionAsTerm)),
    current_expression(_CurID,State),
    current_options(Options),
    ( if( find_action_in_options(ActionAsTerm,Options,State, Action,ActionOpAsTerm,NewID),
    perform_action_tclk(Action,ActionOpAsTerm,NewID,Ident),
    if(perform_single_operation_retry(Options,ActionAsTerm,Action,NewID,State),
    perform_action_tclk(Action,_AlternateActionOpAsTerm,NewID,Ident),
    if(perform_custom_operation_retry(ActionAsTerm,_NewID),true,
    (replace_result_by_variable(ActionAsTerm,A2),
    find_action_in_options(A2,Options,State, Action,_,NewID),
    (silent_mode(on) -> true ; format_with_colour_nl(user_output,[red],'Result of operation call in trace does not match, e.g., ~w leading to state ~w',[Action,NewID])),
    fail
    )
    )
    )
   
    )
    ;
    single_operation_skip(ActionAsTerm,Ident)
    ),
    (get_preference(deterministic_trace_replay,true) -> ! ; true).

perform_single_operation(ActionAsTerm,Ident) :-
    current_options(Options),
    member( (_Id,PActionS,'*permute*',NewID), Options), /* permute action from symmetry reduction */
    perform_action_tclk(PActionS,'*permute*',NewID,Ident), !,
    (silent_mode(on) -> true
    ; ident(Ident), print(' | ** PERMUTING **'),nl),
    perform_single_operation(ActionAsTerm,Ident).

perform_single_operation(ActionAsTerm,Ident) :-
    %%user:current_expression(CurID,State),
    \+ functor(ActionAsTerm,tau,1),
    current_options(Options), %print(options(Options)),nl,
    member( (_Id,AX,tau(X),NewID), Options),
    (silent_mode(on) -> true
    ; ident(Ident), print(' | ** SKIPPING ADDITIONAL TAU in SPEC. **'),nl),
    perform_action_tclk(AX,tau(X),NewID,Ident),
    perform_single_operation(ActionAsTerm,Ident).

perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :-
    functor(ActionAsTerm,'$setup_constants',_), !,
    (get_prob_application_type(tcltk) -> OTHER = ['$partial_setup_constants'] ; OTHER = []),
    perform_alternative_op_with_same_functor(Options, ['$setup_constants' | OTHER],
    'set up constants', 'initialisation of constants',
    ActionAsTerm, Action, NewID),
    %visited_expression(NewID,concrete_constants(C)), ActionAsTerm =.. [_|Args],
    % check that state NewID corresponds to parameters provided for setup_constants in trace file
    %print(check_args),nl, check_initialised_args(Args,C), print('argsok'),nl. % TO DO: try and enable this for all tests
    true.

perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :-
    functor(ActionAsTerm,'$initialise_machine',_),!,
    perform_alternative_op_with_same_functor(Options, ['$initialise_machine'],
    'initialise', 'initialisation',
    ActionAsTerm, Action, NewID),
    true. %visited_expression(NewID,S), (S=const_and_vars(_,VS) -> true ; VS=S), ActionAsTerm =.. [_|Args],

perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :-
    functor(ActionAsTerm,tau,_), arg(1,ActionAsTerm,Arg), nonvar(Arg),!,
    perform_alternative_op_with_same_functor(Options, [tau],
    tau, tau,
    ActionAsTerm, Action, NewID).

perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :-
    functor(ActionAsTerm,F,0), preference(show_eventb_any_arguments,true),
    /* then allow also the same operation name but with more arguments */
    member( (_Id,Action,ActionAsTerm2,NewID), Options),
    functor(ActionAsTerm2,F,FArity), FArity>0,
    formatsilent('% Allowing extra Event-B style ANY arguments.~n',[]).

perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :-
    functor(ActionAsTerm,F,N),N>0, preference(show_eventb_any_arguments,false),
    /* then allow also the same operation name but with more arguments */
    member( (_Id,Action,F,NewID), Options),
    formatsilent('% Allowing operation without Event-B style ANY arguments.~n',[]).

perform_single_operation_retry(Options,ActionAsTerm,Action,NewID,root) :-
    functor(ActionAsTerm,'setup_constants',_), !, % rename to new format
    nl,print('DEPRECATED TRACE FILE'),nl,nl,nl,
    ActionAsTerm =.. [_|Args], ActionAsTerm2 =..['$setup_constants'|Args],
    perform_single_operation_retry(Options,ActionAsTerm2,Action,NewID).

perform_single_operation_retry(Options,ActionAsTerm,Action,NewID,State) :-
    (State=root ; State=concrete_constants(_)),
    functor(ActionAsTerm,'initialise_machine',_), !, % rename to new format
    nl,print('DEPRECATED TRACE FILE'),nl,nl,nl,
    ActionAsTerm =.. [_|Args], ActionAsTerm2 =..['$initialise_machine'|Args],
    perform_single_operation_retry(Options,ActionAsTerm2,Action,NewID).

perform_single_operation_retry(Options,ActionAsTerm,Action,NewID,_State) :-
    perform_single_operation_retry(Options,ActionAsTerm,Action,NewID).

print_fdr([]) :- print('STOP'),nl.

print_fdr([jump|T]) :- print_fdr(T).

print_fdr([action(Str,Term)|T]) :-
    (Term = i(_)
    -> (nl,print(' ( STOP /\\ '))
    ; (Term = tick(_)
    -> print('SKIP ; ')
    ; ((Term = tau(_) ; Term = 'start_cspm_MAIN')
    -> true
    ; (print(Str), print(' -> '))
    )
    )),
    print_fdr(T),
    (Term = i(_)
    -> print(' )')
    ; true
).

print_json_list([],_,_).

print_json_list([H|T],FromID,Stream) :-
    (H=jump(NewID) -> true
    ; print_json_opid(Stream,H,FromID,NewID) -> true
    ; add_error(print_json_list,'Writing operation failed: ',H), NewID=FromID),
    (T==[]
    -> nl(Stream)
    ; format(Stream,',~n',[]), print_json_list(T,NewID,Stream)).

print_json_names([],_).

print_json_names([HName|T],Stream) :-
    b_escape_json_string_atom(HName,EN),
    (T=[] -> format(Stream,' "~w"~n',[EN])
    ; format(Stream,' "~w",~n',[EN])),
    print_json_names(T,Stream).

print_json_opid(Stream,OpId,PrevId,SuccId) :-
    (transition(PrevId,Op,OpId,SuccId) -> PrevId1=PrevId
    ; add_warning(print_json_list,'Cannot find operation id from given source id: ',OpId:from(PrevId):to(SuccId)),
    transition(PrevId1,Op,OpId,SuccId)
    ),
    get_operation_internal_name(Op,OpName), % TO DO: currently this is INITIALISATION instead of $initialise_machine
    (get_possible_language_specific_top_level_event(OpName,ResultNames,ParaNames) -> true
    ; ResultNames=unknown, ParaNames=unknown),
    get_operation_return_values_and_arguments(Op,ReturnValues,Paras),
    % TO DO: extract variables and constants for $initialise_machine, $setup_constants
    format(Stream,' {~n',[]),
    format(Stream,' "name": "~w",~n',[OpName]),
    (get_operation_description_for_transition(PrevId,Op,Desc)
    -> b_escape_json_string_atom(Desc,ED), format(Stream,' "description": "~w",~n',[ED]) ; true),
    (Paras = []
    -> true % do not print Paras to reduce memory in JSON file
    ; format(Stream,' "params": {~n',[]),
    (get_preference(show_eventb_any_arguments,true),
    \+ same_length(Paras,ParaNames)
    -> true % we cannot easily use the parameters during replay; ANY parameters are currently only added when there are no other parameters
    %print_json_paras(Paras,1,unknown,Stream)
    ; print_json_paras(Paras,1,ParaNames,Stream)
    ),
    format(Stream,' },~n',[])
    ),
    (ReturnValues = []
    -> true % do not print results to reduce memory in JSON file
    ; format(Stream,' "results": {~n',[]),
    print_json_paras(ReturnValues,1,ResultNames,Stream),
    format(Stream,' },~n',[])
    ),
    format(Stream,' "destState": {~n',[]),
    get_change_list(PrevId1,SuccId,ChangedVarNames,ChangedValues),
    print_json_paras(ChangedValues,1,ChangedVarNames,Stream),
    format(Stream,' },~n',[]),
    format(Stream,' "destStateNotChanged": [~n',[]),
    get_unchanged_list(PrevId1,SuccId,UnChangedVarNames),
    print_json_names(UnChangedVarNames,Stream),
    format(Stream,' ]~n',[]),
    %format(Stream,' ",preds": null~n',[]), % do not print to reduce memory
    format(Stream,' }',[]).

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

print_json_paras([H|T],Nr,[HName|NT],Stream) :- !, Nr1 is Nr+1,
    b_escape_json_string_atom(HName,EN),
    mytranslate(H,ES),
    format(Stream,' "~w": "~w"',[EN,ES]),
    (T==[] -> nl(Stream)
    ; format(Stream,',~n',[]), print_json_paras(T,Nr1,NT,Stream)).

print_json_paras([H|T],Nr,unknown,Stream) :- Nr1 is Nr+1,
    mytranslate(H,ES),
    !,
    format(Stream,' "para~w": "~w"',[Nr,ES]),
    (T==[] -> nl(Stream)
    ; format(Stream,',~n',[]), print_json_paras(T,Nr1,unknown,Stream)).

print_json_paras(P,Nr,PN,_) :- add_internal_error('Cannot print JSON parameters:',print_json_paras(P,Nr,PN)).

print_trace_as_fdr_check :- silent_mode(on),!.

print_trace_as_fdr_check :-
    print('-- Trace Check Generated by ProB:'),nl,
    get_action_trace(T),
    reverse(T,RT),
    print('PROB_TEST_TRACE = '),print_fdr(RT),
    nl,
    print('assert MAIN [T= PROB_TEST_TRACE'),nl.

print_trace_for_replay(Style,Options,Stream) :-
    op_trace_ids(OpIds),
    reverse(OpIds,Trace),
    print_trace_for_replay(Style,Trace,Options,Stream).

print_trace_for_replay(prolog,Trace,_,Stream) :- !, print_transition_list_prolog(Trace,Stream).

print_trace_for_replay(json,Trace,Options,Stream) :- !, print_transition_list_json(Trace,Options,Stream).

print_trace_for_replay(Style,_,_,_Stream) :-
    add_internal_error('Style not supported: ',print_trace_for_replay(Style,_,_,_)).

print_transition_list_json(Trace,Options,Stream) :-
    get_prob_application_type(ApplType),
    (get_member_option(description,Options,Desc) -> true
    ; ApplType=probcli -> Desc = 'File created by probcli'
    ; ApplType=tcltk -> Desc = 'File created by ProB Tcl/Tk'
    ; Desc = 'File created by ProB'
    ),
    format(Stream,'{~n "description": "~w",~n',[Desc]),
    format(Stream,' "transitionList": [~n',[]),
    temporary_set_preference(expand_avl_upto,-1,CHNG),
    call_cleanup(
    print_json_list(Trace,root,Stream),
    reset_temporary_preference(expand_avl_upto,CHNG)),
    format(Stream,' ],~n "metadata": {~n',[]),
    format(Stream,' "fileType": "~w",~n',['Trace']),
    format(Stream,' "formatVersion": ~w,~n',[1]),
    datime(datime(Yr,Mon,Day,Hr,Min,Sec)),
    number_codes_min_length(Mon,2,MonC),
    number_codes_min_length(Day,2,DayC),
    number_codes_min_length(Hr,2,HrC),
    number_codes_min_length(Min,2,MinC),
    number_codes_min_length(Sec,2,SecC),
    % TODO: rename to createdAt and make optional for testing
    format(Stream,' "savedAt": "~w-~s-~sT~s:~s:~sZ",~n',[Yr,MonC,DayC,HrC,MinC,SecC]), % ~2
    % example: "2020-12-23T14:33:00Z",
    (environ('USER',User)
    -> format(Stream,' "creator": "~w (~w)",~n',[ApplType,User])
    ; format(Stream,' "creator": "~w",~n',[ApplType])
    ),
    version_str(Version),
    format(Stream,' "proBCliVersion": "~w",~n',[Version]),
    revision(Rev),
    format(Stream,' "proBCliRevision": "~w",~n',[Rev]),
    currently_opened_file(File),
    (b_or_z_mode -> b_machine_name(Model) ; get_modulename_filename(File,Model)),
    format(Stream,' "modelName": "~w",~n',[Model]),
    format(Stream,' "modelFile": "~w"~n',[File]),
    format(Stream,' }~n}~n',[]).

print_transition_list_prolog(Trace,Stream) :-
    member(OpId,Trace),
    transition(PrevId,Op,OpId,SuccId),
    (atomic(Op),
    ( transition(PrevId,Op,_,SuccId2), SuccId2 \= SuccId -> true), % another transition with same label Op exists
    translate:get_non_det_modified_vars_in_target_id(Op,SuccId,NonDetVars)
    -> print_quoted(Stream,'$non_det_modified_vars'(Op,NonDetVars))
    ; print_quoted(Stream, Op)
    ),
    format(Stream,'.~n',[]),
    fail.

print_transition_list_prolog(_,_).