b_intelligent_trace_replay

add_parameter_error(Error,Name,ExpressionCodes,OpName,Pos) :-
    translate_operation_name(OpName,TOp),
    ajoin(['Ignoring JSON value for parameter ',Name,' of ',TOp,' due to ',Error,':'], Msg),
    atom_codes(A,ExpressionCodes),
    add_error(translate_json_para,Msg,A,Pos),fail.

add_replay_error(Msg,Term) --> {gen_replay_error(Msg,Term,Err)}, [Err].

add_rest([]) --> [].

add_rest([Bind|T]) --> {is_bind(Bind,ID,_)}, [ID], add_rest(T).

analyse_step_match(TransSpec,FromID,TransID,DeltaList) :-
    TransSpec = transition_spec(OpName, _, ParaStore, ResultStore, DestStore, _UnchangedVars, _Preds, _Postconditions),
    get_sorted_transition_details(FromID,TransID,DestID,TOpName,FullParaStore,FullResultStore),
    (TOpName=OpName -> DeltaList=DL1 ; DeltaList=['Name'|DL1]),
    delta_store_match(FullParaStore,paras,ParaStore,DL1,DL2),
    delta_store_match(FullResultStore,results,ResultStore,DL2,DL3),
    visited_expression(DestID,DestState),
    get_dest_store(DestState,FullDestStore),
    delta_store_match(FullDestStore,dest,DestStore,DL3,DL4),
    % TO DO: UnchangedVars and _Preds
    DL4=[],!.

analyse_step_match(TransSpec,FromID,TransID,DeltaList) :-
    add_internal_error('Call failed:',analyse_step_match(TransSpec,FromID,TransID,DeltaList)),
    DeltaList=['??ERROR??'].

assert_mismatch(Var) :- var(Var),!, Var=optimize.

assert_mismatch(require_mismatch). % probably not useful; difficult to support by predicate

assert_mismatch(optimize).

b_get_op_non_det_modifies(Op,NonDetModifies) :- is_setup_constants_op(Op),
    !,% return all constants as non-det modifies
    b_get_machine_constants(TConsts),get_texpr_ids(TConsts,ND),
    sort(ND,NonDetModifies).

b_get_op_non_det_modifies(OpName,NonDetModifies) :- b_get_operation_non_det_modifies(OpName,NonDetModifies).

b_get_operation_typed_paras('$setup_constants',Paras) :- !,
    Paras=[]. % for trace replay we assume setup_constants to have no parameters

b_get_operation_typed_paras('$initialise_machine',Paras) :- !, Paras=[]. % ditto

b_get_operation_typed_paras('$partial_setup_constants',Paras) :- !, Paras=[]. % ditto

b_get_operation_typed_paras(OpName,Paras) :- b_or_z_mode,!,
    b_get_machine_operation_typed_parameters_for_animation(OpName,Paras).

b_get_operation_typed_paras(OpName,[]) :-
    add_message(replay_json_trace_file,'Not in B mode, cannot obtain parameter info for: ',OpName).

b_get_operation_typed_results('$setup_constants',Results) :- !,
    Results=[]. % for trace replay we assume setup_constants to have no result variables

b_get_operation_typed_results('$initialise_machine',Results) :- !, Results=[]. % ditto

b_get_operation_typed_results('$partial_setup_constants',Results) :- !, Results=[]. % ditto

b_get_operation_typed_results(OpName,Results) :- b_or_z_mode, !, b_get_machine_operation_typed_results(OpName,Results).

b_get_operation_typed_results(_,[]).

bind_id_is_element_of(Vars,Bind) :- is_bind(Bind,ID,_), member(ID,Vars). % we could use ord_member

check_and_adapt_trace_step(transition_spec(OpName, Meta, _, _, DestStore, UnchangedVars,Preds, Postconditions), Step,
    transition_spec(OpName, Meta, [], [], DestStore2,UnchangedVars2,Preds, Postconditions)) -->
    {\+ b_or_z_mode},!,
    exclude_and_collect_errors(unknown_variable_binding(Step,OpName),DestStore,DestStore2),
    exclude_and_collect_errors(unknown_variable(Step,OpName),UnchangedVars,UnchangedVars2).

