47. Re-accommodation before the seller answers🔗

Requirement ONE-705. Of its 5 acceptance criteria, 3 are proven and 2 are open.

rule

Rules.OneOrder.AirlineChange.notifyChange
  (m : Rules.OneOrder.Delivery.MoveReading)
  (a : Rules.OneOrder.AirlineChange.ApplyAt)
  (vo : Rules.OneOrder.AirlineChange.VersionedOrder)
  (c : Rules.OneOrder.AirlineChange.Reaccommodation) :
  Except Rules.OneOrder.Change.ChangeRejection
    Rules.OneOrder.AirlineChange.VersionedOrder
Rules.OneOrder.AirlineChange.notifyChange
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (a :
    Rules.OneOrder.AirlineChange.ApplyAt)
  (vo :
    Rules.OneOrder.AirlineChange.VersionedOrder)
  (c :
    Rules.OneOrder.AirlineChange.Reaccommodation) :
  Except
    Rules.OneOrder.Change.ChangeRejection
    Rules.OneOrder.AirlineChange.VersionedOrder

EARS: When the airline moves a customer to other flights, the system shall replace the affected order item with a new item at the same price, holding a service for each passenger on each new flight.

Story: As a customer whose flights the airline changed, I want the new flights in my order at no extra cost and the old ones kept until I accept, so that I can still choose what to do.

Acceptance criteria:

ONE-705.1: Where an airline change takes effect when it is notified, the system shall replace the changed order item as a paid change does and raise the order version by one.
ONE-705.2: Where an airline change waits for the seller's Accept, the system shall leave the order and its version unchanged when the change is notified.
ONE-705.3: When an airline change takes effect, the system shall give the new order item the original item's price and a service for each passenger of the original item on each new flight.
ONE-705.4: While the seller's Accept of an airline change is pending, the system shall keep the original order item with the status it had.
ONE-705.5: When the airline replaces paid services at no price difference, the system shall mark every service of the new order item READY TO PROCEED.

The replacement is the change rule for a paid change (changeItem): kept services move to the new item, their originals are marked transferred, and the other services of the original item are cancelled and removed, through the delivery status table. When the change takes effect is the reading's (ApplyAt); under the reading where it waits for acceptance, applying it once the seller accepts is the same replacement, which this rule does not model.

47.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-705.1	Proven	Change applied before seller response, Itinerary reaccommodated
ONE-705.2	Proven	Itinerary reaccommodated, A change awaiting Accept leaves the order as it was
ONE-705.3	Proven	Itinerary reaccommodated, New flights for every passenger at the same price
ONE-705.4	Open	Original item kept while Accept is pending, Itinerary reaccommodated
ONE-705.5	Open	Paid status after re-accommodation, Itinerary reaccommodated

47.2. Guarantees🔗

47.2.1. Change applied before seller response🔗

guarantee

