46. Cancelling a flight without re-accommodation🔗

Requirement ONE-704. Of its 6 acceptance criteria, 3 are proven and 3 are open.

rule

Rules.OneOrder.AirlineChange.cancelFlight
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.AirlineChange.FlightRefund) (seg : String)
  (o : Rules.OneOrder.Order) :
  Rules.OneOrder.AirlineChange.FlightCancellation
Rules.OneOrder.AirlineChange.cancelFlight
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r :
    Rules.OneOrder.AirlineChange.FlightRefund)
  (seg : String)
  (o : Rules.OneOrder.Order) :
  Rules.OneOrder.AirlineChange.FlightCancellation

EARS: When the airline cancels a flight and does not re-accommodate the customer, the system shall cancel every live service on that flight with delivery status UNABLE TO DELIVER.

Story: As a customer whose flight the airline cancelled, I want the cancelled services marked and their value returned, so that I do not pay for a flight that will not operate.

Acceptance criteria:

ONE-704.1: When the airline cancels a flight and does not re-accommodate the customer, the system shall mark CANCELLED with delivery status UNABLE TO DELIVER every live service on that flight, in every order item, that the delivery status table lets become UNABLE TO DELIVER.
ONE-704.2: When the airline cancels a flight, the system shall leave every service on other flights unchanged.
ONE-704.3: When the airline cancels a flight, the system shall keep every order item with its reference and price.
ONE-704.4: If the airline cancels a flight of a paid order item and does not re-accommodate the customer, then the system shall refund the customer part of the item's price.
ONE-704.5: When the airline cancels a flight, the system shall mark CANCELLED every order item that holds a CANCELLED service.
ONE-704.6: When the airline cancels a flight and does not re-accommodate the customer, the system shall leave no live service on that flight.

A service is for one passenger on one flight segment, so the services that depend on a flight, such as a bag or a seat on it, are services on the same segment. How much is refunded is the reading's (FlightRefund). The delivery status table has no move to UNABLE TO DELIVER from REQUESTED, IN PROGRESS or SUSPENDED, so a service in one of those statuses keeps it (Delivery.endWith).

46.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-704.1	Proven	Cancel flight while requested, Cancel inbound flight, Services on a cancelled flight are cancelled, Cancel both flights
ONE-704.2	Proven	Other flights are unchanged, Cancel inbound flight
ONE-704.3	Proven	Cancel inbound flight, Order items keep their references and prices
ONE-704.4	Open	Cancel inbound flight, Refund for a cancelled flight, Cancel both flights
ONE-704.5	Open	Cancel inbound flight, Cancelled service in an active item, Cancel both flights
ONE-704.6	Open	Cancel flight while requested, No live service is left on a cancelled flight

46.2. Guarantees🔗

46.2.1. Services on a cancelled flight are cancelled🔗

guarantee

Rules.OneOrder.AirlineChange.cancel_flight_marks
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.AirlineChange.FlightRefund) (seg : String)
  (o : Rules.OneOrder.Order) (i : Rules.OneOrder.OrderItem)
  (hi : i ∈ o.items) (s : Rules.OneOrder.Service) (hs : s ∈ i.services)
  (hseg : s.segment = seg)
  (hlive : Rules.OneOrder.Delivery.isLive s = true)
  (hmove :
    (Rules.OneOrder.Delivery.nextDelivery m
          Rules.OneOrder.Delivery.DeliveryEvent.unable s).isSome =
      true) :
  ∃
    i' ∈
      (Rules.OneOrder.AirlineChange.cancelFlight m r seg o).order.items,
    i'.id = i.id ∧
      { id := s.id, passenger := s.passenger, segment := s.segment,
            status := Rules.OneOrder.ServiceStatus.cancelled,
            delivery :=
              Rules.OneOrder.DeliveryStatus.unableToDeliver } ∈
          i'.services ∧
        s ∉ i'.services
Rules.OneOrder.AirlineChange.cancel_flight_marks
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r :
    Rules.OneOrder.AirlineChange.FlightRefund)
  (seg : String)
  (o : Rules.OneOrder.Order)
  (i : Rules.OneOrder.OrderItem)
  (hi : i ∈ o.items)
  (s : Rules.OneOrder.Service)
  (hs : s ∈ i.services)
  (hseg : s.segment = seg)
  (hlive :
    Rules.OneOrder.Delivery.isLive s =
      true)
  (hmove :
    (Rules.OneOrder.Delivery.nextDelivery
          m
          Rules.OneOrder.Delivery.DeliveryEvent.unable
          s).isSome =
      true) :
  ∃
    i' ∈
      (Rules.OneOrder.AirlineChange.cancelFlight
            m r seg o).order.items,
    i'.id = i.id ∧
      { id := s.id,
            passenger := s.passenger,
            segment := s.segment,
            status :=
              Rules.OneOrder.ServiceStatus.cancelled,
            delivery :=
              Rules.OneOrder.DeliveryStatus.unableToDeliver } ∈
          i'.services ∧
        s ∉ i'.services