check_and_adapt_trace_step(transition_spec(OpName, Meta, ParaStore,ResultStore, DestStore, UnchangedVars,Preds, Postconditions),
    Step,
    transition_spec(OpName2,Meta2,ParaStore2,ResultStore2,DestStore2,UnchangedVars2,Preds2, Postconditions2)) -->
    {b_get_operation_typed_results(OpName,TOpResults)},
    {b_get_operation_typed_paras(OpName,TOpParas)},
    !,
    {OpName2=OpName},
    {Meta2=Meta}, % TO DO: include excluded infos
    {Preds2=Preds}, %TO DO: check if all identifiers bound
    {Postconditions2=Postconditions}, % TODO Check operation names and predicate identifiers
    exclude_and_collect_errors(unknown_para_binding(OpName,TOpParas,'parameter',Step),ParaStore,ParaStore2),
    exclude_and_collect_errors(unknown_para_binding(OpName,TOpResults,'result variable',Step),ResultStore,ResultStore2),
    ({is_setup_constants_op(OpName)}
    -> exclude_and_collect_errors(unknown_constant_binding(Step),DestStore,DestStore2),
    {UnchangedVars2 = []},
    ({UnchangedVars = []} -> []
    ; {add_error(b_intelligent_trace_replay,'Illegal unchanged info for SETUP_CONSTANTS',UnchangedVars)}
    )
    ; exclude_and_collect_errors(unknown_variable_binding(Step,OpName),DestStore,DestStore2),
    exclude_and_collect_errors(unknown_variable(Step,OpName),UnchangedVars,UnchangedVars2)
).

check_and_adapt_trace_step(transition_spec(OpName, Meta,_, _, DestStore, UnchangedVars,Preds, Postconditions), Step,
    transition_spec(_, Meta2, [], [], DestStore2, UnchangedVars2,Preds, Postconditions)) -->
    add_replay_error('Unknown operation: ',OpName), % TODO treat $JUMP
    {Meta2 = [unknown_operation/OpName | Meta]},
    % TODO: maybe do a fuzzy match and check if a new operation not used in the trace file exists
    exclude_and_collect_errors(unknown_variable_binding(Step,OpName),DestStore,DestStore2),
    exclude_and_collect_errors(unknown_variable(Step,OpName),UnchangedVars,UnchangedVars2).

check_model_name(ModelName) :-
    currently_opened_specification_name(CurModelName),!,
    (CurModelName=ModelName -> true
    ; dummy_machine_name(ModelName,CurModelName) % CurModelName = MAIN_MACHINE_FOR_...
    -> true
    ; ModelName = 'dummy(uses)'
    -> true % if modelName is "null" this is the value used
    ; prob2_ui_suffix(ModelName,CurModelName) ->
    % happens when ProB2-UI saves trace files; sometimes it adds (2), ... suffix, see issue #243
    add_message(replay_json_trace_file, 'JSON trace file model name has a ProB2-UI suffix: ', ModelName)
    ; ajoin(['JSON trace file model name ',ModelName,' does not match current model name: '],MMsg),
    add_warning(replay_json_trace_file, MMsg, CurModelName)
).

check_model_name(ModelName) :-
    add_warning(replay_json_trace_file, 'Cannot determine current model name to check stored name:', ModelName).

check_postcondition(state_predicate(Pred),Nr,StateID) -->
    {get_state_for_b_formula(StateID,Pred,State)},
    ({b_test_boolean_expression_for_ground_state(Pred,[],State,'trace replay postconditions',Nr)} ->
    []
    ;
    add_replay_error('Failed postcondition (predicate):',Nr)
).

check_postcondition(operation_enabled(OpName,Pred,Enabled),Nr,StateID) -->
    {
    precise_match_spec(MatchSpec),
    TransitionSpec = transition_spec(OpName,[],[],[],[],[],[Pred],[]),
    (perform_single_replay_step(StateID,_,_,MatchSpec,TransitionSpec) -> Actual = enabled ; Actual = disabled)
    },
    ({Enabled == Actual} ->
    []
    ;
    {ajoin(['Failed postcondition (operation ',OpName,' should be ',Enabled,'):'],Msg)},
    add_replay_error(Msg,Nr)
).

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

