39. Dependents when a flight changes🔗

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

rule

Rules.OneOrder.Ancillaries.replaceFlight
  (e :
    Rules.OneOrder.Ancillaries.ServiceKind →
      Rules.OneOrder.Ancillaries.DependentEffect)
  (r : Rules.OneOrder.Ancillaries.LinkReading)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order) (f : Rules.OneOrder.Service)
  (newSeg : String) : List Rules.OneOrder.Ancillaries.Impact
Rules.OneOrder.Ancillaries.replaceFlight
  (e :
    Rules.OneOrder.Ancillaries.ServiceKind →
      Rules.OneOrder.Ancillaries.DependentEffect)
  (r :
    Rules.OneOrder.Ancillaries.LinkReading)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order)
  (f : Rules.OneOrder.Service)
  (newSeg : String) :
  List Rules.OneOrder.Ancillaries.Impact

EARS: When a flight service is replaced by a flight on another segment, the system shall state for each live service that depends on it the effect the reading gives for its kind.

Story: As a customer whose flight changed, I want to be told what happens to my bag and my seat, so that I know what I still hold on the new flight.

Acceptance criteria:

ONE-604.1: When a flight service is replaced, the system shall state an effect for each live service that depends on it and for no other service.
ONE-604.2: When a flight service is replaced, the system shall give each dependent service the effect the reading gives for its kind.
ONE-604.3: Where a kind of service moves with its flight, the system shall put the moved service on the new segment, for the same passenger and under the same reference.
ONE-604.4: When a flight service is replaced, the system shall not move a seat to a seat that another passenger holds on the new flight.

The effect for each kind is the reading's; which services depend on the flight is the link's (LinkReading). A moved seat keeps its seat number, since the service details are kept by reference.

39.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-604.1	Proven	Seat moved onto taken seat, Every dependent gets one effect
ONE-604.2	Proven	Seat moved onto taken seat, The effect follows the kind of service
ONE-604.3	Proven	A moved service keeps its reference, Seat moved onto taken seat
ONE-604.4	Open	Moved seats on the new flight, Seat moved onto taken seat

39.2. Guarantees🔗

39.2.1. Every dependent gets one effect🔗

guarantee

Rules.OneOrder.Ancillaries.replace_states_each_dependent
  (e :
    Rules.OneOrder.Ancillaries.ServiceKind →
      Rules.OneOrder.Ancillaries.DependentEffect)
  (r : Rules.OneOrder.Ancillaries.LinkReading)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order) (f : Rules.OneOrder.Service)
  (newSeg : String) :
  List.map (fun x ↦ x.service)
      (Rules.OneOrder.Ancillaries.replaceFlight e r d o f newSeg) =
    List.map (fun x ↦ x.id)
      (List.filter Rules.OneOrder.Delivery.isLive
        (Rules.OneOrder.Ancillaries.dependents r d o f))
Rules.OneOrder.Ancillaries.replace_states_each_dependent
  (e :
    Rules.OneOrder.Ancillaries.ServiceKind →
      Rules.OneOrder.Ancillaries.DependentEffect)
  (r :
    Rules.OneOrder.Ancillaries.LinkReading)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order)
  (f : Rules.OneOrder.Service)
  (newSeg : String) :
  List.map (fun x ↦ x.service)
      (Rules.OneOrder.Ancillaries.replaceFlight
        e r d o f newSeg) =
    List.map (fun x ↦ x.id)
      (List.filter
        Rules.OneOrder.Delivery.isLive
        (Rules.OneOrder.Ancillaries.dependents
          r d o f))

The rule states one effect for each live dependent of the replaced flight, in order, and for no other service.

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

Checks acceptance criteria ONE-604.1.

39.2.2. The effect follows the kind of service🔗

guarantee

Rules.OneOrder.Ancillaries.replace_effect_by_kind
  (e :
    Rules.OneOrder.Ancillaries.ServiceKind →
      Rules.OneOrder.Ancillaries.DependentEffect)
  (r : Rules.OneOrder.Ancillaries.LinkReading)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order) (f : Rules.OneOrder.Service)
  (newSeg : String) (x : Rules.OneOrder.Ancillaries.Impact)
  (hx : x ∈ Rules.OneOrder.Ancillaries.replaceFlight e r d o f newSeg) :
  ∃ s ∈ Rules.OneOrder.Ancillaries.dependents r d o f,
    Rules.OneOrder.Delivery.isLive s = true ∧
      x.service = s.id ∧ x.effect = e (d.kind s.id)
Rules.OneOrder.Ancillaries.replace_effect_by_kind
  (e :
    Rules.OneOrder.Ancillaries.ServiceKind →
      Rules.OneOrder.Ancillaries.DependentEffect)
  (r :
    Rules.OneOrder.Ancillaries.LinkReading)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order)
  (f : Rules.OneOrder.Service)
  (newSeg : String)
  (x : Rules.OneOrder.Ancillaries.Impact)
  (hx :
    x ∈
      Rules.OneOrder.Ancillaries.replaceFlight
        e r d o f newSeg) :
  ∃
    s ∈
      Rules.OneOrder.Ancillaries.dependents
        r d o f,
    Rules.OneOrder.Delivery.isLive s =
        true ∧
      x.service = s.id ∧
        x.effect = e (d.kind s.id)

Each stated effect is the reading's effect for the kind of a live dependent of the replaced flight.

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

Checks acceptance criteria ONE-604.2.

39.2.3. A moved service keeps its reference🔗

guarantee

