TCAS II Formal Specification

The Traffic Collision Avoidance System (TCAS) II is one of the most safety-critical systems in commercial aviation. Mandated on all aircraft with more than 30 seats, TCAS provides the last line of defense against mid-air collisions. When two aircraft are on a collision course, TCAS coordinates vertical maneuvers to ensure they diverge one climbs, one descends. This specification models TCAS II Version 7.1, the current standard defined in RTCA DO-185B. Version 7.1 introduced critical improvements over 7.0, particularly in handling cases where the intruder aircraft doesn’t follow their Resolution Advisory (RA). The 2002 Überlingen mid-air collision, where conflicting instructions from TCAS and ATC led to tragedy, drove many of these enhancements.

Why Formally Specify TCAS?

TCAS is a distributed system with real-time constraints, coordination requirements, and safety-critical invariants. Plus I was asked if I could figure it out, this is my attempt at doing so. The specification captures:

Sensitivity levels (SL2-SL7) with altitude-dependent thresholds
Modified tau formula for threat detection that handles low closure rates
DMOD, ZTHR, and ALIM parameters per altitude band
Altitude inhibitions preventing dangerous advisories near the ground
Preventive vs Corrective RA selection based on predicted miss distance
RA timing constraints preventing oscillation between advisories
Multi-threat logic when multiple intruders exist simultaneously
Version 7.1 enhancements for detecting intruder non-compliance

The formal model allows verification of properties like “coordinated RAs always have complementary senses” and “no descent RA is issued below 1100 feet AGL.”

Specification Overview

The specification defines several key components:

Sensitivity Levels

TCAS adjusts its alerting thresholds based on altitude above ground level (AGL). Lower altitudes use more aggressive thresholds because there’s less time and space to maneuver:

Sensitivity Level	Altitude AGL	TAU for RA	DMOD	ALIM
SL2	< 1000 ft	No RA	-	-
SL3	1000-2350 ft	15 sec	0.20 nm	300 ft
SL4	2350-5000 ft	20 sec	0.35 nm	300 ft
SL5	5000-10000 ft	25 sec	0.55 nm	350 ft
SL6	10000-20000 ft	30 sec	0.80 nm	400 ft
SL7	> 20000 ft	35 sec	1.10 nm	600 ft

Advisory Types

The specification models the full RA vocabulary:

Corrective RAs: Require immediate pilot action (Climb, Descend, Increase Climb/Descend, Crossing maneuvers, Reversals)
Preventive RAs: Limit vertical rate without requiring action (Don’t Climb, Don’t Descend, Limit Climb/Descend to specific rates)
Weakening RAs: Reduce RA strength as threat diminishes (Level Off, Maintain VS)

Coordination Protocol

When two TCAS II-equipped aircraft encounter each other, they coordinate via Mode S datalink to ensure complementary maneuvers. The specification models:

Sense selection based on geometry and received coordination
Reversal when same-sense conflict detected
Version 7.1 enhancement: reversal when intruder non-compliance detected

Full TLA+ Specification

------------------------------- MODULE TCAS_v71 -------------------------------
(***************************************************************************)
(* TCAS II Version 7.1 Specification (Per RTCA DO-185B)                    *)
(*                                                                         *)
(* This specification models TCAS II with accurate:                        *)
(* - Sensitivity levels (SL2-SL7) with correct thresholds                  *)
(* - Modified tau formula for threat detection                             *)
(* - DMOD, ZTHR, and ALIM parameters per altitude band                     *)
(* - Altitude inhibitions (no RA below 1000 ft AGL)                        *)
(* - Preventive vs Corrective RA selection                                 *)
(* - RA timing constraints                                                 *)
(* - Full RA type enumeration                                              *)
(***************************************************************************)

EXTENDS Integers, Sequences, FiniteSets, TLC

CONSTANTS
    Aircraft,           \* Set of aircraft identifiers
    MaxAltitudeMSL,     \* Maximum altitude MSL (feet / 100)
    MinAltitudeMSL,     \* Minimum altitude MSL (feet / 100)
    GroundElevation     \* Ground elevation for AGL calculation (feet / 100)

ASSUME
    /\ Aircraft # {}
    /\ MaxAltitudeMSL > MinAltitudeMSL
    /\ GroundElevation >= 0

(***************************************************************************)
(* TCAS II Version 7.1 Threshold Tables (Per DO-185B)                      *)
(*                                                                         *)
(* All altitudes in feet/100, times in seconds, distances in nm*100        *)
(***************************************************************************)

\* Sensitivity Level based on own altitude AGL
\* Returns SL 2-7
SensitivityLevel(altAGL) ==
    IF altAGL < 10 THEN 2       \* < 1000 ft AGL  → SL2 (TA only!)
    ELSE IF altAGL < 24 THEN 3  \* 1000-2350 ft   → SL3
    ELSE IF altAGL < 50 THEN 4  \* 2350-5000 ft   → SL4
    ELSE IF altAGL < 100 THEN 5 \* 5000-10000 ft  → SL5
    ELSE IF altAGL < 200 THEN 6 \* 10000-20000 ft → SL6
    ELSE 7                       \* > 20000 ft     → SL7

\* TAU thresholds for Traffic Advisory (seconds)
TAU_TA(sl) ==
    CASE sl = 2 -> 20
      [] sl = 3 -> 25
      [] sl = 4 -> 30
      [] sl = 5 -> 40
      [] sl = 6 -> 45
      [] sl = 7 -> 48
      [] OTHER -> 48

\* TAU thresholds for Resolution Advisory (seconds)
\* Note: SL2 returns 9999 (effectively infinite) - NO RA at SL2!
TAU_RA(sl) ==
    CASE sl = 2 -> 9999  \* No RA below 1000 ft AGL!
      [] sl = 3 -> 15
      [] sl = 4 -> 20
      [] sl = 5 -> 25
      [] sl = 6 -> 30
      [] sl = 7 -> 35
      [] OTHER -> 35

\* DMOD for Traffic Advisory (nm * 100)
DMOD_TA(sl) ==
    CASE sl = 2 -> 30   \* 0.30 nm
      [] sl = 3 -> 33   \* 0.33 nm
      [] sl = 4 -> 48   \* 0.48 nm
      [] sl = 5 -> 75   \* 0.75 nm
      [] sl = 6 -> 100  \* 1.00 nm
      [] sl = 7 -> 130  \* 1.30 nm
      [] OTHER -> 130

\* DMOD for Resolution Advisory (nm * 100)
DMOD_RA(sl) ==
    CASE sl = 2 -> 9999  \* No RA at SL2
      [] sl = 3 -> 20    \* 0.20 nm
      [] sl = 4 -> 35    \* 0.35 nm
      [] sl = 5 -> 55    \* 0.55 nm
      [] sl = 6 -> 80    \* 0.80 nm
      [] sl = 7 -> 110   \* 1.10 nm
      [] OTHER -> 110

\* ZTHR (Vertical threshold) for TA (feet)
\* Note: All sensitivity levels use 850 ft for TA threshold
ZTHR_TA(sl) == 850

\* ZTHR (Vertical threshold) for RA (feet)
ZTHR_RA(sl) ==
    CASE sl = 2 -> 9999  \* No RA at SL2
      [] sl = 3 -> 600
      [] sl = 4 -> 600
      [] sl = 5 -> 600
      [] sl = 6 -> 600
      [] sl = 7 -> 700
      [] OTHER -> 700

\* ALIM - Altitude Limit for RA (target separation in feet)
ALIM(sl) ==
    CASE sl = 2 -> 9999  \* No RA at SL2
      [] sl = 3 -> 300
      [] sl = 4 -> 300
      [] sl = 5 -> 350
      [] sl = 6 -> 400
      [] sl = 7 -> 600
      [] OTHER -> 600

(***************************************************************************)
(* Above FL420 Special Thresholds (Per DO-185B)                            *)
(*                                                                         *)
(* Above FL420 (42,000 ft), TCAS uses expanded thresholds due to higher    *)
(* aircraft performance and thinner air affecting climb/descent rates.     *)
(***************************************************************************)

\* Check if aircraft is above FL420 (42,000 ft = 420 in our units)
IsAboveFL420(altMSL) == altMSL >= 420

\* ZTHR for TA above FL420 (expanded from 850 to 1200 ft)
ZTHR_TA_FL420 == 1200

\* ZTHR for RA above FL420 (expanded from 700 to 800 ft)
ZTHR_RA_FL420 == 800

\* ALIM above FL420 (expanded from 600 to 700 ft)
ALIM_FL420 == 700

\* Get effective ZTHR_TA considering FL420
EffectiveZTHR_TA(sl, altMSL) ==
    IF IsAboveFL420(altMSL) THEN ZTHR_TA_FL420
    ELSE ZTHR_TA(sl)

\* Get effective ZTHR_RA considering FL420
EffectiveZTHR_RA(sl, altMSL) ==
    IF IsAboveFL420(altMSL) THEN ZTHR_RA_FL420
    ELSE ZTHR_RA(sl)

