42. Value of one bundled service🔗

Requirement ONE-607. Of its 4 acceptance criteria, 2 are proven and 2 are open.

rule

Rules.OneOrder.Ancillaries.removeFromBundle
  (m : Rules.OneOrder.Delivery.MoveReading)
  (sh : Rules.OneOrder.Ancillaries.BundleShare)
  (o : Rules.OneOrder.Order) (item : String) (ids : List String) :
  Except Rules.OneOrder.Ancillaries.BundleRejection
    (Rules.OneOrder.Order × Rules.Core.Money)
Rules.OneOrder.Ancillaries.removeFromBundle
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (sh :
    Rules.OneOrder.Ancillaries.BundleShare)
  (o : Rules.OneOrder.Order)
  (item : String) (ids : List String) :
  Except
    Rules.OneOrder.Ancillaries.BundleRejection
    (Rules.OneOrder.Order ×
      Rules.Core.Money)

EARS: When a seller removes services from a bundle, the system shall cancel them and return their share of the bundle price under the reading.

Story: As a customer who drops one passenger from a bundled trip, I want back the part of the price that passenger's services were worth, so that I pay only for what I keep.

Acceptance criteria:

ONE-607.1: When services are removed from a bundle, the system shall mark each named live service that the delivery status table lets be removed CANCELLED with delivery status REMOVED and leave the bundle's other services and its price as they were.
ONE-607.2: When services are removed from a bundle, the system shall return the sum of the shares of the services it cancels under the reading, in the bundle's currency.
ONE-607.3: When services are removed from a bundle, the system shall return no more than the bundle price.
ONE-607.4: When every service of a bundle is removed, the system shall return the whole bundle price.

A bundle here is one order item holding several services, as on the guide's bundles page. The share of each service is the reading's (BundleShare). Whether the rest of the bundle is repriced, as the cancellation page suggests, is not modelled. A service is removed through the delivery status table (Delivery.endWith), and a named service the table does not let be removed, such as one still REQUESTED, stays as it was and is not paid back.

42.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-607.1	Proven	Removed services are cancelled, Bundle after removal
ONE-607.2	Proven	A removal returns the services' shares, Bundle shares
ONE-607.3	Open	A removal returns no more than the bundle price, Bundle shares
ONE-607.4	Open	Removing a whole bundle returns its price, Bundle shares

42.2. Guarantees🔗

42.2.1. Removed services are cancelled🔗

guarantee

