40. Choosing seats🔗

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

rule

Rules.OneOrder.Ancillaries.chooseSeats
  (maps : List Rules.OneOrder.Ancillaries.SeatMap)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order)
  (cs : List Rules.OneOrder.Ancillaries.SeatChoice) :
  Except Rules.OneOrder.Ancillaries.SeatRejection
    (Rules.OneOrder.Order × Rules.OneOrder.Ancillaries.ServiceDetails)
Rules.OneOrder.Ancillaries.chooseSeats
  (maps :
    List
      Rules.OneOrder.Ancillaries.SeatMap)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order)
  (cs :
    List
      Rules.OneOrder.Ancillaries.SeatChoice) :
  Except
    Rules.OneOrder.Ancillaries.SeatRejection
    (Rules.OneOrder.Order ×
      Rules.OneOrder.Ancillaries.ServiceDetails)

EARS: When a seller chooses seats for passengers, the system shall add one order item for each seat the seat map marks available, and refuse the request if any seat chosen is not.

Story: As a passenger, I want the seat I chose to be mine alone, so that I do not find someone else in it.

Acceptance criteria:

ONE-605.1: If a seat choice names a seat that the seat map of its segment does not mark available, then the system shall refuse the request.
ONE-605.2: When a seat request is accepted, the system shall keep the existing order items and add one order item for each seat chosen, at the seat's price, holding one seat service for that passenger on that segment.
ONE-605.3: The system shall never let two passengers hold the same seat on the same segment.
ONE-605.4: The system shall let a passenger hold at most one live seat on each segment.

The rule records each new seat service as a seat with its number in the service details it returns. It checks each choice against the seat map only, which is all the guide describes.

40.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-605.1	Proven	A seat the map does not offer is refused, Occupied seat refused
ONE-605.2	Proven	Each seat becomes its own order item, Same seat twice, Second seat same passenger
ONE-605.3	Open	One passenger per seat, Same seat twice
ONE-605.4	Open	Second seat same passenger, One seat per passenger per segment

40.2. Guarantees🔗

40.2.1. A seat the map does not offer is refused🔗

guarantee

Rules.OneOrder.Ancillaries.choose_seats_refuses_unavailable
  (maps : List Rules.OneOrder.Ancillaries.SeatMap)
  (d : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order)
  (cs : List Rules.OneOrder.Ancillaries.SeatChoice)
  (c : Rules.OneOrder.Ancillaries.SeatChoice) (hc : c ∈ cs)
  (hmap : ∀ m ∈ maps, m.segment = c.segment → c.seat ∉ m.available) :
  ∃ e,
    Rules.OneOrder.Ancillaries.chooseSeats maps d o cs = Except.error e
Rules.OneOrder.Ancillaries.choose_seats_refuses_unavailable
  (maps :
    List
      Rules.OneOrder.Ancillaries.SeatMap)
  (d :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o : Rules.OneOrder.Order)
  (cs :
    List
      Rules.OneOrder.Ancillaries.SeatChoice)
  (c :
    Rules.OneOrder.Ancillaries.SeatChoice)
  (hc : c ∈ cs)
  (hmap :
    ∀ m ∈ maps,
      m.segment = c.segment →
        c.seat ∉ m.available) :
  ∃ e,
    Rules.OneOrder.Ancillaries.chooseSeats
        maps d o cs =
      Except.error e

A request that chooses a seat the seat map of its segment does not mark available is refused.

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

Checks acceptance criteria ONE-605.1.

40.2.2. Each seat becomes its own order item🔗

guarantee

Rules.OneOrder.Ancillaries.choose_seats_items
  (maps : List Rules.OneOrder.Ancillaries.SeatMap)
  (d d' : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o o' : Rules.OneOrder.Order)
  (cs : List Rules.OneOrder.Ancillaries.SeatChoice)
  (h :
    Rules.OneOrder.Ancillaries.chooseSeats maps d o cs =
      Except.ok (o', d')) :
  o'.items =
      o.items ++
        List.map (Rules.OneOrder.Ancillaries.seatItem o.id) cs ∧
    ∀ c ∈ cs,
      (Rules.OneOrder.Ancillaries.seatItem o.id c).price = c.price ∧
        List.map (fun s ↦ (s.passenger, s.segment))
            (Rules.OneOrder.Ancillaries.seatItem o.id c).services =
          [(c.passenger, c.segment)]
Rules.OneOrder.Ancillaries.choose_seats_items
  (maps :
    List
      Rules.OneOrder.Ancillaries.SeatMap)
  (d d' :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o o' : Rules.OneOrder.Order)
  (cs :
    List
      Rules.OneOrder.Ancillaries.SeatChoice)
  (h :
    Rules.OneOrder.Ancillaries.chooseSeats
        maps d o cs =
      Except.ok (o', d')) :
  o'.items =
      o.items ++
        List.map
          (Rules.OneOrder.Ancillaries.seatItem
            o.id)
          cs ∧
    ∀ c ∈ cs,
      (Rules.OneOrder.Ancillaries.seatItem
              o.id c).price =
          c.price ∧
        List.map
            (fun s ↦
              (s.passenger, s.segment))
            (Rules.OneOrder.Ancillaries.seatItem
                o.id c).services =
          [(c.passenger, c.segment)]