\* Get effective ALIM considering FL420
EffectiveALIM(sl, altMSL) ==
    IF IsAboveFL420(altMSL) THEN ALIM_FL420
    ELSE ALIM(sl)

(***************************************************************************)
(* HMD Filter (Horizontal Miss Distance) Per DO-185B                       *)
(*                                                                         *)
(* The HMD filter prevents false alerts when aircraft will pass with       *)
(* adequate horizontal separation even if tau criteria are met.            *)
(* HMD = predicted horizontal distance at closest point of approach (CPA)  *)
(***************************************************************************)

\* HMD threshold for TA (nm * 100) - same as DMOD_TA
HMD_TA(sl) == DMOD_TA(sl)

\* HMD threshold for RA (nm * 100) - same as DMOD_RA
HMD_RA(sl) == DMOD_RA(sl)

\* Calculate predicted HMD (Horizontal Miss Distance) at CPA
\* Per DO-185B: HMD is the predicted horizontal distance at closest point of approach
\*
\* For a more accurate model (but still simplified without bearing):
\* - If aircraft are closing (rDot < 0), HMD depends on crossing geometry
\* - Head-on collision course: HMD ≈ 0
\* - Crossing/passing: HMD depends on lateral offset
\*
\* Improved approximation: Use range rate magnitude relative to closure
\* If closure is fast relative to range, likely head-on (HMD small)
\* If closure is slow, likely crossing (HMD larger, proportional to range)
PredictedHMD(a, b) ==
    LET r == horizontalRange[a][b]
        rDot == rangeRate[a][b]
        \* tau computation: if not closing (rDot >= 0), no CPA approaching
        tau == IF rDot >= 0 THEN 9999
               ELSE r \div (-rDot)  \* Time to CPA in seconds
    IN IF rDot >= 0 THEN r           \* Diverging or parallel - HMD is at least current range
       ELSE IF tau > 120 THEN r      \* Far away (> 2 min), use current range
       ELSE IF tau < 5 THEN 0        \* Very close to CPA, minimal HMD
       \* For intermediate cases: estimate based on closure geometry
       \* Faster closure relative to range suggests more direct approach (lower HMD)
       \* Closure rate of 1 nm/min at 1 nm range = direct approach
       \* Use: HMD ≈ r * (1 - closure_factor) where closure_factor = min(1, |rDot|*60/r)
       ELSE LET closureFactor == Min(100, ((-rDot) * 60 * 100) \div Max(1, r))
            IN (r * (100 - closureFactor)) \div 100

\* HMD filter passes (threat not filtered out)
HMDFilterPasses_TA(a, b) ==
    PredictedHMD(a, b) < HMD_TA(sensitivityLvl[a])

HMDFilterPasses_RA(a, b) ==
    PredictedHMD(a, b) < HMD_RA(sensitivityLvl[a])

(***************************************************************************)
(* TCAS Operating Modes                                                    *)
(*                                                                         *)
(* TCAS II can operate in three modes:                                     *)
(* - Standby: TCAS surveillance only, no advisories                        *)
(* - TAOnly: Traffic Advisories only, no Resolution Advisories             *)
(* - TARA: Full TA/RA capability (normal operation)                        *)
(***************************************************************************)

TCASMode == {"Standby", "TAOnly", "TARA"}

(***************************************************************************)
(* Aural Annunciations (Per TCAS II v7.1)                                  *)
(*                                                                         *)
(* TCAS provides aural alerts to pilots for each advisory type.            *)
(***************************************************************************)

AuralType == {
    "None",
    \* Traffic Advisory
    "TrafficTraffic",           \* "Traffic, Traffic"
    \* Corrective RAs
    "ClimbClimb",               \* "Climb, Climb"
    "DescendDescend",           \* "Descend, Descend"
    "IncreaseClimb",            \* "Increase Climb, Increase Climb"
    "IncreaseDescend",          \* "Increase Descent, Increase Descent"
    "ClimbClimbNow",            \* "Climb, Climb NOW" (reversal)
    "DescendDescendNow",        \* "Descend, Descend NOW" (reversal)
    "ClimbCrossingClimb",       \* "Climb, Crossing Climb"
    "DescendCrossingDescend",   \* "Descend, Crossing Descend"
    \* Preventive RAs
    "MonitorVerticalSpeed",     \* "Monitor Vertical Speed"
    \* Weakening/Clear (v7.1: "Adjust VS" replaced by "Level Off")
    "MaintainVerticalSpeed",    \* "Maintain Vertical Speed, Maintain"
    "LevelOffLevelOff",         \* "Level Off, Level Off" (v7.1 replacement for "Adjust VS")
    "ClearOfConflict"           \* "Clear of Conflict"
}

\* Map RA type to aural annunciation
\* Note: v7.1 replaced "Adjust Vertical Speed" with "Level Off, Level Off"
AuralForRA(ra) ==
    CASE ra = "Climb" -> "ClimbClimb"
      [] ra = "Descend" -> "DescendDescend"
      [] ra = "IncreaseClimb" -> "IncreaseClimb"
      [] ra = "IncreaseDescend" -> "IncreaseDescend"
      [] ra = "ReversalToClimb" -> "ClimbClimbNow"
      [] ra = "ReversalToDescend" -> "DescendDescendNow"
      [] ra = "CrossingClimb" -> "ClimbCrossingClimb"
      [] ra = "CrossingDescend" -> "DescendCrossingDescend"
      [] ra = "DontClimb" -> "MonitorVerticalSpeed"
      [] ra = "DontDescend" -> "MonitorVerticalSpeed"
      [] ra \in {"LimitClimb500", "LimitClimb1000", "LimitClimb2000",
                 "LimitDescend500", "LimitDescend1000", "LimitDescend2000"}
           -> "MonitorVerticalSpeed"
      [] ra = "LevelOff" -> "LevelOffLevelOff"
      [] ra = "MaintainVS" -> "MaintainVerticalSpeed"
      [] ra = "MonitorVS" -> "MonitorVerticalSpeed"
      [] ra = "TA" -> "TrafficTraffic"
      [] OTHER -> "None"

(***************************************************************************)
(* Transponder and TCAS Equipment                                          *)
(***************************************************************************)

TransponderMode == {"Off", "ModeA", "ModeC", "ModeS", "Failed"}
TCASLevel == {"None", "TCAS_I", "TCAS_II"}

(***************************************************************************)
(* RA Types (Per TCAS II Version 7.1)                                      *)
(***************************************************************************)

\* Corrective RAs - require immediate pilot action
CorrectiveRA == {
    "Climb",              \* Climb at 1500-2000 fpm
    "Descend",            \* Descend at 1500-2000 fpm
    "IncreaseClimb",      \* Increase climb to 2500 fpm
    "IncreaseDescend",    \* Increase descent to 2500 fpm
    "CrossingClimb",      \* Climb, crossing through intruder altitude
    "CrossingDescend",    \* Descend, crossing through intruder altitude
    "ReversalToClimb",    \* Reverse from descend to climb
    "ReversalToDescend"   \* Reverse from climb to descend
}

