Skip to content

Advanced Semantic Analysis in Rave

As airline rule sets grow in complexity, developers must understand not only how to write functional rules but also how the compiler interprets those rules to optimize the search space. Rave utilizes semantic analysis and static code analysis at compile-time to automatically determine rule properties, guiding the Pairing Generator's traversal strategy.

This document explores the semantic analysis framework used to classify rules, inspired by extended type checking and abstract interpretation.

1. The Goal of Semantic Analysis

The primary goal of analyzing Rave code at compile-time is to automate the detection of patterns that impact generation efficiency.

During Pairing Generation, the system builds candidate trips leg by leg. When an incomplete trip violates a rule, the generator must decide whether to:

  1. Prune the branch: If no future leg additions can make the trip legal (a Final Rule).
  2. Continue searching: If future leg additions might eventually make the trip legal (an Illegal Subchain Rule).

By annotating the Abstract Syntax Trees (ASTs) of the code with semantic properties, the compiler can automatically deduce whether a rule is a Final Rule or an Illegal Subchain Rule.

2. Attribute Inference

The Rave compiler uses inference rules (similar to typing rules) to propagate semantic attributes bottom-up through the AST. Every expression is checked against these rules.

Range Attributes

These attributes describe the numerical value range of an expression:

  • NonNegative: The expression evaluates to \(\ge 0\) (e.g., a flight's duration).
  • NonPositive: The expression evaluates to \(\le 0\).
graph TD
    A[Expression: e1 + e2]
    B[e1: NonNegative]
    C[e2: NonNegative]
    B --> A
    C --> A
    A -.-> D{Inferred: NonNegative}

Dependency & Constantness Attributes

These attributes track whether an expression changes as new legs are added:

  • ConstVal: An expression defined by a constant value.
  • LevelDependent: An expression whose evaluation changes in continued instances (e.g., adding legs to a duty).
  • LevelConstant: An expression whose value does not change as the current level instance grows (e.g., the starting time of a duty remains the same regardless of how many legs are added afterward).

3. Direction in Value (Monotonicity)

Understanding how numerical values change as the generator adds legs is crucial.

  • Monotonic Sum: A sum-expression whose subexpression is known to be either nonnegative or nonpositive.
  • NonDecreasing: A monotonic sum with a nonnegative subexpression is nondecreasing. As legs are added, the sum can only grow or stay the same.

4. Direction in Legality

By combining range, constantness, and value direction, the compiler infers the Direction in Legality for boolean expressions. This defines how the boolean evaluation behaves during trip generation:

  1. Non-increasing in Legality (NiL): A boolean expression instance that evaluates to false can never have a continuation that evaluates to true.
  2. Pattern: [NonDecreasing Expression] <= [Constant]

  3. Conclusion: If a rule's defining expression is NiL, it is a Final Rule.

  4. Non-decreasing in Legality (NdL): A boolean expression instance that evaluates to true can never have a continuation that evaluates to false.

  5. Pattern: [NonDecreasing Expression] >= [Constant]

  6. Conclusion: If a rule's defining expression is NdL, it is an Illegal Subchain Rule.

  7. NonFinal: A boolean expression lacking linear direction (e.g., comparing two variable expressions). These are safely treated as Illegal Subchain Rules to prevent accidental pruning of valid search spaces.