36. Dependent service and its parent🔗

Requirement ONE-601. Of its 4 acceptance criteria, 3 are proven and 1 is open.

rule

Rules.OneOrder.Ancillaries.dependents
  (r : Rules.OneOrder.Ancillaries.LinkReading)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order) (f : Rules.OneOrder.Service) :
  List Rules.OneOrder.Service
Rules.OneOrder.Ancillaries.dependents
  (r :
    Rules.OneOrder.Ancillaries.LinkReading)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order)
  (f : Rules.OneOrder.Service) :
  List Rules.OneOrder.Service

EARS: The system shall count as dependent on a flight service the ancillary services of the order that the link between dependent and parent ties to it.

Story: As an airline, I want to know which bags, seats and meals depend on a flight, so that a change to the flight reaches every service it affects.

Acceptance criteria:

ONE-601.1: Where the order links a dependent service to its parent by reference, the system shall count an ancillary service of the order as dependent on a flight service exactly when it names that flight service as its parent.
ONE-601.2: Where the order links a dependent service to its parent through passenger and segment, the system shall count an ancillary service of the order as dependent on a flight service exactly when it is for the same passenger on the same segment.
ONE-601.3: The system shall count no flight service as a dependent.
ONE-601.4: When an order holds an ancillary service and a flight service for the same passenger and segment, the system shall count the ancillary service as dependent on that flight service.

Which link holds is the reading's (LinkReading). Under the reference reading an ancillary may name another ancillary as its parent, such as a lounge pass naming a premium seat. The rule counts dependents of flights only, so such a pass depends on no flight.

36.1. How each acceptance criterion is checked🔗

A criterion is proven when a guarantee below proves it for every input, and example only when only examples check it.

Criterion	Status	Checked by
ONE-601.1	Proven	Dependents by reference, Seat without reference
ONE-601.2	Proven	Seat without reference, Dependents through passenger and segment
ONE-601.3	Proven	Seat without reference, A flight is never a dependent
ONE-601.4	Open	Seat without reference, Every ancillary reaches its flight

36.2. Guarantees🔗

36.2.1. Dependents by reference🔗

guarantee

Rules.OneOrder.Ancillaries.dependents_by_reference
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order) (f s : Rules.OneOrder.Service) :
  s ∈
      Rules.OneOrder.Ancillaries.dependents
        Rules.OneOrder.Ancillaries.LinkReading.reference d o f ↔
    s ∈ Rules.OneOrder.Ancillaries.services o ∧
      d.isFlight f = true ∧
        d.isFlight s = false ∧ d.parent s.id = some f.id
Rules.OneOrder.Ancillaries.dependents_by_reference
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order)
  (f s : Rules.OneOrder.Service) :
  s ∈
      Rules.OneOrder.Ancillaries.dependents
        Rules.OneOrder.Ancillaries.LinkReading.reference
        d o f ↔
    s ∈
        Rules.OneOrder.Ancillaries.services
          o ∧
      d.isFlight f = true ∧
        d.isFlight s = false ∧
          d.parent s.id = some f.id

Under the reference reading, a service is a dependent of a flight service exactly when it is an ancillary of the order that names that flight service as its parent.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria ONE-601.1.

36.2.2. Dependents through passenger and segment🔗

guarantee

Rules.OneOrder.Ancillaries.dependents_by_passenger_segment
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order) (f s : Rules.OneOrder.Service) :
  s ∈
      Rules.OneOrder.Ancillaries.dependents
        Rules.OneOrder.Ancillaries.LinkReading.passengerSegment d o f ↔
    s ∈ Rules.OneOrder.Ancillaries.services o ∧
      d.isFlight f = true ∧
        d.isFlight s = false ∧
          s.passenger = f.passenger ∧ s.segment = f.segment