check_postconditions([Postcondition|Postconditions],Nr,StateID) -->
    check_postcondition(Postcondition,Nr,StateID),
    {Nr1 is Nr+1},
    check_postconditions(Postconditions,Nr1,StateID).

check_replay_status(imperfect,Steps,_) :- !,
    ajoin(['Imperfect replay, steps replayed: '],Msg),
    add_warning(replay_json_trace_file,Msg, Steps).

check_replay_status(partial,Steps,AllSteps) :- !,
    ajoin(['Replay of all ',AllSteps,' steps not possible, steps replayed: '],Msg),
    add_error(replay_json_trace_file,Msg, Steps).

check_replay_status(perfect,Steps,_) :-
    add_message(replay_json_trace_file,'Perfect replay possible, steps replayed: ', Steps).

check_step_postconditions(transition_spec(_, _, _, _, _, _, _, Postconditions),StateID) -->
    check_postconditions(Postconditions,1,StateID).

check_value_equal(ID,Val1,Val2) :-
    temporary_set_preference(allow_enumeration_of_infinite_types,true,OldValueOfPref),
    call_cleanup(check_value_equal_aux(ID,Val1,Val2),
    reset_temporary_preference(allow_enumeration_of_infinite_types,OldValueOfPref)).

check_value_equal_aux(ID,closure(P1,T1,B1),C2) :- C2 = closure(P2,T2,B2),
    C1 = closure(P1,T1,B1),
    !, % we have two symbolic values
    (same_closure(C1,C2)
    -> true
    ; % simple comparison failed, now try and normalize the symbolic values and compare again
    temporary_set_preference(normalize_ast,true,CHANGE),
    % normalize_ast_sort_commutative should probably be false, unless we improve the sorting
    %print(compiling_cur_value(ID)),nl,
    clean_up(B1,[],B1C),
    %we could call: b_compiler:b_compile_closure(closure(P1,T1,B1C),closure(P12,T12,B12)),
    %print(compiling_trace_value(ID)),nl,
    clean_up(B2,[],B2C),
    reset_temporary_preference(normalize_ast,CHANGE),
    (same_closure(closure(P1,T1,B1C),closure(P2,T2,B2C))
    -> true
    ; Val=closure(P1,T1,B1C), Val2 = closure(P2,T2,B2C),
    debug_mode(on),
    translate_bvalue_with_limit(Val,500,V1), translate_bvalue_with_limit(Val2,500,V2),
    formatsilent_with_colour(user_output,[red],'==> Symbolic Mismatch for ~w:~n ~w~n (trace) ~w~n',[ID,V1,V2]),
    % trace, same_closure(closure(P1,T1,B1C),closure(P2,T2,B2C)),
    fail
)
).

check_value_equal_aux(ID,Val1,Val2) :-
    catch(
    equal_object_time_out(Val1,Val2,ID,2500),
    enumeration_warning(_A,_B,_C,_D,_E),
    (format_with_colour(user_output,[red],'==> Enumeration warning when comparing values for ~w~n',[ID]),fail)
).

convert_prolog_trace_step(Fact,
    transition_spec(OpName,Meta,ParaStore,ResultStore,DestStore,Unchanged,PredList,[])) :-
    PredList=[], Unchanged=[], Meta=[], DestStore = [],
    decompose_operation(Fact,OpName,ParaStore,ResultStore).

count_mismatches(FullStore,Key,PartialStore,Mismatches) :-
    count_mismatches_aux(FullStore,Key,PartialStore,0,Mismatches).

count_mismatches_aux(_,_,[],Acc,Res) :- !,Res=Acc.

count_mismatches_aux([],Key,PartialStore,_,_) :-
    ajoin(['Saved trace step contains unknown bindings for ',Key,': '],Msg),
    add_error(b_intelligent_trace_replay,Msg,PartialStore),
    fail.

