Quelle  java_connection.pvs

java_connection[D,H,caD,caH,caTime: posreal] : THEORY
BEGIN
  IMPORTING vertical, vertical_los, space_3D, repulsive, horizontal_los_criterion

  s,v,vo,vi,nvo: VAR Vect3
  minrelvs     : VAR posreal
  epsh, epsv   : VAR Sign

  verticalCoordination(s,v) : Sign =
     IF vertical_los?[H](s`z) AND horizontal_los?[D](s) THEN
         vertical_los[D,H,caD,caH,caTime].verticalCoordinationLoS(s,v)
     ELSE
          space_3D[D,H].verticalCoordinationConflict(s,v)   
     ENDIF

  verticalRepulsiveCriterion(s, vo, vi, nvo, minrelvs, epsv): boolean = 
     vertical_los_criterion?[D,H](s,vo-vi,epsv,minrelvs)(nvo-vi)

  % horizontalRepulsiveCriteria(s, vo, vi, nvo, epsh): boolean = 
  %    horizontal_los_criterion.horizRepulsiveCriteria2D(s, vo, vi, nvo, epsh)

END java_connection