sap

add_events_aux(all) :- b_top_level_operation(Event), assert_cb_uncovered_event(Event).

add_events_aux([H|T]) :- member(Event,[H|T]),
    match_event(Event,MatchedEvent),
    assert_cb_uncovered_event(MatchedEvent).

add_events_aux(final(List)) :- member(Event,List),
    match_event(Event,MatchedEvent),
    assert_cb_uncovered_event(MatchedEvent), assertz(cb_final_event(MatchedEvent)).

add_sep([],[]).

add_sep([A],R) :- !, R=[A].

add_sep([A|T],[A,' '|AT]) :- add_sep(T,AT).

add_target_events(Desc) :- add_events_aux(Desc),fail.

add_target_events(_).

all_uncovered_events_are_final :- cb_uncovered_event(Ev), \+ cb_final_event(Ev),!,fail.

all_uncovered_events_are_final.

analyse_transitions([],[]).

analyse_transitions([op(_Id,Operation,Succ)|Orest],[Succ|Srest]) :-
    % the arguments of the event are not interesting to us
    specfile:get_operation_name(Operation,Event), %functor(Operation,Event,_),
    % if Event is one of the events we monitor, we mark
    % the destination node as a node from where we look for
    % a path to a target node.
    (wanted_event(Event) -> assert_event_dest(Succ,Event) ; true),
    analyse_transitions(Orest,Srest).

assert_abstract_events(Event,Refines) :-
    member(Abstract,Refines), assertz( is_global_event(Event,Abstract) ),
    % (fail-loop)
    fail.

assert_abstract_events(_,_).

assert_bfs_nodes([],_,[],[]).

assert_bfs_nodes([Node|Rest],Depth,NewNodes,OldNodes) :-
    ( node_covered(Node,_NodeDepth) -> % we already encountered Node, ignore
    NewNodes = NewRest,
    OldNodes = [Node|OldRest]
    ; % this is a new node
    NewNodes = [Node|NewRest],
    OldNodes = OldRest,
    assertz( node_covered(Node,Depth) ), % mark as covered
    assertz( bfs_node(Node,Depth) )), % put it into the FIFO queue for the breadth-first search
    assert_bfs_nodes(Rest,Depth,NewRest,OldRest).

assert_cb_uncovered_event(E) :- \+ b_top_level_operation(E),!,
    add_error(cbc_cover,'Unknown event: ',E).

assert_cb_uncovered_event(E) :- assertz(cb_uncovered_event(E)), assertz(cb_target_event(E)).

assert_covered(E) :- retractall(wanted_event_to_cover(E)).

assert_event_dest(Node,Event) :-
    ( event_dest(Node,Event) -> true % information was already present, ignore
    ;
    assertz( event_dest(Node,Event) ),
    % if a target node can be reached from Node, we have a path in the explored
    % state-space that includes the Event and ends in a target node.
    ( target_reachable(Node,_) ->
    ( retract( target_needed(Event) ) -> true; true)
    ; true)).

assert_local_events([]).

assert_local_events([Event|Erest]) :-
    get_operation_info(Event,Info),
    ( member(refines(Ref),Info) ->
    assert_abstract_events(Event,Ref)
    ; assertz(is_local_event(Event))),
    assert_local_events(Erest).

assert_predecessors([],_).

assert_predecessors([Node|Rest],Pre) :-
    ( predecessor(Node,Pre) -> true % information already there, ignore
    ; assertz(predecessor(Node,Pre))),
    assert_predecessors(Rest,Pre).

assert_target_reachable(Node,DistToTarget) :-
    ( target_reachable(Node,OldDistToTarget) ->
    ( OldDistToTarget =< DistToTarget ->
    true % information already there, ignore
    ;
    retract( target_reachable(Node,_) ),
    assert_target_reachable2(Node,DistToTarget)
    )
    ;
    assert_target_reachable2(Node,DistToTarget)
).

assert_target_reachable2(Node,DistToTarget) :-
    assertz( target_reachable(Node,DistToTarget) ), fail.

assert_target_reachable2(Node,_DistToTarget) :-
    % the node can be reached by Event, so we know
    % that we have a path in the explored state-space that contains
    % Event a ends in a target node.
    event_dest(Node,Event),
    retract( target_needed(Event) ),
    % (this is a fail-loop)
    fail.