Every live service on the cancelled flight that the delivery status table lets become UNABLE TO DELIVER is replaced, in the same order item, by the same service marked CANCELLED with delivery status UNABLE TO DELIVER, under every reading of the sources.

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

Checks acceptance criteria ONE-704.1.

46.2.2. Other flights are unchanged🔗

guarantee

Rules.OneOrder.AirlineChange.cancel_flight_keeps_others
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.AirlineChange.FlightRefund) (seg : String)
  (o : Rules.OneOrder.Order) (i : Rules.OneOrder.OrderItem)
  (hi : i ∈ o.items) (s : Rules.OneOrder.Service) (hs : s ∈ i.services)
  (hseg : s.segment ≠ seg) :
  ∃
    i' ∈
      (Rules.OneOrder.AirlineChange.cancelFlight m r seg o).order.items,
    i'.id = i.id ∧ s ∈ i'.services
Rules.OneOrder.AirlineChange.cancel_flight_keeps_others
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r :
    Rules.OneOrder.AirlineChange.FlightRefund)
  (seg : String)
  (o : Rules.OneOrder.Order)
  (i : Rules.OneOrder.OrderItem)
  (hi : i ∈ o.items)
  (s : Rules.OneOrder.Service)
  (hs : s ∈ i.services)
  (hseg : s.segment ≠ seg) :
  ∃
    i' ∈
      (Rules.OneOrder.AirlineChange.cancelFlight
            m r seg o).order.items,
    i'.id = i.id ∧ s ∈ i'.services

Every service on another flight stays as it was, in the same order item.

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

Checks acceptance criteria ONE-704.2.

46.2.3. Order items keep their references and prices🔗

guarantee

Rules.OneOrder.AirlineChange.cancel_flight_keeps_items
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.AirlineChange.FlightRefund) (seg : String)
  (o : Rules.OneOrder.Order) :
  List.map (fun i ↦ (i.id, i.price))
      (Rules.OneOrder.AirlineChange.cancelFlight m r seg
            o).order.items =
    List.map (fun i ↦ (i.id, i.price)) o.items
Rules.OneOrder.AirlineChange.cancel_flight_keeps_items
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r :
    Rules.OneOrder.AirlineChange.FlightRefund)
  (seg : String)
  (o : Rules.OneOrder.Order) :
  List.map (fun i ↦ (i.id, i.price))
      (Rules.OneOrder.AirlineChange.cancelFlight
            m r seg o).order.items =
    List.map (fun i ↦ (i.id, i.price))
      o.items

The order keeps every order item, in the same order, with its reference and price.

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

Checks acceptance criteria ONE-704.3.

46.2.4. Refund for a cancelled flight🔗

guarantee

Rules.OneOrder.AirlineChange.cancel_flight_refunds
  (mr : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.AirlineChange.FlightRefund) (seg : String)
  (o : Rules.OneOrder.Order) (i : Rules.OneOrder.OrderItem)
  (hi : i ∈ o.items) (hprice : 0 < i.price.amount)
  (s : Rules.OneOrder.Service) (hs : s ∈ i.services)
  (hseg : s.segment = seg)
  (hpaid :
    s.status = Rules.OneOrder.ServiceStatus.confirmed ∧
      s.delivery = Rules.OneOrder.DeliveryStatus.readyToProceed) :
  ∃ m,
    (i.id, m) ∈
        (Rules.OneOrder.AirlineChange.cancelFlight mr r seg o).refunds ∧
      0 < m.amount
Rules.OneOrder.AirlineChange.cancel_flight_refunds
  (mr :
    Rules.OneOrder.Delivery.MoveReading)
  (r :
    Rules.OneOrder.AirlineChange.FlightRefund)
  (seg : String)
  (o : Rules.OneOrder.Order)
  (i : Rules.OneOrder.OrderItem)
  (hi : i ∈ o.items)
  (hprice : 0 < i.price.amount)
  (s : Rules.OneOrder.Service)
  (hs : s ∈ i.services)
  (hseg : s.segment = seg)
  (hpaid :
    s.status =
        Rules.OneOrder.ServiceStatus.confirmed ∧
      s.delivery =
        Rules.OneOrder.DeliveryStatus.readyToProceed) :
  ∃ m,
    (i.id, m) ∈
        (Rules.OneOrder.AirlineChange.cancelFlight
            mr r seg o).refunds ∧
      0 < m.amount

