38. Cancelling a flight with ancillaries🔗

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

rule

Rules.OneOrder.Ancillaries.cancelItems
  (m : Rules.OneOrder.Delivery.MoveReading)
  (h : Rules.OneOrder.Ancillaries.DependentHandling)
  (r : Rules.OneOrder.Ancillaries.LinkReading)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (allows : String → Bool) (o : Rules.OneOrder.Order)
  (named : List String) :
  Except Rules.OneOrder.Ancillaries.CancelRejection Rules.OneOrder.Order
Rules.OneOrder.Ancillaries.cancelItems
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (h :
    Rules.OneOrder.Ancillaries.DependentHandling)
  (r :
    Rules.OneOrder.Ancillaries.LinkReading)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (allows : String → Bool)
  (o : Rules.OneOrder.Order)
  (named : List String) :
  Except
    Rules.OneOrder.Ancillaries.CancelRejection
    Rules.OneOrder.Order

EARS: When a seller cancels order items, the system shall cancel every live service of the items named and treat the services that depend on a cancelled flight as the reading says.

Story: As a seller, I want to know what happens to a customer's bag and seat when I cancel their flight, so that the customer neither keeps a service they cannot use nor loses one they were promised.

Acceptance criteria:

ONE-603.1: When a seller cancels order items, the system shall mark every live service of each named item that the delivery status table lets be removed CANCELLED with delivery status REMOVED.
ONE-603.2: If a seller names an order item whose conditions do not allow cancellation, then the system shall refuse the request.
ONE-603.3: When a seller cancels order items, the system shall leave as it was every service outside the named items that does not depend on a cancelled flight.
ONE-603.4: When a seller cancels a flight, the system shall leave no live service that depends on it.
ONE-603.5: The system shall never cancel a live service of an order item whose conditions do not allow cancellation.
ONE-603.6: When the conditions of an order item allow cancellation, the system shall let the seller cancel it.

What happens to the dependents is the reading's (DependentHandling); which services depend on a flight is the link's (LinkReading). The refund is not modelled; whose conditions govern the refund of a dependent cancelled with its flight is an open point. The conditions of each order item are given by item reference. A service is removed through the delivery status table (Delivery.endWith), so one still REQUESTED from the airline stays as it was.

38.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-603.1	Proven	Cancel flight with bag, Named items are cancelled
ONE-603.2	Proven	Refuse until named blocks, Items that may not be cancelled are refused
ONE-603.3	Proven	Other services are kept, Cancel flight with bag
ONE-603.4	Open	Cancel flight with bag, No live dependent of a cancelled flight
ONE-603.5	Open	Dependents keep their own conditions, Cancel flight with bag
ONE-603.6	Open	Refuse until named blocks, A cancellable item can be cancelled

38.2. Guarantees🔗

38.2.1. Named items are cancelled🔗

guarantee