count_mismatches_aux([Bind1|T],Key,[Bind2|T2],Acc,Res) :-
    is_bind(Bind1,ID,Val), is_bind(Bind2,ID,Val2),!,
    (check_value_equal(ID,Val,Val2)
    -> count_mismatches_aux(T,Key,T2,Acc,Res)
    ; (debug_mode(off) -> true
    ; translate_bvalue_with_limit(Val,200,V1), translate_bvalue_with_limit(Val2,200,V2),
    formatsilent_with_colour(user_output,[red],'==> Mismatch for ~w ~w:~n ~w~n (trace) ~w~n',[Key,ID,V1,V2])
    %nl,print(Val),nl,nl,print(Val2),nl,nl,
    ),
    inc_mismatches(Acc,Acc1,Res),
    count_mismatches_aux(T,Key,T2,Acc1,Res)
).

count_mismatches_aux([_ID|T],Key,PartialStore,Acc,Res) :- count_mismatches_aux(T,Key,PartialStore,Acc,Res).

count_store_mismatches(FullStore,PartialStore,Key,MatchSpec,MismatchesIn,MismatchesOut) :-
    get_match_spec_val(Key,MatchSpec,MatchVal), !,
    (MatchVal=match
    -> MismatchesIn=MismatchesOut,
    count_mismatches(FullStore,Key,PartialStore,0)
    ; count_mismatches(FullStore,Key,PartialStore,Mismatches),
    MismatchesOut is MismatchesIn+Mismatches,
    %print(new_mm(MismatchesOut,Key,MatchVal,Mismatches)),nl,
    (Mismatches=0 -> true
    ; assert_mismatch(MatchVal))
).

count_store_mismatches(_,_,_Key,_,M,M). % key does not exist; no matching required

create_position(From-To,File,ProBPos) :-
    ProBPos=src_position_with_filename_and_ec(From,1,To,1,File).

create_sorted_store([],Paras,OpName,SortedParaStore) :- Paras = [_|_],
    get_preference(show_eventb_any_arguments,false),!,
    add_message(b_intelligent_trace_replay,'Prolog trace file contains values for virtual parameters (set SHOW_EVENTB_ANY_VALUES to TRUE to better replay this trace file): ',OpName),
    SortedParaStore = [].

create_sorted_store(ParaNames,[],_OpName,SortedParaStore) :- ParaNames = [_|_],
    get_preference(show_eventb_any_arguments,true),!,
    add_message(b_intelligent_trace_replay,'Prolog trace file contains no values for parameters (maybe SHOW_EVENTB_ANY_VALUES was FALSE when trace file was created): ',ParaNames),
    SortedParaStore = [].

create_sorted_store(ParaNames,Paras,OpName,SortedParaStore) :-
    create_local_store_for_operation(ParaNames,Paras,OpName,ParaStore),
    sort(ParaStore,SortedParaStore).

decompose_operation('-->'(OpTerm,Results),OpName,ParaStore,ResultStore) :- !,
    decompose_operation2(OpTerm,OpName,ParaStore),
    (b_get_machine_operation_result_names(OpName,ResultNames)
    -> create_sorted_store(ResultNames,Results,OpName,ResultStore)
    ; ResultStore = []).

decompose_operation(OpTerm,OpName,ParaStore,[]) :- decompose_operation2(OpTerm,OpName,ParaStore).

decompose_operation2(OpTerm,OpName,ParaStore) :-
    functor(OpTerm,Functor,Arity),
    is_setup_or_init(Functor,OpName),
    !,
    % the order of constants, variables etc has changed in ProB;
    % in general we cannot reconstruct the association of the arguments to variables or constants
    (Arity=0 -> true
    ; add_message(b_intelligent_trace_replay,'Ignoring parameters of:',OpName)),
    ParaStore=[].

decompose_operation2(OpTerm,OpName,ParaStore) :-
    OpTerm =.. [OpName|Paras],
    (b_get_machine_operation_parameter_names_for_animation(OpName,ParaNames)
    -> create_sorted_store(ParaNames,Paras,OpName,ParaStore)
    ; ParaStore = [],
    add_error(read_prolog_trace_file,'Unknown operation in trace file:',OpName)
).

default_match_specs([MatchSpec,MS2,MS3]) :-
    precise_match_spec(MatchSpec), % require precise replay
    ignore_dest_match_spec(MS2),
    opname_optimize_match_spec(MS3).