assert_target_reachable2(Node,DistToTarget) :-
    % propagate the information to the predecessors
    % (if we can reach a target node from this node, we also can
    % reach the target node from each predecessor node.)
    predecessor(Node,Pre),
    update_minimal_path_for_events(Pre,Node,DistToTarget),
    NewDistToTarget is DistToTarget + 1,
    assert_target_reachable(Pre,NewDistToTarget),
    % (this is a fail-loop)
    fail.

assert_target_reachable2(_,_).

b_ordered_get_operation(Event,CoveredStatus) :-
    findall(Event,get_feasible_event_name(Event),AllEvents),
    include(cb_uncovered_event,AllEvents,Uncovered),
    exclude(cb_uncovered_event,AllEvents,Covered),
    % Note: we do a findall and exclude/include first to avoid side-effects from modifying cb_uncovered_event
    % and possibly forgetting an event
    %print(uncovered(Uncovered)),nl,
    ( CoveredStatus=uncovered,
    member(Event,Uncovered)
    ;
    CoveredStatus=covered,
    member(Event,Covered),
    \+ bmachine:b_operation_cannot_modify_state(Event),
    \+ cb_final_event(Event) % it is already covered; no need to cover it again
). % no use in using a query/skip operation at the end

cb_catch_finalize(TargetPredicate,FinalState,Trace,Event,WF,Result,Timeout,TO_Success) :-
    catch_clpfd_overflow_call3(
    cb_finalize_path_aux(TargetPredicate,FinalState,Trace,Event,WF,Result,Timeout,TO_Success),
    warning,
    (printsilent('@OVERFLOW@'), Result=path, TO_Success = time_out)).

cb_covered_event(Event) :- % TO DO: this may give false positives; if an event was not marked to be covered initially and has not yet occured
    b_top_level_operation(Event), \+ cb_uncovered_event(Event).

cb_feasible_uncovered_event(E) :- cb_uncovered_event(E), \+ infeasible_operation_cache(E).

cb_finalize_path_aux(TargetPredicate,_FinalState,Trace,Event,WF,Result,Timeout,TO_Success) :-
    % if the target predicate is just true, we can store every found path
    % directly as a possible test trace, too.
    is_truth(TargetPredicate),!, % avoid ground_wait_flags twice if path infeasible
    % now check if the path makes sense as either testcase or path; if not: no use in enumerating
    (is_potential_new_test_case(Trace) -> Result = testcase % replace by is_potential_test_case if you want more tests in the test xml files
    ; is_potential_path_to_be_stored(Trace,Event) -> Result = path), % paths are not written to xml file
    ground_wait_flags_with_timeout(WF,Timeout,TO_Success),
    !.

cb_finalize_path_aux(TargetPredicate,FinalState,Trace,Event,WF,RESULT,Timeout,TO_Success) :-
    is_potential_new_test_case(Trace),
    % Note: if the target predicate is fulfilled in the last state, we
    % can store the solution as a test trace.
    (bounded_model_checking_invariant,
    b_specialized_invariant_for_op(Event,SpecINV) % only computed if get_preference(use_po,true)
    -> bsyntaxtree:create_negation(SpecINV,NegSpecINV),
    eval_predicate(NegSpecINV,FinalState,WF),
    (debug_mode(on) -> print('Specialized Invariant Target: '),translate:print_bexpr(SpecINV),nl ; true)
    ; eval_predicate(TargetPredicate,FinalState,WF),
    (debug_mode(on) -> print('Target: '),translate:print_bexpr(TargetPredicate),nl ; true)
    ),
    % print(grounding_with_predicate(Event,Trace)),nl,
    ground_wait_flags_with_timeout(WF,Timeout,TO_Success),
    (RESULT == testcase -> true % we are only looking for testcases not paths where we do not reach the target predicate
    ; TO_Success = time_out -> printsilent('@Timeout@'), %nl,print(Trace),nl,
    fail % try and find a solution without target predicate below
    ; true),
    !,
    RESULT=testcase.

cb_finalize_path_aux(_TargetPredicate,_FinalState,Trace,Event,WF,path,Timeout,TO_Success) :-
    % if the path is not feasible with the target predicate applied to the
    % last state, it still might be feasible as a starting point for other traces.
    is_potential_path_to_be_stored(Trace,Event),
    % print(grounding_without_predicate(_Trace)),nl,
    ground_wait_flags_with_timeout(WF,Timeout,TO_Success),!.

