SSL cr3d.pvs

%------------------------------------------------------------------------------
% cr3d.pvs
% ACCoRD v.1.0
% Conflict resolution correctness
%------------------------------------------------------------------------------

cr3d[D,H:posreal] : THEORY
BEGIN

  IMPORTING horizontal_cr[D],
            vertical_cr[D,H],
            criteria_3D[D,H]

  sp        : VAR Sp_vect3 % 3-D separation
  nvo,nvi   : VAR Vect3
  vo,vi     : VAR Nzv2_vect3
  hst       : VAR Horizontal_Strategy
  vst       : VAR Vertical_Strategy
  epsh,epsv : VAR Sign

  cr?(sp,vo,vi,hst,vst)(nvo) : bool =
    horizontal_sep?(sp) AND horizontal_cr?(sp,vo,vi,hst(sp,vo-vi))(nvo) OR
    vertical_cr?(sp,vo,vi,hst(sp,vo-vi),vst(sp,vo-vi))(nvo)

  cr_satifies_criterion_3D : THEOREM
    conflict?(sp,vo-vi) AND
    cr?(sp,vo,vi,hst,vst)(nvo) IMPLIES
    criterion_3D?(sp,vo-vi,hst(sp,vo-vi),vst(sp,vo-vi))(nvo-vi)

  cr3d?(sp,vo,vi)(nvo) : bool =
    cr?(sp,vo,vi,horizontalCoordination,verticalCoordinationConflict)(nvo)

  cr3d_satifies_criterion_3D : THEOREM
    conflict?(sp,vo-vi) AND
    cr3d?(sp,vo,vi)(nvo) IMPLIES
    criterion_3D?(sp,vo-vi,horizontalCoordination(sp,vo-vi),verticalCoordinationConflict(sp,vo-vi))(nvo-vi)

  %--------------------------%
  % THEOREM: Independence    %
  %--------------------------%

  cr_independence: THEOREM
    conflict?(sp,vo-vi) AND
    cr?(sp,vo,vi,hst,vst)(nvo)
    IMPLIES 
      NOT conflict?(sp,nvo-vi)

  cr3d_independence: THEOREM
    conflict?(sp,vo-vi) AND
    cr3d?(sp,vo,vi)(nvo)
    IMPLIES 
      NOT conflict?(sp,nvo-vi)

  %--------------------------%
  % THEOREM: Coordination    %
  %--------------------------%

  cr_coordination: THEOREM
    conflict?(sp,vo-vi) AND
    cr?(sp,vo,vi,hst,vst)(nvo) AND
    cr?(-sp,vi,vo,hst,vst)(nvi)
    IMPLIES 
      NOT conflict?(sp,nvo-nvi)

  cr3d_coordination: THEOREM
    conflict?(sp,vo-vi) AND
    cr3d?(sp,vo,vi)(nvo) AND
    cr3d?(-sp,vi,vo)(nvi)
    IMPLIES 
      NOT conflict?(sp,nvo-nvi)

END cr3d