mcdc_coverage

add_criteria(Op,Pred,InfoTree) :-
    retract(nr_of_criteria(Nr)), N1 is Nr+1,
    assertz(nr_of_criteria(N1)),
    assertz(criteria(N1,Op,Pred,InfoTree)).

analyse_individual_invariant(Style,Inv,'FALSE',ID) :-
    (invariant_violated(ID)
    ;
    Style \= quick,
    not_invariant_checked(ID), % also check seen distinct states, where invariant not processed
    find_invariant_violation_among_not_checked_nodes(ID) % compute invariant; store result
    ;
    Style=precise, not_all_transitions_added(ID)
    ),
    visited_expression(ID,State),
    state_corresponds_to_initialised_b_machine(State,CurBState),
    \+ b_interpreter:check_invariant_predicate_with_time_out(ID,Inv,CurBState),
    !.

analyse_individual_invariant(_,_Inv,'TRUE',ID) :-
    (is_initial_state_id(ID) -> true ; ID='none').

analyse_inv(Style,InvList,TS,Value,ID,PosInfo) :-
    member(Inv,InvList),
    translate_bexpression_with_limit(Inv,100,TS),
    get_position_info(Inv,PosInfo),
    analyse_individual_invariant(Style,Inv,Value,ID).

check_criteria(Nr,Result) :-
    criteria(Nr,OpName,Pred,InfoTree),
    translate:translate_bexpression_with_limit(Pred,TS),
    format('~nChecking: ~w : ~w~n',[OpName,TS]),
    explain(InfoTree,0),
    %translate:print_bexpr(Neg),nl,
    (test_boolean_expression_in_node(ResID,Pred)
    -> print(criterion_satisfied_in(ResID)),nl,nl,
    Result = ResID
    ; Result = uncovered
).

construct_mcdc_invariant_criteria(Level) :-
    get_mcdc_invariant_coverage_criterion(Level,InvName,RequiredCoverageCriterionPred,Tree),
    add_criteria(InvName,RequiredCoverageCriterionPred,Tree),
    fail.

construct_mcdc_invariant_criteria(_) :- nr_of_criteria(Nr), format('Nr of MC/DC INV criteria: ~w~n',[Nr]).

construct_mcdc_operation_criteria(Level) :-
    get_mcdc_coverage_criterion(Level,OpName,RequiredCoverageCriterionPred,Tree),
    add_criteria(OpName,RequiredCoverageCriterionPred,Tree),
    fail.

construct_mcdc_operation_criteria(_) :- nr_of_criteria(Nr), format('Nr of MC/DC criteria: ~w~n',[Nr]).

explain(true(Pred),L) :- !, indent(L), print('TRUE: '),print_bexpr(Pred),nl.

explain(false(Pred),L) :- !, indent(L), print('FALSE: '),print_bexpr(Pred),nl.

explain(conjunct_true(PosNr,Pred,InnerTree),L) :- !,
    indent(L), format('Conjunct ~w TRUE: ',[PosNr]), print_bexpr(Pred),
    nl,
    L1 is L+1, explain(InnerTree,L1).

explain(conjunct_false(PosNr,Pred,InnerTree),L) :- !,
    get_position_info(Pred,PI),
    indent(L), format('Conjunct ~w~w individually FALSE: ',[PosNr,PI]), %print_bexpr(Pred),
    nl,
    L1 is L+1, explain(InnerTree,L1).

explain(disjunct_true(PosNr,Pred,InnerTree),L) :- !,
    get_position_info(Pred,PI),
    indent(L), format('Disjunct ~w~w individually TRUE: ',[PosNr,PI]), %print_bexpr(Pred),
    nl,
    L1 is L+1, explain(InnerTree,L1).

explain(disjunct_false(PosNr,Pred,InnerTree),L) :- !,
    get_position_info(Pred,PI),
    indent(L), format('Disjunct ~w~w FALSE: ',[PosNr,PI]), print_bexpr(Pred),
    nl,
    L1 is L+1, explain(InnerTree,L1).

explain(implication_true(lhs_false,Pred,InnerTree),L) :- !,
    get_position_info(Pred,PI),
    indent(L), format('Implication LHS~w individually FALSE: ',[PI]), %print_bexpr(Pred),
    nl,
    L1 is L+1, explain(InnerTree,L1).

explain(implication_true(rhs_true,Pred,InnerTree),L) :- !,
    get_position_info(Pred,PI),
    indent(L), format('Implication RHS~w individually TRUE: ',[PI]), %print_bexpr(Pred),
    nl,
    L1 is L+1, explain(InnerTree,L1).