cb_finalize_path_with_timeout(TargetPredicate,FinalState,Trace,Event,WF,Result,Timeout,TO_Success) :-
    call_residue(
    cb_catch_finalize(TargetPredicate,FinalState,Trace,Event,WF,Result,Timeout,TO_Success2),Residue),
    (TO_Success2=time_out -> TO_Success=TO_Success2 % when time-out occurs there can be residues
    ; Residue = [] -> TO_Success=TO_Success2
    ; add_internal_error('Call had residue: ',trace_residue(Trace,Residue)/cb_finalize_path_with_timeout),
    %flush_output, print('GOAL:'),nl,tools_printing:print_goal(Residue),nl,
    TO_Success=time_out % as we have pending co-routines: assume time-out
).

cb_find_constants_state_in_statespace(ConstantsState,_ConstId) :-
    empty_state(ConstantsState),!,fail.

cb_find_constants_state_in_statespace(ConstantsState,ConstId) :-
    transition(root,_,ConstId),
    visited_expression(ConstId,concrete_constants(ConstantsState)),!.

cb_find_paths(Length,TargetPredicate,MaxLength,Timeout) :-
    (all_uncovered_events_are_final
    -> (CoveredStatus = uncovered ; CoveredStatus = covered), % force using uncovered operations first in b_ordered_get_operation
    % this only works if once an uncovered operation becomes covered it no longer needs to be enumerated; otherwise we will miss paths
    format_silent_msg('~nCBC test search: starting length ~w (~w events)~n',[Length,CoveredStatus])
    ; format_silent_msg('~nCBC test search: starting length ~w~n',[Length])),
    print_cb_uncovered_events,
    statistics(walltime,[StartWTime,_]),
    % set up template for Path = PrefixPath ^ [Event]
    cb_prefix_trace(Length,PreLength,PrefixPath,Event,Path),
    % choose any existing prefix of length PreLength for which a CBC solution was found:
    cb_path(PreLength,PrefixPath,LastStateId),
    % TO DO: maybe also try cb_timeout_path(PreLength,PrefixPath), LastStateId = no_state
    \+ useless_prefix(PrefixPath), % avoid using operations that do not change the state
    statistics(walltime,[WT,_]), Delta is WT-StartWTime,
    (Delta>1000 -> nls ; true), % too long lines on terminal slow things down
    (debug_mode(on) -> format_msg('~nTrying to extend path of length ~w: ~w~n',[Length,PrefixPath])
    ; printsilent('*'),printsilent(Length)),flush_output,
    % print(prefix(PrefixPath)),nl,
    % check if full coverage not yet achieved:
    \+ cb_test_case_algorithm_finished,
    % now choose any event; uncovered ones first:
    b_ordered_get_operation(Event,CoveredStatus),
    \+ bounded_model_checking_complete, % check again ; we may have found a solution with the previous event
    possible_trace(PrefixPath,Event,Length), % check if trace is in principle possible
    printsilent('.'),flush_output,
    % statistics information: store that we attempt another path of length Length:
    count_path(Length),
    (Length>=MaxLength -> Result=testcase, % no need to find partial solutions now
    cb_feasible_uncovered_event(Event) % only set up paths for feasible Events we want to cover
    ; true
    ),
    print_cb_stats(Length,StartWTime),
    % and try to set up that path PrefixPath ^ [Event]
    debug_println(9,setting_up_path(Path,Event)),
    cb_set_up_path(Path,Event,TargetPredicate,LastStateId,Timeout,Result),
    % now store info that we have found a solution for length Length with Result
    debug_println(19,found_solution(Length,Result,Path)),
    count_found(Length,Result),
    % fail-loop
    fail.

cb_find_paths(Length,_TargetPredicate,_MaxLengthOfTestCase,_Timeout) :-
    % success if a path or testcase of this length was generated, fail otherwise
    (cb_path(Length,_,_) -> true ; counter(testcase_count(Length),TC), TC>0).

cb_get_initialised_state([(_Id,_Op,Src,_Dst)|_],InitState) :-
    visited_expression(Src,Store),
    expand_const_and_vars_to_full_store(Store,InitState).

cb_has_uncovered_events :-
    cb_uncovered_event(_),!.

cb_has_uncovered_feasible_events :-
    cb_feasible_uncovered_event(_),!.

cb_mark_all_covered([],[]).

cb_mark_all_covered([Event|Rest],NewCover) :-
    ( retract(cb_uncovered_event(Event)) -> NewCover=[Event|RestCover],
    format_silent_ok('~nCBC test search: covered event ~w~n',[Event])
    ; NewCover=RestCover),
    cb_mark_all_covered(Rest,RestCover).

