16. Changing an order item🔗

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

rule

Rules.OneOrder.Change.changeItem
  (m : Rules.OneOrder.Delivery.MoveReading) (o : Rules.OneOrder.Order)
  (c : Rules.OneOrder.Change.ItemChange) :
  Except Rules.OneOrder.Change.ChangeRejection Rules.OneOrder.Order
Rules.OneOrder.Change.changeItem
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (o : Rules.OneOrder.Order)
  (c : Rules.OneOrder.Change.ItemChange) :
  Except
    Rules.OneOrder.Change.ChangeRejection
    Rules.OneOrder.Order

EARS: When a seller has accepted and paid a change to an order item, the system shall add a new item with the services the change keeps and cancel the services it does not keep.

Story: As an airline, I want a changed item's kept services to move to the new item under the same references, so that each service is delivered and accounted for once.

Acceptance criteria:

ONE-204.1: When a change keeps a service of the changed item, the system shall give the new item a service with the same reference, passenger, segment and delivery status.
ONE-204.2: When a change keeps a service of the changed item, the system shall mark the original copy transferred and leave its delivery status as it was.
ONE-204.3: When a change does not keep a service of the changed item and the delivery status table lets it be removed, the system shall mark it cancelled and removed.
ONE-204.4: When a change is made, the system shall keep the order's item references distinct.
ONE-204.5: When a change is made, the system shall mark the changed item cancelled.

The original copy keeps its delivery status because the worked examples show it so: after the change, the transferred copies are still READY TO PROCEED. A service the change does not keep is removed through the delivery status table (Delivery.endWith), so a service already DELIVERED, such as an outbound flight already flown, stays as it was.

16.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-204.1	Proven	Change keeping outbound, Kept services keep their references
ONE-204.2	Proven	Change keeping outbound, Originals of kept services are transferred
ONE-204.3	Proven	Change after outbound flown, Change keeping outbound, Change replacing all, Services not kept are cancelled
ONE-204.4	Proven	Changes keep item references distinct, Change reusing reference
ONE-204.5	Open	Transferred originals hold no value, Change keeping outbound

16.2. Guarantees🔗

16.2.1. Kept services keep their references🔗

guarantee