\* Preventive RAs - limit vertical rate (don't go there)
PreventiveRA == {
    "DontClimb",          \* Don't climb (maintain or descend)
    "DontDescend",        \* Don't descend (maintain or climb)
    "LimitClimb500",      \* Limit climb to 500 fpm
    "LimitClimb1000",     \* Limit climb to 1000 fpm
    "LimitClimb2000",     \* Limit climb to 2000 fpm
    "LimitDescend500",    \* Limit descent to 500 fpm
    "LimitDescend1000",   \* Limit descent to 1000 fpm
    "LimitDescend2000"    \* Limit descent to 2000 fpm
}

\* Weakening RAs - reduce the RA strength
\* Note: "Adjust Vertical Speed" was REPLACED by "Level Off" in v7.1
WeakeningRA == {
    "LevelOff",           \* Reduce vertical rate to 0 (v7.1 replaces "Adjust VS")
    "MaintainVS",         \* Maintain current VS
    "MonitorVS"           \* Monitor VS (becoming advisory)
}

AllRATypes == CorrectiveRA \cup PreventiveRA \cup WeakeningRA
AdvisoryType == AllRATypes \cup {"None", "TA"}
RASense == {"None", "Up", "Down"}
ComplianceState == {"Complying", "NotComplying", "NoAdvisory"}

(***************************************************************************)
(* State Variables                                                         *)
(***************************************************************************)

VARIABLES
    \* Aircraft physical state
    altitudeMSL,        \* Altitude MSL (feet / 100)
    altitudeAGL,        \* Altitude AGL (feet / 100) - for inhibitions
    verticalRate,       \* Vertical rate (feet/min / 100)
    horizontalRange,    \* Range to other aircraft (nm * 100)
    rangeRate,          \* Range rate / closure rate (nm/sec * 100, negative = closing)
    verticalSep,        \* Vertical separation (feet / 100)

    \* Equipment state
    transponder,        \* Transponder mode
    tcasEquipped,       \* TCAS equipment level
    tcasMode,           \* TCAS operating mode (Standby/TAOnly/TARA)

    \* TCAS computed state
    sensitivityLvl,     \* Current sensitivity level (2-7)

    \* Advisory state
    advisory,           \* Current advisory
    raSense,            \* RA sense (Up/Down/None)
    raIssuedTime,       \* When RA was issued (for timing constraints)
    intruders,          \* Set of threatening aircraft
    auralAlert,         \* Current aural annunciation

    \* Coordination state
    coordinatedSense,   \* Sense being coordinated via Mode S
    receivedCoord,      \* Coordination received from intruder

    \* Pilot state
    pilotCompliance,

    \* System time
    time

vars == <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange, rangeRate,
          verticalSep, transponder, tcasEquipped, tcasMode, sensitivityLvl,
          advisory, raSense, raIssuedTime, intruders, auralAlert,
          coordinatedSense, receivedCoord, pilotCompliance, time>>

(***************************************************************************)
(* Type Invariant                                                          *)
(***************************************************************************)

TypeOK ==
    /\ altitudeMSL \in [Aircraft -> MinAltitudeMSL..MaxAltitudeMSL]
    /\ altitudeAGL \in [Aircraft -> 0..(MaxAltitudeMSL - GroundElevation)]
    /\ verticalRate \in [Aircraft -> -60..60]  \* ±6000 fpm
    /\ horizontalRange \in [Aircraft -> [Aircraft -> 0..500]]  \* 0-5 nm
    /\ rangeRate \in [Aircraft -> [Aircraft -> -100..100]]
    /\ verticalSep \in [Aircraft -> [Aircraft -> -500..500]]
    /\ transponder \in [Aircraft -> TransponderMode]
    /\ tcasEquipped \in [Aircraft -> TCASLevel]
    /\ tcasMode \in [Aircraft -> TCASMode]
    /\ sensitivityLvl \in [Aircraft -> 2..7]
    /\ advisory \in [Aircraft -> AdvisoryType]
    /\ raSense \in [Aircraft -> RASense]
    /\ raIssuedTime \in [Aircraft -> Nat]
    /\ intruders \in [Aircraft -> SUBSET Aircraft]
    /\ auralAlert \in [Aircraft -> AuralType]
    /\ coordinatedSense \in [Aircraft -> RASense]
    /\ receivedCoord \in [Aircraft -> RASense]
    /\ pilotCompliance \in [Aircraft -> ComplianceState]
    /\ time \in Nat

(***************************************************************************)
(* Helper Functions                                                        *)
(***************************************************************************)

Abs(x) == IF x < 0 THEN -x ELSE x
Max(x, y) == IF x > y THEN x ELSE y
Min(x, y) == IF x < y THEN x ELSE y

\* Can aircraft 'a' see aircraft 'b' via TCAS?
CanSee(a, b) ==
    /\ a # b
    /\ tcasEquipped[a] \in {"TCAS_I", "TCAS_II"}
    /\ transponder[b] \in {"ModeC", "ModeS"}

\* Can coordination occur between a and b?
CanCoordinate(a, b) ==
    /\ a # b
    /\ tcasEquipped[a] = "TCAS_II"
    /\ tcasEquipped[b] = "TCAS_II"
    /\ transponder[a] = "ModeS"
    /\ transponder[b] = "ModeS"

(***************************************************************************)
(* Intruder Compliance Detection (TCAS II v7.1 Enhancement)                *)
(*                                                                         *)
(* Version 7.1 monitors the intruder's vertical rate to detect when they   *)
(* are NOT following their coordinated RA. If non-compliance is detected,  *)
(* TCAS can issue a reversal to the compliant aircraft.                    *)
(***************************************************************************)

\* Detect if intruder b is not complying with their RA
\* This looks at intruder's actual vertical rate vs expected behavior
\* based on the coordination sense they sent (which indicates their RA sense)
IntruderNotComplying(a, b) ==
    /\ CanCoordinate(a, b)
    /\ receivedCoord[a] # "None"  \* We received coordination from them
    /\ LET intruderSense == receivedCoord[a]  \* Their coordinated sense
           intruderVR == verticalRate[b]       \* Their actual vertical rate
           \* Compliance threshold: should show significant response
           \* Positive VR means climbing, negative means descending
       IN \/ (intruderSense = "Up" /\ intruderVR < 5)    \* Should climb but isn't
          \/ (intruderSense = "Down" /\ intruderVR > -5) \* Should descend but isn't

\* Check if enough time has passed to expect pilot response
PilotResponseOverdue(a) ==
    time - raIssuedTime[a] >= EXPECTED_PILOT_RESPONSE

\* Detect if intruder is definitively not complying (after response time)
\* This is used to trigger v7.1 enhanced reversal logic
IntruderDefinitelyNotComplying(a, b) ==
    /\ IntruderNotComplying(a, b)
    /\ b \in intruders[a]
    /\ raIssuedTime[b] > 0  \* Intruder has an active RA
    /\ time - raIssuedTime[b] >= EXPECTED_PILOT_RESPONSE  \* Response time elapsed

(***************************************************************************)
(* Modified Tau Calculation (Per DO-185B)                                  *)
(*                                                                         *)
(* τ_mod = -(r² - DMOD²) / (r × ṙ)                                        *)
(*                                                                         *)
(* This handles low closure rate scenarios better than simple tau.         *)
(***************************************************************************)

\* Modified horizontal tau for TA
\* Protected against division by zero when r = 0
ModifiedTauTA(a, b) ==
    LET r == horizontalRange[a][b]
        rDot == rangeRate[a][b]
        dmod == DMOD_TA(sensitivityLvl[a])
    IN IF rDot >= 0 THEN 9999              \* Not closing
       ELSE IF r = 0 THEN 0                \* At collision point
       ELSE IF r <= dmod THEN 0            \* Already inside DMOD
       ELSE ((r * r) - (dmod * dmod)) \div ((-rDot) * r)

\* Modified horizontal tau for RA
\* Protected against division by zero when r = 0
ModifiedTauRA(a, b) ==
    LET r == horizontalRange[a][b]
        rDot == rangeRate[a][b]
        dmod == DMOD_RA(sensitivityLvl[a])
    IN IF rDot >= 0 THEN 9999
       ELSE IF r = 0 THEN 0                \* At collision point
       ELSE IF r <= dmod THEN 0
       ELSE ((r * r) - (dmod * dmod)) \div ((-rDot) * r)

\* Vertical tau (time to co-altitude in SECONDS)
\* Note: verticalRate is in feet/min/100, so we need to convert properly
\* Result must be in seconds to match horizontal tau calculations
VerticalTau(a, b) ==
    LET altDiff == verticalSep[a][b] * 100  \* Convert to feet
        vrDiff == (verticalRate[b] - verticalRate[a]) * 100  \* feet/min
    IN IF vrDiff = 0 THEN 9999
       ELSE IF (altDiff * vrDiff) < 0 THEN 9999  \* Diverging vertically
       \* Result is (feet / feet/min) = minutes, multiply by 60 to get seconds
       ELSE (Abs(altDiff) * 60) \div Abs(vrDiff)

(***************************************************************************)
(* Threat Detection (Per DO-185B)                                          *)
(*                                                                         *)
(* TA Condition: τ_mod < TAU_TA AND vertical_sep < ZTHR_TA                *)
(* RA Condition: τ_mod < TAU_RA AND vertical_sep < ZTHR_RA AND SL >= 3    *)
(***************************************************************************)

\* Traffic Advisory condition (with HMD filter and FL420 support)
TACondition(a, b) ==
    /\ CanSee(a, b)
    /\ tcasMode[a] \in {"TAOnly", "TARA"}   \* Not in Standby
    /\ ModifiedTauTA(a, b) < TAU_TA(sensitivityLvl[a])
    /\ Abs(verticalSep[a][b]) * 100 < EffectiveZTHR_TA(sensitivityLvl[a], altitudeMSL[a])
    /\ HMDFilterPasses_TA(a, b)             \* HMD filter

\* Resolution Advisory condition (with HMD filter and FL420 support)
RACondition(a, b) ==
    /\ CanSee(a, b)
    /\ tcasEquipped[a] = "TCAS_II"
    /\ tcasMode[a] = "TARA"                 \* Full TA/RA mode only
    /\ sensitivityLvl[a] >= 3               \* No RA at SL2!
    /\ ModifiedTauRA(a, b) < TAU_RA(sensitivityLvl[a])
    /\ Abs(verticalSep[a][b]) * 100 < EffectiveZTHR_RA(sensitivityLvl[a], altitudeMSL[a])
    /\ HMDFilterPasses_RA(a, b)             \* HMD filter

(***************************************************************************)
(* Altitude Inhibitions (Per DO-185B)                                      *)
(*                                                                         *)
(* Below 1000 ft AGL: No RAs (SL2)                                         *)
(* Below 1100 ft AGL: No Descend RAs                                       *)
(* Below 1550 ft AGL: No Increase Descend RAs                              *)
(***************************************************************************)

\* Can any RA be issued?
RANotInhibited(a) ==
    altitudeAGL[a] >= 10  \* >= 1000 ft AGL

\* Can Descend RA be issued?
DescendRANotInhibited(a) ==
    altitudeAGL[a] >= 11  \* >= 1100 ft AGL

\* Can Increase Descend RA be issued?
IncreaseDescendNotInhibited(a) ==
    altitudeAGL[a] >= 16  \* >= 1550 ft AGL

\* Can Crossing Descend RA be issued?
\* Same inhibition as regular Descend RA
CrossingDescendNotInhibited(a) ==
    altitudeAGL[a] >= 11  \* >= 1100 ft AGL

(***************************************************************************)
(* RA Selection Logic                                                      *)
(*                                                                         *)
(* 1. Calculate predicted VMD (Vertical Miss Distance) at CPA             *)
(* 2. If VMD >= ALIM: Issue preventive RA                                  *)
(* 3. If VMD < ALIM: Issue corrective RA                                   *)
(* 4. Select sense based on geometry and coordination                      *)
(***************************************************************************)

\* Predict vertical miss distance at CPA
PredictedVMD(a, b) ==
    LET tau == Min(ModifiedTauRA(a, b), VerticalTau(a, b))
        \* Project altitudes forward by tau seconds
        altA_atCPA == altitudeMSL[a] + (verticalRate[a] * tau \div 60)
        altB_atCPA == altitudeMSL[b] + (verticalRate[b] * tau \div 60)
    IN Abs(altA_atCPA - altB_atCPA) * 100  \* In feet

\* Determine if preventive RA is sufficient
IsPreventiveSufficient(a, b) ==
    PredictedVMD(a, b) >= ALIM(sensitivityLvl[a])

\* Select RA sense considering coordination, inhibitions, and own aircraft trajectory
\* Per DO-185B: Prefer sense that requires less deviation from current trajectory
SelectSense(a, b) ==
    LET theirCoord == receivedCoord[a]
        myAlt == altitudeMSL[a]
        theirAlt == altitudeMSL[b]
        myVR == verticalRate[a]  \* Own vertical rate (positive = climbing)
        \* Threshold for "significant" vertical rate (500 fpm = 5 in our units)
        significantVR == 5
    IN
    \* Priority 1: If coordination received, comply with complementary sense
    IF theirCoord = "Up" THEN "Down"
    ELSE IF theirCoord = "Down" THEN "Up"
    \* Priority 2: Check altitude inhibitions
    ELSE IF ~DescendRANotInhibited(a) THEN "Up"  \* Can't descend near ground
    \* Priority 3: If already in significant climb/descent, prefer that direction
    \* This minimizes required maneuver deviation (DO-185B optimization)
    ELSE IF myVR >= significantVR THEN "Up"      \* Already climbing, continue up
    ELSE IF myVR <= -significantVR THEN "Down"   \* Already descending, continue down
    \* Priority 4: Select based on geometry - maneuver away from intruder
    ELSE IF myAlt > theirAlt THEN "Up"     \* Above intruder: climb away
    ELSE IF myAlt < theirAlt THEN "Down"   \* Below intruder: descend away
    ELSE "Up"  \* Same altitude, default to climb

\* Determine if crossing RA is needed
\* Crossing RA is issued when own aircraft must pass through intruder's altitude
\* to achieve safe separation (intruder is between own and target altitude)
NeedsCrossingRA(a, b) ==
    LET myAlt == altitudeMSL[a]
        theirAlt == altitudeMSL[b]
        sense == SelectSense(a, b)
        alim == EffectiveALIM(sensitivityLvl[a], altitudeMSL[a])
        targetAlt == IF sense = "Up" THEN theirAlt + (alim \div 100) + 1
                     ELSE theirAlt - (alim \div 100) - 1
    IN \* Crossing needed if intruder is between current and target altitude
       \/ (sense = "Up" /\ theirAlt > myAlt /\ theirAlt < targetAlt)
       \/ (sense = "Down" /\ theirAlt < myAlt /\ theirAlt > targetAlt)

\* Select specific RA type (with crossing RA support and altitude inhibitions)
SelectRA(a, b) ==
    LET sense == SelectSense(a, b)
        preventive == IsPreventiveSufficient(a, b)
        crossing == NeedsCrossingRA(a, b)
    IN IF preventive
       THEN IF sense = "Up" THEN "DontDescend" ELSE "DontClimb"
       ELSE IF crossing
            THEN IF sense = "Up" THEN "CrossingClimb"
                 \* CrossingDescend has same inhibition as regular Descend
                 ELSE IF CrossingDescendNotInhibited(a) THEN "CrossingDescend"
                 ELSE "Descend"  \* Fall back to regular Descend if crossing inhibited
       ELSE IF sense = "Up" THEN "Climb" ELSE "Descend"

(***************************************************************************)
(* Multi-Threat RA Selection (Per DO-185B)                                 *)
(*                                                                         *)
(* When multiple intruders exist, TCAS must select a single RA that        *)
(* provides safe separation from ALL threats. If no single sense works,    *)
(* TCAS may issue a composite RA (level off, or pass through).             *)
(***************************************************************************)

\* Count threats above own aircraft
ThreatsAbove(a) ==
    {b \in intruders[a] : altitudeMSL[b] > altitudeMSL[a]}

\* Count threats below own aircraft
ThreatsBelow(a) ==
    {b \in intruders[a] : altitudeMSL[b] < altitudeMSL[a]}

\* Count co-altitude threats
ThreatsCoAlt(a) ==
    {b \in intruders[a] : altitudeMSL[b] = altitudeMSL[a]}

\* Determine if a single sense can provide separation from all threats
SingleSensePossible(a) ==
    \/ Cardinality(ThreatsAbove(a)) = 0  \* Can climb
    \/ Cardinality(ThreatsBelow(a)) = 0  \* Can descend

\* Select sense considering ALL threats (multi-threat logic)
SelectMultiThreatSense(a) ==
    LET above == Cardinality(ThreatsAbove(a))
        below == Cardinality(ThreatsBelow(a))
        coordReceived == receivedCoord[a]
    IN
    \* If coordination received, comply with complementary sense
    IF coordReceived = "Up" THEN "Down"
    ELSE IF coordReceived = "Down" THEN "Up"
    \* Check altitude inhibitions
    ELSE IF ~DescendRANotInhibited(a) THEN "Up"
    \* Select based on threat geometry
    ELSE IF above = 0 THEN "Up"        \* No threats above, climb
    ELSE IF below = 0 THEN "Down"      \* No threats below, descend
    \* Both above and below threats - select based on minimum separation needed
    ELSE IF above <= below THEN "Up"   \* Fewer threats above, try to climb
    ELSE "Down"

\* Check if any intruder requires a crossing maneuver
AnyIntruderNeedsCrossing(a) ==
    \E b \in intruders[a] : NeedsCrossingRA(a, b)

\* Select RA for multi-threat scenario
\* Enhanced to consider crossing RAs when needed
SelectMultiThreatRA(a) ==
    LET sense == SelectMultiThreatSense(a)
        \* Check if preventive is sufficient for ALL threats
        allPreventiveSufficient ==
            \A b \in intruders[a] : IsPreventiveSufficient(a, b)
        \* Check if any intruder requires crossing maneuver
        needsCrossing == AnyIntruderNeedsCrossing(a)
    IN IF ~SingleSensePossible(a)
       THEN "LevelOff"  \* Cannot escape up or down - level off
       ELSE IF allPreventiveSufficient
            THEN IF sense = "Up" THEN "DontDescend" ELSE "DontClimb"
       ELSE IF needsCrossing
            THEN \* Crossing RA needed - check altitude inhibitions
                 IF sense = "Up" THEN "CrossingClimb"
                 ELSE IF CrossingDescendNotInhibited(a) THEN "CrossingDescend"
                 ELSE "Descend"  \* Fall back if crossing inhibited
            ELSE IF sense = "Up" THEN "Climb" ELSE "Descend"

\* Issue RA considering multiple threats
IssueMultiThreatRA(a) ==
    /\ advisory[a] \in {"None", "TA"}
    /\ RANotInhibited(a)
    /\ Cardinality(intruders[a]) > 1  \* Multiple threats
    /\ \E b \in intruders[a] : RACondition(a, b)
    /\ LET selectedRA == SelectMultiThreatRA(a)
           sense == SelectMultiThreatSense(a)
       IN /\ advisory' = [advisory EXCEPT ![a] = selectedRA]
          /\ raSense' = [raSense EXCEPT ![a] = sense]
          /\ raIssuedTime' = [raIssuedTime EXCEPT ![a] = time]
          /\ coordinatedSense' = [coordinatedSense EXCEPT ![a] =
                                  IF \E b \in intruders[a] : CanCoordinate(a, b)
                                  THEN sense ELSE "None"]
          /\ auralAlert' = [auralAlert EXCEPT ![a] = AuralForRA(selectedRA)]
    /\ pilotCompliance' = [pilotCompliance EXCEPT ![a] = "NotComplying"]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, transponder, tcasEquipped, tcasMode,
                   sensitivityLvl, intruders, receivedCoord, time>>

(***************************************************************************)
(* RA Timing Constraints (Per DO-185B)                                     *)
(***************************************************************************)

MIN_RA_DURATION == 5        \* Minimum 5 seconds before changing RA
MIN_REVERSAL_DELAY == 5     \* Minimum 5 seconds before reversal
MIN_WEAKENING_DELAY == 10   \* Minimum 10 seconds before weakening
EXPECTED_PILOT_RESPONSE == 5 \* Expected pilot response time (5 seconds per DO-185B)
CLEAR_OF_CONFLICT_DELAY == 5 \* Delay before announcing "Clear of Conflict" (DO-185B)

CanModifyRA(a) ==
    time - raIssuedTime[a] >= MIN_RA_DURATION

CanReverseRA(a) ==
    time - raIssuedTime[a] >= MIN_REVERSAL_DELAY

CanWeakenRA(a) ==
    time - raIssuedTime[a] >= MIN_WEAKENING_DELAY

(***************************************************************************)
(* Initial State                                                           *)
(***************************************************************************)

Init ==
    /\ altitudeMSL \in [Aircraft -> MinAltitudeMSL..MaxAltitudeMSL]
    /\ altitudeAGL = [a \in Aircraft |-> altitudeMSL[a] - GroundElevation]
    /\ verticalRate = [a \in Aircraft |-> 0]
    /\ horizontalRange = [a \in Aircraft |->
                          [b \in Aircraft |-> IF a = b THEN 0 ELSE 200]]
    /\ rangeRate = [a \in Aircraft |->
                    [b \in Aircraft |-> IF a = b THEN 0 ELSE 0]]
    /\ verticalSep = [a \in Aircraft |->
                      [b \in Aircraft |-> altitudeMSL[a] - altitudeMSL[b]]]
    /\ transponder \in [Aircraft -> TransponderMode]
    /\ tcasEquipped \in [Aircraft -> TCASLevel]
    \* TCAS mode: TARA for TCAS II, TAOnly for TCAS I, Standby for None
    /\ tcasMode = [a \in Aircraft |->
                   IF tcasEquipped[a] = "TCAS_II" THEN "TARA"
                   ELSE IF tcasEquipped[a] = "TCAS_I" THEN "TAOnly"
                   ELSE "Standby"]
    /\ sensitivityLvl = [a \in Aircraft |-> SensitivityLevel(altitudeAGL[a])]
    /\ advisory = [a \in Aircraft |-> "None"]
    /\ raSense = [a \in Aircraft |-> "None"]
    /\ raIssuedTime = [a \in Aircraft |-> 0]
    /\ intruders = [a \in Aircraft |-> {}]
    /\ auralAlert = [a \in Aircraft |-> "None"]
    /\ coordinatedSense = [a \in Aircraft |-> "None"]
    /\ receivedCoord = [a \in Aircraft |-> "None"]
    /\ pilotCompliance = [a \in Aircraft |-> "NoAdvisory"]
    /\ time = 0

(***************************************************************************)
(* Actions                                                                 *)
(***************************************************************************)

\* Update sensitivity level based on current AGL altitude
UpdateSensitivityLevel(a) ==
    /\ sensitivityLvl' = [sensitivityLvl EXCEPT ![a] =
                          SensitivityLevel(altitudeAGL[a])]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, transponder, tcasEquipped, tcasMode,
                   advisory, raSense, raIssuedTime, intruders, auralAlert,
                   coordinatedSense, receivedCoord, pilotCompliance, time>>