Rules.OneOrder.AirlineChange.notify_at_notice
  (m : Rules.OneOrder.Delivery.MoveReading)
  (vo : Rules.OneOrder.AirlineChange.VersionedOrder)
  (c : Rules.OneOrder.AirlineChange.Reaccommodation)
  (vo' : Rules.OneOrder.AirlineChange.VersionedOrder)
  (h :
    Rules.OneOrder.AirlineChange.notifyChange m
        Rules.OneOrder.AirlineChange.ApplyAt.notice vo c =
      Except.ok vo') :
  ∃ old,
    List.find? (fun x ↦ decide (x.id = c.item)) vo.order.items =
        some old ∧
      Rules.OneOrder.Change.changeItem m vo.order (c.toItemChange old) =
          Except.ok vo'.order ∧
        vo'.version = vo.version + 1
Rules.OneOrder.AirlineChange.notify_at_notice
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (vo :
    Rules.OneOrder.AirlineChange.VersionedOrder)
  (c :
    Rules.OneOrder.AirlineChange.Reaccommodation)
  (vo' :
    Rules.OneOrder.AirlineChange.VersionedOrder)
  (h :
    Rules.OneOrder.AirlineChange.notifyChange
        m
        Rules.OneOrder.AirlineChange.ApplyAt.notice
        vo c =
      Except.ok vo') :
  ∃ old,
    List.find?
          (fun x ↦ decide (x.id = c.item))
          vo.order.items =
        some old ∧
      Rules.OneOrder.Change.changeItem m
            vo.order
            (c.toItemChange old) =
          Except.ok vo'.order ∧
        vo'.version = vo.version + 1

Where the change takes effect at notice, the order is the order after the change rule for a paid change, one version higher.

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

Checks acceptance criteria ONE-705.1.

47.2.2. A change awaiting Accept leaves the order as it was🔗

guarantee

Rules.OneOrder.AirlineChange.notify_at_acceptance
  (m : Rules.OneOrder.Delivery.MoveReading)
  (vo : Rules.OneOrder.AirlineChange.VersionedOrder)
  (c : Rules.OneOrder.AirlineChange.Reaccommodation)
  (vo' : Rules.OneOrder.AirlineChange.VersionedOrder)
  (h :
    Rules.OneOrder.AirlineChange.notifyChange m
        Rules.OneOrder.AirlineChange.ApplyAt.acceptance vo c =
      Except.ok vo') :
  vo' = vo
Rules.OneOrder.AirlineChange.notify_at_acceptance
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (vo :
    Rules.OneOrder.AirlineChange.VersionedOrder)
  (c :
    Rules.OneOrder.AirlineChange.Reaccommodation)
  (vo' :
    Rules.OneOrder.AirlineChange.VersionedOrder)
  (h :
    Rules.OneOrder.AirlineChange.notifyChange
        m
        Rules.OneOrder.AirlineChange.ApplyAt.acceptance
        vo c =
      Except.ok vo') :
  vo' = vo

Where the change waits for the seller's Accept, the order and its version are as they were at notice.

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

Checks acceptance criteria ONE-705.2.

47.2.3. New flights for every passenger at the same price🔗

guarantee

Rules.OneOrder.AirlineChange.notify_new_item
  (m : Rules.OneOrder.Delivery.MoveReading)
  (vo : Rules.OneOrder.AirlineChange.VersionedOrder)
  (c : Rules.OneOrder.AirlineChange.Reaccommodation)
  (vo' : Rules.OneOrder.AirlineChange.VersionedOrder)
  (h :
    Rules.OneOrder.AirlineChange.notifyChange m
        Rules.OneOrder.AirlineChange.ApplyAt.notice vo c =
      Except.ok vo') :
  ∃ old ∈ vo.order.items,
    old.id = c.item ∧
      ∃ ni ∈ vo'.order.items,
        ni.id = c.newItem ∧
          ni.price = old.price ∧
            ∀ p ∈ Rules.OneOrder.AirlineChange.passengersOf old,
              ∀ seg ∈ c.newSegments,
                ∃ s ∈ ni.services, s.passenger = p ∧ s.segment = seg
Rules.OneOrder.AirlineChange.notify_new_item
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (vo :
    Rules.OneOrder.AirlineChange.VersionedOrder)
  (c :
    Rules.OneOrder.AirlineChange.Reaccommodation)
  (vo' :
    Rules.OneOrder.AirlineChange.VersionedOrder)
  (h :
    Rules.OneOrder.AirlineChange.notifyChange
        m
        Rules.OneOrder.AirlineChange.ApplyAt.notice
        vo c =
      Except.ok vo') :
  ∃ old ∈ vo.order.items,
    old.id = c.item ∧
      ∃ ni ∈ vo'.order.items,
        ni.id = c.newItem ∧
          ni.price = old.price ∧
            ∀
              p ∈
                Rules.OneOrder.AirlineChange.passengersOf
                  old,
              ∀ seg ∈ c.newSegments,
                ∃ s ∈ ni.services,
                  s.passenger = p ∧
                    s.segment = seg

When the change takes effect, the new order item has the original item's price and a service for each passenger of the original item on each new flight.

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

Checks acceptance criteria ONE-705.3.

47.2.4. Original item kept while Accept is pending🔗

guarantee

Rules.OneOrder.AirlineChange.accept_pending_keeps_original
  (m : Rules.OneOrder.Delivery.MoveReading)
  (v : Rules.OneOrder.ValueReading)
  (a : Rules.OneOrder.AirlineChange.ApplyAt)
  (vo : Rules.OneOrder.AirlineChange.VersionedOrder)
  (c : Rules.OneOrder.AirlineChange.Reaccommodation)
  (vo' : Rules.OneOrder.AirlineChange.VersionedOrder)
  (h :
    Rules.OneOrder.AirlineChange.notifyChange m a vo c = Except.ok vo')
  (i : Rules.OneOrder.OrderItem) (hi : i ∈ vo.order.items)
  (hid : i.id = c.item) :
  ∃ i' ∈ vo'.order.items,
    i'.id = c.item ∧
      Rules.OneOrder.itemStatuses v i' = Rules.OneOrder.itemStatuses v i
Rules.OneOrder.AirlineChange.accept_pending_keeps_original
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (v : Rules.OneOrder.ValueReading)
  (a :
    Rules.OneOrder.AirlineChange.ApplyAt)
  (vo :
    Rules.OneOrder.AirlineChange.VersionedOrder)
  (c :
    Rules.OneOrder.AirlineChange.Reaccommodation)
  (vo' :
    Rules.OneOrder.AirlineChange.VersionedOrder)
  (h :
    Rules.OneOrder.AirlineChange.notifyChange
        m a vo c =
      Except.ok vo')
  (i : Rules.OneOrder.OrderItem)
  (hi : i ∈ vo.order.items)
  (hid : i.id = c.item) :
  ∃ i' ∈ vo'.order.items,
    i'.id = c.item ∧
      Rules.OneOrder.itemStatuses v i' =
        Rules.OneOrder.itemStatuses v i

While the seller's Accept of an airline change is pending, the original order item keeps the status it had.

Open question for the business. In the itinerary change worked example the change is already in the order while Accept is pending: the original item is CANCELLED at the next version. A customer who would rather keep the original flights cannot get them back, so Accept offers no real choice. The example itineraryReaccommodated shows it under the reading that applies the change at notice. Is a change awaiting acceptance provisional, and does declining it restore the original item or only let the customer cancel or reshop from the changed order?

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

Checks acceptance criteria ONE-705.4.

47.2.5. Paid status after re-accommodation🔗

guarantee

Rules.OneOrder.AirlineChange.reaccommodated_paid
  (m : Rules.OneOrder.Delivery.MoveReading)
  (a : Rules.OneOrder.AirlineChange.ApplyAt)
  (vo : Rules.OneOrder.AirlineChange.VersionedOrder)
  (c : Rules.OneOrder.AirlineChange.Reaccommodation)
  (vo' : Rules.OneOrder.AirlineChange.VersionedOrder)
  (h :
    Rules.OneOrder.AirlineChange.notifyChange m a vo c = Except.ok vo')
  (old : Rules.OneOrder.OrderItem)
  (hold :
    List.find? (fun x ↦ decide (x.id = c.item)) vo.order.items =
      some old)
  (hpaid :
    ∀ s ∈ old.services,
      s.delivery = Rules.OneOrder.DeliveryStatus.readyToProceed)
  (hfresh : ∀ i ∈ vo.order.items, i.id ≠ c.newItem)
  (ni : Rules.OneOrder.OrderItem) :
  ni ∈ vo'.order.items →
    ni.id = c.newItem →
      ∀ s ∈ ni.services,
        s.delivery = Rules.OneOrder.DeliveryStatus.readyToProceed
Rules.OneOrder.AirlineChange.reaccommodated_paid
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (a :
    Rules.OneOrder.AirlineChange.ApplyAt)
  (vo :
    Rules.OneOrder.AirlineChange.VersionedOrder)
  (c :
    Rules.OneOrder.AirlineChange.Reaccommodation)
  (vo' :
    Rules.OneOrder.AirlineChange.VersionedOrder)
  (h :
    Rules.OneOrder.AirlineChange.notifyChange
        m a vo c =
      Except.ok vo')
  (old : Rules.OneOrder.OrderItem)
  (hold :
    List.find?
        (fun x ↦ decide (x.id = c.item))
        vo.order.items =
      some old)
  (hpaid :
    ∀ s ∈ old.services,
      s.delivery =
        Rules.OneOrder.DeliveryStatus.readyToProceed)
  (hfresh :
    ∀ i ∈ vo.order.items,
      i.id ≠ c.newItem)
  (ni : Rules.OneOrder.OrderItem) :
  ni ∈ vo'.order.items →
    ni.id = c.newItem →
      ∀ s ∈ ni.services,
        s.delivery =
          Rules.OneOrder.DeliveryStatus.readyToProceed

When the airline replaces paid services at no price difference, every service of the new order item is READY TO PROCEED.

Open question for the business. In the itinerary change worked example the services the airline creates start CONFIRMED, a status the Order concept reserves for services still awaiting payment, although the customer paid in full and the exchange is even. If CONFIRMED is read as unpaid, a payment time limit could apply to a trip the customer already paid for. The example itineraryReaccommodated shows the new services CONFIRMED. Does the paid status carry across an airline change?

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

Checks acceptance criteria ONE-705.5.

47.3. Examples🔗

47.3.1. Itinerary reaccommodated🔗

example

Rules.OneOrder.AirlineChange.itineraryReaccommodated :
  List Rules.OneOrder.AirlineChange.Reaccommodated
Rules.OneOrder.AirlineChange.itineraryReaccommodated :
  List
    Rules.OneOrder.AirlineChange.Reaccommodated

Given a paid return trip at 1,000.00 EUR, ready to proceed, at order version 1.

When the airline moves both flights to other flights at no price difference and notifies the seller with Accept pending, under each reading of when the change takes effect.

Then where it takes effect at notice, as in the itinerary change worked example, the order is at version 2, the original item is CANCELLED while Accept is pending, and the new item at 1,000.00 EUR holds the new flights with delivery status CONFIRMED, although the customer paid in full. Where it waits for Accept, the order is as it was.

What Lean computed:

Reading	Version	Original	New item	New price	New flights	New delivery
in effect at notice	2	cancelled	active	1000.00 EUR	SEG-OUT-2, SEG-IN-2	confirmed, confirmed
waits for Accept	1	active	none	none	none	none

Checks acceptance criteria ONE-705.1, ONE-705.2, ONE-705.3, ONE-705.4, ONE-705.5.

47.4. Open question🔗

The guarantee Original item kept while Accept is pending is open: the example Itinerary reaccommodated shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

47.5. Open question🔗

The guarantee Paid status after re-accommodation is open: the example Itinerary reaccommodated shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.