Top File of PVS ACCoRD Library

 
%------------------------------------------------------------------------------
% top.pvs
% ACCoRD v1.0
%------------------------------------------------------------------------------

top : THEORY
BEGIN

  IMPORTING 

    %%%% Utilities and Constants
    util,
    horizontal_dist_convexity,
    vertical_dist_convexity,

    %%%% Basic Definitions 
    definitions,
    gs_only,
    trk_only,
    opt_trk_gs,

    %%%% Horizontal Criteria 
    horizontal,
    horizontal_criteria,
    horizontal_criterion_line,
    line_solutions,
    tangent_line,
    predicate_coordination_2D,

    %%%% Horizontal Resolutions
    trk_line,
    gs_line,
    opt_line,
    horizontal_cr,

    %%%% Loss of Separation
    repulsive,
    horizontal_los_criterion,
    horizontal_los,
    vertical_los_criterion,
    vertical_los_crit_CA,
%    vertical_los,

    %%%% Vertical Conflict Detection
    cd_vertical,

    %%%% 2-D Conflict Detection 
    omega_v2,
    horizontal_sq_dtca,
    cd2d,
    cd2d_inf,
    cd3d_inf,

    %%%% 2-D Bands
    bands_util,
    gs_bands_2D,
    track,
    trk_bands_2D,
    bands_2D,

    %%%% 1-D Vertical Criteria
    vertical,
    vz_criteria,

    %%%% 3-D Criteria
    space_3D,
    circle_criterion,
    vertical_criterion,
    circle_solutions,
    predicate_coordination,
    criteria_3D,

    %%%% 3-D Horizonal Resolution Algorithms
    gs_circle,
    trk_circle,
    opt_vertical,

    %%%% Vertical Resolution Algorithms
    vs_only,
    vs_circle,
    vertical_cr,

    %%%% 3-D Conflict Detection 
    cd3d,
    cd_sphere,
    delay_3D,
    tca_3D,
    tca_3D_interval,

    %%%% Conflict Resolution
    cr3d,

    %%%% 3-D Bands
    vs_bands,
    bands_3D,

    %%%% Other Algorithms
%    repulsive_turn,
    repulsive_iterative,
    losr_iterative,
    kb,  % Karl Bilimoria's Geometric Optimization
%    mvp, % Modified Voltage Potential

    %%%% Flight plans
    flightplan,

    %%%% Conflict detection for state-based ownship and intent-based intruder
    cd3d_si,

    %%%% Conflict detection for intent-based ownship and intruder
    cd3d_ii,

    %%%% Prevention bands for state-based ownship and intent-based intruder
    bands_si,

    %%%% Auxilliary files for fseqs

    fseqs_aux_2D,
    fseqs_aux_vertical%,

    %%%% Higher level functions used in Java and C++
%    java_connection

END top

The tag identifies links that are outside the NASA domain