\* Detect and track intruders
DetectIntruders(a) ==
    /\ tcasEquipped[a] \in {"TCAS_I", "TCAS_II"}
    /\ tcasMode[a] # "Standby"
    /\ intruders' = [intruders EXCEPT ![a] =
                     {b \in Aircraft : TACondition(a, b)}]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, transponder, tcasEquipped, tcasMode,
                   sensitivityLvl, advisory, raSense, raIssuedTime, auralAlert,
                   coordinatedSense, receivedCoord, pilotCompliance, time>>

\* Issue Traffic Advisory
IssueTA(a) ==
    /\ advisory[a] = "None"
    /\ \E b \in Aircraft : TACondition(a, b) /\ ~RACondition(a, b)
    /\ advisory' = [advisory EXCEPT ![a] = "TA"]
    /\ auralAlert' = [auralAlert EXCEPT ![a] = "TrafficTraffic"]
    /\ raIssuedTime' = [raIssuedTime EXCEPT ![a] = time]  \* Track TA issue time for clear delay
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, transponder, tcasEquipped, tcasMode,
                   sensitivityLvl, raSense, intruders,
                   coordinatedSense, receivedCoord, pilotCompliance, time>>

\* Issue Resolution Advisory
IssueRA(a) ==
    /\ advisory[a] \in {"None", "TA"}
    /\ RANotInhibited(a)
    /\ \E b \in Aircraft :
        /\ RACondition(a, b)
        /\ LET selectedRA == SelectRA(a, b)
               sense == SelectSense(a, b)
           IN /\ advisory' = [advisory EXCEPT ![a] = selectedRA]
              /\ raSense' = [raSense EXCEPT ![a] = sense]
              /\ raIssuedTime' = [raIssuedTime EXCEPT ![a] = time]
              /\ coordinatedSense' = [coordinatedSense EXCEPT ![a] =
                                      IF CanCoordinate(a, b) THEN sense ELSE "None"]
              /\ auralAlert' = [auralAlert EXCEPT ![a] = AuralForRA(selectedRA)]
    /\ pilotCompliance' = [pilotCompliance EXCEPT ![a] = "NotComplying"]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, transponder, tcasEquipped, tcasMode,
                   sensitivityLvl, intruders, receivedCoord, time>>