explain(equivalence_true(rhs_false,Pred,InnerTree),L) :- !,
    get_position_info(Pred,PI),
    indent(L), format('Equivalence RHS~w FALSE: ',[PI]), %print_bexpr(Pred),
    nl,
    L1 is L+1, explain(InnerTree,L1).

explain(equivalence_true(lhs_true,Pred,InnerTree),L) :- !,
    get_position_info(Pred,PI),
    indent(L), format('Equivalence LHS~w TRUE: ',[PI]), %print_bexpr(Pred),
    nl,
    L1 is L+1, explain(InnerTree,L1).

explain(equivalence_false(Pos,Pred,InnerTree),L) :- !,
    get_position_info(Pred,PI),
    indent(L), format('Equivalence ~w ~w: ',[Pos,PI]), %print_bexpr(Pred),
    nl,
    L1 is L+1, explain(InnerTree,L1).

explain(negation(InnerTree),L) :- !,
    indent(L), print('NEGATION'),
    nl,
    L1 is L+1, explain(InnerTree,L1).

explain(implication_false(lhs_true,Pred,InnerTree),L) :- !,
    get_position_info(Pred,PI),
    indent(L), format('Implication F with LHS~w TRUE: ',[PI]), %print_bexpr(Pred),
    nl,
    L1 is L+1, explain(InnerTree,L1).

explain(implication_false(rhs_false,Pred,InnerTree),L) :- !,
    get_position_info(Pred,PI),
    indent(L), format('Implication F with RHS~w FALSE: ',[PI]), %print_bexpr(Pred),
    nl,
    L1 is L+1, explain(InnerTree,L1).

explain(Term,L) :- indent(L), print(Term),nl,
    add_internal_error('Uncovered Info Tree: ', explain(Term,L)).

get_criteria_info(Nr,OpName,CritMsg,PredS,Source) :-
    criteria(Nr,OpName,_Pred,InfoTree),
    get_criteria_tree_info(InfoTree,CritMsg,Pred,Source),
    translate_bexpression_with_limit(Pred,40,PredS).

get_criteria_tree_info(true(Pred),'TRUE',Pred,PosInfo) :- !, get_position_info(Pred,PosInfo).

get_criteria_tree_info(false(Pred),'FALSE',Pred,PosInfo) :- !, get_position_info(Pred,PosInfo).

get_criteria_tree_info(conjunct_true(PosNr,CPred,InnerTree),Msg,Pred,Source) :- !,
    get_criteria_tree_info(InnerTree,IMsg,Pred,ISource),
    use_position_info_if_not_defined(ISource,CPred,Source),
    ajoin(['&(',PosNr,')T; ',IMsg],Msg).

get_criteria_tree_info(conjunct_false(PosNr,CPred,InnerTree),Msg,Pred,Source) :- !,
    get_criteria_tree_info(InnerTree,IMsg,Pred,ISource),
    use_position_info_if_not_defined(ISource,CPred,Source),
    ajoin(['&(',PosNr,')F; ',IMsg],Msg).

get_criteria_tree_info(disjunct_true(PosNr,DPred,InnerTree),Msg,Pred,Source) :- !,
    get_criteria_tree_info(InnerTree,IMsg,Pred,ISource),
    use_position_info_if_not_defined(ISource,DPred,Source),
    ajoin(['or(',PosNr,')T; ',IMsg],Msg).

get_criteria_tree_info(disjunct_false(PosNr,DPred,InnerTree),Msg,Pred,Source) :- !,
    get_criteria_tree_info(InnerTree,IMsg,Pred,ISource),
    use_position_info_if_not_defined(ISource,DPred,Source),
    ajoin(['or(',PosNr,')F; ',IMsg],Msg).

get_criteria_tree_info(implication_true(PosLR,ImpPred,InnerTree),Msg,Pred,Source) :- !,
    get_criteria_tree_info(InnerTree,IMsg,Pred,ISource),
    use_position_info_if_not_defined(ISource,ImpPred,Source),
    ajoin(['=>(',PosLR,')T; ',IMsg],Msg).

get_criteria_tree_info(implication_false(PosLR,ImpPred,InnerTree),Msg,Pred,Source) :- !,
    get_criteria_tree_info(InnerTree,IMsg,Pred,ISource),
    use_position_info_if_not_defined(ISource,ImpPred,Source),
    ajoin(['=>(',PosLR,')F; ',IMsg],Msg).