delta_store_match(_,_,[]) --> !.

delta_store_match([],_Key,Rest)
    --> add_rest(Rest). % these bindings were probably filtered out during replay and error messages were generated

delta_store_match([Bind1|T],Key,[Bind2|T2]) -->
    {is_bind(Bind1,ID,Val), is_bind(Bind2,ID,Val2)},
    !,
    ({check_value_equal(ID,Val,Val2)}
    -> []
    ; %translate_bvalue_with_limit(Val,100,V1), translate_bvalue_with_limit(Val2,100,V2),
    [ID] % TO DO: provided detailed explanation using values
    ),delta_store_match(T,Key,T2).

delta_store_match([_ID|T],Key,PartialStore) --> delta_store_match(T,Key,PartialStore).

enabled_kind('ENABLEDNESS',enabled).

enabled_kind('DISABLEDNESS',disabled).

equal_object_time_out(Val1,Val2,ID,TO) :-
    safe_time_out(equal_object(Val1,Val2,ID),TO,TimeOutRes),
    (TimeOutRes = time_out
    -> format_with_colour(user_output,[red],'==> Timeout when comparing values for ~w~n',[ID]),fail
    ; true).

error_occured_during_replay(MatchInfoList) :-
    member(replay_step(_,Errs),MatchInfoList), replay_error_occured(Errs),!.

exclude_and_collect_errors(_Pred,[],[]) --> [].

exclude_and_collect_errors(Pred,[H|T],Res) --> {call(Pred,H,Error)},!,
    [Error],
    exclude_and_collect_errors(Pred,T,Res).

exclude_and_collect_errors(Pred,[H|T],[H|Res]) --> % include item
    exclude_and_collect_errors(Pred,T,Res).

extract_json_model_name(json(ObjList),MachineName) :-
    get_json_key_object(metadata,ObjList,List),
    get_json_attribute(modelName,List,string(MC)),
    atom_codes(MachineName,MC).

flexible_perform_single_replay_step(FromID,TransID,DestID,[MatchSpec1|TMS],TransitionSpec,MName) :-
    skip_match_spec(FromID,TransitionSpec,MatchSpec1),!,
    debug_println(9,skipping_redundant_failing_check(MatchSpec1)),
    flexible_perform_single_replay_step(FromID,TransID,DestID,TMS,TransitionSpec,MName).

flexible_perform_single_replay_step(FromID,TransID,DestID,[MatchSpec1|TMS],TransitionSpec,MName) :-
    if(perform_single_replay_step(FromID,TransID,DestID,MatchSpec1,TransitionSpec),
    get_match_spec_txt(MatchSpec1,MName),
    flexible_perform_single_replay_step(FromID,TransID,DestID,TMS,TransitionSpec,MName)
).

gen_replay_error(Msg,Term,rerror(FullMSg)) :- ajoin([Msg,Term],FullMSg).

generate_predicate_from_bind(Kind,TypedIDs,json_bind(ID,Val,Type,Pos),b(Res,pred,[])) :-
    (member(b(identifier(ID),ExpectedType,_),TypedIDs) ->
    (unify_types_strict(ExpectedType,Type)
    -> TID = b(identifier(ID),ExpectedType,[]), TVal = b(value(Val),ExpectedType,[]),
    Res = equal(TID,TVal)
    ; pretty_type(ExpectedType,ETS), pretty_type(Type,TS), write(clash(Kind,ID,ETS,TS)),nl,
    % error should probably be caught earlier:
    add_warning(b_intelligent_trace_replay,'Ignoring value for stored identifier due to type clash: ',ID,Pos),
    Res = truth
    )
    ; % the identifier is not in the list and should be ignored here; sanity checks are made somewhere else
    Res = truth
).

generate_predicate_from_bind(Kind,TypedIDs,bind(ID,Val),R) :- % bind without type infos, e.g., from unchanged store
    generate_predicate_from_bind(Kind,TypedIDs,json_bind(ID,Val,any,unkown),R).