cb_prefix_trace(Length,PreLength,PrefixPath,Event,Path) :-
    PreLength is Length-1,
    length(PrefixPath,PreLength),append(PrefixPath,[Event],Path).

cb_save_found_test_case(Trace,Sequence) :- % print(found(Trace)),nl,
    % mark all events in Trace as covered
    cb_mark_all_covered(Trace,NewCover),
    (bounded_model_checking -> assertz(bounded_model_checking_complete) ; true),
    cb_get_initialised_state(Sequence,InitState),
    % Sequence is a list of (_Id,Op,Src,Dst)
    (NewCover=[] -> true
    ; store_test_case(NewCover,Sequence)
    ),
    cb_write_test_case(Sequence,InitState).

cb_save_new_step(Trace,Event,Result,LastStateId,Sequence) :-
    (retract(cb_uncovered_event_in_path(Event))
    -> (debug_mode(on) -> format_ok('Covered event ~w~n',[Event]) ; printsilent('#')) ; true),
    ( Result == testcase
    -> (cb_final_event(Event) -> cb_save_path_testcase_only(Trace,LastStateId) ; cb_save_path(Trace,LastStateId)),
    cb_save_found_test_case(Trace,Sequence)
    ; cb_save_path(Trace,LastStateId)).

cb_save_path(Trace,LastStateId) :-
    length(Trace,CurDepth),
    assertz(cb_path(CurDepth,Trace,LastStateId)).

cb_save_path_testcase_only(Trace,LastStateId) :- % save mainly for Tcl/Tk tree viewer
    length(Trace,CurDepth),
    assertz(cb_path_testcase_only(CurDepth,Trace,LastStateId)).

cb_set_up_events(Trace,InitialState,ConstantsState,FinalState,DetailedTrace,WF,WF2) :-
    DetailedTrace = dt1(States,Operations,OpTransInfos),
    testcase_set_up_events(Trace,InitialState,ConstantsState,Operations,States,FinalState,OpTransInfos,WF,WF2).

cb_set_up_path(Trace,Event,TargetPredicate,StateId,Timeout,Result) :-
    % StateID is the last state of the previously found path Trace (without Event)
    cb_try_state_caching, % if true: try to use model checking paths found; currently disabled
    StateId \== no_state,
    lookup_state(StateId,ConstantState,InState),
    init_wait_flags(WF,[cb_set_up_path]),
    set_up_transition(Event,Operation,ConstantState,InState,OutState,TransInfo,WF),
    cb_finalize_path_with_timeout(TargetPredicate,OutState,Trace,Event,WF,LResult,Timeout,TO_Success),
    ( TO_Success = time_out ->
    cb_write_timeout(Timeout,Trace),fail
    ;
    cb_store_single_step_in_statespace(ConstantState,OutState,StateId,Operation,TransInfo,LastStateId,Sequence),
    cb_save_new_step(Trace,Event,LResult,LastStateId,Sequence),
    % if we did not find a test case, just a normal step, we need to fall back
    % to constraint solving on the full path
    !,
    ( LResult==testcase -> Result=testcase
    ; cb_set_up_path(Trace,Event,TargetPredicate,no_state,Timeout,testcase) -> Result=testcase
    ; Result = path)).

cb_set_up_path(Trace,Event,TargetPredicate,_StateId,Timeout,Result) :-
    init_wait_flags(WF,[cb_set_up_path]),
    % set up constants and initialisation:
    testcase_initialise(ConstantsState,InitialState,Initialisation,TransInfo,WF),
    combine_detail_infos(ConstantsState,InitialState,Initialisation,TransInfo,DT1,DT),
    cb_set_up_events(Trace,InitialState,ConstantsState,FinalState,DT1,WF,WF2),
    % either find a real testcase where TargetPredicate holds at end
    % or find a path where TargetPredicate does not hold at end:
    cb_finalize_path_with_timeout(TargetPredicate,FinalState,Trace,Event,WF2,Result,Timeout,TO_Success),
    !,
    ( TO_Success = time_out ->
    cb_write_timeout(Timeout,Trace),
    fail
    ; (Result=testcase, bounded_model_checking -> format_err('Found BMC counter example (~w)~n',[Trace])
    ; debug_mode(on) -> format_ok('Found ~w path for ~w (~w)~n',[Result,Event,Trace])
    ; Result=testcase -> printsilent('!') %,print(Trace),nl
    ; printsilent('+')
    ),
    cb_store_path_in_statespace(DT,LastStateId,Sequence), % only do if path required or new testcase generated
    cb_save_new_step(Trace,Event,Result,LastStateId,Sequence)
).