get_criteria_tree_info(equivalence_true(PosLR,ImpPred,InnerTree),Msg,Pred,Source) :- !,
    get_criteria_tree_info(InnerTree,IMsg,Pred,ISource),
    use_position_info_if_not_defined(ISource,ImpPred,Source),
    ajoin(['<=>(',PosLR,')T; ',IMsg],Msg).

get_criteria_tree_info(equivalence_false(PosLR,ImpPred,InnerTree),Msg,Pred,Source) :- !,
    get_criteria_tree_info(InnerTree,IMsg,Pred,ISource),
    use_position_info_if_not_defined(ISource,ImpPred,Source),
    ajoin(['<=>(',PosLR,')F; ',IMsg],Msg).

get_criteria_tree_info(negation(X),Msg,Pred,Source) :- !,
    get_criteria_tree_info(X,IMsg,Pred,Source),
    ajoin(['neg: ',IMsg],Msg).

get_criteria_tree_info(T,'UNKNOWN',error,'') :- add_internal_error('Unknown Info Tree: ',T).

get_individual_criteria(Nr,OpName,CriterionMsg,PredS,Result,Source) :-
    get_criteria_info(Nr,OpName,CriterionMsg,PredS,Source),
    enter_new_error_scope(ScopeID,mcdc_check_criteria(Nr)),
    check_criteria(Nr,Result),
    exit_error_scope(ScopeID,ErrOcc,mcdc_check_criteria(Nr)),
    (ErrOcc=true
    -> format('Error occured during MC/DC checking of criteria ~w (~w)~n ~w~n Result: ~w~n',[Nr,OpName,PredS,Result])
    % TO DO: reset errors
    ; true).

get_invariant_name(conjunct_true(PosNr,SinglePred,_InnerTree),Name) :- !,
    (bsyntaxtree:get_texpr_label(SinglePred,Name) -> true
    ; ajoin(['INV',PosNr],Name)).

get_invariant_name(_,'INV').

get_mcdc_coverage_criterion(Level,OpName,RequiredCoverageCriterionPred,Tree) :-
    get_operation_enabling_condition(OpName,Parameters,EnablingCondition,_BecomesSuchVars,_Precise,false,true),
    % TO DO: partition; avoid lifting becomes_such_that conditions
    % (in EventB the feasibility PO will ensure that Guard => BecomeSuchThat is ok)
    dif(OpName, '$initialise_machine'),
    (mcdc_true(Level,EnablingCondition,TargetPred,Tree) ;
    mcdc_false(Level,EnablingCondition,TargetPred,Tree) ),
    construct_optimized_exists(Parameters,TargetPred,RequiredCoverageCriterionPred),
    translate:print_bexpr(RequiredCoverageCriterionPred),nl.

get_mcdc_invariant_coverage_criterion(Level,InvName,TargetPred,Tree) :-
    b_get_invariant_from_machine(InvPred),
    mcdc_true(Level,InvPred,TargetPred,Tree), % we do not expect an INVARIANT to be false: only call mcdc_true
    get_invariant_name(Tree,InvName).

get_position_info(Expr,PosStr) :-
    bsyntaxtree:get_texpr_labels(Expr,Names),!,
    ajoin([' @', Names],PosStr).

get_position_info(Expr,PosStr) :- !,get_tk_table_position_info(Expr,PosStr).

indent(0) :- print('+--> ').

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

mcdc_false(0,Predicate,TargetPred,Res) :- !, Res = false(Predicate),
    create_negation(Predicate,TargetPred).

mcdc_false(Level,Predicate,TargetPred, Res) :-
    is_a_conjunct(Predicate,_,_),
    !, L1 is Level-1,
    Res = conjunct_false(PosNr,SinglePred,InnerTree),
    % check that every conjunct can be set individually to false:
    % A1 & ... Ai & ... Ak ----------> A1 & A2 ... not(Ai) & ... Ak
    conjunction_to_list(Predicate,List),
    select_pred(List, Rest1, SinglePred, Rest2, PosNr),
    mcdc_false(L1,SinglePred, InnerTargetPred, InnerTree),
    append(Rest1,[InnerTargetPred|Rest2],NewConj), % TO DO: better treatment for well-definedness !?
    % if SinglePred is a WD-Guard for Rest2: do not require to analyse Rest2 ?!
    conjunct_predicates(NewConj,TargetPred).

