41. Price of an a-la-carte selection🔗

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

rule

Rules.OneOrder.Ancillaries.chooseAlaCarte (orderId : String)
  (oi : Rules.OneOrder.Ancillaries.AlaCarteItem)
  (c : Rules.OneOrder.Ancillaries.AlaCarteChoice) :
  Except Rules.OneOrder.Ancillaries.AlaCarteRejection
    (List Rules.OneOrder.OrderItem)
Rules.OneOrder.Ancillaries.chooseAlaCarte
  (orderId : String)
  (oi :
    Rules.OneOrder.Ancillaries.AlaCarteItem)
  (c :
    Rules.OneOrder.Ancillaries.AlaCarteChoice) :
  Except
    Rules.OneOrder.Ancillaries.AlaCarteRejection
    (List Rules.OneOrder.OrderItem)

EARS: When a seller chooses an a-la-carte offer item for passengers and segments it lists as eligible, the system shall create one order item for each passenger and segment chosen, at the unit price times the quantity.

Story: As a seller, I want an extra bag priced the same way every time, so that I can quote the customer the right amount before they pay.

Acceptance criteria:

ONE-606.1: If an a-la-carte choice names a passenger or a segment that the offer item does not list as eligible, then the system shall refuse it.
ONE-606.2: When an a-la-carte choice is accepted, the system shall create one order item for each passenger and segment chosen, each holding one service for that passenger on that segment.
ONE-606.3: When an a-la-carte choice is accepted, the system shall price each order item at the unit price times the quantity.
ONE-606.4: When an a-la-carte choice is accepted, the system shall make the total price of its order items the unit price times the quantity times the number of passengers and segments chosen.
ONE-606.5: When an a-la-carte offer item is ordered, the system shall create exactly one order item from it.

The unit of the unit price is not named in the guide; the model prices per passenger and segment, as the add bag worked example does. The last criterion is the rule that each offer item becomes one order item, as accept makes it (ONE-001.1).

41.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-606.1	Proven	Ineligible choices are refused, Bag for ineligible passenger
ONE-606.2	Proven	Bag over two journeys, One order item per passenger and segment
ONE-606.3	Proven	Price of each a-la-carte order item, Bag over two journeys
ONE-606.4	Proven	Total of an a-la-carte choice, Bag over two journeys
ONE-606.5	Open	Bag over two journeys, One order item per a-la-carte offer item

41.2. Guarantees🔗

41.2.1. Ineligible choices are refused🔗

guarantee

Rules.OneOrder.Ancillaries.alacarte_refuses_ineligible
  (orderId : String) (oi : Rules.OneOrder.Ancillaries.AlaCarteItem)
  (c : Rules.OneOrder.Ancillaries.AlaCarteChoice)
  (h :
    (∃ p ∈ c.passengers, p ∉ oi.passengers) ∨
      ∃ seg ∈ c.segments, seg ∉ oi.segments)
  (items : List Rules.OneOrder.OrderItem) :
  Rules.OneOrder.Ancillaries.chooseAlaCarte orderId oi c ≠
    Except.ok items
Rules.OneOrder.Ancillaries.alacarte_refuses_ineligible
  (orderId : String)
  (oi :
    Rules.OneOrder.Ancillaries.AlaCarteItem)
  (c :
    Rules.OneOrder.Ancillaries.AlaCarteChoice)
  (h :
    (∃ p ∈ c.passengers,
        p ∉ oi.passengers) ∨
      ∃ seg ∈ c.segments,
        seg ∉ oi.segments)
  (items :
    List Rules.OneOrder.OrderItem) :
  Rules.OneOrder.Ancillaries.chooseAlaCarte
      orderId oi c ≠
    Except.ok items

A choice that names a passenger or a segment the offer item does not list as eligible is refused.

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

Checks acceptance criteria ONE-606.1.

41.2.2. One order item per passenger and segment🔗

guarantee