Rules.OneOrder.Ancillaries.cancel_items_named
  (m : Rules.OneOrder.Delivery.MoveReading)
  (h : Rules.OneOrder.Ancillaries.DependentHandling)
  (r : Rules.OneOrder.Ancillaries.LinkReading)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (allows : String → Bool) (o o' : Rules.OneOrder.Order)
  (named : List String)
  (hok :
    Rules.OneOrder.Ancillaries.cancelItems m h r d allows o named =
      Except.ok o')
  (i : Rules.OneOrder.OrderItem) (hi : i ∈ o.items)
  (hn : i.id ∈ named) :
  ∃ i' ∈ o'.items,
    i'.id = i.id ∧
      ∀ s ∈ i.services,
        Rules.OneOrder.Delivery.isLive s = true →
          (Rules.OneOrder.Delivery.nextDelivery m
                  Rules.OneOrder.Delivery.DeliveryEvent.remove
                  s).isSome =
              true →
            { id := s.id, passenger := s.passenger,
                segment := s.segment,
                status := Rules.OneOrder.ServiceStatus.cancelled,
                delivery := Rules.OneOrder.DeliveryStatus.removed } ∈
              i'.services
Rules.OneOrder.Ancillaries.cancel_items_named
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (h :
    Rules.OneOrder.Ancillaries.DependentHandling)
  (r :
    Rules.OneOrder.Ancillaries.LinkReading)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (allows : String → Bool)
  (o o' : Rules.OneOrder.Order)
  (named : List String)
  (hok :
    Rules.OneOrder.Ancillaries.cancelItems
        m h r d allows o named =
      Except.ok o')
  (i : Rules.OneOrder.OrderItem)
  (hi : i ∈ o.items) (hn : i.id ∈ named) :
  ∃ i' ∈ o'.items,
    i'.id = i.id ∧
      ∀ s ∈ i.services,
        Rules.OneOrder.Delivery.isLive s =
            true →
          (Rules.OneOrder.Delivery.nextDelivery
                  m
                  Rules.OneOrder.Delivery.DeliveryEvent.remove
                  s).isSome =
              true →
            { id := s.id,
                passenger := s.passenger,
                segment := s.segment,
                status :=
                  Rules.OneOrder.ServiceStatus.cancelled,
                delivery :=
                  Rules.OneOrder.DeliveryStatus.removed } ∈
              i'.services

Every named item is in the order afterwards with each live service that the delivery status table lets be removed CANCELLED with delivery status REMOVED, under every reading.

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

Checks acceptance criteria ONE-603.1.

38.2.2. Items that may not be cancelled are refused🔗

guarantee

Rules.OneOrder.Ancillaries.cancel_items_refuses_not_cancellable
  (m : Rules.OneOrder.Delivery.MoveReading)
  (h : Rules.OneOrder.Ancillaries.DependentHandling)
  (r : Rules.OneOrder.Ancillaries.LinkReading)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (allows : String → Bool) (o : Rules.OneOrder.Order)
  (named : List String) (id : String) (hn : id ∈ named)
  (hno : allows id = false) (o' : Rules.OneOrder.Order) :
  Rules.OneOrder.Ancillaries.cancelItems m h r d allows o named ≠
    Except.ok o'
Rules.OneOrder.Ancillaries.cancel_items_refuses_not_cancellable
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (h :
    Rules.OneOrder.Ancillaries.DependentHandling)
  (r :
    Rules.OneOrder.Ancillaries.LinkReading)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (allows : String → Bool)
  (o : Rules.OneOrder.Order)
  (named : List String) (id : String)
  (hn : id ∈ named)
  (hno : allows id = false)
  (o' : Rules.OneOrder.Order) :
  Rules.OneOrder.Ancillaries.cancelItems m
      h r d allows o named ≠
    Except.ok o'

A request that names an item whose conditions do not allow cancellation is refused, under every reading.

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

Checks acceptance criteria ONE-603.2.

38.2.3. Other services are kept🔗

guarantee

Rules.OneOrder.Ancillaries.cancel_items_keeps_others
  (m : Rules.OneOrder.Delivery.MoveReading)
  (h : Rules.OneOrder.Ancillaries.DependentHandling)
  (r : Rules.OneOrder.Ancillaries.LinkReading)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (allows : String → Bool) (o o' : Rules.OneOrder.Order)
  (named : List String)
  (hok :
    Rules.OneOrder.Ancillaries.cancelItems m h r d allows o named =
      Except.ok o')
  (i : Rules.OneOrder.OrderItem) (hi : i ∈ o.items) (hn : i.id ∉ named)
  (s : Rules.OneOrder.Service) (hs : s ∈ i.services)
  (hdep :
    Rules.OneOrder.Ancillaries.isLiveDependent r d
        (Rules.OneOrder.Ancillaries.namedFlights d o named) s =
      false) :
  ∃ i' ∈ o'.items, i'.id = i.id ∧ s ∈ i'.services
Rules.OneOrder.Ancillaries.cancel_items_keeps_others
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (h :
    Rules.OneOrder.Ancillaries.DependentHandling)
  (r :
    Rules.OneOrder.Ancillaries.LinkReading)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (allows : String → Bool)
  (o o' : Rules.OneOrder.Order)
  (named : List String)
  (hok :
    Rules.OneOrder.Ancillaries.cancelItems
        m h r d allows o named =
      Except.ok o')
  (i : Rules.OneOrder.OrderItem)
  (hi : i ∈ o.items) (hn : i.id ∉ named)
  (s : Rules.OneOrder.Service)
  (hs : s ∈ i.services)
  (hdep :
    Rules.OneOrder.Ancillaries.isLiveDependent
        r d
        (Rules.OneOrder.Ancillaries.namedFlights
          d o named)
        s =
      false) :
  ∃ i' ∈ o'.items,
    i'.id = i.id ∧ s ∈ i'.services

Every service outside the named items that is not a live dependent of a cancelled flight is in the order afterwards, in the same item, under every reading.

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

Checks acceptance criteria ONE-603.3.

38.2.4. No live dependent of a cancelled flight🔗

guarantee

Rules.OneOrder.Ancillaries.cancel_items_no_live_dependents
  (m : Rules.OneOrder.Delivery.MoveReading)
  (h : Rules.OneOrder.Ancillaries.DependentHandling)
  (r : Rules.OneOrder.Ancillaries.LinkReading)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (allows : String → Bool) (o o' : Rules.OneOrder.Order)
  (named : List String)
  (hok :
    Rules.OneOrder.Ancillaries.cancelItems m h r d allows o named =
      Except.ok o')
  (f : Rules.OneOrder.Service)
  (hf : f ∈ Rules.OneOrder.Ancillaries.namedFlights d o named)
  (s : Rules.OneOrder.Service)
  (hs : s ∈ Rules.OneOrder.Ancillaries.services o')
  (hdep : Rules.OneOrder.Ancillaries.dependsOn r d f s = true) :
  Rules.OneOrder.Delivery.isLive s = false
Rules.OneOrder.Ancillaries.cancel_items_no_live_dependents
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (h :
    Rules.OneOrder.Ancillaries.DependentHandling)
  (r :
    Rules.OneOrder.Ancillaries.LinkReading)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (allows : String → Bool)
  (o o' : Rules.OneOrder.Order)
  (named : List String)
  (hok :
    Rules.OneOrder.Ancillaries.cancelItems
        m h r d allows o named =
      Except.ok o')
  (f : Rules.OneOrder.Service)
  (hf :
    f ∈
      Rules.OneOrder.Ancillaries.namedFlights
        d o named)
  (s : Rules.OneOrder.Service)
  (hs :
    s ∈
      Rules.OneOrder.Ancillaries.services
        o')
  (hdep :
    Rules.OneOrder.Ancillaries.dependsOn r
        d f s =
      true) :
  Rules.OneOrder.Delivery.isLive s = false

After a seller cancels a flight, no live service depends on it.

Open question for the business. Under the reading where the dependents stay as they are, a cancelled flight leaves its bag confirmed on a segment the passenger no longer flies. The example cancelFlightWithBag shows it. The other two readings keep the guarantee when every live service of the order can be removed (cancel_items_no_live_dependents_of_not_leave). A bag still REQUESTED from the airline cannot be: the delivery status table has no move from REQUESTED to REMOVED, so it stays live under every reading. Should cancelling a flight cancel its bag and seat, refuse until the seller names them, or leave them in place, and what happens to one the airline has not yet confirmed?

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

Checks acceptance criteria ONE-603.4.

38.2.5. Dependents keep their own conditions🔗

guarantee

Rules.OneOrder.Ancillaries.cancel_items_respects_conditions
  (m : Rules.OneOrder.Delivery.MoveReading)
  (h : Rules.OneOrder.Ancillaries.DependentHandling)
  (r : Rules.OneOrder.Ancillaries.LinkReading)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (allows : String → Bool) (o o' : Rules.OneOrder.Order)
  (named : List String)
  (hok :
    Rules.OneOrder.Ancillaries.cancelItems m h r d allows o named =
      Except.ok o')
  (i : Rules.OneOrder.OrderItem) (hi : i ∈ o.items)
  (hno : allows i.id = false) (s : Rules.OneOrder.Service)
  (hs : s ∈ i.services) :
  ∃ i' ∈ o'.items, i'.id = i.id ∧ s ∈ i'.services
Rules.OneOrder.Ancillaries.cancel_items_respects_conditions
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (h :
    Rules.OneOrder.Ancillaries.DependentHandling)
  (r :
    Rules.OneOrder.Ancillaries.LinkReading)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (allows : String → Bool)
  (o o' : Rules.OneOrder.Order)
  (named : List String)
  (hok :
    Rules.OneOrder.Ancillaries.cancelItems
        m h r d allows o named =
      Except.ok o')
  (i : Rules.OneOrder.OrderItem)
  (hi : i ∈ o.items)
  (hno : allows i.id = false)
  (s : Rules.OneOrder.Service)
  (hs : s ∈ i.services) :
  ∃ i' ∈ o'.items,
    i'.id = i.id ∧ s ∈ i'.services

A live service of an item whose conditions do not allow cancellation is in the order afterwards as it was.

Open question for the business. Under the reading where dependents are cancelled with their flight, cancelling a flight cancels the extra bag bought for it, although the bag's conditions do not allow cancellation, as in the add bag worked example. The example cancelFlightWithBag shows it. The other two readings keep the guarantee (cancel_items_respects_conditions_of_not_cancel_with). Whose conditions govern a dependent cancelled with its flight, and its refund: the dependent's own or the flight's?

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

Checks acceptance criteria ONE-603.5.

38.2.6. A cancellable item can be cancelled🔗

guarantee

Rules.OneOrder.Ancillaries.cancel_items_allowed
  (m : Rules.OneOrder.Delivery.MoveReading)
  (h : Rules.OneOrder.Ancillaries.DependentHandling)
  (r : Rules.OneOrder.Ancillaries.LinkReading)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (allows : String → Bool) (o : Rules.OneOrder.Order)
  (i : Rules.OneOrder.OrderItem) (hi : i ∈ o.items)
  (ha : allows i.id = true) :
  ∃ named,
    i.id ∈ named ∧
      ∃ o',
        Rules.OneOrder.Ancillaries.cancelItems m h r d allows o named =
          Except.ok o'
Rules.OneOrder.Ancillaries.cancel_items_allowed
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (h :
    Rules.OneOrder.Ancillaries.DependentHandling)
  (r :
    Rules.OneOrder.Ancillaries.LinkReading)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (allows : String → Bool)
  (o : Rules.OneOrder.Order)
  (i : Rules.OneOrder.OrderItem)
  (hi : i ∈ o.items)
  (ha : allows i.id = true) :
  ∃ named,
    i.id ∈ named ∧
      ∃ o',
        Rules.OneOrder.Ancillaries.cancelItems
            m h r d allows o named =
          Except.ok o'

An order item whose conditions allow cancellation can be cancelled by some request that names it.

Open question for the business. Under the reading where a cancellation is refused until the seller names the dependents too, a flight whose extra bag may not be cancelled can never be cancelled: naming the flight alone is refused for the bag, and naming the bag too is refused by the bag's conditions. The example refuseUntilNamedBlocks shows it. The other two readings keep the guarantee (cancel_items_allowed_of_not_refuse). Should a dependent's conditions be able to stop its flight from being cancelled?

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

Checks acceptance criteria ONE-603.6.

38.3. Examples🔗

38.3.1. Cancel flight with bag🔗

example

Rules.OneOrder.Ancillaries.cancelFlightWithBag :
  List Rules.OneOrder.Ancillaries.CancelCase
Rules.OneOrder.Ancillaries.cancelFlightWithBag :
  List
    Rules.OneOrder.Ancillaries.CancelCase

Given the add bag worked example: a flight for PAX-1 on SEG-OUT, and an extra bag on the same flight in its own item, whose conditions do not allow cancellation.

When the seller cancels the flight item alone, under each reading of what happens to its dependents.

Then where dependents are cancelled with the flight, the bag is cancelled against its own conditions. Where the seller must name them too, the request is refused. Where they stay in place, the flight is cancelled and the bag stays confirmed on a flight the passenger no longer holds.

What Lean computed:

Reading	Named	Refusal	Flight	Bag
cancel with the flight	ITM-FLT	none	cancelled	cancelled
refuse until named	ITM-FLT	dependent not named XBAG-OUT	confirmed	confirmed
leave in place	ITM-FLT	none	cancelled	confirmed

Checks acceptance criteria ONE-603.1, ONE-603.3, ONE-603.4, ONE-603.5.

38.3.2. Refuse until named blocks🔗

example

Rules.OneOrder.Ancillaries.refuseUntilNamedBlocks :
  List Rules.OneOrder.Ancillaries.CancelCase
Rules.OneOrder.Ancillaries.refuseUntilNamedBlocks :
  List
    Rules.OneOrder.Ancillaries.CancelCase

Given the same order: a flight, and an extra bag whose conditions do not allow cancellation.

When the seller, under the reading where a cancellation is refused until the dependents are named, cancels the flight alone, and then the flight and the bag together.

Then both requests are refused: the first because the bag is not named, the second because the bag's conditions do not allow cancellation. The flight cannot be cancelled at all.

What Lean computed:

Reading	Named	Refusal	Flight	Bag
refuse until named	ITM-FLT	dependent not named XBAG-OUT	confirmed	confirmed
refuse until named	ITM-FLT, ITM-XBAG	not cancellable ITM-XBAG	confirmed	confirmed

Checks acceptance criteria ONE-603.2, ONE-603.6.

38.4. Open question🔗

The guarantee No live dependent of a cancelled flight is open: the example Cancel flight with bag shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

38.5. Open question🔗

The guarantee Dependents keep their own conditions is open: the example Cancel flight with bag shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

38.6. Open question🔗

The guarantee A cancellable item can be cancelled is open: the example Refuse until named blocks shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.