mcdc_false(Level,Predicate,TargetPred, Res) :- Level>1,
    is_a_disjunct(Predicate,_,_),
    !, L1 is Level-1,
    Res = disjunct_false(PosNr,SinglePred,InnerTree),
    % select every disjunct and check that we can make it false (with the rest also false) and cover its inner MCDC criteria
    disjunction_to_list(Predicate,List),
    select_pred(List, Rest1, SinglePred, Rest2, PosNr),
    maplist(create_negation,Rest1,NRest1), maplist(create_negation,Rest2,NRest2), % negate all other disjuncts
    mcdc_false(L1,SinglePred, InnerTargetPred, InnerTree), % compute inner MCDC criteria for selected conjunct SinglePred
    append(NRest1,[InnerTargetPred|NRest2],TargetList),
    conjunct_predicates(TargetList,TargetPred).

mcdc_false(Level,Predicate,TargetPred, Res) :- Level>1,
    is_an_implication(Predicate,LHS,RHS),
    % check LHS & not(RHS) and generate MCDC criteria for LHS and RHS if Level>1
    !, L1 is Level-1,
    Res = implication_false(Pos,Pred,InnerTree),
    ( mcdc_true(L1,LHS,InnerTargetPred,InnerTree), % TRUE <=> TRUE with focus on LHS
    Pos = lhs_true, Pred = LHS,
    create_negation(RHS,NRHS),
    conjunct_predicates([InnerTargetPred,NRHS],TargetPred)
    ;
    mcdc_false(L1,RHS,InnerTargetPred,InnerTree), % FALSE <=> FALSE with focus on RHS
    Pos = rhs_false, Pred = RHS,
    conjunct_predicates([LHS,InnerTargetPred],TargetPred)
).

mcdc_false(Level,Predicate,TargetPred, Res) :-
    is_an_equivalence(Predicate,LHS,RHS),
    !, L1 is Level-1,
    Res = equivalence_false(Pos,Pred,InnerTree),
    ( /* focus on LHS */ % We create FALSE <=> TRUE and focus on LHS
    mcdc_false(L1,LHS,InnerTargetPred,InnerTree),
    Pos = lhs_false, Pred = LHS,
    conjunct_predicates([InnerTargetPred,RHS],TargetPred)
    ;/* focus on RHS */
    mcdc_true(L1,RHS,InnerTargetPred,InnerTree), % we generate FALSE <=> TRUE and focus on RHS
    Pos = rhs_false, Pred = RHS,
    create_negation(LHS,NLHS),
    conjunct_predicates([NLHS,InnerTargetPred],TargetPred)
).

mcdc_false(Level,Predicate,TargetPred, Res) :-
    is_a_negation(Predicate,NPred),
    !,
    Res = negation(InnerTree),
    mcdc_true(Level,NPred,TargetPred, InnerTree).

mcdc_false(_,Predicate,TargetPred,Res) :- !,
    Res = false(Predicate),
    create_negation(Predicate,TargetPred).

mcdc_true(0,Predicate,TargetPred, ResTree) :- !, ResTree=true(TargetPred), TargetPred=Predicate.

mcdc_true(Level,Predicate,TargetPred, Res) :- Level>1,
    is_a_conjunct(Predicate,_,_),
    !, L1 is Level-1,
    Res = conjunct_true(PosNr,SinglePred,InnerTree),
    % select every conjunct and check that we can make it true (with the rest also true) and cover its inner MCDC criteria
    conjunction_to_list(Predicate,List),
    select_pred(List, Rest1, SinglePred, Rest2, PosNr),
    mcdc_true(L1,SinglePred, InnerTargetPred, InnerTree), % compute inner MCDC criteria for selected conjunct SinglePred
    append(Rest1,[InnerTargetPred|Rest2],TargetList),
    conjunct_predicates(TargetList,TargetPred).

mcdc_true(Level,Predicate,TargetPred, Res) :-
    is_a_disjunct(Predicate,_,_),
    !, L1 is Level-1,
    Res = disjunct_true(PosNr,SinglePred,InnerTree),
    % check that every disjunct can be set individually to true:
    % A1 or ... Ai or ... Ak ----------> not(A1) & not(A2) ... Ai & ... not(Ak)
    disjunction_to_list(Predicate,DisjList),
    select_pred(DisjList, Rest1, SinglePred, Rest2, PosNr),
    mcdc_true(L1,SinglePred, InnerTargetPred, InnerTree),
    maplist(create_negation,Rest1,NRest1),
    maplist(create_negation,Rest2,NRest2),
    append(NRest1,[InnerTargetPred|NRest2],TargetList),
    conjunct_predicates(TargetList,TargetPred).