\* Receive coordination from intruder (Mode S)
ReceiveCoordination(a, b) ==
    /\ a # b
    /\ CanCoordinate(a, b)
    /\ coordinatedSense[b] # "None"
    /\ receivedCoord[a] = "None"
    /\ receivedCoord' = [receivedCoord EXCEPT ![a] = coordinatedSense[b]]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, transponder, tcasEquipped, tcasMode,
                   sensitivityLvl, advisory, raSense, raIssuedTime, intruders,
                   auralAlert, coordinatedSense, pilotCompliance, time>>

\* Strengthen RA (increase vertical rate requirement)
\* Note: IncreaseClimb has no altitude inhibition, but IncreaseDescend is inhibited below 1550 ft AGL
\* Strengthening can occur when:
\*   1. Threat has escalated (tau is less than half the threshold), OR
\*   2. Pilot hasn't responded after expected response time (v7.1 enhancement)
StrengthenRA(a) ==
    /\ advisory[a] \in {"Climb", "Descend"}
    /\ CanModifyRA(a)
    /\ \E b \in Aircraft :
        /\ RACondition(a, b)
        /\ \/ ModifiedTauRA(a, b) < TAU_RA(sensitivityLvl[a]) \div 2  \* Escalating threat
           \/ /\ PilotResponseOverdue(a)                              \* No response yet (v7.1)
              /\ pilotCompliance[a] = "NotComplying"
    /\ LET newRA == IF advisory[a] = "Climb"
                    THEN "IncreaseClimb"  \* No altitude inhibition for Increase Climb
                    ELSE IF IncreaseDescendNotInhibited(a) THEN "IncreaseDescend" ELSE advisory[a]
       IN /\ advisory' = [advisory EXCEPT ![a] = newRA]
          /\ auralAlert' = [auralAlert EXCEPT ![a] = AuralForRA(newRA)]
    /\ raIssuedTime' = [raIssuedTime EXCEPT ![a] = time]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, transponder, tcasEquipped, tcasMode,
                   sensitivityLvl, raSense, intruders,
                   coordinatedSense, receivedCoord, pilotCompliance, time>>

\* Reverse RA (change sense due to coordination)
ReverseRA(a) ==
    /\ advisory[a] \in CorrectiveRA
    /\ CanReverseRA(a)
    /\ \E b \in Aircraft :
        /\ RACondition(a, b)
        /\ CanCoordinate(a, b)
        /\ raSense[a] = raSense[b]  \* Same sense conflict
    /\ LET newSense == IF raSense[a] = "Up" THEN "Down" ELSE "Up"
           newRA == IF newSense = "Up" THEN "ReversalToClimb" ELSE "ReversalToDescend"
           canReverse == DescendRANotInhibited(a) \/ newSense = "Up"
       IN IF ~canReverse
          THEN UNCHANGED <<advisory, raSense, auralAlert, coordinatedSense>>
          ELSE /\ advisory' = [advisory EXCEPT ![a] = newRA]
               /\ raSense' = [raSense EXCEPT ![a] = newSense]
               /\ auralAlert' = [auralAlert EXCEPT ![a] = AuralForRA(newRA)]
               /\ coordinatedSense' = [coordinatedSense EXCEPT ![a] = newSense]
    /\ raIssuedTime' = [raIssuedTime EXCEPT ![a] = time]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, transponder, tcasEquipped, tcasMode,
                   sensitivityLvl, intruders, receivedCoord, pilotCompliance, time>>