generate_predicates_from_store(Kind,TVars,DestStore,DestPreds) :-
    maplist(b_intelligent_trace_replay:generate_predicate_from_bind(Kind,TVars),DestStore,DestPreds).

get_bind_txt(Bind,Txt) :- is_bind(Bind,Id,Val),
    simple_val(Val), !, % TODO: add parameter for short/long text
    translate_bvalue_with_limit(Val,100,V1),
    ajoin([Id,'=',V1],Txt).

get_bind_txt(Bind,Id) :- is_bind(Bind,Id,_).

get_dest_store(concrete_constants(C),SC) :- !, sort(C,SC).

get_dest_store(Store,Vars) :- b_or_z_mode,!, extract_variables_from_state(Store,Vars).

get_dest_store(_,[]). % CSP,... has no concept of variables

get_expected_type(ID,variable,ExpectedType) :- bmachine_is_precompiled, b_is_variable(ID,ExpectedType).

get_expected_type(ID,constant,ExpectedType) :- bmachine_is_precompiled, b_is_constant(ID,ExpectedType).

get_from_match_list([replay_step(MI,Errors)|T],MatchInfo,TkErrors,T) :-
    maplist(get_replay_error,Errors,TkErrors),
    (MI=precise,TkErrors=[_|_] -> MatchInfo=precise_with_errs ; MatchInfo=MI).

get_from_match_list([],'-',['-'],[]).

get_ireplay_status(CurStepNr,Steps,Finished) :-
    loaded_json_trace_file(_,_,Steps),
    current_replay_step(CurStepNr),
    (CurStepNr =< Steps
    -> Finished=not_finished
    ; Finished=finished).

get_json_attribute(Attr,ObjList,Value) :- member(Equality,ObjList),
    is_json_equality_attr(Equality,Attr,Value).

get_json_attribute_with_pos(Attr,ObjList,File,Value,Pos) :-
    member(Equality,ObjList),
    is_json_equality_attr_with_pos(Equality,File,Attr,Value,Pos).

get_json_key_list(Key,JSON,List) :-
    get_json_attribute(Key,JSON,JList),
    JList \= @(null),
    (JList = array(List) -> true
    ; add_internal_error('Illegal JSON list for key:',Key:JList),
    fail
).

get_json_key_object(Key,JSON,Object) :-
    get_json_attribute(Key,JSON,JObject),
    JObject \= @(null),
    (JObject = json(Object) -> true
    ; add_internal_error('Illegal JSON object for key:',Key:JObject),
    fail
).

get_machine_identifiers(Op,TConsts) :- is_setup_constants_op(Op), !, b_get_machine_constants(TConsts).

get_machine_identifiers(_,TVars) :- b_get_machine_variables(TVars).

get_match_spec_txt(match_spec(_,Name,_),Name).

get_match_spec_val(Key,match_spec(_,_,List),Res) :- member(Key/Val,List),!,Res=Val.

get_opt_match_spec_val(Key,MS,Res) :- get_match_spec_val(Key,MS,Val),!, Res=Val.

get_opt_match_spec_val(_,_,optimize).

get_replay_error(rerror(Msg),Msg).

get_replay_info_text(replay(FromID,TransID,MatchInfo,Errors),TextAtoms) :-
    transition(FromID,OperationTerm,TransID,_ToID),
    translate_event_with_limit(OperationTerm,40,OpTxt),
    !,
    (Errors=[] -> TextAtoms = [' * REPLAYED (', MatchInfo,') : ',OpTxt]
    ; length(Errors,NrErrors),
    TextAtoms = [' * REPLAYED (', MatchInfo, ', errors: ',NrErrors,') : ', OpTxt]
).

get_replay_info_text(skipped,[' SKIPPED']) :- !.

get_replay_info_text(X,[X]).

get_rerror(Err,Msg) :- get_replay_error(Err,Msg),!.

get_rerror(Err,Msg) :- atom(Err),!,Msg=Err.

get_rerror(Err,F) :- functor(Err,F).

get_sorted_transition_details(FromID,TransID,DestID,TOpName,SortedPS,SortedRS) :-
    get_transition_details(FromID,TransID,DestID,TOpName,FullParaStore,FullResultStore),
    sort(FullParaStore,SortedPS),
    sort(FullResultStore,SortedRS).

