runtime_profiler

constant_instantiates(NodeID,Label,SuccID,Color,Style) :-
    Color=red4, Style=solid, Label = 'inst',
    Category = constant_computation(Phase,Infos), Phase = propagate_value,
    total_runtime(NodeID,Category,_RT,_WT,_Calls,_MaxWT,_MaxWitnessID,_Min),
    member(instantiates(List),Infos),
    member(SuccID,List), SuccID \= NodeID.

constant_profile_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color) :- SubGraph=none,
    Category = constant_computation(Phase,_Infos),
    total_runtime(NodeID,Category,_RT,WT,_Calls,_MaxWT,_MaxWitnessID,_Min),
    (abstract_constant(NodeID,_) -> Kind=abstract ; Kind=concrete),
    Phase \= propagate_value,
    Shape = box,
    (total_runtime(NodeID,constant_computation(propagate_value,_),_,WT2,_,_,_,_)
    -> ajoin([NodeID,'\\n ',Kind,'\\n ',Phase,'\\n',WT, ' ms','\\n + ',WT2, ' ms'],NodeDesc)
    ; ajoin([NodeID,'\\n ',Kind,'\\n ',Phase,'\\n',WT, ' ms'],NodeDesc)
    ),
    Style='rounded', Color=gray90.

constants_profiling_on :- preference(performance_monitoring_on,true). % TODO: maybe use other preference later

dec_recur(X) :- retract(recursion_level(X1)), X is X1-1,
    assertz(recursion_level(X)).

get_category_call_name(top_level,N) :- !,
    get_specification_description(operation,N). % also shows invariants though

get_category_call_name(external_functions,N) :- !, N='Function'.

get_category_call_name(cache_hashing_input_values,N) :- !, N='Hash_Input'.

get_category_call_name(cache_load_constants,N) :- !, N='Load_Constants'.

get_category_call_name(cache_load_constants_failed,N) :- !, N='Load_Constants_KO'.

get_category_call_name(cache_load_operations_index,N) :- !, N='Load_Operations_Index'.

get_category_call_name(cache_load_operations_index_failed,N) :- !, N='Load_Operations_Index_KO'.

get_category_call_name(cache_load_transitions,N) :- !, N='Load_Transition'.

get_category_call_name(cache_store_transitions,N) :- !, N='Store'.

get_category_call_name(_,N) :- !, N='Call'.

get_cprofile_list(cprofile(RT,WT,PropWT,Calls,PP,Kind,Ann,Phase,IDInfo0,InstItself,DetVal,IList),
    list([PP,Kind,Ann,RT,WT,PropWT,Calls,IDInfo,InstItself,DetVal,IList])) :-
    (Phase = phase0 -> IDInfo = IDInfo0 ; IDInfo = [Phase|IDInfo0]).

get_profile_list(profile(RT,WT,Calls,MaxWT,AN,Cat,MaxID,Min),list([PPS,RT,WT,Calls,MaxWT,MaxID,Min])) :-
    translate_pp(AN,Cat,PPS).

get_value_info(Var,ValKind) :- var(Var),!, ValKind=variable.

get_value_info(closure(_,_,_),ValKind) :- !, ValKind=symbolic.

get_value_info(avl_set(_),ValKind) :- !, ValKind=avl_set.

get_value_info(rec(_),ValKind) :- !, ValKind=record.

get_value_info(int(_),ValKind) :- !, ValKind=integer.

get_value_info(string(_),ValKind) :- !, ValKind=string.

get_value_info(fd(_,GS),ValKind) :- !, ValKind=GS.

get_value_info(freeval(_ID,_,_),ValKind) :- !, ValKind=freeval.

get_value_info(pred_false,ValKind) :- !, ValKind=boolean.

get_value_info(pred_true,ValKind) :- !, ValKind=boolean.

get_value_info([],ValKind) :- !, ValKind=empty_set.

get_value_info(O,other) :- functor(O,F,N), write(other(F,N)),nl,fail.

inc_recur(X) :- retract(recursion_level(X)), X1 is X+1,
    assertz(recursion_level(X1)).

indent(0) :- !.

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

irrelevant_profile_entry(ID,constant_computation(Phase,IDInfo),0) :-
    Phase = propagate_value, % only show propagations if relevant runtime or instantiates something other than itself
    (member(instantiates(List),IDInfo) -> List = [ID] ; true).

is_value_info(avl_set).

is_value_info(boolean).

is_value_info(empty_set).

is_value_info(freeval).

is_value_info(integer).

is_value_info(record).

is_value_info(symbolic).

is_value_info(string).