Rules.OneOrder.Ancillaries.dependents_by_passenger_segment
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order)
  (f s : Rules.OneOrder.Service) :
  s ∈
      Rules.OneOrder.Ancillaries.dependents
        Rules.OneOrder.Ancillaries.LinkReading.passengerSegment
        d o f ↔
    s ∈
        Rules.OneOrder.Ancillaries.services
          o ∧
      d.isFlight f = true ∧
        d.isFlight s = false ∧
          s.passenger = f.passenger ∧
            s.segment = f.segment

Under the passenger and segment reading, a service is a dependent of a flight service exactly when it is an ancillary of the order for the same passenger on the same segment.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria ONE-601.2.

36.2.3. A flight is never a dependent🔗

guarantee

Rules.OneOrder.Ancillaries.dependent_not_flight
  (r : Rules.OneOrder.Ancillaries.LinkReading)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order) (f s : Rules.OneOrder.Service)
  (h : s ∈ Rules.OneOrder.Ancillaries.dependents r d o f) :
  d.isFlight s = false
Rules.OneOrder.Ancillaries.dependent_not_flight
  (r :
    Rules.OneOrder.Ancillaries.LinkReading)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order)
  (f s : Rules.OneOrder.Service)
  (h :
    s ∈
      Rules.OneOrder.Ancillaries.dependents
        r d o f) :
  d.isFlight s = false

No flight service is ever counted as a dependent, under either reading.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria ONE-601.3.

36.2.4. Every ancillary reaches its flight🔗

guarantee

Rules.OneOrder.Ancillaries.dependents_cover
  (r : Rules.OneOrder.Ancillaries.LinkReading)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order) (f s : Rules.OneOrder.Service)
  (hs : s ∈ Rules.OneOrder.Ancillaries.services o)
  (hf : d.isFlight f = true) (ha : d.isFlight s = false)
  (hp : s.passenger = f.passenger) (hseg : s.segment = f.segment) :
  s ∈ Rules.OneOrder.Ancillaries.dependents r d o f
Rules.OneOrder.Ancillaries.dependents_cover
  (r :
    Rules.OneOrder.Ancillaries.LinkReading)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order)
  (f s : Rules.OneOrder.Service)
  (hs :
    s ∈
      Rules.OneOrder.Ancillaries.services
        o)
  (hf : d.isFlight f = true)
  (ha : d.isFlight s = false)
  (hp : s.passenger = f.passenger)
  (hseg : s.segment = f.segment) :
  s ∈
    Rules.OneOrder.Ancillaries.dependents
      r d o f

An ancillary for the same passenger and segment as a flight service of the order is counted as dependent on it, under either reading.

Open question for the business. Under the reference reading only an ancillary that names its flight counts. In the seat worked example the seat services name no flight service, so a seat for the passenger on the flight is not a dependent of it, and a change to the flight reports no impact on the seat. The example seatWithoutReference shows it. Which link defines the dependency: a reference to the parent, or the shared passenger and segment? And may an ancillary depend on another ancillary, such as a lounge pass on a premium seat?

Open The proof is not complete. See the open questions chapter.

Checks acceptance criteria ONE-601.4.

36.3. Examples🔗

36.3.1. Seat without reference🔗

example

Rules.OneOrder.Ancillaries.seatWithoutReference :
  List Rules.OneOrder.Ancillaries.DependentsFound
Rules.OneOrder.Ancillaries.seatWithoutReference :
  List
    Rules.OneOrder.Ancillaries.DependentsFound

Given the seat example order: flights for PAX01 and PAX02 on SEG1, a bag for PAX01 that names its flight as parent, and seats 12B for PAX01 and 12C for PAX02 that name no flight.

When the dependents of PAX01's flight are worked out under each reading of the link.

Then by reference only the bag depends on the flight; through passenger and segment the bag and seat 12B do. Under the reference reading a change to PAX01's flight reports no impact on seat 12B.

What Lean computed:

Reading	Dependents
by reference	BAG-1
by passenger and segment	BAG-1, SEAT-12B

Checks acceptance criteria ONE-601.1, ONE-601.2, ONE-601.3, ONE-601.4.

36.4. Open question🔗

The guarantee Every ancillary reaches its flight is open: the example Seat without reference shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.