get_trace_step_info(StepNr,StepDescr) :-
    json_trace_replay_step(StepNr,TransSpec,StaticErrors),
    get_transition_spec_txt(TransSpec,TTxt),
    (StaticErrors = [] -> StaticTT=[]
    ; length(StaticErrors,NrStaticErrors),
    StaticTT = [' (static errors: ',NrStaticErrors,')']
    ),
    (json_trace_replayed_info(StepNr,Info),
    get_replay_info_text(Info,TextAtoms)
    -> append(StaticTT,TextAtoms,TT),
    ajoin([StepNr,': ',TTxt | TT],StepDescr)
    ; ajoin([StepNr,': ',TTxt | StaticTT],StepDescr)
).

get_transition_details(FromID,TransID,DestID,OpName,ParaStore,ResultStore) :-
    transition(FromID,OperationTerm,TransID,DestID),
    get_operation_internal_name(OperationTerm,OpName),
    get_transition_details_aux(OpName,OperationTerm,DestID,ParaStore,ResultStore).

get_transition_details_aux('$setup_constants',_,DestID,ParaStore,ResultStore) :- !,
    ResultStore=[],
    visited_expression(DestID,DestState),
    state_corresponds_to_set_up_constants_only(DestState,ParaStore).

get_transition_details_aux('$initialise_machine',_,DestID,ParaStore,ResultStore) :- !,
    ResultStore=[],
    visited_expression(DestID,DestState),
    extract_variables_from_state(DestState,ParaStore).

get_transition_details_aux(OpName,OperationTerm,_,ParaStore,ResultStore) :-
    get_local_states_for_operation_transition(OpName,OperationTerm,ParaStore,ResultStore).

get_transition_name(FromID,TransID,OpName) :-
    transition(FromID,OperationTerm,TransID,_),
    get_operation_name(OperationTerm,OpName).

get_transition_spec_meta(transition_spec(_, Meta, _, _, _, _, _, _),Meta).

get_transition_spec_op(transition_spec(OpName, _, _, _, _, _, _, _),OpName).

get_transition_spec_txt(transition_spec(OpName, Meta, ParaStore, ResultStore,
    _DestStore, _Unchanged, _Preds, _Postconditions),Txt) :-
    (member(description/Desc,Meta) -> ajoin([Desc,' :: '],DescTxt) ; DescTxt = ''),
    (nonvar(OpName) -> OpTxt=OpName
    ; member(unknown_operation/OldOpName,Meta) -> ajoin(['?[',OldOpName,']'],OpTxt)
    ; OpTxt='?'),
    (ParaStore = [] -> ParaText1='', ParaText2=''
    ; ParaText1=' paras: ',
    maplist(get_bind_txt,ParaStore,Paras),
    ajoin_with_sep(Paras,',',ParaText2)
    ),
    (ResultStore = [] -> ResultText1='', ResultText2=''
    ; ResultText1=' results: ',
    maplist(get_bind_txt,ResultStore,Results),
    ajoin_with_sep(Results,',',ResultText2)
    ),!,
    ajoin([DescTxt,OpTxt,ParaText1,ParaText2,ResultText1,ResultText2],Txt).

get_transition_spec_txt(TS,'???') :- add_internal_error('Unknown transition spec:',TS).

get_unchanged_store(_,[],UnchangedStore) :- !, UnchangedStore=[].

get_unchanged_store(FromID,UnchangedVars,UnchangedStore) :-
    % copy old values to UnchangedStore
    visited_expression(FromID,FromState),
    extract_variables_from_state(FromState,FullFromStore),
    sort(FullFromStore,SortedStore),
    % TODO: generate warning when unchanged variable does not exist?
    include(b_intelligent_trace_replay:bind_id_is_element_of(UnchangedVars),SortedStore,UnchangedStore).

id_is_element_of(Vars,TID) :- def_get_texpr_id(TID,ID), member(ID,Vars).

ignore_dest_match_spec(match_spec(_,params_and_results,KeyVals)) :-
    KeyVals = [opname/match,paras/match,preds/match,results/match,nondet_vars/match,dest/optimize,unchanged/optimize].