\* Reverse RA due to intruder non-compliance (TCAS II v7.1 enhancement)
\* This is the key v7.1 improvement: if we detect that the intruder is NOT
\* following their RA (e.g., descending when they should climb), we reverse
\* our own RA to maintain separation.
ReverseRADueToIntruderNonCompliance(a) ==
    /\ advisory[a] \in CorrectiveRA
    /\ CanReverseRA(a)
    /\ pilotCompliance[a] = "Complying"  \* Own aircraft IS complying
    /\ \E b \in Aircraft :
        /\ RACondition(a, b)
        /\ IntruderDefinitelyNotComplying(a, b)
        \* Intruder is not responding correctly, so we need to reverse
    /\ LET newSense == IF raSense[a] = "Up" THEN "Down" ELSE "Up"
           newRA == IF newSense = "Up" THEN "ReversalToClimb" ELSE "ReversalToDescend"
       IN IF ~DescendRANotInhibited(a) /\ newSense = "Down"
          THEN UNCHANGED <<advisory, raSense, auralAlert, coordinatedSense>>  \* Can't reverse to descend near ground
          ELSE /\ advisory' = [advisory EXCEPT ![a] = newRA]
               /\ raSense' = [raSense EXCEPT ![a] = newSense]
               /\ auralAlert' = [auralAlert EXCEPT ![a] = AuralForRA(newRA)]
               /\ coordinatedSense' = [coordinatedSense EXCEPT ![a] = newSense]
    /\ raIssuedTime' = [raIssuedTime EXCEPT ![a] = time]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, transponder, tcasEquipped, tcasMode,
                   sensitivityLvl, intruders, receivedCoord, pilotCompliance, time>>

\* Weaken RA (reduce strength as threat diminishes)
WeakenRA(a) ==
    /\ advisory[a] \in CorrectiveRA
    /\ CanWeakenRA(a)
    /\ \A b \in intruders[a] : PredictedVMD(a, b) >= EffectiveALIM(sensitivityLvl[a], altitudeMSL[a]) * 2
    /\ advisory' = [advisory EXCEPT ![a] = "LevelOff"]
    /\ auralAlert' = [auralAlert EXCEPT ![a] = "LevelOffLevelOff"]
    /\ raIssuedTime' = [raIssuedTime EXCEPT ![a] = time]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, transponder, tcasEquipped, tcasMode,
                   sensitivityLvl, raSense, intruders,
                   coordinatedSense, receivedCoord, pilotCompliance, time>>

\* Clear advisory when threat resolved
\* Per DO-185B: Delay clearing to prevent rapid cycling of advisories
ClearAdvisory(a) ==
    /\ advisory[a] # "None"
    /\ \A b \in Aircraft : ~TACondition(a, b)
    \* Delay before clearing - must have been active for at least CLEAR_OF_CONFLICT_DELAY
    /\ time - raIssuedTime[a] >= CLEAR_OF_CONFLICT_DELAY
    /\ advisory' = [advisory EXCEPT ![a] = "None"]
    /\ raSense' = [raSense EXCEPT ![a] = "None"]
    /\ auralAlert' = [auralAlert EXCEPT ![a] = "ClearOfConflict"]
    /\ coordinatedSense' = [coordinatedSense EXCEPT ![a] = "None"]
    /\ receivedCoord' = [receivedCoord EXCEPT ![a] = "None"]
    /\ intruders' = [intruders EXCEPT ![a] = {}]
    /\ pilotCompliance' = [pilotCompliance EXCEPT ![a] = "NoAdvisory"]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, transponder, tcasEquipped, tcasMode,
                   sensitivityLvl, raIssuedTime, time>>

\* Environment: Aircraft approach (closing)
AircraftApproach(a, b) ==
    /\ a # b
    /\ horizontalRange[a][b] > 0
    /\ horizontalRange' = [horizontalRange EXCEPT ![a][b] = @ - 1, ![b][a] = @ - 1]
    /\ rangeRate' = [rangeRate EXCEPT ![a][b] = -1, ![b][a] = -1]  \* Closing
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, verticalSep,
                   transponder, tcasEquipped, tcasMode, sensitivityLvl,
                   advisory, raSense, raIssuedTime, intruders, auralAlert,
                   coordinatedSense, receivedCoord, pilotCompliance, time>>

\* Environment: Aircraft diverge (separating)
AircraftDiverge(a, b) ==
    /\ a # b
    /\ horizontalRange[a][b] < 500  \* Don't diverge beyond max range
    /\ horizontalRange' = [horizontalRange EXCEPT ![a][b] = @ + 1, ![b][a] = @ + 1]
    /\ rangeRate' = [rangeRate EXCEPT ![a][b] = 1, ![b][a] = 1]  \* Opening
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, verticalSep,
                   transponder, tcasEquipped, tcasMode, sensitivityLvl,
                   advisory, raSense, raIssuedTime, intruders, auralAlert,
                   coordinatedSense, receivedCoord, pilotCompliance, time>>

\* Environment: Aircraft maintain range (parallel flight)
AircraftParallel(a, b) ==
    /\ a # b
    /\ rangeRate[a][b] # 0  \* Currently closing or opening
    /\ rangeRate' = [rangeRate EXCEPT ![a][b] = 0, ![b][a] = 0]  \* Parallel
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange, verticalSep,
                   transponder, tcasEquipped, tcasMode, sensitivityLvl,
                   advisory, raSense, raIssuedTime, intruders, auralAlert,
                   coordinatedSense, receivedCoord, pilotCompliance, time>>

\* Transponder fails
TransponderFail(a) ==
    /\ transponder[a] \in {"ModeA", "ModeC", "ModeS"}
    /\ transponder' = [transponder EXCEPT ![a] = "Failed"]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, tcasEquipped, tcasMode, sensitivityLvl,
                   advisory, raSense, raIssuedTime, intruders, auralAlert,
                   coordinatedSense, receivedCoord, pilotCompliance, time>>

\* Transponder turned off by pilot
TransponderOff(a) ==
    /\ transponder[a] \in {"ModeA", "ModeC", "ModeS"}
    /\ transponder' = [transponder EXCEPT ![a] = "Off"]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, tcasEquipped, tcasMode, sensitivityLvl,
                   advisory, raSense, raIssuedTime, intruders, auralAlert,
                   coordinatedSense, receivedCoord, pilotCompliance, time>>

\* Transponder turned on or reset after failure
TransponderOn(a) ==
    /\ transponder[a] \in {"Off", "Failed"}
    /\ transponder' = [transponder EXCEPT ![a] = "ModeS"]  \* Default to Mode S
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, tcasEquipped, tcasMode, sensitivityLvl,
                   advisory, raSense, raIssuedTime, intruders, auralAlert,
                   coordinatedSense, receivedCoord, pilotCompliance, time>>

\* Transponder mode degrades (Mode S → Mode C, Mode C → Mode A)
TransponderDegrade(a) ==
    /\ \/ /\ transponder[a] = "ModeS"
          /\ transponder' = [transponder EXCEPT ![a] = "ModeC"]
       \/ /\ transponder[a] = "ModeC"
          /\ transponder' = [transponder EXCEPT ![a] = "ModeA"]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, tcasEquipped, tcasMode, sensitivityLvl,
                   advisory, raSense, raIssuedTime, intruders, auralAlert,
                   coordinatedSense, receivedCoord, pilotCompliance, time>>

(***************************************************************************)
(* TCAS Mode Switching Actions                                             *)
(***************************************************************************)

\* Switch TCAS to Standby mode (surveillance only, no advisories)
SetTCASStandby(a) ==
    /\ tcasEquipped[a] \in {"TCAS_I", "TCAS_II"}
    /\ tcasMode[a] # "Standby"
    /\ tcasMode' = [tcasMode EXCEPT ![a] = "Standby"]
    \* Clear any active advisories when switching to standby
    /\ advisory' = [advisory EXCEPT ![a] = "None"]
    /\ raSense' = [raSense EXCEPT ![a] = "None"]
    /\ auralAlert' = [auralAlert EXCEPT ![a] = "None"]
    /\ intruders' = [intruders EXCEPT ![a] = {}]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, transponder, tcasEquipped,
                   sensitivityLvl, raIssuedTime,
                   coordinatedSense, receivedCoord, pilotCompliance, time>>

\* Switch TCAS to TA Only mode (traffic advisories only)
\* Note: This is the maximum capability for TCAS I equipment
SetTCASTAOnly(a) ==
    /\ tcasEquipped[a] \in {"TCAS_I", "TCAS_II"}
    /\ tcasMode[a] # "TAOnly"
    /\ tcasMode' = [tcasMode EXCEPT ![a] = "TAOnly"]
    \* Downgrade any active RA to TA
    /\ IF advisory[a] \in CorrectiveRA \cup PreventiveRA \cup WeakeningRA
       THEN /\ advisory' = [advisory EXCEPT ![a] = "TA"]
            /\ raSense' = [raSense EXCEPT ![a] = "None"]
            /\ auralAlert' = [auralAlert EXCEPT ![a] = "TrafficTraffic"]
       ELSE UNCHANGED <<advisory, raSense, auralAlert>>
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, transponder, tcasEquipped,
                   sensitivityLvl, raIssuedTime, intruders,
                   coordinatedSense, receivedCoord, pilotCompliance, time>>