When the airline cancels a flight of a paid order item and does not re-accommodate the customer, the customer gets part of the item's price back.

Open question for the business. The flight cancellation worked example offers no follow-up action and no refund, and no source says whether a flight the airline cannot deliver entitles the customer to money back. Because the price is set per order item, no source says how much of it belongs to one flight either. Under the reading the worked example shows, a paid return trip at 1,000.00 EUR whose inbound flight is cancelled gets nothing back. The example cancelInboundFlight shows it. Is a refund owed when the airline cancels a flight without re-accommodation, and how much of an item's price belongs to that flight?

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

Checks acceptance criteria ONE-704.4.

46.2.5. Cancelled service in an active item🔗

guarantee

Rules.OneOrder.AirlineChange.cancel_flight_cancelled_items
  (m : Rules.OneOrder.Delivery.MoveReading)
  (v : Rules.OneOrder.ValueReading)
  (r : Rules.OneOrder.AirlineChange.FlightRefund) (seg : String)
  (o : Rules.OneOrder.Order)
  (hbefore :
    ∀ i ∈ o.items,
      (∃ s ∈ i.services,
          s.status = Rules.OneOrder.ServiceStatus.cancelled) →
        Rules.OneOrder.itemStatuses v i =
          [Rules.OneOrder.ItemStatus.cancelled])
  (i : Rules.OneOrder.OrderItem) :
  i ∈
      (Rules.OneOrder.AirlineChange.cancelFlight m r seg
            o).order.items →
    (∃ s ∈ i.services,
        s.status = Rules.OneOrder.ServiceStatus.cancelled) →
      Rules.OneOrder.itemStatuses v i =
        [Rules.OneOrder.ItemStatus.cancelled]
Rules.OneOrder.AirlineChange.cancel_flight_cancelled_items
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (v : Rules.OneOrder.ValueReading)
  (r :
    Rules.OneOrder.AirlineChange.FlightRefund)
  (seg : String)
  (o : Rules.OneOrder.Order)
  (hbefore :
    ∀ i ∈ o.items,
      (∃ s ∈ i.services,
          s.status =
            Rules.OneOrder.ServiceStatus.cancelled) →
        Rules.OneOrder.itemStatuses v i =
          [Rules.OneOrder.ItemStatus.cancelled])
  (i : Rules.OneOrder.OrderItem) :
  i ∈
      (Rules.OneOrder.AirlineChange.cancelFlight
            m r seg o).order.items →
    (∃ s ∈ i.services,
        s.status =
          Rules.OneOrder.ServiceStatus.cancelled) →
      Rules.OneOrder.itemStatuses v i =
        [Rules.OneOrder.ItemStatus.cancelled]

After the airline cancels a flight, every order item that holds a CANCELLED service is itself CANCELLED, provided this held before.

Open question for the business. The Order concept ties a CANCELLED service to a cancelled order item, and the cancellation page treats cancelling some services of an item as a change. The flight cancellation worked example cancels one flight's services and leaves the item as it was. A return trip whose inbound flight is cancelled keeps an active outbound flight, so the item stays ACTIVE with CANCELLED services in it, under every reading. The example cancelInboundFlight shows it. Should the airline replace the item, as a change does, or may an active item hold cancelled services?

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

Checks acceptance criteria ONE-704.5.

46.2.6. No live service is left on a cancelled flight🔗

guarantee

Rules.OneOrder.AirlineChange.cancel_flight_leaves_no_live
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.AirlineChange.FlightRefund) (seg : String)
  (o : Rules.OneOrder.Order) (i : Rules.OneOrder.OrderItem) :
  i ∈
      (Rules.OneOrder.AirlineChange.cancelFlight m r seg
            o).order.items →
    ∀ s ∈ i.services,
      s.segment = seg → Rules.OneOrder.Delivery.isLive s = false
Rules.OneOrder.AirlineChange.cancel_flight_leaves_no_live
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r :
    Rules.OneOrder.AirlineChange.FlightRefund)
  (seg : String)
  (o : Rules.OneOrder.Order)
  (i : Rules.OneOrder.OrderItem) :
  i ∈
      (Rules.OneOrder.AirlineChange.cancelFlight
            m r seg o).order.items →
    ∀ s ∈ i.services,
      s.segment = seg →
        Rules.OneOrder.Delivery.isLive s =
          false

When the airline cancels a flight and does not re-accommodate the customer, no live service is left on that flight.

Open question for the business. The flight's services are ended through the delivery status table, and the table has no move to UNABLE TO DELIVER from REQUESTED, IN PROGRESS or SUSPENDED, under any reading. A service the airline has not yet confirmed therefore stays live on a flight that will not operate. The example cancelFlightWhileRequested shows it. What delivery status does a requested, in-progress or suspended service take when its flight is cancelled?

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

