%------------------------------------------------------------------------------
% criteria_3D.pvs
% ACCoRD v.1.0
%------------------------------------------------------------------------------

criteria_3D[D,H:posreal] : THEORY
BEGIN

  IMPORTING vertical_criterion[D,H],
     horizontal_criterion_line[D]%,

  sp        : VAR Sp_vect3 % 3-D separation
  s,v,nv,
  nvo,nvi   : VAR Vect3
  vo,vi     : VAR Nzv2_vect3
  epsh,epsv : VAR Sign

  criterion_3D?(sp,v,epsh,epsv)(nv) : bool = 
    (horizontal_sep?(sp) AND horizontal_criterion?(sp,epsh)(nv)) OR
    (vertical_criterion?(epsv)(sp,v)(nv) AND
     (horizontal_los?(sp) OR
      horizontal_criterion?(sp,epsh)(nv-v)))

  criterion_3D_independence : THEOREM
    conflict?(sp,v) AND
    criterion_3D?(sp,v,epsh,epsv)(nv) 
    IMPLIES
      NOT conflict?(sp,nv)

  criterion_3D_coordination : THEOREM
    conflict?(sp,vo-vi) AND
    criterion_3D?(sp,vo-vi,epsh,epsv)(nvo-vi) AND
    criterion_3D?(-sp,vi-vo,epsh,-epsv)(nvi-vo) IMPLIES
    NOT  conflict?(sp,nvo-nvi)

END criteria_3D