mcdc_true(Level,Predicate,TargetPred, Res) :-
    is_an_implication(Predicate,LHS,RHS),
    !, L1 is Level-1,
    Res = implication_true(Pos,Pred,InnerTree),
    ( mcdc_false(L1,LHS,InnerTargetPred,InnerTree),
    Pos = lhs_false, Pred = LHS,
    create_negation(RHS,NRHS),
    % check not(LHS) & not(RHS) -> relevant that LHS is false, otherwise implication false
    conjunct_predicates([InnerTargetPred,NRHS],TargetPred)
    ;
    mcdc_true(L1,RHS,InnerTargetPred,InnerTree),
    Pos = rhs_true, Pred = RHS,
    % check LHS & RHS -> relevant that RHS is true, otherwise implication false
    conjunct_predicates([LHS,InnerTargetPred],TargetPred)
).

mcdc_true(Level,Predicate,TargetPred, Res) :-
    is_an_equivalence(Predicate,LHS,RHS),
    !, L1 is Level-1,
    Res = equivalence_true(Pos,Pred,InnerTree),
    ( /* focus on LHS */ % We try and create TRUE <=> TRUE; we could decide based upon structure of LHS/RHS
    mcdc_true(L1,LHS,InnerTargetPred,InnerTree),
    Pos = lhs_true, Pred = LHS,
    conjunct_predicates([InnerTargetPred,RHS],TargetPred)
    ;/* focus on RHS */
    mcdc_false(L1,RHS,InnerTargetPred,InnerTree), % we could generate mcdc_true(L1,RHS) also
    Pos = rhs_false, Pred = RHS,
    create_negation(LHS,NLHS),
    conjunct_predicates([NLHS,InnerTargetPred],TargetPred)
).

mcdc_true(Level,Predicate,TargetPred, Res) :-
    is_a_negation(Predicate,NPred),
    !,
    Res = negation(InnerTree),
    mcdc_false(Level,NPred,TargetPred, InnerTree).

mcdc_true(_,Predicate,Predicate,true(Predicate)).

nr_of_criteria(0).

reset_criteria :- retractall(criteria(_,_,_,_)),
    retractall(nr_of_criteria(_)), assertz(nr_of_criteria(0)).

select_pred(List, Rest1, Pred, Rest2, PosNr) :-
    append(Rest1,[Pred|Rest2],List), length(Rest1,L1), PosNr is L1+1.

tcltk_compute_mcdc_invariant_coverage(Res) :-
    get_preference(mc_dc_default_level,Level),
    tcltk_compute_mcdc_invariant_coverage(Level,Res).

tcltk_compute_mcdc_invariant_coverage(Level,list([list(['Nr','Invariant','Path to Condition', 'Condition', 'Result', 'Source'])|Result])) :-
    reset_criteria,
    construct_mcdc_invariant_criteria(Level),
    findall(list([Nr,Operation,CriterionMsg,PredS,Result,Source]),
    get_individual_criteria(Nr,Operation,CriterionMsg,PredS,Result,Source),
    Result).

tcltk_compute_mcdc_operation_coverage(Res) :-
    get_preference(mc_dc_default_level,Level),
    tcltk_compute_mcdc_operation_coverage(Level,Res).

tcltk_compute_mcdc_operation_coverage(Level,list([list(['Nr','Operation','Path to Condition', 'Condition', 'Result', 'Source'])|Result])) :-
    reset_criteria,
    construct_mcdc_operation_criteria(Level),
    findall(list([Nr,Operation,CriterionMsg,PredS,Result,Source]),
    get_individual_criteria(Nr,Operation,CriterionMsg,PredS,Result,Source),
    Result).

tcltk_get_invariant_coverage(list([list(['INVARIANT','VALUE','State ID','Source'])|ResList])) :-
    enter_new_error_scope(L,tcltk_get_invariant_coverage),
    b_get_invariant_from_machine(Invariant),
    conjunction_to_list(Invariant,InvList),
    set_unicode_mode,
    call_cleanup(findall(list([TS,Value,ID,PosInfo]),analyse_inv(normal,InvList,TS,Value,ID,PosInfo),ResList),
    unset_unicode_mode),
    exit_error_scope(L,_ErrOcc,tcltk_get_invariant_coverage).

test_boolean_expression_in_node(ResID,BoolExpr) :-
    visited_expression(ResID,CurState),
    state_corresponds_to_initialised_b_machine(CurState,CurBState),
    b_test_boolean_expression_cs(BoolExpr,[],CurBState,'MCDC coverage',ResID).

use_position_info_if_not_defined('',Expr,PosStr) :- !, get_position_info(Expr,PosStr).

use_position_info_if_not_defined(PosStr,_,PosStr).