Checks acceptance criteria ONE-704.6.

46.3. Examples🔗

46.3.1. Cancel flight while requested🔗

example

Rules.OneOrder.AirlineChange.cancelFlightWhileRequested :
  Rules.OneOrder.AirlineChange.FlightCancelled
Rules.OneOrder.AirlineChange.cancelFlightWhileRequested :
  Rules.OneOrder.AirlineChange.FlightCancelled

Given the paid return trip at 1,000.00 EUR, with its bag on the inbound flight still REQUESTED from the airline.

When the airline cancels the inbound flight and does not move the customer to another one.

Then the inbound flight is CANCELLED with delivery status UNABLE TO DELIVER. The bag stays REQUESTED, and live, on a flight that will not operate, because the delivery status table has no move from REQUESTED to UNABLE TO DELIVER.

What Lean computed:

Item: ORDITM-1
Price: 1000.00 EUR
Services: see the table below.
Cautious: active
Strict: active
Refund as shown: 0.00 EUR
Refund by flight: 500.00 EUR

Services:

Service	Segment	Status	Delivery
SVC-OUT	SEG-OUT	confirmed	ready to proceed
SVC-IN	SEG-IN	cancelled	unable to deliver
BAG-IN	SEG-IN	requested	requested

Checks acceptance criteria ONE-704.1, ONE-704.6, ONE-105.2.

46.3.2. Cancel both flights🔗

example

Rules.OneOrder.AirlineChange.cancelBothFlights :
  Rules.OneOrder.AirlineChange.FlightCancelled
Rules.OneOrder.AirlineChange.cancelBothFlights :
  Rules.OneOrder.AirlineChange.FlightCancelled

Given the same paid return trip at 1,000.00 EUR.

When the airline cancels the inbound flight and then the outbound flight, and moves the customer to neither.

Then every service is CANCELLED with delivery status UNABLE TO DELIVER. Under the strict reading the item is CANCELLED; under the cautious reading, where UNABLE TO DELIVER holds value, it stays ACTIVE with only CANCELLED services. Under the reading the worked example shows, nothing is refunded for a trip that will not operate.

What Lean computed:

Item: ORDITM-1
Price: 1000.00 EUR
Services: see the table below.
Cautious: active
Strict: cancelled
Refund as shown: 0.00 EUR
Refund by flight: 1000.00 EUR

Services:

Service	Segment	Status	Delivery
SVC-OUT	SEG-OUT	cancelled	unable to deliver
SVC-IN	SEG-IN	cancelled	unable to deliver
BAG-IN	SEG-IN	cancelled	unable to deliver

Checks acceptance criteria ONE-704.1, ONE-704.4, ONE-704.5.

46.3.3. Cancel inbound flight🔗

example

Rules.OneOrder.AirlineChange.cancelInboundFlight :
  Rules.OneOrder.AirlineChange.FlightCancelled
Rules.OneOrder.AirlineChange.cancelInboundFlight :
  Rules.OneOrder.AirlineChange.FlightCancelled

Given a paid return trip at 1,000.00 EUR in one order item: the outbound flight, the inbound flight and a bag on the inbound flight.

When the airline cancels the inbound flight and does not move the customer to another one.

Then the inbound flight and its bag are CANCELLED with delivery status UNABLE TO DELIVER, and the outbound flight is as it was. The item keeps its reference and price and stays ACTIVE under both readings, with CANCELLED services in it. Under the reading the worked example shows, nothing is refunded; a reading that refunds an equal share per flight returns 500.00 EUR.

What Lean computed:

Item: ORDITM-1
Price: 1000.00 EUR
Services: see the table below.
Cautious: active
Strict: active
Refund as shown: 0.00 EUR
Refund by flight: 500.00 EUR

Services:

Service	Segment	Status	Delivery
SVC-OUT	SEG-OUT	confirmed	ready to proceed
SVC-IN	SEG-IN	cancelled	unable to deliver
BAG-IN	SEG-IN	cancelled	unable to deliver

Checks acceptance criteria ONE-704.1, ONE-704.2, ONE-704.3, ONE-704.4, ONE-704.5.

46.4. Open question🔗

The guarantee Refund for a cancelled flight is open: the example Cancel both flights, Cancel inbound flight shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

46.5. Open question🔗

The guarantee Cancelled service in an active item is open: the example Cancel both flights, Cancel inbound flight shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

46.6. Open question🔗

The guarantee No live service is left on a cancelled flight is open: the example Cancel flight while requested shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.