Rules.OneOrder.Ancillaries.bundle_removes
  (mr : Rules.OneOrder.Delivery.MoveReading)
  (sh : Rules.OneOrder.Ancillaries.BundleShare)
  (o o' : Rules.OneOrder.Order) (item : String) (ids : List String)
  (m : Rules.Core.Money)
  (h :
    Rules.OneOrder.Ancillaries.removeFromBundle mr sh o item ids =
      Except.ok (o', m)) :
  ∃ i ∈ o.items,
    i.id = item ∧
      ∃ i' ∈ o'.items,
        i'.id = i.id ∧
          i'.price = i.price ∧
            (∀ s ∈ i.services,
                ids.contains s.id = true →
                  Rules.OneOrder.Delivery.isLive s = true →
                    (Rules.OneOrder.Delivery.nextDelivery mr
                            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) ∧
              ∀ s ∈ i.services,
                ids.contains s.id = false → s ∈ i'.services
Rules.OneOrder.Ancillaries.bundle_removes
  (mr :
    Rules.OneOrder.Delivery.MoveReading)
  (sh :
    Rules.OneOrder.Ancillaries.BundleShare)
  (o o' : Rules.OneOrder.Order)
  (item : String) (ids : List String)
  (m : Rules.Core.Money)
  (h :
    Rules.OneOrder.Ancillaries.removeFromBundle
        mr sh o item ids =
      Except.ok (o', m)) :
  ∃ i ∈ o.items,
    i.id = item ∧
      ∃ i' ∈ o'.items,
        i'.id = i.id ∧
          i'.price = i.price ∧
            (∀ s ∈ i.services,
                ids.contains s.id = true →
                  Rules.OneOrder.Delivery.isLive
                        s =
                      true →
                    (Rules.OneOrder.Delivery.nextDelivery
                            mr
                            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) ∧
              ∀ s ∈ i.services,
                ids.contains s.id =
                    false →
                  s ∈ i'.services

After an accepted removal the bundle is in the order with its reference and price, each named live service that the delivery status table lets be removed CANCELLED with delivery status REMOVED, and every service that is not named as it was, under every reading.

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

Checks acceptance criteria ONE-607.1.

42.2.2. A removal returns the services' shares🔗

guarantee

Rules.OneOrder.Ancillaries.bundle_returns_shares
  (mr : Rules.OneOrder.Delivery.MoveReading)
  (sh : Rules.OneOrder.Ancillaries.BundleShare)
  (o o' : Rules.OneOrder.Order) (item : String) (ids : List String)
  (m : Rules.Core.Money)
  (h :
    Rules.OneOrder.Ancillaries.removeFromBundle mr sh o item ids =
      Except.ok (o', m))
  (i : Rules.OneOrder.OrderItem)
  (hi : List.find? (fun x ↦ x.id == item) o.items = some i) :
  m =
    {
      amount :=
        (List.map (sh.share i)
            (List.filter
              (fun s ↦
                ids.contains s.id && Rules.OneOrder.Delivery.isLive s &&
                  (Rules.OneOrder.Delivery.nextDelivery mr
                      Rules.OneOrder.Delivery.DeliveryEvent.remove
                      s).isSome)
              i.services)).sum,
      currency := i.price.currency }
Rules.OneOrder.Ancillaries.bundle_returns_shares
  (mr :
    Rules.OneOrder.Delivery.MoveReading)
  (sh :
    Rules.OneOrder.Ancillaries.BundleShare)
  (o o' : Rules.OneOrder.Order)
  (item : String) (ids : List String)
  (m : Rules.Core.Money)
  (h :
    Rules.OneOrder.Ancillaries.removeFromBundle
        mr sh o item ids =
      Except.ok (o', m))
  (i : Rules.OneOrder.OrderItem)
  (hi :
    List.find? (fun x ↦ x.id == item)
        o.items =
      some i) :
  m =
    {
      amount :=
        (List.map (sh.share i)
            (List.filter
              (fun s ↦
                ids.contains s.id &&
                    Rules.OneOrder.Delivery.isLive
                      s &&
                  (Rules.OneOrder.Delivery.nextDelivery
                      mr
                      Rules.OneOrder.Delivery.DeliveryEvent.remove
                      s).isSome)
              i.services)).sum,
      currency := i.price.currency }

An accepted removal returns the sum of the shares of the services it cancels under the reading, in the bundle's currency: the named live services that the delivery status table lets be removed.

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

Checks acceptance criteria ONE-607.2.

42.2.3. A removal returns no more than the bundle price🔗

guarantee

Rules.OneOrder.Ancillaries.bundle_return_le_price
  (mr : Rules.OneOrder.Delivery.MoveReading)
  (sh : Rules.OneOrder.Ancillaries.BundleShare)
  (o o' : Rules.OneOrder.Order) (item : String) (ids : List String)
  (m : Rules.Core.Money)
  (h :
    Rules.OneOrder.Ancillaries.removeFromBundle mr sh o item ids =
      Except.ok (o', m))
  (i : Rules.OneOrder.OrderItem)
  (hi : List.find? (fun x ↦ x.id == item) o.items = some i) :
  m.amount ≤ i.price.amount
Rules.OneOrder.Ancillaries.bundle_return_le_price
  (mr :
    Rules.OneOrder.Delivery.MoveReading)
  (sh :
    Rules.OneOrder.Ancillaries.BundleShare)
  (o o' : Rules.OneOrder.Order)
  (item : String) (ids : List String)
  (m : Rules.Core.Money)
  (h :
    Rules.OneOrder.Ancillaries.removeFromBundle
        mr sh o item ids =
      Except.ok (o', m))
  (i : Rules.OneOrder.OrderItem)
  (hi :
    List.find? (fun x ↦ x.id == item)
        o.items =
      some i) :
  m.amount ≤ i.price.amount

An accepted removal returns no more than the bundle price, under every reading.

Open question for the business. The guide prices a bundle only as a whole. Under a reading that gives each service its stand-alone price, a 1,000.00 EUR bundle of two flights at 470.00 EUR and two bags at 60.00 EUR returns 1,060.00 EUR when every service is removed. The example bundleShares shows it. How does a bundle price split among its services: by stated component prices, by stand-alone prices, or not at all?

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

Checks acceptance criteria ONE-607.3.

42.2.4. Removing a whole bundle returns its price🔗

guarantee

Rules.OneOrder.Ancillaries.bundle_return_all
  (mr : Rules.OneOrder.Delivery.MoveReading)
  (sh : Rules.OneOrder.Ancillaries.BundleShare)
  (o o' : Rules.OneOrder.Order) (item : String) (ids : List String)
  (m : Rules.Core.Money)
  (h :
    Rules.OneOrder.Ancillaries.removeFromBundle mr sh o item ids =
      Except.ok (o', m))
  (i : Rules.OneOrder.OrderItem)
  (hi : List.find? (fun x ↦ x.id == item) o.items = some i)
  (hall :
    ∀ s ∈ i.services,
      s.id ∈ ids ∧ Rules.OneOrder.Delivery.isLive s = true) :
  m.amount = i.price.amount
Rules.OneOrder.Ancillaries.bundle_return_all
  (mr :
    Rules.OneOrder.Delivery.MoveReading)
  (sh :
    Rules.OneOrder.Ancillaries.BundleShare)
  (o o' : Rules.OneOrder.Order)
  (item : String) (ids : List String)
  (m : Rules.Core.Money)
  (h :
    Rules.OneOrder.Ancillaries.removeFromBundle
        mr sh o item ids =
      Except.ok (o', m))
  (i : Rules.OneOrder.OrderItem)
  (hi :
    List.find? (fun x ↦ x.id == item)
        o.items =
      some i)
  (hall :
    ∀ s ∈ i.services,
      s.id ∈ ids ∧
        Rules.OneOrder.Delivery.isLive s =
          true) :
  m.amount = i.price.amount

Removing every service of a bundle, all of them live, returns the whole bundle price, under every reading.

Open question for the business. Under a reading that gives no share to any service, removing a passenger's flight and bag from a 1,000.00 EUR bundle returns nothing, and so does removing every service. The example bundleShares shows it. Does removing part of a bundle return part of its price, and does removing all of it return all of it?

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

Checks acceptance criteria ONE-607.4.

42.3. Examples🔗

42.3.1. Bundle after removal🔗

example

Rules.OneOrder.Ancillaries.bundleAfterRemoval :
  Except Rules.OneOrder.Ancillaries.BundleRejection
    Rules.OneOrder.Ancillaries.BundleAfter
Rules.OneOrder.Ancillaries.bundleAfterRemoval :
  Except
    Rules.OneOrder.Ancillaries.BundleRejection
    Rules.OneOrder.Ancillaries.BundleAfter

Given the same bundle at 1,000.00 EUR.

When the seller removes PAX02's flight and bag.

Then PAX02's flight and bag are CANCELLED with delivery status REMOVED, PAX01's flight and bag are as they were, and the item keeps its price of 1,000.00 EUR.

What Lean computed:

Accepted. The result:

Price: 1000.00 EUR
Services: see the table below.

Services:

Service	Status	Delivery
FLT-1	confirmed	ready to proceed
BAG-1	confirmed	ready to proceed
FLT-2	cancelled	removed
BAG-2	cancelled	removed

Checks acceptance criteria ONE-607.1.

42.3.2. Bundle shares🔗

example

Rules.OneOrder.Ancillaries.bundleShares :
  List Rules.OneOrder.Ancillaries.BundleCase
Rules.OneOrder.Ancillaries.bundleShares :
  List
    Rules.OneOrder.Ancillaries.BundleCase

Given the seat worked example's bundle: one order item at 1,000.00 EUR holding both passengers' flights and bags, all paid.

When the seller removes PAX02's flight and bag, and then, separately, every service, under three readings of how the bundle price splits.

Then with stated component prices, PAX02's part returns 500.00 EUR and the whole bundle returns 1,000.00 EUR. With stand-alone prices, the whole bundle returns 1,060.00 EUR, more than was paid. With no share, nothing is returned, even for the whole bundle.

What Lean computed:

Reading	Removed	Returned
stated component prices	PAX02's flight and bag	500.00 EUR
stated component prices	every service	1000.00 EUR
stand-alone prices	PAX02's flight and bag	530.00 EUR
stand-alone prices	every service	1060.00 EUR
no share	PAX02's flight and bag	0.00 EUR
no share	every service	0.00 EUR

Checks acceptance criteria ONE-607.2, ONE-607.3, ONE-607.4.

42.4. Open question🔗

The guarantee A removal returns no more than the bundle price is open: the example Bundle shares shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

42.5. Open question🔗

The guarantee Removing a whole bundle returns its price is open: the example Bundle shares shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.