cb_store_path_in_statespace(dt(ConstantsState1,States1,Operations,TransInfos),LastStateId,RealOperations) :-
    normalise_states([ConstantsState1|States1],[ConstantsState|States]),
    add_constants_to_state_space(ConstantsState,States,ConstStates,_SetupSequence,StartStateId),
    add_operations_to_state_space(Operations,StartStateId,ConstStates,TransInfos,OpSequence),
    OpSequence = [_InitOp|RealOperations],
    last(OpSequence,(_,_,_,LastStateId)).

cb_store_single_step_in_statespace(ConstantsState,State1,PrevStateId,Operation,TransInfo,NewStateId,[Tuple]) :-
    normalise_state(State1,State2),
    ( cb_find_constants_state_in_statespace(ConstantsState,ConstId) ->
    remove_constants_from_state([State2],ConstantsState,ConstId,[State])
    ;
    State = State2),
    add_operations_to_state_space([Operation],PrevStateId,[State],[TransInfo],[Tuple]),
    Tuple = (_,_,_,NewStateId).

cb_test_case_algorithm_finished :-
    (cb_has_uncovered_feasible_events -> bounded_model_checking_complete ; true).

cb_test_cases_init_search(Events) :-
    reset_counters,
    retractall(cb_path(_,_,_)), % retract all found paths
    retractall(cb_path_testcase_only(_,_,_)),
    retractall(cb_timeout_path(_,_)),
    assertz(cb_path(0,[],no_state)), % generate an intial path; Note: we assume the initialisation is feasible
    % set up all coverage targets:
    retractall(cb_uncovered_event(_)),
    retractall(cb_uncovered_event_in_path(_)),
    retractall(cb_target_event(_)),
    retractall(cb_final_event(_)),
    cb_test_cases_init_uncovered_in_path,
    add_target_events(Events).

cb_test_cases_init_uncovered_in_path :-
    b_top_level_operation(Event),
    assertz(cb_uncovered_event_in_path(Event)),
    count_total_events,
    fail.

cb_test_cases_init_uncovered_in_path.

cb_test_cases_loop(CurLength,TargetPred,MaxLengthOfTestCase,Timeout) :-
    cb_test_cases_step(CurLength,TargetPred,MaxLengthOfTestCase,Timeout,Result),
    (Result=paths_found
    -> L1 is CurLength+1,
    cb_test_cases_loop(L1,TargetPred,MaxLengthOfTestCase,Timeout)
    ; Result=limit_reached -> check_progress_possible
    ; Result=no_test_found -> check_progress_possible
    ; true
).

cb_test_cases_step(1,TargetPred,_MaxLengthOfTestCase,Timeout,Res) :- bounded_model_checking,
    % check if INITIALISATION can violate INVARIANT or Deadlock
    Events = [], Length=0,
    count_path(Length),
    call_with_smt_mode_enabled(create_testcase_path(init,Events,TargetPred,Timeout,PathResult)),
    debug_println(19,init_bmc_check(PathResult)),
    PathResult = [_|_], % Result contains e.g., (0,$initialise_machine(int(-1)),root,0) and possibly set_up_constants
    !,
    Res =paths_found,
    format_err('~nBMC counterexample found, Length=~w~n',[Length]),
    assertz(bounded_model_checking_complete), count_found(0,testcase),
    store_test_case(['$initialise_machine'],PathResult).

cb_test_cases_step(CurLengthOfTestCase,_TargetPred,_MaxLengthOfTestCase,_Timeout,success) :-
    cb_test_case_algorithm_finished,
    !,
    L1 is CurLengthOfTestCase-1,
    format_msg('~nCBC Algorithm finished (~w)~n',[L1]),
    (debug_mode(on), specfile:currently_opened_file(F) -> format_msg(' File: ~w~n',[F]) ; true).

cb_test_cases_step(CurLengthOfTestCase,_TargetPred,MaxLengthOfTestCase,_Timeout,limit_reached) :-
    CurLengthOfTestCase > MaxLengthOfTestCase,!,
    format_warn('~nLimit Reached: ~w~n',[MaxLengthOfTestCase]).

