tcltk_tree_inspector

cbc_get_direct_descendant(CBC_Path,NewPath) :-
    append(CBC_Path,[_],NewPath),
    cbc_get_path(_,NewPath,_).

cbc_get_path(Depth,CBC_Path,Last) :- cb_path(Depth,CBC_Path,Last).

cbc_get_path(Depth,CBC_Path,timeout) :- cb_timeout_path(Depth,CBC_Path).

cbc_get_path(Depth,CBC_Path,Last) :- cb_path_testcase_only(Depth,CBC_Path,Last).

cbc_path_info(TTI_Path,Event,Depth,Last,NrOfPaths,NrOfTests,NrOfSubs,Tags) :-
    translate_tti_path_to_term(cbc_tests,TTI_Path,CBC_Path),
    %print(cbc(CBC_Path)),nl,
    cbc_get_path(Depth,CBC_Path,Last),
    (CBC_Path = [] -> Event = 'INITIALISATION' ; last(CBC_Path,Event)),
    append(CBC_Path,_,Prefix),
    findall(Last,cb_path(_,Prefix,_),AllPathsWithPrefix),
    length(AllPathsWithPrefix,NrOfPaths),
    findall(Last,stored_test_case_op_trace(_,Prefix),AllTestsWithPrefix),
    length(AllTestsWithPrefix,NrOfTests),
    findall(Desc,cbc_get_direct_descendant(CBC_Path,Desc),AllDirectDescPaths),
    store_tti_paths(AllDirectDescPaths,0,TTI_Path,cbc_tests),
    length(AllDirectDescPaths,NrOfSubs),
    (stored_test_case_op_trace(_TestNr,CBC_Path)
    -> Tags = [ptrue] % we have generated a test-case from this path
    ; NrOfTests>0 -> Tags = []
    ; Tags = [darkgray]).

cbc_test_node_info([],'',[0,0,0,0],1,[]) :- % top-level; not shown in view
    assertz(tti_path_to_term(cbc_tests,[],[])).

cbc_test_node_info([0|TTI_Path],Event,[Depth,Last,NrOfPaths,NrOfTests],NrOfSubs,Tags) :-
    %print(find(TTI_Path)),nl,
    cbc_path_info(TTI_Path,Event,Depth,Last,NrOfPaths,NrOfTests,NrOfSubs,Tags),
    %print(found(TTI_Path,Event,Depth,Last,NrOfPaths,NrOfSubs)),nl,
    true.

get_state_space_node_id([],ID,acc(FromID,TransID,AVL),result(ID,FromID,TransID,Cycle)) :-
    (avl_fetch(ID,AVL) -> Cycle=cyle ; Cycle=fresh).

get_state_space_node_id([TopIndex|RestIndex],FromID,acc(PrevFromID,_,AVL),Result) :-
    state_space_children(FromID,Childs),
    avl_store(PrevFromID,AVL,true,NewAVL),
    nth0(TopIndex,Childs,t(TransID,NewID)), % TODO: detect if the last ID is a repetition and tag it differently
    get_state_space_node_id(RestIndex,NewID,acc(FromID,TransID,NewAVL),Result).

get_state_space_node_id_from_root(Pindex,Result) :-
    empty_avl(E),
    get_state_space_node_id(Pindex,root,acc(root,-1,E),Result).

nr_state_space_children(FromID,Nr) :-
    state_space_children(FromID,L),
    length(L,Nr).

reset_tcltk_tree_inspector :- retractall(tti_path_to_term(_,_,_)).

state_space_children(FromID,Childs) :-
    CheckInvariant = true,
    compute_all_transitions_if_necessary(FromID,CheckInvariant),
    findall(t(TransID,DestID),transition(FromID,_OperationTerm,TransID,DestID),Childs).

store_tti_paths([],_,_,_).

store_tti_paths([DescendantTerm|T],ChildNr,TTI_Path,TTI_Tree_Type) :-
    append(TTI_Path,[ChildNr],NewPath),
    assertz(tti_path_to_term(TTI_Tree_Type,NewPath,DescendantTerm)),
    %print(stored(NewPath,DescendantTerm)),nl,
    ChildNr1 is ChildNr+1,
    store_tti_paths(T,ChildNr1,TTI_Path,TTI_Tree_Type).

translate_tti_path_to_term(TTI_Tree_Type,TTI_Path,PrologTerm) :-
    (tti_path_to_term(TTI_Tree_Type,TTI_Path,R) -> PrologTerm=R
    ; add_internal_error('Cannot translate: ',
    translate_tti_path_to_term(TTI_Tree_Type,TTI_Path,PrologTerm)),
    PrologTerm = []).

tti_column_info(ast,header,'Node',100,300,w).

tti_column_info(ast,0,'Type',20,80,center).

tti_column_info(ast,1,'Infos',20,90,w).

tti_column_info(ast,2,'Quantified Ids',20,80,center).

tti_column_info(cbc_tests,header,'Event',100,400,w).

tti_column_info(cbc_tests,0,'Depth', 20,70,center).

tti_column_info(cbc_tests,1,'StateID', 25,70,center).

tti_column_info(cbc_tests,2,'Nr.Paths', 25,70,center).

tti_column_info(cbc_tests,3,'Nr.Tests', 25,70,center).

tti_column_info(state_space,header,'Transition',100,400,w).

tti_column_info(state_space,0,'Depth', 15,50,center).

tti_column_info(state_space,1,'StateID', 20,50,center).

tti_column_info(state_space,2,'Inv', 15,30,center).

tti_column_info(state_space,3,'TransID', 25,70,center).

tti_column_info(_,_,'??',20,40,center).

tti_column_name(TreeType,Column,Name) :-
    tti_column_info(TreeType,Column,Name,_MinWidth,_Width,_Anchor).

tti_get_node_info(empty,_,'-',list([]),0,list([])) :- !.

tti_get_node_info(cbc_tests,Pindex,Text,list(Columns),NrOfSubs,list(Tags)) :- !,
    cbc_test_node_info(Pindex,Text,Columns,NrOfSubs,Tags).

tti_get_node_info(ast,Pindex,Text,list([Type,Infos,QIDs]),NrOfSubs,list(Tags)) :-
    tcltk_get_node_info(Pindex,Text,Type,Infos,QIDs,NrOfSubs),
    (Type = write(pred) -> Tags = [ptrue] ; Type = write(subst) -> Tags = [pfalse]
    ; Type = write('') -> Tags = [gray5]
    ; Tags = [darkblue]).

tti_get_node_info(state_space,Pindex,Text,list([Depth,ID,INV,TransID]),NrOfSubs,list(Tags)) :- !,
    length(Pindex,Depth),
    get_state_space_node_id_from_root(Pindex,result(ID,FromID,TransID,Cycle)),
    nr_state_space_children(ID,NrOfSubs),
    (transition(FromID,OpTerm,TransID,ID)
    -> translate_event_with_src_and_target_id(OpTerm,FromID,ID,Text)
    ; Text = '(root)'
    ),
    (invariant_violated(ID) -> INV='KO'
    ; invariant_not_yet_checked(ID) -> INV='?'
    ; INV = 'ok'),
    (INV='KO' -> Tags = [pfalse]
    ; Cycle=cyle -> Tags = [darkgray]
    ; Tags=[darkblue]).

tti_number_of_columns(empty,Nr) :- !, Nr=0.

tti_number_of_columns(Type,Nr) :-
    findall(C,(tti_column_name(Type,C,_), number(C)),L),
    length(L,Nr).