Rules.OneOrder.Ancillaries.alacarte_item_per_passenger_segment
  (orderId : String) (oi : Rules.OneOrder.Ancillaries.AlaCarteItem)
  (c : Rules.OneOrder.Ancillaries.AlaCarteChoice)
  (items : List Rules.OneOrder.OrderItem)
  (h :
    Rules.OneOrder.Ancillaries.chooseAlaCarte orderId oi c =
      Except.ok items) :
  List.map
      (fun x ↦ List.map (fun s ↦ (s.passenger, s.segment)) x.services)
      items =
    List.map (fun ps ↦ [ps]) (c.passengers ×ˢ c.segments)
Rules.OneOrder.Ancillaries.alacarte_item_per_passenger_segment
  (orderId : String)
  (oi :
    Rules.OneOrder.Ancillaries.AlaCarteItem)
  (c :
    Rules.OneOrder.Ancillaries.AlaCarteChoice)
  (items : List Rules.OneOrder.OrderItem)
  (h :
    Rules.OneOrder.Ancillaries.chooseAlaCarte
        orderId oi c =
      Except.ok items) :
  List.map
      (fun x ↦
        List.map
          (fun s ↦
            (s.passenger, s.segment))
          x.services)
      items =
    List.map (fun ps ↦ [ps])
      (c.passengers ×ˢ c.segments)

An accepted choice gives one order item for each pair of a passenger and a segment chosen, each holding one service for that passenger on that segment.

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

Checks acceptance criteria ONE-606.2.

41.2.3. Price of each a-la-carte order item🔗

guarantee

Rules.OneOrder.Ancillaries.alacarte_item_price (orderId : String)
  (oi : Rules.OneOrder.Ancillaries.AlaCarteItem)
  (c : Rules.OneOrder.Ancillaries.AlaCarteChoice)
  (items : List Rules.OneOrder.OrderItem)
  (h :
    Rules.OneOrder.Ancillaries.chooseAlaCarte orderId oi c =
      Except.ok items)
  (i : Rules.OneOrder.OrderItem) (hi : i ∈ items) :
  i.price =
    { amount := oi.unitPrice.amount * c.quantity,
      currency := oi.unitPrice.currency }
Rules.OneOrder.Ancillaries.alacarte_item_price
  (orderId : String)
  (oi :
    Rules.OneOrder.Ancillaries.AlaCarteItem)
  (c :
    Rules.OneOrder.Ancillaries.AlaCarteChoice)
  (items : List Rules.OneOrder.OrderItem)
  (h :
    Rules.OneOrder.Ancillaries.chooseAlaCarte
        orderId oi c =
      Except.ok items)
  (i : Rules.OneOrder.OrderItem)
  (hi : i ∈ items) :
  i.price =
    {
      amount :=
        oi.unitPrice.amount * c.quantity,
      currency := oi.unitPrice.currency }

Each order item of an accepted choice costs the unit price times the quantity.

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

Checks acceptance criteria ONE-606.3.

41.2.4. Total of an a-la-carte choice🔗

guarantee

Rules.OneOrder.Ancillaries.alacarte_total (orderId : String)
  (oi : Rules.OneOrder.Ancillaries.AlaCarteItem)
  (c : Rules.OneOrder.Ancillaries.AlaCarteChoice)
  (items : List Rules.OneOrder.OrderItem)
  (h :
    Rules.OneOrder.Ancillaries.chooseAlaCarte orderId oi c =
      Except.ok items) :
  (List.map (fun x ↦ x.price.amount) items).sum =
    oi.unitPrice.amount * c.quantity *
      (c.passengers.length * c.segments.length)
Rules.OneOrder.Ancillaries.alacarte_total
  (orderId : String)
  (oi :
    Rules.OneOrder.Ancillaries.AlaCarteItem)
  (c :
    Rules.OneOrder.Ancillaries.AlaCarteChoice)
  (items : List Rules.OneOrder.OrderItem)
  (h :
    Rules.OneOrder.Ancillaries.chooseAlaCarte
        orderId oi c =
      Except.ok items) :
  (List.map (fun x ↦ x.price.amount)
        items).sum =
    oi.unitPrice.amount * c.quantity *
      (c.passengers.length *
        c.segments.length)