observe_runtime_wf(Timer,Msg,Span,WF) :-
    preference(performance_monitoring_on,true),
    Timer = [Start,WStart],
    !,
    get_preference(performance_monitoring_expansion_limit,Limit),
    statistics(runtime,[End,_]), TotRuntime is End-Start,
    statistics(walltime,[WEnd,_]), TotWalltime is WEnd-WStart,
    (TotWalltime>=Limit
    -> ajoin([TotWalltime,' ms'],Time),
    add_message_wf(delay,Msg,Time,Span,WF),
    ( get_call_stack(WF,Stack),
    member(id_equality_evaluation(ID,constant,_Pos),Stack),
    get_waitflags_phase(WF,Phase),
    Cat = constant_computation(Phase,[long_closure_expansion]),
    register_profiler_runtime(ID,Cat,unknown,TotRuntime,TotWalltime),
    fail
    ; true)
    ; true).

observe_runtime_wf(_StartMs,_Msg,_,_).

opt_category(ast_cleanup,cleanup).

opt_category(cache_load_constants,cache).

opt_category(cache_load_constants_failed,cache).

opt_category(cache_load_operations_index,cache).

opt_category(cache_load_operations_index_failed,cache).

opt_category(cache_hashing_input_values,cache).

opt_category(cache_load_transitions,cache).

opt_category(cache_store_transitions,cache).

opt_category(external_functions,external).

opt_category(well_def_analyser,wd).

opt_stop_profile(_,_,_,_,_) :- preference(prob_profiling_on,false), !.

opt_stop_profile(Category,Label,StateID,[RT1,WT1],Threshold) :-
    statistics(walltime,[WT2,_]), DWT is WT2-WT1, DWT>=Threshold,
    !,
    statistics(runtime,[RT2,_]),
    DRT is RT2-RT1,
    register_profiler_runtime(Label,Category,StateID,DRT,DWT).

opt_stop_profile(_,_,_,_,_).

print_runtime_profile :-
    format('---- ProB Runtime Profiler ----~n',[]),
    format('---- Time spent in B operations and invariant evaluation~n',[]),
    (get_preference(prob_profiling_on,false) ->
    format('---- *** set preference PROFILING_INFO to TRUE to obtain more information!~n',[]) ; true),
    print_runtime_profile(top_level),
   
    format('---- Time spent evaluating CONSTANTS (defined by equations)~n',[]),
    (\+ constants_profiling_on ->
    format('---- *** set preference PERFORMANCE_INFO to TRUE to obtain more information!~n',[]) ; true),
    print_runtime_profile(constant_computation(_,_)),
   
    (opt_category(Category,_),
    \+ \+ total_runtime(_,Category,_,_,_,_,_,_),
    format('---- Time spent evaluating ~w~n',[Category]),
    print_runtime_profile(Category),
    fail
    ;
    true).

print_runtime_profile(Cat) :-
    get_category_call_name(Cat,Col1Header),
    format(' ~w : ~w ms (~w ms walltime & ~w - ~w ms walltime; #calls ~w)~n',
    [Col1Header,'Total Runtime','Total','Minimum','Maximum','Number of Calls']),
    findall(profile(RT,WT,Calls,MaxWT,PP,Cat,MaxID,Min),relevant_total_runtime(PP,Cat,RT,WT,Calls,MaxWT,MaxID,Min),List),
    sort(List,SL),
    reverse(SL,RSL),
    maplist(print_runtime_profile_info,RSL),
    findall(WT2,relevant_total_runtime(_PP1,Cat,_RT1,WT2,_Calls,_MaxWT1,_MaxID1,_),WList),
    sumlist(WList,TotalWT),
    findall(Calls2,relevant_total_runtime(_PP2,Cat,_RT2,WT2,Calls2,_MaxWT2,_MaxID2,_),WList2),
    sumlist(WList2,TotalCalls),
    format(' Total Walltime: ~w ms for #calls ~w~n',[TotalWT,TotalCalls]).

print_runtime_profile_info(profile(RT,WT,NrCalls,MaxWT,PP,Cat,MaxID,Min)) :-
    translate_pp(PP,Cat,PPS),
    (MaxID=unknown
    -> format(' ~w : ~w ms (~w ms walltime & ~w - ~w ms walltime; #calls ~w)~n',
    [PPS,RT,WT,Min,MaxWT,NrCalls])
    ; format(' ~w : ~w ms (~w ms walltime & ~w - ~w ms walltime (max for ~w); #calls ~w)~n',
    [PPS,RT,WT,Min,MaxWT,MaxID,NrCalls])
).

profile_failure_driven_loop(ActionName) :- profile_failure_driven_loop(ActionName,unknown).

profile_failure_driven_loop(_,_) :- preference(prob_profiling_on,false), !.

profile_failure_driven_loop(ActionName,StateID) :-
    start_profile(ActionName,Info),
    %format('Start Action ----> ~w (~w)~n',[ActionName,Info]),
    register_time(ActionName,StateID,Info).