cb_test_cases_step(CurLengthOfTestCase,TargetPred,MaxLengthOfTestCase,Timeout,paths_found) :-
    % now try to find a path of length CurLengthOfTestCase
    call_with_smt_mode_enabled(cb_find_paths(CurLengthOfTestCase,TargetPred,MaxLengthOfTestCase,Timeout)),
    !,
    (bounded_model_checking_complete -> format_err('~nBMC counterexample found, Length=~w~n',[CurLengthOfTestCase])
    ; \+ cb_has_uncovered_events -> format_ok('~nEverything covered, Length=~w~n',[CurLengthOfTestCase])
    ; \+ cb_has_uncovered_feasible_events -> format_ok('~nEverything feasible covered, Length=~w~n',[CurLengthOfTestCase])
    ; true).

cb_test_cases_step(CurLengthOfTestCase,_TargetPred,MaxLengthOfTestCase,_Timeout,Res) :-
    % either everything covered or MaxLength reached or no way to extend current paths
    (CurLengthOfTestCase = MaxLengthOfTestCase
    -> format_warn('~nCould not generate a test case of length ~w~n',[CurLengthOfTestCase]),
    Res = no_test_found
    ; format_warn('~nCould not generate a path of length ~w~n',[CurLengthOfTestCase]),
    Res = no_path_found
).

cb_timed_testcases(TargetPred,MaxLengthOfTestCase,Timeout) :-
    statistics(walltime, [Start|_]),
    InitialLength = 1,
    cb_test_cases_loop(InitialLength,TargetPred,MaxLengthOfTestCase,Timeout),
    statistics(walltime, [End|_]),
    Runtime is End - Start,
    write_results(Runtime).

cb_var_is_modified(Name,NewValue,Src) :-
    memberchk(bind(Name,OldValue),Src),!,
    not_equal_object(OldValue,NewValue).

cb_var_is_modified(Name,_NewValue,Src) :-
    nonmember(bind(Name,_OldValue),Src).

cb_write_test_case(Sequence,InitState) :-
    xml_write(' <test_case>\n'),
    if(cb_xml_initialisation(InitState),true,add_internal_error('Call failed: ',cb_xml_initialisation(InitState))),
    if(cb_xml_sequence(Sequence),true,add_internal_error('Call failed: ',cb_xml_sequence(Sequence))),
    xml_write(' </test_case>\n'),
    flush_output_xml.

cb_write_timeout(Timeout,Events) :-
    length(Events,Length),
    count_timeout(Length),
    printsilent(timeout),flush_output,
    assertz(cb_timeout_path(Length,Events)),
    xml_write(' <!-- timeout ('),xml_write(Timeout),xml_write(') ms) for events '),
    cb_write_timeouts2(Events),
    xml_write(' --!>\n'),flush_output_xml.

cb_write_timeouts2([Event]) :-
    !,xml_write(Event).

cb_write_timeouts2([Event|Erest]) :-
    xml_write(Event),xml_write(','),cb_write_timeouts2(Erest).

cb_xml_init2(Store,Identifiers,Type) :-
    get_texpr_id(TId,Id),
    member(TId,Identifiers),
    lookup_value(Id,Store,BValue),
    cb_xml_value(Id,Type,BValue),
    fail.

cb_xml_init2(_Store,_Identifiers,_Type).

cb_xml_initialisation(InitState) :-
    xml_write(' <initialisation>\n'),
    b_get_machine_constants(Constants),cb_xml_init2(InitState,Constants,constant),
    b_get_machine_variables(Variables),cb_xml_init2(InitState,Variables,variable),
    xml_write(' </initialisation>\n').

cb_xml_modified(Src,bind(Name,NewValue)) :-
    cb_var_is_modified(Name,NewValue,Src),!,
    cb_xml_value_element(modified,Name,NewValue).

cb_xml_modified(_,_).

cb_xml_parameter(_Event,Prefix,Parameter,BValue) :-
    get_texpr_id(Parameter,Id),!,
    (is_internal_parameter(Prefix,Id) -> true % do not print it
    ; cb_xml_value_element(value,Id,BValue)).

cb_xml_parameter(Event,Prefix,Parameter,BValue) :-
    add_internal_error('Call failed: ',cb_xml_parameter(Event,Prefix,Parameter,BValue)).

cb_xml_sequence([]).