An accepted seat request keeps the existing order items and adds one item for each seat chosen, at the seat's price, 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-605.2.

40.2.3. One passenger per seat🔗

guarantee

Rules.OneOrder.Ancillaries.choose_seats_one_passenger_per_seat
  (maps : List Rules.OneOrder.Ancillaries.SeatMap)
  (d d' : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o o' : Rules.OneOrder.Order)
  (cs : List Rules.OneOrder.Ancillaries.SeatChoice)
  (h0 :
    ∀ a ∈ Rules.OneOrder.Ancillaries.seatsHeld d o,
      ∀ b ∈ Rules.OneOrder.Ancillaries.seatsHeld d o,
        a.segment = b.segment →
          a.seat = b.seat → a.passenger = b.passenger)
  (hmap :
    ∀ a ∈ Rules.OneOrder.Ancillaries.seatsHeld d o,
      ∀ m ∈ maps, m.segment = a.segment → a.seat ∉ m.available)
  (h :
    Rules.OneOrder.Ancillaries.chooseSeats maps d o cs =
      Except.ok (o', d'))
  (a : Rules.OneOrder.Ancillaries.SeatAssignment) :
  a ∈ Rules.OneOrder.Ancillaries.seatsHeld d' o' →
    ∀ b ∈ Rules.OneOrder.Ancillaries.seatsHeld d' o',
      a.segment = b.segment →
        a.seat = b.seat → a.passenger = b.passenger
Rules.OneOrder.Ancillaries.choose_seats_one_passenger_per_seat
  (maps :
    List
      Rules.OneOrder.Ancillaries.SeatMap)
  (d d' :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o o' : Rules.OneOrder.Order)
  (cs :
    List
      Rules.OneOrder.Ancillaries.SeatChoice)
  (h0 :
    ∀
      a ∈
        Rules.OneOrder.Ancillaries.seatsHeld
          d o,
      ∀
        b ∈
          Rules.OneOrder.Ancillaries.seatsHeld
            d o,
        a.segment = b.segment →
          a.seat = b.seat →
            a.passenger = b.passenger)
  (hmap :
    ∀
      a ∈
        Rules.OneOrder.Ancillaries.seatsHeld
          d o,
      ∀ m ∈ maps,
        m.segment = a.segment →
          a.seat ∉ m.available)
  (h :
    Rules.OneOrder.Ancillaries.chooseSeats
        maps d o cs =
      Except.ok (o', d'))
  (a :
    Rules.OneOrder.Ancillaries.SeatAssignment) :
  a ∈
      Rules.OneOrder.Ancillaries.seatsHeld
        d' o' →
    ∀
      b ∈
        Rules.OneOrder.Ancillaries.seatsHeld
          d' o',
      a.segment = b.segment →
        a.seat = b.seat →
          a.passenger = b.passenger

When no seat is held by two passengers on a segment, and the seat maps mark no held seat available, an accepted seat request keeps it so.

Open question for the business. The guide checks a seat choice against the seat map and states no rule that a seat goes to one passenger. One request that chooses 12B on the same flight for two passengers passes, since the seat map marks 12B available for each choice. The example sameSeatTwice shows it. Is a seat checked against the other choices of the same request, against every order on the flight, or only against the seat map? And is the unit the passenger segment or the leg the aircraft flies?

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

Checks acceptance criteria ONE-605.3.

40.2.4. One seat per passenger per segment🔗

guarantee