illegal_json_binding_type(destState,ID,Type,Pos) :- get_expected_type(ID,Kind,ExpectedType),!,
    \+ unify_types_strict(Type,ExpectedType), pretty_type(Type,TS), pretty_type(ExpectedType,ETS),
    ajoin(['Ignoring JSON destState value for ',Kind,' ',ID,' due to illegal type ',TS, ', expected:'], Msg),
    add_error(translate_json_para,Msg,ETS,Pos).

illegal_json_binding_type(destState,ID,_Type,Pos) :-
    add_error(translate_json_para,'Ignoring JSON destState value for unknown identifier:',ID,Pos).

illegal_json_binding_type(params(Op),ID,_Type,Pos) :-
    b_or_z_mode, % otherwise no types available
    \+ b_top_level_operation(Op), !,
    findall(KOpid,b_top_level_operation(KOpid),Ops),
    (get_possible_fuzzy_matches_and_completions_msg(Op,Ops,FMsg)
    -> ajoin(['Ignoring JSON value for parameter ',ID,' of unknown operation (did you mean ',FMsg,' ?) : '], Msg)
    ; ajoin(['Ignoring JSON value for parameter ',ID,' of unknown operation: '], Msg)),
    add_error(translate_json_para,Msg,Op,Pos).

illegal_json_binding_type(params(Op),ID,Type,Pos) :-
    b_or_z_mode, % otherwise no types available
    b_get_machine_operation_typed_parameters_for_animation(Op,Params),
    member(b(identifier(ID),ExpectedType,_),Params),!,
    \+ unify_types_strict(Type,ExpectedType), pretty_type(Type,TS), pretty_type(ExpectedType,ETS),
    ajoin(['Ignoring JSON value for parameter ',ID,' of operation ', Op, ' due to illegal type ',TS, ', expected:'], Msg),
    add_error(translate_json_para,Msg,ETS,Pos).

illegal_json_binding_type(params(Op),ID,_Type,Pos) :-
    b_or_z_mode, % otherwise show_eventb_any_arguments makes no sense
    (b_get_machine_operation_typed_parameters_for_animation(Op,[]),
    get_preference(show_eventb_any_arguments,false)
    % TODO: check if ID is a valid virtual parameter, or if trace file was generated with preference set to true
    -> ajoin(['Ignoring JSON value for parameter ',ID,', operation has no parameters (setting SHOW_EVENTB_ANY_VALUES to TRUE may help):'],Msg)
    ; ajoin(['Ignoring JSON value for unknown parameter ',ID,' for:'],Msg)
    ),
    add_error(translate_json_para,Msg,Op,Pos).

illegal_json_binding_type(results(Op),ID,Type,Pos) :-
    b_or_z_mode, % otherwise there are no typred results available
    b_get_machine_operation_typed_results(Op,Results), member(b(identifier(ID),ExpectedType,_),Results),!,
    \+ unify_types_strict(Type,ExpectedType), pretty_type(Type,TS), pretty_type(ExpectedType,ETS),
    ajoin(['Ignoring JSON value for result ',ID,' of operation ', Op, ' due to illegal type ',TS], Msg),
    add_error(translate_json_para,Msg,ETS,Pos).

illegal_json_binding_type(results(_Op),ID,_Type,Pos) :-
    add_error(translate_json_para,'Ignoring JSON value for unknown operation result:',ID,Pos).

illegal_type(Var,Type,_Value,ValType,_ValPos,Kind,Step,ErrorTerm) :-
    \+ unify_types_strict(Type,ValType),
    pretty_type(ValType,VTS), pretty_type(Type,TS),
    ajoin(['Ignoring ',Kind, ' at step ', Step,
    ' due to unexpected type of value (', VTS, ' instead of ',TS,') for: '],ErrMsg),
    gen_replay_error(ErrMsg,Var,ErrorTerm).

inc_mismatches(X,_,Res) :- number(Res),X>Res,!,fail. % we will never reach Res; could be 0 for perfect match

inc_mismatches(Acc,Acc1,_) :- Acc1 is Acc+1.