Rules.OneOrder.Change.change_keeps_services
  (m : Rules.OneOrder.Delivery.MoveReading)
  (o o' : Rules.OneOrder.Order) (c : Rules.OneOrder.Change.ItemChange)
  (h : Rules.OneOrder.Change.changeItem m o c = Except.ok o')
  (old : Rules.OneOrder.OrderItem)
  (hold :
    List.find? (fun x ↦ decide (x.id = c.item)) o.items = some old)
  (s : Rules.OneOrder.Service) (hs : s ∈ old.services)
  (hk : s.id ∈ c.kept) :
  ∃ i ∈ o'.items,
    i.id = c.newItem ∧
      { id := s.id, passenger := s.passenger, segment := s.segment,
          status := Rules.OneOrder.ServiceStatus.confirmed,
          delivery := s.delivery } ∈
        i.services
Rules.OneOrder.Change.change_keeps_services
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (o o' : Rules.OneOrder.Order)
  (c : Rules.OneOrder.Change.ItemChange)
  (h :
    Rules.OneOrder.Change.changeItem m o
        c =
      Except.ok o')
  (old : Rules.OneOrder.OrderItem)
  (hold :
    List.find?
        (fun x ↦ decide (x.id = c.item))
        o.items =
      some old)
  (s : Rules.OneOrder.Service)
  (hs : s ∈ old.services)
  (hk : s.id ∈ c.kept) :
  ∃ i ∈ o'.items,
    i.id = c.newItem ∧
      { id := s.id,
          passenger := s.passenger,
          segment := s.segment,
          status :=
            Rules.OneOrder.ServiceStatus.confirmed,
          delivery := s.delivery } ∈
        i.services

Every service a change keeps has a copy in the new item with the same reference, passenger, segment and delivery status, confirmed.

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

Checks acceptance criteria ONE-204.1.

16.2.2. Originals of kept services are transferred🔗

guarantee

Rules.OneOrder.Change.change_marks_transferred
  (m : Rules.OneOrder.Delivery.MoveReading)
  (o o' : Rules.OneOrder.Order) (c : Rules.OneOrder.Change.ItemChange)
  (h : Rules.OneOrder.Change.changeItem m o c = Except.ok o')
  (old : Rules.OneOrder.OrderItem)
  (hold :
    List.find? (fun x ↦ decide (x.id = c.item)) o.items = some old)
  (s : Rules.OneOrder.Service) (hs : s ∈ old.services)
  (hk : s.id ∈ c.kept) :
  ∃ i ∈ o'.items,
    i.id = c.item ∧
      { id := s.id, passenger := s.passenger, segment := s.segment,
          status := Rules.OneOrder.ServiceStatus.transferred,
          delivery := s.delivery } ∈
        i.services
Rules.OneOrder.Change.change_marks_transferred
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (o o' : Rules.OneOrder.Order)
  (c : Rules.OneOrder.Change.ItemChange)
  (h :
    Rules.OneOrder.Change.changeItem m o
        c =
      Except.ok o')
  (old : Rules.OneOrder.OrderItem)
  (hold :
    List.find?
        (fun x ↦ decide (x.id = c.item))
        o.items =
      some old)
  (s : Rules.OneOrder.Service)
  (hs : s ∈ old.services)
  (hk : s.id ∈ c.kept) :
  ∃ i ∈ o'.items,
    i.id = c.item ∧
      { id := s.id,
          passenger := s.passenger,
          segment := s.segment,
          status :=
            Rules.OneOrder.ServiceStatus.transferred,
          delivery := s.delivery } ∈
        i.services

Every service a change keeps stays in the changed item marked transferred, with everything else about it, its delivery status included, as it was.

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

Checks acceptance criteria ONE-204.2.

16.2.3. Services not kept are cancelled🔗

guarantee

Rules.OneOrder.Change.change_cancels_others
  (m : Rules.OneOrder.Delivery.MoveReading)
  (o o' : Rules.OneOrder.Order) (c : Rules.OneOrder.Change.ItemChange)
  (h : Rules.OneOrder.Change.changeItem m o c = Except.ok o')
  (old : Rules.OneOrder.OrderItem)
  (hold :
    List.find? (fun x ↦ decide (x.id = c.item)) o.items = some old)
  (s : Rules.OneOrder.Service) (hs : s ∈ old.services)
  (hk : s.id ∉ c.kept)
  (hrem :
    (Rules.OneOrder.Delivery.nextDelivery m
          Rules.OneOrder.Delivery.DeliveryEvent.remove s).isSome =
      true) :
  ∃ i ∈ o'.items,
    i.id = c.item ∧
      { id := s.id, passenger := s.passenger, segment := s.segment,
          status := Rules.OneOrder.ServiceStatus.cancelled,
          delivery := Rules.OneOrder.DeliveryStatus.removed } ∈
        i.services
Rules.OneOrder.Change.change_cancels_others
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (o o' : Rules.OneOrder.Order)
  (c : Rules.OneOrder.Change.ItemChange)
  (h :
    Rules.OneOrder.Change.changeItem m o
        c =
      Except.ok o')
  (old : Rules.OneOrder.OrderItem)
  (hold :
    List.find?
        (fun x ↦ decide (x.id = c.item))
        o.items =
      some old)
  (s : Rules.OneOrder.Service)
  (hs : s ∈ old.services)
  (hk : s.id ∉ c.kept)
  (hrem :
    (Rules.OneOrder.Delivery.nextDelivery
          m
          Rules.OneOrder.Delivery.DeliveryEvent.remove
          s).isSome =
      true) :
  ∃ i ∈ o'.items,
    i.id = c.item ∧
      { id := s.id,
          passenger := s.passenger,
          segment := s.segment,
          status :=
            Rules.OneOrder.ServiceStatus.cancelled,
          delivery :=
            Rules.OneOrder.DeliveryStatus.removed } ∈
        i.services

Every service a change does not keep, and that the delivery status table lets be removed, stays in the changed item, cancelled and removed, under every reading of the sources.

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

Checks acceptance criteria ONE-204.3.

16.2.4. Changes keep item references distinct🔗

guarantee

Rules.OneOrder.Change.change_item_refs_unique
  (m : Rules.OneOrder.Delivery.MoveReading)
  (o o' : Rules.OneOrder.Order) (c : Rules.OneOrder.Change.ItemChange)
  (h : Rules.OneOrder.Change.changeItem m o c = Except.ok o')
  (hids : (List.map (fun x ↦ x.id) o.items).Nodup) :
  (List.map (fun x ↦ x.id) o'.items).Nodup
Rules.OneOrder.Change.change_item_refs_unique
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (o o' : Rules.OneOrder.Order)
  (c : Rules.OneOrder.Change.ItemChange)
  (h :
    Rules.OneOrder.Change.changeItem m o
        c =
      Except.ok o')
  (hids :
    (List.map (fun x ↦ x.id)
        o.items).Nodup) :
  (List.map (fun x ↦ x.id) o'.items).Nodup

A change keeps the order's item references distinct: the changed item keeps its reference, and the new item's reference is not already used.

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

Checks acceptance criteria ONE-204.4.

16.2.5. Transferred originals hold no value🔗

guarantee

Rules.OneOrder.Change.change_original_cancelled
  (m : Rules.OneOrder.Delivery.MoveReading)
  (v : Rules.OneOrder.ValueReading) (o o' : Rules.OneOrder.Order)
  (c : Rules.OneOrder.Change.ItemChange)
  (h : Rules.OneOrder.Change.changeItem m o c = Except.ok o')
  (i : Rules.OneOrder.OrderItem) (hi : i ∈ o'.items)
  (hid : i.id = c.item) :
  Rules.OneOrder.itemStatuses v i =
    [Rules.OneOrder.ItemStatus.cancelled]
Rules.OneOrder.Change.change_original_cancelled
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (v : Rules.OneOrder.ValueReading)
  (o o' : Rules.OneOrder.Order)
  (c : Rules.OneOrder.Change.ItemChange)
  (h :
    Rules.OneOrder.Change.changeItem m o
        c =
      Except.ok o')
  (i : Rules.OneOrder.OrderItem)
  (hi : i ∈ o'.items)
  (hid : i.id = c.item) :
  Rules.OneOrder.itemStatuses v i =
    [Rules.OneOrder.ItemStatus.cancelled]

After a change, the changed item is cancelled, under every reading of the guide.

Open question for the business. The worked examples leave the transferred copies in the changed item READY TO PROCEED and show the item CANCELLED. The guide's item status rule judges value by delivery status alone, and a service READY TO PROCEED holds value under every reading, so the changed item stays active and the kept service holds value in both items. The example changeKeepingOutbound shows it. Does the TRANSFERRED status take away a service's value, or should the original copy move to a delivery status that holds none?

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

Checks acceptance criteria ONE-204.5.

16.3. Examples🔗

16.3.1. Change after outbound flown🔗

example

Rules.OneOrder.Change.changeAfterOutboundFlown :
  Except Rules.OneOrder.Change.ChangeRejection
    Rules.OneOrder.Change.ChangedOrder
Rules.OneOrder.Change.changeAfterOutboundFlown :
  Except
    Rules.OneOrder.Change.ChangeRejection
    Rules.OneOrder.Change.ChangedOrder

Given the trip order with its outbound flight already flown, so DELIVERED, and its inbound flight ready to proceed.

When the seller accepts and pays a change that keeps no service and puts a new inbound flight in a new item at 900.00 EUR.

Then the inbound service is cancelled and removed. The outbound service stays DELIVERED, because the delivery status table lets no event move a delivered service.

What Lean computed:

Accepted. The result:

Items: see the table below.
Services: see the table below.

Items:

Item	Price	Cautious	Strict
ORDITM-1	1000.00 EUR	closed	closed
ORDITM-2	900.00 EUR	active	active

Services:

Item	Service	Status	Delivery
ORDITM-1	SVC-OUT	confirmed	delivered
ORDITM-1	SVC-IN	cancelled	removed
ORDITM-2	SVC-IN-2	confirmed	ready to proceed

Checks acceptance criteria ONE-204.3, ONE-105.2.

16.3.2. Change keeping outbound🔗

example

Rules.OneOrder.Change.changeKeepingOutbound :
  Except Rules.OneOrder.Change.ChangeRejection
    Rules.OneOrder.Change.ChangedOrder
Rules.OneOrder.Change.changeKeepingOutbound :
  Except
    Rules.OneOrder.Change.ChangeRejection
    Rules.OneOrder.Change.ChangedOrder

Given the trip order, paid and ready to proceed.

When the seller accepts and pays a change that keeps the outbound flight and replaces the inbound flight, in a new item at 900.00 EUR. This is the shape of worked example EXM_ORD_003B.

Then the new item holds the outbound service under the same reference, and the original copy is transferred and still READY TO PROCEED. The replaced inbound service is cancelled and removed. Under both readings the original item is active, where the worked example shows it cancelled, and the outbound service holds value in both items.

What Lean computed:

Accepted. The result:

Items: see the table below.
Services: see the table below.

Items:

Item	Price	Cautious	Strict
ORDITM-1	1000.00 EUR	active	active
ORDITM-2	900.00 EUR	active	active

Services:

Item	Service	Status	Delivery
ORDITM-1	SVC-OUT	transferred	ready to proceed
ORDITM-1	SVC-IN	cancelled	removed
ORDITM-2	SVC-OUT	confirmed	ready to proceed
ORDITM-2	SVC-IN-2	confirmed	ready to proceed

Checks acceptance criteria ONE-204.1, ONE-204.2, ONE-204.3, ONE-204.5.

16.3.3. Change replacing all🔗

example

Rules.OneOrder.Change.changeReplacingAll :
  Except Rules.OneOrder.Change.ChangeRejection
    Rules.OneOrder.Change.ChangedOrder
Rules.OneOrder.Change.changeReplacingAll :
  Except
    Rules.OneOrder.Change.ChangeRejection
    Rules.OneOrder.Change.ChangedOrder

Given the trip order, paid and ready to proceed.

When the seller accepts and pays a change that keeps no service and puts a new inbound flight in a new item at 900.00 EUR.

Then both original services are cancelled and removed, and the original item is cancelled under both readings.

What Lean computed:

Accepted. The result:

Items: see the table below.
Services: see the table below.

Items:

Item	Price	Cautious	Strict
ORDITM-1	1000.00 EUR	cancelled	cancelled
ORDITM-2	900.00 EUR	active	active

Services:

Item	Service	Status	Delivery
ORDITM-1	SVC-OUT	cancelled	removed
ORDITM-1	SVC-IN	cancelled	removed
ORDITM-2	SVC-IN-2	confirmed	ready to proceed

Checks acceptance criteria ONE-204.3.

16.3.4. Change reusing reference🔗

example

Rules.OneOrder.Change.changeReusingReference :
  Except Rules.OneOrder.Change.ChangeRejection
    Rules.OneOrder.Change.ChangedOrder
Rules.OneOrder.Change.changeReusingReference :
  Except
    Rules.OneOrder.Change.ChangeRejection
    Rules.OneOrder.Change.ChangedOrder

Given the trip order, paid and ready to proceed.

When the seller asks for a change whose new item would reuse the reference of the item being changed.

Then the change is refused, so the order's item references stay distinct.

What Lean computed:

Rejected: duplicate item reference.

Checks acceptance criteria ONE-204.4.

16.4. Open question🔗

The guarantee Transferred originals hold no value is open: the example Change keeping outbound shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.