cb_xml_sequence([(_Id,Op,Src,Dst)|Rest]) :- !,
    specfile:get_operation_name(Op,Name),
    cb_xml_step(Name,Op,Src,Dst), % TO DO: also provide operation parameters
    cb_xml_sequence(Rest).

cb_xml_sequence([loop(_ID)]).

cb_xml_step(Event,Op,SrcId,DstId) :-
    b_get_machine_operation(Event,_,Parameters,_),
    Parameters = [_|_],!,
    xml_write(' <step name=\"'),xml_write(Event),xml_write('\">\n'),
    specfile:get_operation_arguments(Op,Args), % TO DO: maybe also write out return arguments ?!
    xml_write_parameters(Event,Parameters,Args),
    expand_state(SrcId,Src),
    expand_state(DstId,Dst),
    maplist(cb_xml_modified(Src),Dst),
    xml_write(' </step>\n').

cb_xml_step(Event,_,_Src,_Dst) :-
    xml_write(' <step name=\"'),xml_write(Event),xml_write('\" />\n').

cb_xml_value(Id,Type,BValue) :-
    translate_bvalue(BValue,SValue),
    xml_write(' <value type=\"'),"
    xml_write(Type),
    xml_write('\" name=\"'),xml_write(Id),xml_write('\">'),"
    xml_write(SValue),xml_write('</value>\n').

cb_xml_value_element(Element,Name,Value) :-
    xml_write(' <'),xml_write(Element),
    xml_write(' name=\"'),xml_write(Name),xml_write('\">'),
    xml_write_b_value(Value),
    !,
    xml_write('</'),xml_write(Element),xml_write('>\n').

cb_xml_value_element(Element,Name,Value) :-
    add_internal_error('Call failed: ',cb_xml_value_element(Element,Name,Value)).

cbc_gen_test_cases(EventsToCover,TargetPredicate,MaxLength,Filename,UncoveredEvents) :-
    cbc_reset_gen_test_cases(EventsToCover),
    open_xml_testcase(Filename),
    get_preference(time_out,Timeout),
    call_with_smt_mode_enabled(
    call_cleanup(cb_timed_testcases(TargetPredicate, MaxLength, Timeout),
    close_xml_testcase)),
    cbc_get_uncovered_events(UncoveredEvents).

cbc_gen_test_cases_finish_tasks :-
    close_xml_testcase.

cbc_gen_test_cases_from_string(Events,TargetString,MaxDepth,Filename,Uncovered) :-
    % parse target predicate for test-case sequences
    parse_cbc_target_predicate(TargetString,Target),
    cbc_gen_test_cases(Events,Target,MaxDepth,Filename,Uncovered).

cbc_gen_test_cases_task_step(EventSelection,TargetString,MaxLength,Filename, Final, Len, Task) :-
    % first translate Tk EventSelection Number list into Events
    get_selected_events(EventSelection,_AllEvents,EventsToCover),
    % parse target predicate for test-case sequences
    parse_cbc_target_predicate(TargetString,TargetPredicate),
   
    (Final=1 -> cbc_reset_gen_test_cases(final(EventsToCover))
    ; cbc_reset_gen_test_cases(EventsToCover)),
    get_preference(time_out,Timeout),
   
    open_xml_testcase(Filename),
    Task = sap: cb_test_cases_step(Len,TargetPredicate,MaxLength,Timeout,_),
    between(1,MaxLength,Len).

cbc_get_nr_uncovered_events(Len) :-
    cbc_get_uncovered_events(UncoveredEvents),
    length(UncoveredEvents,Len).

cbc_get_uncovered_events(UncoveredEvents) :-
    findall(E,cb_uncovered_event(E),UncoveredEvents).

cbc_reset_gen_test_cases(EventsToCover) :-
    reset_test_cases,
    cb_test_cases_init_search(EventsToCover).

check_operation_can_be_enabled_by(PreviousEvent,Event) :-
    TIMEOUT = 500, % TO DO : pass timeout from cb_find_paths and divide by 5? (default in cb_find_paths is 2500)
    (operation_can_be_enabled_by_cache(PreviousEvent,Event,R) -> R \= failure
    ; operation_can_be_enabled_by(PreviousEvent,Event,TIMEOUT,R) ->
    assertz(operation_can_be_enabled_by_cache(PreviousEvent,Event,R)),
    R \= failure
    ; assertz(operation_can_be_enabled_by_cache(PreviousEvent,Event,failure)),
    fail
).