The order items of an accepted choice cost, in total, the unit price times the quantity times the number of passengers and segments chosen.

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

Checks acceptance criteria ONE-606.4.

41.2.5. One order item per a-la-carte offer item🔗

guarantee

Rules.OneOrder.Ancillaries.alacarte_one_item (orderId : String)
  (oi : Rules.OneOrder.Ancillaries.AlaCarteItem)
  (c : Rules.OneOrder.Ancillaries.AlaCarteChoice)
  (items : List Rules.OneOrder.OrderItem)
  (h :
    Rules.OneOrder.Ancillaries.chooseAlaCarte orderId oi c =
      Except.ok items) :
  items.length = 1
Rules.OneOrder.Ancillaries.alacarte_one_item
  (orderId : String)
  (oi :
    Rules.OneOrder.Ancillaries.AlaCarteItem)
  (c :
    Rules.OneOrder.Ancillaries.AlaCarteChoice)
  (items : List Rules.OneOrder.OrderItem)
  (h :
    Rules.OneOrder.Ancillaries.chooseAlaCarte
        orderId oi c =
      Except.ok items) :
  items.length = 1

An a-la-carte offer item becomes exactly one order item, as every offer item does when an offer is accepted.

Open question for the business. The add bag worked example orders a 50.00 bag at quantity 1 for one passenger over two journeys and gets two order items of 50.00, so one offer item becomes two order items and the bag costs 100.00. The example bagOverTwoJourneys shows it. Does one offer item become one order item, as the order structure says, or one per passenger and segment, as the worked example shows? And what is the unit of the unit price: a passenger on a segment, a journey, or the order?

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

Checks acceptance criteria ONE-606.5.

41.3. Examples🔗

41.3.1. Bag for ineligible passenger🔗

example

Rules.OneOrder.Ancillaries.bagForIneligiblePassenger :
  Except Rules.OneOrder.Ancillaries.AlaCarteRejection
    Rules.OneOrder.Ancillaries.AlaCarteCase
Rules.OneOrder.Ancillaries.bagForIneligiblePassenger :
  Except
    Rules.OneOrder.Ancillaries.AlaCarteRejection
    Rules.OneOrder.Ancillaries.AlaCarteCase

Given the same extra bag, offered for PAX-1 only.

When the seller chooses it for PAX-2 on the outbound journey.

Then the choice is refused: the offer item does not list PAX-2.

What Lean computed:

Rejected: passenger not eligible PAX-2.

Checks acceptance criteria ONE-606.1.

41.3.2. Bag over two journeys🔗

example

Rules.OneOrder.Ancillaries.bagOverTwoJourneys :
  Except Rules.OneOrder.Ancillaries.AlaCarteRejection
    Rules.OneOrder.Ancillaries.AlaCarteCase
Rules.OneOrder.Ancillaries.bagOverTwoJourneys :
  Except
    Rules.OneOrder.Ancillaries.AlaCarteRejection
    Rules.OneOrder.Ancillaries.AlaCarteCase

Given the extra bag of the add bag worked example at 50.00 EUR a unit, for PAX-1 on the outbound and inbound journeys.

When the seller chooses it for PAX-1 on both journeys at quantity 1.

Then the one offer item becomes two order items of 50.00 EUR, one per journey, and the bag costs 100.00 EUR.

What Lean computed:

Accepted. The result:

Order items: 2
Prices: see the table below.
Total: 100.00 EUR

Prices:

Amount	Currency
5000	EUR
5000	EUR

Checks acceptance criteria ONE-606.2, ONE-606.3, ONE-606.4, ONE-606.5.

41.4. Open question🔗

The guarantee One order item per a-la-carte offer item is open: the example Bag over two journeys shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.