\* Switch TCAS to full TA/RA mode (normal operation)
SetTCASTARA(a) ==
    /\ tcasEquipped[a] = "TCAS_II"  \* Only TCAS II supports RA
    /\ tcasMode[a] # "TARA"
    /\ tcasMode' = [tcasMode EXCEPT ![a] = "TARA"]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, transponder, tcasEquipped,
                   sensitivityLvl, advisory, raSense, raIssuedTime, intruders,
                   auralAlert, coordinatedSense, receivedCoord, pilotCompliance, time>>

(***************************************************************************)
(* Pilot Actions                                                           *)
(***************************************************************************)

\* Pilot complies with RA by adjusting vertical rate
PilotComply(a) ==
    /\ advisory[a] \in CorrectiveRA
    /\ pilotCompliance[a] = "NotComplying"
    /\ LET targetRate ==
           CASE advisory[a] \in {"Climb", "CrossingClimb", "ReversalToClimb"} -> 20
             [] advisory[a] \in {"Descend", "CrossingDescend", "ReversalToDescend"} -> -20
             [] advisory[a] = "IncreaseClimb" -> 25
             [] advisory[a] = "IncreaseDescend" -> -25
             [] OTHER -> 0
       IN verticalRate' = [verticalRate EXCEPT ![a] = targetRate]
    /\ pilotCompliance' = [pilotCompliance EXCEPT ![a] = "Complying"]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, horizontalRange, rangeRate, verticalSep,
                   transponder, tcasEquipped, tcasMode, sensitivityLvl,
                   advisory, raSense, raIssuedTime, intruders, auralAlert,
                   coordinatedSense, receivedCoord, time>>

\* Pilot ignores RA (models non-compliance for verification)
PilotIgnoreRA(a) ==
    /\ advisory[a] \in CorrectiveRA \cup PreventiveRA
    /\ pilotCompliance[a] = "NotComplying"
    \* Pilot continues current action (no vertical rate change)
    /\ UNCHANGED vars

\* Pilot complies with preventive RA by limiting vertical rate
PilotComplyPreventive(a) ==
    /\ advisory[a] \in PreventiveRA
    /\ pilotCompliance[a] = "NotComplying"
    /\ LET limitedRate ==
           CASE advisory[a] = "DontClimb" ->
                IF verticalRate[a] > 0 THEN 0 ELSE verticalRate[a]
             [] advisory[a] = "DontDescend" ->
                IF verticalRate[a] < 0 THEN 0 ELSE verticalRate[a]
             [] advisory[a] = "LimitClimb500" ->
                IF verticalRate[a] > 5 THEN 5 ELSE verticalRate[a]
             [] advisory[a] = "LimitClimb1000" ->
                IF verticalRate[a] > 10 THEN 10 ELSE verticalRate[a]
             [] advisory[a] = "LimitClimb2000" ->
                IF verticalRate[a] > 20 THEN 20 ELSE verticalRate[a]
             [] advisory[a] = "LimitDescend500" ->
                IF verticalRate[a] < -5 THEN -5 ELSE verticalRate[a]
             [] advisory[a] = "LimitDescend1000" ->
                IF verticalRate[a] < -10 THEN -10 ELSE verticalRate[a]
             [] advisory[a] = "LimitDescend2000" ->
                IF verticalRate[a] < -20 THEN -20 ELSE verticalRate[a]
             [] OTHER -> verticalRate[a]
       IN verticalRate' = [verticalRate EXCEPT ![a] = limitedRate]
    /\ pilotCompliance' = [pilotCompliance EXCEPT ![a] = "Complying"]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, horizontalRange, rangeRate, verticalSep,
                   transponder, tcasEquipped, tcasMode, sensitivityLvl,
                   advisory, raSense, raIssuedTime, intruders, auralAlert,
                   coordinatedSense, receivedCoord, time>>

(***************************************************************************)
(* Aircraft Movement Actions                                               *)
(***************************************************************************)

\* Aircraft changes altitude based on vertical rate
AircraftMove(a) ==
    /\ LET newAltMSL == altitudeMSL[a] + verticalRate[a]
           clampedMSL == IF newAltMSL > MaxAltitudeMSL THEN MaxAltitudeMSL
                         ELSE IF newAltMSL < MinAltitudeMSL THEN MinAltitudeMSL
                         ELSE newAltMSL
           newAltAGL == clampedMSL - GroundElevation
       IN /\ altitudeMSL' = [altitudeMSL EXCEPT ![a] = clampedMSL]
          /\ altitudeAGL' = [altitudeAGL EXCEPT ![a] =
                             IF newAltAGL < 0 THEN 0 ELSE newAltAGL]
    \* Update vertical separation with all other aircraft
    \* Note: Self-separation (a,a) must always be 0
    /\ verticalSep' = [x \in Aircraft |->
                       [y \in Aircraft |->
                        IF x = y THEN 0  \* Self-separation is always 0
                        ELSE IF x = a THEN altitudeMSL'[a] - altitudeMSL[y]
                        ELSE IF y = a THEN altitudeMSL[x] - altitudeMSL'[a]
                        ELSE verticalSep[x][y]]]
    /\ UNCHANGED <<verticalRate, horizontalRange, rangeRate,
                   transponder, tcasEquipped, tcasMode, sensitivityLvl,
                   advisory, raSense, raIssuedTime, intruders, auralAlert,
                   coordinatedSense, receivedCoord, pilotCompliance, time>>

\* Aircraft changes vertical rate
ChangeVerticalRate(a) ==
    /\ \E newRate \in {-30, -20, -10, 0, 10, 20, 30} :
        /\ newRate # verticalRate[a]
        /\ verticalRate' = [verticalRate EXCEPT ![a] = newRate]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, horizontalRange, rangeRate, verticalSep,
                   transponder, tcasEquipped, tcasMode, sensitivityLvl,
                   advisory, raSense, raIssuedTime, intruders, auralAlert,
                   coordinatedSense, receivedCoord, pilotCompliance, time>>

\* Clear aural alert after it has been announced
ClearAuralAlert(a) ==
    /\ auralAlert[a] # "None"
    /\ auralAlert' = [auralAlert EXCEPT ![a] = "None"]
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, transponder, tcasEquipped, tcasMode,
                   sensitivityLvl, advisory, raSense, raIssuedTime, intruders,
                   coordinatedSense, receivedCoord, pilotCompliance, time>>

\* Time tick
Tick ==
    /\ time' = time + 1
    /\ UNCHANGED <<altitudeMSL, altitudeAGL, verticalRate, horizontalRange,
                   rangeRate, verticalSep, transponder, tcasEquipped, tcasMode,
                   sensitivityLvl, advisory, raSense, raIssuedTime, intruders,
                   auralAlert, coordinatedSense, receivedCoord, pilotCompliance>>

(***************************************************************************)
(* Next State                                                              *)
(***************************************************************************)

Next ==
    \* TCAS system actions
    \/ \E a \in Aircraft : UpdateSensitivityLevel(a)
    \/ \E a \in Aircraft : DetectIntruders(a)
    \/ \E a \in Aircraft : IssueTA(a)
    \/ \E a \in Aircraft : IssueRA(a)
    \/ \E a \in Aircraft : IssueMultiThreatRA(a)
    \/ \E a, b \in Aircraft : ReceiveCoordination(a, b)
    \/ \E a \in Aircraft : StrengthenRA(a)
    \/ \E a \in Aircraft : ReverseRA(a)
    \/ \E a \in Aircraft : ReverseRADueToIntruderNonCompliance(a)
    \/ \E a \in Aircraft : WeakenRA(a)
    \/ \E a \in Aircraft : ClearAdvisory(a)
    \/ \E a \in Aircraft : ClearAuralAlert(a)
    \* TCAS mode switching
    \/ \E a \in Aircraft : SetTCASStandby(a)
    \/ \E a \in Aircraft : SetTCASTAOnly(a)
    \/ \E a \in Aircraft : SetTCASTARA(a)
    \* Pilot actions
    \/ \E a \in Aircraft : PilotComply(a)
    \/ \E a \in Aircraft : PilotComplyPreventive(a)
    \/ \E a \in Aircraft : PilotIgnoreRA(a)
    \* Aircraft movement
    \/ \E a \in Aircraft : AircraftMove(a)
    \/ \E a \in Aircraft : ChangeVerticalRate(a)
    \/ \E a, b \in Aircraft : AircraftApproach(a, b)
    \/ \E a, b \in Aircraft : AircraftDiverge(a, b)
    \/ \E a, b \in Aircraft : AircraftParallel(a, b)
    \* Transponder actions
    \/ \E a \in Aircraft : TransponderFail(a)
    \/ \E a \in Aircraft : TransponderOff(a)
    \/ \E a \in Aircraft : TransponderOn(a)
    \/ \E a \in Aircraft : TransponderDegrade(a)
    \* Time
    \/ Tick