Rules.OneOrder.Ancillaries.replace_moves
  (e :
    Rules.OneOrder.Ancillaries.ServiceKind →
      Rules.OneOrder.Ancillaries.DependentEffect)
  (r : Rules.OneOrder.Ancillaries.LinkReading)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order) (f : Rules.OneOrder.Service)
  (newSeg : String) (x : Rules.OneOrder.Ancillaries.Impact)
  (hx : x ∈ Rules.OneOrder.Ancillaries.replaceFlight e r d o f newSeg)
  (hmove : x.effect = Rules.OneOrder.Ancillaries.DependentEffect.move) :
  ∃ s ∈ Rules.OneOrder.Ancillaries.dependents r d o f,
    x.moved =
        some
          { id := s.id, passenger := s.passenger, segment := newSeg,
            status := Rules.OneOrder.ServiceStatus.confirmed,
            delivery := s.delivery } ∧
      x.service = s.id
Rules.OneOrder.Ancillaries.replace_moves
  (e :
    Rules.OneOrder.Ancillaries.ServiceKind →
      Rules.OneOrder.Ancillaries.DependentEffect)
  (r :
    Rules.OneOrder.Ancillaries.LinkReading)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order)
  (f : Rules.OneOrder.Service)
  (newSeg : String)
  (x : Rules.OneOrder.Ancillaries.Impact)
  (hx :
    x ∈
      Rules.OneOrder.Ancillaries.replaceFlight
        e r d o f newSeg)
  (hmove :
    x.effect =
      Rules.OneOrder.Ancillaries.DependentEffect.move) :
  ∃
    s ∈
      Rules.OneOrder.Ancillaries.dependents
        r d o f,
    x.moved =
        some
          { id := s.id,
            passenger := s.passenger,
            segment := newSeg,
            status :=
              Rules.OneOrder.ServiceStatus.confirmed,
            delivery := s.delivery } ∧
      x.service = s.id

A dependent whose effect is to move is put on the new segment, for the same passenger, under the same reference, confirmed.

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

Checks acceptance criteria ONE-604.3.

39.2.4. Moved seats on the new flight🔗

guarantee

Rules.OneOrder.Ancillaries.replace_no_seat_clash
  (e :
    Rules.OneOrder.Ancillaries.ServiceKind →
      Rules.OneOrder.Ancillaries.DependentEffect)
  (r : Rules.OneOrder.Ancillaries.LinkReading)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order) (f : Rules.OneOrder.Service)
  (newSeg : String)
  (held : List Rules.OneOrder.Ancillaries.SeatAssignment)
  (a : Rules.OneOrder.Ancillaries.SeatAssignment)
  (ha :
    a ∈
      Rules.OneOrder.Ancillaries.movedSeats d
        (Rules.OneOrder.Ancillaries.replaceFlight e r d o f newSeg))
  (b : Rules.OneOrder.Ancillaries.SeatAssignment) (hb : b ∈ held)
  (hseg : b.segment = a.segment) (hseat : b.seat = a.seat) :
  b.passenger = a.passenger
Rules.OneOrder.Ancillaries.replace_no_seat_clash
  (e :
    Rules.OneOrder.Ancillaries.ServiceKind →
      Rules.OneOrder.Ancillaries.DependentEffect)
  (r :
    Rules.OneOrder.Ancillaries.LinkReading)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order)
  (f : Rules.OneOrder.Service)
  (newSeg : String)
  (held :
    List
      Rules.OneOrder.Ancillaries.SeatAssignment)
  (a :
    Rules.OneOrder.Ancillaries.SeatAssignment)
  (ha :
    a ∈
      Rules.OneOrder.Ancillaries.movedSeats
        d
        (Rules.OneOrder.Ancillaries.replaceFlight
          e r d o f newSeg))
  (b :
    Rules.OneOrder.Ancillaries.SeatAssignment)
  (hb : b ∈ held)
  (hseg : b.segment = a.segment)
  (hseat : b.seat = a.seat) :
  b.passenger = a.passenger

No seat moved by a flight replacement lands on a seat another passenger holds on the new flight.

Open question for the business. Under a reading where seats move with their flight, a seat keeps its number on the new flight, and nothing checks the new flight's seat map. A passenger's paid seat 12C moves to a flight on which another passenger already holds 12C. The example seatMovedOntoTakenSeat shows it. What happens to a seat when its flight is replaced: does it move, and to which seat, or is it refunded, stored or reshopped?

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

Checks acceptance criteria ONE-604.4.

39.3. Examples🔗

39.3.1. Seat moved onto taken seat🔗

example

Rules.OneOrder.Ancillaries.seatMovedOntoTakenSeat :
  List Rules.OneOrder.Ancillaries.ReplacementLine
Rules.OneOrder.Ancillaries.seatMovedOntoTakenSeat :
  List
    Rules.OneOrder.Ancillaries.ReplacementLine

Given a paid flight for PAX-1 on SEG-1 with paid seat 12C and a bag, and a new flight on SEG-2 on which PAX-9 already holds seat 12C.

When the airline replaces PAX-1's flight with the one on SEG-2, under two readings of the effect on each kind of dependent.

Then where every dependent moves, seat 12C and the bag move to SEG-2, and seat 12C on the new flight is already PAX-9's. Where seats are reshopped, only the bag moves and the customer must choose a seat again.

What Lean computed:

Reading	Service	Effect	Moves to	Seat already held by
every dependent moves	SEAT-12C	move	SEG-2	PAX-9
every dependent moves	BAG-1	move	SEG-2	none
seats are reshopped	SEAT-12C	reshop	none	none
seats are reshopped	BAG-1	move	SEG-2	none

Checks acceptance criteria ONE-604.1, ONE-604.2, ONE-604.3, ONE-604.4.

39.4. Open question🔗

The guarantee Moved seats on the new flight is open: the example Seat moved onto taken seat shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.