profile_recursion(Call,Name,Arg) :-
    inc_recur(X),
    statistics(walltime,[Start,_]),
    indent(X),format('>> ~w,~w,~w ms (ENTER),~w~n',[X1,Name,Start,Arg]),
    call_cleanup(Call,
    (statistics(walltime,[End,_]), Tot is End-Start,
    indent(X),format('<< ~w,~w,~w ms (EXIT)~n',[X1,Name,Tot]),
    reset_recur(X)
)).

profile_single_call(Label,C) :- profile_single_call(Label,top_level,unknown,C).

profile_single_call(Label,StateID,C) :- profile_single_call(Label,top_level,StateID,C).

profile_single_call(_,_,_,Call) :- preference(prob_profiling_on,false), !, call(Call).

profile_single_call(Label,Category,StateID,C) :-
    start_profile(Label,StartInfo),
    if(call(C),
    stop_profile(Label,Category,StateID,StartInfo),
    (stop_profile(Label,Category,StateID,StartInfo),fail)).

recursion_level(0).

register_profiler_runtime(_,_,_,_,_) :- preference(prob_profiling_on,false), !.

register_profiler_runtime(ProgramPoint,Category,StateID,RTime,WTime) :-
    (var(ProgramPoint) -> PP2='unknown' ; PP2 = ProgramPoint),
    (retract(total_runtime(PP2,Category,OldR,OldW,Calls,Max,MaxID,Min))
    -> true
    ; OldR=0,OldW=0,Max=0,MaxID=StateID,Calls=0,Min=inf
    ),
    ((RTime<0 ; WTime <0) -> write(negative_runtime(PP2,StateID,RTime,WTime)),nl ; true),
    NewR is OldR+RTime, NewW is OldW+WTime, NewCalls is Calls+1,
    (WTime > Max -> NewMax = WTime, NewMaxID=StateID ; NewMax = Max, NewMaxID=MaxID),
    (number(Min), Min < WTime -> NewMin = Min ; NewMin = WTime),
    assertz(total_runtime(PP2,Category,NewR,NewW,NewCalls,NewMax,NewMaxID,NewMin)).

register_time(_,_,_).

register_time(AN,StateID,Info) :-
    stop_profile(AN,StateID,Info),
    fail.

relevant_cst_profile_entry(cprofile(RT,WT,PropWT,Calls,PP,Kind,Ann,Phase,IDInfo,InstItself,ValInfo,InstList)) :-
    (try_get_unique_constants_state(CstState) -> true ; CstState=[]),
    (Category = constant_computation(Phase,IDInfo0),
    relevant_total_runtime(PP,Category,RT,WT,Calls,_MaxWT,_MaxWitnessID,_Min),
    Phase \= propagate_value,
    (abstract_constant(PP,_) -> Kind=abstract ; concrete_constant(PP,_) -> Kind=concrete ; Kind=unknown)
    ;
    (constants_profiling_on -> Phase = no_equation_detected
    ; Phase = '-'), % constants profiling on needed to keep track of all equations (except arith. at the moment)
    RT=0, WT=0, PropWT=0, Calls=0, IDInfo0 = [],
    (abstract_constant(PP,_), Kind=abstract ; concrete_constant(PP,_), Kind=concrete),
    \+ total_runtime(PP,constant_computation(_,_),_,_,_,_,_,_) % we have no profiling info at all for PP
    ),
    (get_det_solution_for_constant_value_kind(PP,DetValInfo)
    -> DetSolFound = true,
    exclude(is_value_info,IDInfo0,IDInfo)
    ; DetValInfo = '-',
    DetSolFound = false, IDInfo0=IDInfo
    ),
    ( (DetSolFound=false ; DetValInfo='LARGE-VALUE'),
    member(bind(PP,CstVal),CstState), translate_bvalue_kind(CstVal,ValInfo)
    -> SolFound=true
    ; ValInfo=DetValInfo, SolFound=DetSolFound
    ),
    % now check whether there are infos about propagation phase:
    (total_runtime(PP,constant_computation(propagate_value,PropInfo),_,PropWT,_,_,_,_)
    -> (member(instantiates(IList),PropInfo) ->
    (select(PP,IList,InstList)
    -> InstItself=yes, % Equation determined directly the value
    % check if we have a long closure expansion entry
    % this has already been counted in the regular entry for the constant computation
    (member(long_closure_expansion,IDInfo), Phase=phase0 -> fail ; true)
    ; (DetSolFound=true -> InstItself = 'delayed'
    ; SolFound=true -> InstItself = 'non-det'
    ; InstItself='NO'),
    InstList=IList)
    ; % no instantiation list stored; performance monitoring not on
    (SolFound=true -> InstItself='-' ; InstItself='NO'),
    InstList = '-'
    )
    ; PropWT = 0,
    (DetSolFound=true -> InstItself='-' ; InstItself='NO'),
    InstList='-'
    ),
    (constant_variable_marked_as_expand(PP) -> Ann=expand
    ; constant_variable_marked_as_memo(PP) -> Ann=memo
    ; Ann = ''
).

