b_intelligent_trace_replay

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_get_machine_operation_typed_parameters(OpName,Paras).

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_get_machine_operation_typed_results(OpName,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, 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_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(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(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),!.

evaluate_codes_value(ExpressionCodes,Type,Value) :-
    eval_strings:repl_parse_expression(ExpressionCodes,Typed,Type,Error), Error=none,
    eval_strings:eval_expression_direct(Typed,Value).

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_attribute(metadata,ObjList,json(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) :- extract_variables_from_state(Store,Vars).

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 \= [],
    (JList = [_|_] -> List=JList
    ; add_internal_error('Illegal JSON list for key:',Key:JList),
    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].

ignore_return_match_spec(match_spec(_,parameters_only,KeyVals)) :-
    KeyVals = [opname/match,paras/match,results/optimize,nondet_vars/optimize].

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

illegal_json_binding_type(destState,ID,Type,Pos) :- b_is_constant(ID,ExpectedType),!,
    \+ unify_types_strict(Type,ExpectedType), pretty_type(Type,TS),
    ajoin(['Ignoring JSON value for constant ',ID,' due to illegal type:'], Msg),
    add_error(translate_json_para,Msg,TS,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_get_machine_operation_typed_parameters(Op,Params), member(b(identifier(ID),ExpectedType,_),Params),!,
    \+ unify_types_strict(Type,ExpectedType), pretty_type(Type,TS),
    ajoin(['Ignoring JSON value for parameter ',ID,' of operation ', Op, ' due to illegal type:'], Msg),
    add_error(translate_json_para,Msg,TS,Pos).

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

illegal_json_binding_type(results(Op),ID,Type,Pos) :-
    b_get_machine_operation_typed_results(Op,Results), member(b(identifier(ID),ExpectedType,_),Results),!,
    \+ unify_types_strict(Type,ExpectedType), pretty_type(Type,TS),
    ajoin(['Ignoring JSON value for result ',ID,' of operation ', Op, ' due to illegal type:'], Msg),
    add_error(translate_json_para,Msg,TS,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) ; 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_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_trace_file_body(Stream,1,T)
).

parse_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_trace_file_body(Stream,Step,Trace)
    ; Trace = [TransSpec|T],
    convert_prolog_trace_step(Term,TransSpec),
    S1 is Step + 1,
    parse_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).

perform_single_replay_step_by_pred(FromID,TransID,DestID,
    MatchSpec,
    transition_spec(OpName, _, ParaStore, ResultStore, DestStore, UnchangedVars, Preds,
    _Postconditions)) :-
    nonvar(OpName), % we currently cannot execute by predicate without knowing OpName
    (node_not_fully_explored(FromID,OpName) -> true
    ; debug_format(19,'Node ~w fully explored for ~w; no use in attempting execute by predicate~n',[FromID,OpName]),
    fail
    ),
    mark_match_spec_as_used(MatchSpec),
    !,
    (ParaStore \= [], % check parameters of operation
    get_match_spec_val(paras,MatchSpec,match)
    -> b_get_operation_typed_paras(OpName,Parameters),
    generate_predicates_from_store(operation_parameters,Parameters,ParaStore,ParaPreds)
    ; ParaPreds = []),
    (ResultStore \= [], % check return values of operation
    get_match_spec_val(results,MatchSpec,match)
    -> b_get_operation_typed_results(OpName,Results),
    generate_predicates_from_store(operation_results,Results,ResultStore,ResultPreds)
    ; ResultPreds = []),
    get_machine_identifiers(OpName,TVars),
    (DestStore = [] -> DestPreds=[]
    ; get_match_spec_val(dest,MatchSpec,match)
    -> generate_predicates_from_store(dest_variables,TVars,DestStore,DestPreds)
    ; get_match_spec_val(nondet_vars,MatchSpec,match)
    -> b_get_op_non_det_modifies(OpName,NonDetModifies),
    include(b_intelligent_trace_replay:id_is_element_of(NonDetModifies),TVars,NDVars),
    generate_predicates_from_store(non_det_vars,NDVars,DestStore,DestPreds)
    ; DestPreds=[]
    ),
    get_unchanged_store(FromID,UnchangedVars,UnchangedStore),
    (UnchangedStore = [] -> UnchangedPreds=[]
    ; get_match_spec_val(unchanged,MatchSpec,match) ->
    generate_predicates_from_store(unchanged_vars,TVars,UnchangedStore,UnchangedPreds)
    ; get_match_spec_val(nondet_vars,MatchSpec,match) ->
    include(b_intelligent_trace_replay:id_is_element_of(NonDetModifies),TVars,NDVars),
    generate_predicates_from_store(non_det_vars,NDVars,UnchangedStore,UnchangedPreds)
    ; UnchangedPreds=[]
    ),
    (get_match_spec_val(preds,MatchSpec,match) -> AddPreds=Preds ; AddPreds=[]),
    append([ParaPreds,ResultPreds,DestPreds,UnchangedPreds,AddPreds],AllPreds),
    conjunct_predicates(AllPreds,Pred),
    format('Trying to execute ~w in state ~w by predicate: ',[OpName,FromID]), translate:print_bexpr(Pred),nl,
    tcltk_interface:tcltk_add_user_executed_operation_typed(OpName,FromID,_,Pred,TransID,DestID).

perform_single_replay_step_statespace(FromID,TransID,DestID,
    MatchSpec,
    transition_spec(OpName, _, ParaStore, ResultStore, DestStore, UnchangedVars, Preds, _Postconditions),
    Mismatches) :-
    mark_match_spec_as_used(MatchSpec),
    get_opt_match_spec_val(opname,MatchSpec,OpMatch),
    compute_all_transitions_if_necessary(FromID,false), % could be made optional
    (OpMatch==match -> TOpName=OpName ; true),
    get_sorted_transition_details(FromID,TransID,DestID,TOpName,FullParaStore,FullResultStore),
    (TOpName=OpName -> MM0 = 0 ; MM0=1, assert_mismatch(OpMatch)),
    count_store_mismatches(FullParaStore,ParaStore,paras,MatchSpec,MM0,MM1), % check if parameters match
    count_store_mismatches(FullResultStore,ResultStore,results,MatchSpec,MM1,MM2), % check if operation return values match
    get_unchanged_store(FromID,UnchangedVars,UnchangedStore),
    (DestStore=[], UnchangedStore=[]
    -> MM6=MM2
    ; % check if variables in destination state match
    visited_expression(DestID,DestState),
    get_dest_store(DestState,FullDestStore),
    count_store_mismatches(FullDestStore,DestStore,dest,MatchSpec,MM2,MM3),
    count_store_mismatches(FullDestStore,UnchangedStore,unchanged,MatchSpec,MM3,MM4),
    (get_match_spec_val(nondet_vars,MatchSpec,_)
    -> b_get_op_non_det_modifies(OpName,NonDetModifies),
    include(b_intelligent_trace_replay:bind_id_is_element_of(NonDetModifies),DestStore,D1),
    count_store_mismatches(FullDestStore,D1,nondet_vars,MatchSpec,MM4,MM5),
    include(b_intelligent_trace_replay:bind_id_is_element_of(NonDetModifies),UnchangedStore,D2),
    count_store_mismatches(FullDestStore,D2,nondet_vars,MatchSpec,MM5,MM6)
    ; MM6=MM4
    )
    ),
    Mismatches = MM6,
    (Preds=[] -> true
    ; get_match_spec_val(preds,MatchSpec,match)
    -> bsyntaxtree:conjunct_predicates(Preds,Pred),
    format('Testing preds in destination state ~w after ~w: ',[FromID,DestID]),translate:print_bexpr(Pred),nl,
    % TODO: insert_before_substitution_variables for $0 vars; check that it is consistent with Tcl/Tk and ProB2-UI
    % maybe use annotate_becomes_such_vars or find_used_primed_ids
    append(FullResultStore,FullParaStore,LocalStore),
    b_test_boolean_expression_for_ground_state(Pred,LocalStore,FullDestStore,'trace replay', OpName)
    ; true
).