Spec == Init /\ [][Next]_vars

(***************************************************************************)
(* Fairness Conditions                                                     *)
(***************************************************************************)

\* TCAS must eventually process threats
Fairness ==
    /\ \A a \in Aircraft : WF_vars(DetectIntruders(a))
    /\ \A a \in Aircraft : WF_vars(IssueTA(a))
    /\ \A a \in Aircraft : WF_vars(IssueRA(a))
    /\ \A a \in Aircraft : WF_vars(IssueMultiThreatRA(a))
    /\ \A a \in Aircraft : WF_vars(ClearAdvisory(a))
    /\ \A a \in Aircraft : WF_vars(UpdateSensitivityLevel(a))

FairSpec == Spec /\ Fairness

(***************************************************************************)
(* Safety Properties                                                       *)
(***************************************************************************)

\* No RA issued below 1000 ft AGL (SL2)
NoRABelowSL2 ==
    \A a \in Aircraft :
        sensitivityLvl[a] = 2 => advisory[a] \in {"None", "TA"}

\* No Descend RA below 1100 ft AGL
NoDescendRABelowThreshold ==
    \A a \in Aircraft :
        altitudeAGL[a] < 11 =>
        advisory[a] \notin {"Descend", "IncreaseDescend", "ReversalToDescend"}

\* Coordinated RAs have complementary senses
CoordinatedRAsComplementary ==
    \A a, b \in Aircraft :
        /\ a # b
        /\ advisory[a] \in CorrectiveRA
        /\ advisory[b] \in CorrectiveRA
        /\ CanCoordinate(a, b)
        /\ b \in intruders[a]
        => raSense[a] # raSense[b]

\* RA timing constraints respected
RATimingRespected ==
    \A a \in Aircraft :
        advisory[a] \in {"ReversalToClimb", "ReversalToDescend"} =>
        time - raIssuedTime[a] >= MIN_REVERSAL_DELAY

\* No advisory possible without TCAS equipment
NoAdvisoryWithoutTCAS ==
    \A a \in Aircraft :
        tcasEquipped[a] = "None" => advisory[a] = "None"

\* No RA possible with only TCAS I
NoRAWithTCAS_I ==
    \A a \in Aircraft :
        tcasEquipped[a] = "TCAS_I" =>
        advisory[a] \in {"None", "TA"}

\* TCAS I cannot be in TA/RA mode (only Standby or TAOnly)
TCAS_I_ModeConstraint ==
    \A a \in Aircraft :
        tcasEquipped[a] = "TCAS_I" =>
        tcasMode[a] \in {"Standby", "TAOnly"}

\* Multi-threat RAs still maintain complementary senses when possible
MultiThreatCoordination ==
    \A a, b \in Aircraft :
        /\ a # b
        /\ advisory[a] \in CorrectiveRA
        /\ advisory[b] \in CorrectiveRA
        /\ CanCoordinate(a, b)
        /\ b \in intruders[a]
        /\ a \in intruders[b]
        /\ SingleSensePossible(a)
        /\ SingleSensePossible(b)
        => raSense[a] # raSense[b]

\* Collision avoidance when both aircraft visible (fundamental TCAS guarantee)
NoCollisionWhenVisible ==
    \A a, b \in Aircraft :
        /\ a # b
        /\ horizontalRange[a][b] = 0
        /\ CanSee(a, b)
        /\ CanSee(b, a)
        => Abs(verticalSep[a][b]) >= 3  \* 300 ft minimum

\* V7.1 Enhancement: System monitors for intruder non-compliance
\* If intruder is not complying after expected response time, TCAS should
\* be able to detect this (IntruderDefinitelyNotComplying will be true)
IntruderNonComplianceDetectable ==
    \A a, b \in Aircraft :
        /\ a # b
        /\ advisory[a] \in CorrectiveRA
        /\ advisory[b] \in CorrectiveRA
        /\ CanCoordinate(a, b)
        /\ receivedCoord[a] # "None"
        /\ pilotCompliance[a] = "Complying"
        /\ pilotCompliance[b] = "NotComplying"
        /\ time - raIssuedTime[b] >= EXPECTED_PILOT_RESPONSE
        => IntruderNotComplying(a, b)

\* TCAS mode constraints
NoRAInTAOnlyMode ==
    \A a \in Aircraft :
        tcasMode[a] = "TAOnly" =>
        advisory[a] \notin (CorrectiveRA \cup PreventiveRA \cup WeakeningRA)

NoAdvisoryInStandbyMode ==
    \A a \in Aircraft :
        tcasMode[a] = "Standby" =>
        advisory[a] = "None"

\* FL420 threshold constraints
FL420ThresholdsUsed ==
    \A a \in Aircraft :
        IsAboveFL420(altitudeMSL[a]) =>
        EffectiveALIM(sensitivityLvl[a], altitudeMSL[a]) = ALIM_FL420

\* Crossing RA issued when needed
CrossingRAWhenAppropriate ==
    \A a \in Aircraft :
        advisory[a] \in {"CrossingClimb", "CrossingDescend"} =>
        \E b \in intruders[a] : NeedsCrossingRA(a, b)

\* Aural alert corresponds to advisory
AuralMatchesAdvisory ==
    \A a \in Aircraft :
        advisory[a] \in CorrectiveRA \cup PreventiveRA =>
        auralAlert[a] \in AuralType \ {"None", "ClearOfConflict"}

(***************************************************************************)
(* Liveness Properties                                                     *)
(***************************************************************************)

\* If there's a threat, eventually an advisory is issued
EventualAdvisory ==
    \A a, b \in Aircraft :
        (TACondition(a, b)) ~> (advisory[a] # "None")

\* If RA is issued, pilot eventually complies (or advisory is cleared)
\* Note: Non-compliance is also modeled (PilotIgnoreRA), so we check for
\* either compliance OR advisory resolution
EventualResponse ==
    \A a \in Aircraft :
        (advisory[a] \in CorrectiveRA) ~>
        (pilotCompliance[a] = "Complying" \/ advisory[a] = "None")

\* Threats are eventually resolved
EventualResolution ==
    \A a \in Aircraft :
        (advisory[a] # "None") ~> (advisory[a] = "None")

=============================================================================

Key Safety Properties

The specification verifies several critical invariants:

NoRABelowSL2

No Resolution Advisory can be issued when an aircraft is below 1000 ft AGL (Sensitivity Level 2). At this altitude, pilots need to focus on landing/takeoff and shouldn’t be distracted by TCAS maneuvers.

NoDescendRABelowThreshold

Descend RAs are inhibited below 1100 ft AGL to prevent TCAS from commanding descent into terrain.

CoordinatedRAsComplementary

When two TCAS II-equipped aircraft coordinate, their RAs must have complementary senses—if one climbs, the other descends. This prevents both aircraft from maneuvering in the same direction.

IntruderNonComplianceDetectable

The v7.1 enhancement: if the intruder isn’t following their RA after the expected pilot response time (5 seconds), the system detects this and can trigger a reversal for the compliant aircraft.

Model Checking Configuration

To run this specification, create a configuration file:

CONSTANTS
    Aircraft = {a1, a2}
    MaxAltitudeMSL = 500
    MinAltitudeMSL = 0
    GroundElevation = 0

INIT Init
NEXT Next

INVARIANTS
    TypeOK
    NoRABelowSL2
    NoDescendRABelowThreshold
    CoordinatedRAsComplementary
    NoAdvisoryWithoutTCAS

PROPERTIES
    EventualAdvisory
    EventualResolution

The state space grows quickly with more aircraft. For practical model checking, 2-3 aircraft with bounded altitude ranges work well(ish)

Overview

TLA+

Alloy

AD Tier Model Specifications

Binary Analysis Series

Malware Analysis

Aviation Systems Series

Tools

TCAS II Formal Specification

Why Formally Specify TCAS?

Specification Overview

Sensitivity Levels

Advisory Types

Coordination Protocol

Full TLA+ Specification

Key Safety Properties

NoRABelowSL2

NoDescendRABelowThreshold

CoordinatedRAsComplementary

IntruderNonComplianceDetectable

Model Checking Configuration

Overview

TLA+

Alloy

AD Tier Model Specifications

Binary Analysis Series

Malware Analysis

Aviation Systems Series

Tools

​Why Formally Specify TCAS?

​Specification Overview

​Sensitivity Levels

​Advisory Types

​Coordination Protocol

​Full TLA+ Specification

​Key Safety Properties

​NoRABelowSL2

​NoDescendRABelowThreshold

​CoordinatedRAsComplementary

​IntruderNonComplianceDetectable

​Model Checking Configuration

Why Formally Specify TCAS?

Specification Overview

Sensitivity Levels

Advisory Types

Coordination Protocol

Full TLA+ Specification

Key Safety Properties

NoRABelowSL2

NoDescendRABelowThreshold

CoordinatedRAsComplementary

IntruderNonComplianceDetectable

Model Checking Configuration