b_intelligent_trace_replay

add_parameter_error(Error,Name,ExpressionCodes,Pos) :-
    ajoin(['Ignoring JSON value for parameter ',Name,' 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),DestStore,DestStore2),
    exclude_and_collect_errors(unknown_variable(Step),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),DestStore,DestStore2),
    exclude_and_collect_errors(unknown_variable(Step),UnchangedVars,UnchangedVars2)
).

check_and_adapt_trace_step(transition_spec(OpName, Meta,_, _, DestStore, UnchangedVars,Preds, Postconditions), Step,
    transition_spec(_, Meta, [], [], DestStore2, UnchangedVars2,Preds, Postconditions)) -->
    add_replay_error('Unknown operation: ',OpName),
    exclude_and_collect_errors(unknown_variable_binding(Step),DestStore,DestStore2),
    exclude_and_collect_errors(unknown_variable(Step),UnchangedVars,UnchangedVars2).

check_model_name(ModelName) :-
    b_machine_name(CurModelName),
    (CurModelName=ModelName -> true
    ; dummy_machine_name(ModelName,CurModelName) % CurModelName = MAIN_MACHINE_FOR_...
    ; (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_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)
).

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_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_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_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_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 = ''),
    (var(OpName) -> OpTxt='?' ; OpTxt=OpName),
    (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 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 value for unknown identifier:',ID,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.

is_bind(bind(ID,Val),ID,Val).

is_bind(json_bind(ID,Val,_,_),ID,Val).

is_json_equality_attr('='(Attr,Val),Attr,Val).

is_json_equality_attr('='(Attr,Val,_Pos),Attr,Val). % we have position infos

is_json_equality_attr_with_pos('='(Attr,Val),_File,Attr,Val,unknown).

is_json_equality_attr_with_pos('='(Attr,Val,JPos),File,Attr,Val,ProBPos) :- create_position(JPos,File,ProBPos).

is_setup_constants_op('$setup_constants').

is_setup_constants_op('$partial_setup_constants').

is_setup_or_init('$initialise_machine','$initialise_machine').

is_setup_or_init(initialise_machine,'$initialise_machine'). % old style

is_setup_or_init(setup_constants,'$setup_constants'). % old style

is_setup_or_init(Op,Op) :- is_setup_constants_op(Op).

mark_match_spec_as_used(match_spec(used,_,_)).

match_spec_has_optimize_field(match_spec(_,_,KeyVals)) :- member(_/optimize,KeyVals).

match_spec_was_used(match_spec(UsedFlag,_,_)) :- UsedFlag==used.

node_not_fully_explored(FromID,OpName) :-
    (max_reached_for_node(FromID)
    ; not_all_transitions_added(FromID)
    ; not_interesting(FromID)
    ; time_out_for_node(FromID,OpName,_)).

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

parse_prolog_trace_file(File,Stream,ModelName,Trace) :-
    safe_read_stream(Stream,0,Term),!,
    (Term = end_of_file
    -> Trace = [], ModelName = 'dummy(uses)',
    add_warning(read_prolog_trace_file,'Empty trace file: ',File)
    ; (Term = machine(ModelName)
    -> Trace = T
    ; Trace = [Term|T],
    add_warning(read_prolog_trace_file,'File does not start with a machine/1 fact: ',Term)
    ),
    parse_prolog_trace_file_body(Stream,1,T)
).

parse_prolog_trace_file_body(Stream,Step,Trace) :-
    safe_read_stream(Stream,Step,Term),!,
    (Term = end_of_file
    -> Trace = []
    ; skip_prolog_term(Term)
    -> add_message(read_prolog_trace_file,'Skipping: ',Term),
    parse_prolog_trace_file_body(Stream,Step,Trace)
    ; Trace = [TransSpec|T],
    convert_prolog_trace_step(Term,TransSpec),
    S1 is Step + 1,
    parse_prolog_trace_file_body(Stream,S1,T)
).

perform_single_replay_step(FromID,TransID,DestID,MatchSpec,TransSpec) :-
    %format('* FROM: ~w ',[FromID]),portray_match_spec(MatchSpec),nl,
    (match_spec_has_optimize_field(MatchSpec)
    -> findall(sol(MM,TID,DID),
    perform_single_replay_step_statespace(FromID,TID,DID,MatchSpec,TransSpec,MM),
    Sols),
    mark_match_spec_as_used(MatchSpec),
    length(Sols,NrSols),
    min_member(sol(Mismatches,TransID,DestID),Sols),
    format('Min. nr of mismatches found ~w among ~w candidate steps (starting from state ~w). ~n',[Mismatches,NrSols,FromID])
    ; % just find first solution:
    perform_single_replay_step_statespace(FromID,TransID,DestID,MatchSpec,TransSpec,_)
).

perform_single_replay_step(FromID,TransID,DestID,MatchSpec,TransSpec) :-
    perform_single_replay_step_by_pred(FromID,TransID,DestID,MatchSpec,TransSpec).