%
%
% Purpose : integration fault model with mapping to the 
%           results-based fault model.
%
%

integration_fault_model[N:posnat]: THEORY

  BEGIN
  IMPORTING 
     finite_sets_below_extra[N]

  p : VAR below(N)

  % the fault types for the integration fault model
  fault_class: TYPE =
    {good,                     
     omissive_symmetric,       
     omissive_asymmetric,
     transmissive_symmetric, 
     single_error_asymmetric,
     transmissive_asymmetric}

  fcl : var fault_class

  correct_denotation?(fcl) : bool =
    good?(fcl) OR omissive_symmetric?(fcl) OR omissive_asymmetric?(fcl)

  symmetric_denotation?(fcl) : bool = 
    good?(fcl) OR omissive_symmetric?(fcl) OR transmissive_symmetric?(fcl)

  single_denotation?(fcl) : bool =    
    NOT transmissive_asymmetric?(fcl)


  node_status: TYPE = [below(N) -> fault_class]

  status: VAR node_status

  good(status) : finite_set[below(N)] = {p | good?(status(p))}
  omissive_symmetric(status) : finite_set[below(N)] =
    {p | omissive_symmetric?(status(p))}
  omissive_asymmetric(status) : finite_set[below(N)] =
    {p | omissive_asymmetric?(status(p))}
  transmissive_symmetric(status)   : finite_set[below(N)] =
    {p | transmissive_symmetric?(status(p))}
  single_error_asymmetric(status)  : finite_set[below(N)] =
    {p | single_error_asymmetric?(status(p))}
  transmissive_asymmetric(status)  : finite_set[below(N)] =
    {p | transmissive_asymmetric?(status(p))}

  correct_denotation(status) : finite_set[below(N)] = 
     {p | correct_denotation?(status(p))}
  symmetric_denotation(status): finite_set[below(N)] = 
     {p | symmetric_denotation?(status(p))}
  single_denotation(status): finite_set[below(N)] = 
     {p | single_denotation?(status(p))}


  symmetric_single_denotation: LEMMA
    subset?(symmetric_denotation(status), single_denotation(status))


END integration_fault_model