Rules.OneOrder.Ancillaries.choose_seats_one_seat_per_passenger
  (maps : List Rules.OneOrder.Ancillaries.SeatMap)
  (d d' : Rules.OneOrder.Ancillaries.ServiceDetails)
  (o o' : Rules.OneOrder.Order)
  (cs : List Rules.OneOrder.Ancillaries.SeatChoice)
  (h0 :
    ∀ a ∈ Rules.OneOrder.Ancillaries.seatsHeld d o,
      ∀ b ∈ Rules.OneOrder.Ancillaries.seatsHeld d o,
        a.passenger = b.passenger →
          a.segment = b.segment → a.seat = b.seat)
  (hmap :
    ∀ a ∈ Rules.OneOrder.Ancillaries.seatsHeld d o,
      ∀ m ∈ maps, m.segment = a.segment → a.seat ∉ m.available)
  (h :
    Rules.OneOrder.Ancillaries.chooseSeats maps d o cs =
      Except.ok (o', d'))
  (a : Rules.OneOrder.Ancillaries.SeatAssignment) :
  a ∈ Rules.OneOrder.Ancillaries.seatsHeld d' o' →
    ∀ b ∈ Rules.OneOrder.Ancillaries.seatsHeld d' o',
      a.passenger = b.passenger →
        a.segment = b.segment → a.seat = b.seat
Rules.OneOrder.Ancillaries.choose_seats_one_seat_per_passenger
  (maps :
    List
      Rules.OneOrder.Ancillaries.SeatMap)
  (d d' :
    Rules.OneOrder.Ancillaries.ServiceDetails)
  (o o' : Rules.OneOrder.Order)
  (cs :
    List
      Rules.OneOrder.Ancillaries.SeatChoice)
  (h0 :
    ∀
      a ∈
        Rules.OneOrder.Ancillaries.seatsHeld
          d o,
      ∀
        b ∈
          Rules.OneOrder.Ancillaries.seatsHeld
            d o,
        a.passenger = b.passenger →
          a.segment = b.segment →
            a.seat = b.seat)
  (hmap :
    ∀
      a ∈
        Rules.OneOrder.Ancillaries.seatsHeld
          d o,
      ∀ m ∈ maps,
        m.segment = a.segment →
          a.seat ∉ m.available)
  (h :
    Rules.OneOrder.Ancillaries.chooseSeats
        maps d o cs =
      Except.ok (o', d'))
  (a :
    Rules.OneOrder.Ancillaries.SeatAssignment) :
  a ∈
      Rules.OneOrder.Ancillaries.seatsHeld
        d' o' →
    ∀
      b ∈
        Rules.OneOrder.Ancillaries.seatsHeld
          d' o',
      a.passenger = b.passenger →
        a.segment = b.segment →
          a.seat = b.seat

When each passenger holds at most one seat on each segment, and the seat maps mark no held seat available, an accepted seat request keeps it so.

Open question for the business. The guide does not say whether choosing a seat replaces a seat the passenger already holds. A passenger who holds 12B and chooses 14A in a second request holds both, each in its own active order item. The example secondSeatSamePassenger shows it. May a passenger hold an extra seat, for comfort or for a large instrument, and does choosing a new seat cancel the old one, with what refund?

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

Checks acceptance criteria ONE-605.4.

40.3. Examples🔗

40.3.1. Occupied seat refused🔗

example

Rules.OneOrder.Ancillaries.occupiedSeatRefused :
  Rules.OneOrder.Ancillaries.SeatCase
Rules.OneOrder.Ancillaries.occupiedSeatRefused :
  Rules.OneOrder.Ancillaries.SeatCase

Given PAX01 holds seat 12B on SEG1, and the seat map marks 12C and 14A available.

When the seller chooses 12B for PAX02.

Then the request is refused: the seat map does not mark 12B available.

What Lean computed:

Refusal: not available SEG1 12B
Held: see the table below.

Held:

Passenger	Segment	Seat
PAX01	SEG1	12B

Checks acceptance criteria ONE-605.1.

40.3.2. Same seat twice🔗

example

Rules.OneOrder.Ancillaries.sameSeatTwice :
  Rules.OneOrder.Ancillaries.SeatCase
Rules.OneOrder.Ancillaries.sameSeatTwice :
  Rules.OneOrder.Ancillaries.SeatCase

Given two passengers on flight SEG1 with no seats, and a seat map that marks 12B available.

When the seller chooses 12B for PAX01 and 12B for PAX02 in one request.

Then both choices pass the seat map, and both passengers hold seat 12B on SEG1.

What Lean computed:

Refusal: none
Held: see the table below.

Held:

Passenger	Segment	Seat
PAX01	SEG1	12B
PAX02	SEG1	12B

Checks acceptance criteria ONE-605.2, ONE-605.3.

40.3.3. Second seat same passenger🔗

example

Rules.OneOrder.Ancillaries.secondSeatSamePassenger :
  Rules.OneOrder.Ancillaries.SeatCase
Rules.OneOrder.Ancillaries.secondSeatSamePassenger :
  Rules.OneOrder.Ancillaries.SeatCase

Given PAX01 holds seat 12B on SEG1, and the seat map marks 12C and 14A available.

When the seller chooses 14A for PAX01 in a second request.

Then the choice passes the seat map, and PAX01 holds both 12B and 14A on SEG1, each in its own order item.

What Lean computed:

Refusal: none
Held: see the table below.

Held:

Passenger	Segment	Seat
PAX01	SEG1	12B
PAX01	SEG1	14A

Checks acceptance criteria ONE-605.2, ONE-605.4.

40.4. Open question🔗

The guarantee One passenger per seat is open: the example Same seat twice shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

40.5. Open question🔗

The guarantee One seat per passenger per segment is open: the example Second seat same passenger shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.