relevant_total_runtime(PP,Cat,RT,WT,Calls,MaxWT,MaxID,Min) :-
    total_runtime(PP,Cat,RT,WT,Calls,MaxWT,MaxID,Min),
    \+ irrelevant_profile_entry(PP,Cat,WT).

reset_recur(X) :- retract(recursion_level(_)), assertz(recursion_level(X)).

reset_runtime_profiler :- % print('RESET '),nl, print_runtime_profile,
    retractall(total_runtime(_,_,_,_,_,_,_,_)).

runtime_observe_available :- preference(performance_monitoring_on,true).

runtime_profile_available :- preference(prob_profiling_on,true).

start_profile(_,P) :- preference(prob_profiling_on,false), !, P=[0,0].

start_profile(_Label,[RT1,WT1]) :-
    statistics(runtime,[RT1,_Delta]),
    statistics(walltime,[WT1,_]).

stop_constant_profile(Val,Phase,ID,IDInfo,Timer) :-
    (get_value_info(Val,ValKind) -> IDInfo2 = [ValKind|IDInfo] ; IDInfo2=IDInfo),
    opt_stop_profile(constant_computation(Phase,IDInfo2),ID,root,Timer,0).

stop_profile(Label,StateID,StartTimes) :-
    stop_profile(Label,top_level,StateID,StartTimes).

stop_profile(_,_,_,_) :- preference(prob_profiling_on,false), !.

stop_profile(Label,Category,StateID,[RT1,WT1]) :-
    statistics(runtime,[RT2,_]),
    statistics(walltime,[WT2,_]),
    DRT is RT2-RT1, DWT is WT2-WT1,
    %dec_recur(X),indent(X), format('<< ~w, ~w, ~w ms (EXIT)~n',[X,Label,DWT]),
    %format('Runtime for ~w : ~w ms (~w wall)~n',[Label:Category,DRT,DWT]),
    register_profiler_runtime(Label,Category,StateID,DRT,DWT).

tcltk_dot_constants_profile_info(File) :-
    gen_dot_graph(File,constant_profile_predicate,constant_instantiates).

tcltk_get_constants_profile_info(
    list([list(['Constant','Kind','@desc',
    'Computation Runtime (ms)',
    'Computation Walltime (ms)', 'Propagation Walltime (ms)',
    '# Calls','Other Infos', 'Valued','Det.Value','Instantiates'])|ResL])) :-
    (is_concrete_constants_state_id(_) ->
    (constants_profiling_on -> ResL = L ; ResL = [['Set PROFILING_INFO and PERFORMANCE_INFO preference to TRUE for full infos.']|L])
    ; is_initial_state_id(_) -> ResL = [['The machine has no constants to analyse!']|L]
    ; ResL = [['No constants values computed yet. SETUP_CONSTANTS first!']|L]),
    findall(ProfileTerm, relevant_cst_profile_entry(ProfileTerm),List),
    sort(List,SL),
    reverse(SL,RSL),
    maplist(get_cprofile_list,RSL,L).

tcltk_get_multiple_profile_infos(Class,list(Result)) :-
    Sep = list(['-','-','-','-','-','-','-']),
    findall([Sep|L], (opt_category(C,Class), tcltk_get_profile_info(C,list(L))), Ls),
    append(Ls,Result).

tcltk_get_operations_profile_info(List) :-
    tcltk_get_profile_info(top_level,List).

tcltk_get_profile_info(List) :- tcltk_get_profile_info(_,List).

tcltk_get_profile_info(Category,
    list([list([Column1,'Total Runtime','Total Walltime',
    '# Calls','Max. Walltime','Max. Witness ID', 'Min. Walltime'])|L])) :-
    get_category_call_name(Category,Column1),
    findall(profile(RT,WT,Calls,MaxWT,AN,Category,MaxWitnessID,Min),
    relevant_total_runtime(AN,Category,RT,WT,Calls,MaxWT,MaxWitnessID,Min),List),
    sort(List,SL),
    reverse(SL,RSL),
    maplist(get_profile_list,RSL,L).

translate_pp(PP,Cat,PPS) :- member(Cat,[top_level,external_functions,well_def_analyser]),!,
    translate_term_into_atom(PP,PPS).

translate_pp(PP,constant_computation(Phase,IDInfo),PPS) :- !,
    ajoin([PP,'::',Phase,'::',IDInfo],PPS). % TODO: improve rendering of IDInfo

translate_pp(PP,Category,PPS) :- ajoin([PP,'::',Category],PPS).