58. Questions from the ONE Order rules🔗
59 guarantees are open in the ONE Order rules. Each is a place where IATA's public material is vague or silent, so the rule as written allows a case the guarantee forbids. An example the build computes shows that case, and the question under it is for the business to answer. The model does not decide it.
58.1. Each item has exactly one status🔗
🔗open question
Each order item has exactly one status, active, cancelled or closed.
Open question for the business. The guide's three conditions overlap and
leave gaps. An item whose one service was delivered and then transferred to
another item meets both the cancelled condition (every service transferred,
none holding value) and the closed condition (a service delivered, the rest
delivered or removed). The example deliveredThenTransferred shows it.
Which status wins, and should a delivered service be transferable at all?
It checks acceptance criteria ONE-002.4 of requirement ONE-002, Order item status.
58.2. Every order is opened or closed🔗
🔗open question
Every order with at least one service is opened or closed.
Open question for the business. The guide closes an order only when every
service is delivered or removed, and keeps it opened only while a service
holds value. It does not say whether an expired, not claimed or failed
service holds value. Under a reading where an expired service holds none, an
order whose only service expired is neither opened nor closed. The example
expiredService shows it. Does an expired service hold value, and
should an order with one be closed?
It checks acceptance criteria ONE-003.4 of requirement ONE-003, Order status.
58.3. Payment before delivery starts🔗
🔗open question
A service that starts REQUESTED or CONFIRMED never reaches READY TO PROCEED,
READY TO DELIVER, IN PROGRESS or DELIVERED while no payment for it has
succeeded, whatever other events happen to it.
Open question for the business. The sources treat READY TO PROCEED as the
payment gate but never forbid delivery from CONFIRMED, and they do not say
whether an UNABLE TO DELIVER service returns to READY TO PROCEED once the
constraint lifts. Under a reading that allows either move, a service nobody
paid for is delivered. The examples deliveredBeforePayment and
unpaidAfterForceMajeure show it. May delivery start before payment,
and when an UNABLE TO DELIVER service can be delivered again, does it return
to the status it left or to READY TO PROCEED?
It checks acceptance criteria ONE-101.4 of requirement ONE-101, Moves between delivery statuses.
58.4. Orders whose services are all final are closed🔗
🔗open question
An order whose services have all reached a final delivery status is closed,
under every reading of the guide.
Open question for the business. The guide closes an order only when every
service is DELIVERED or REMOVED. EXPIRED, NOT CLAIMED and FAILED TO DELIVER
are final too, but an order whose services end in them is never closed. Under
a reading where such a service holds value the order stays opened for good;
under one where it holds none the order has no status. The examples
noShowOrder and failedDeliveryOrder show it. Should an order
close once every service is final, and do EXPIRED, NOT CLAIMED and FAILED TO
DELIVER hold value?
It checks acceptance criteria ONE-103.4 of requirement ONE-103, Final delivery statuses.
58.5. Due amounts net to the difference🔗
🔗open question
For every change or cancellation the airline prices, the amount due to the
airline less the amount due by the airline is the new price, less the old
price, plus the penalty, plus the forfeited amount.
Open question for the business. Two cases break it. When the seller asks to
keep the value of cancelled items for later use, the guide shows both due
amounts as zero, while the formula gives the whole refundable value as due by
the airline; the example respendCancellation shows it. Under the reading
that waives a penalty above the refundable value, the airline charges less
than the penalty, so the formula overstates what the customer pays; the
example penaltyAboveRefund shows it. Should the value held for later use
count as the new price, and is a penalty above the refundable value collected
or waived?
It checks acceptance criteria ONE-201.5 of requirement ONE-201, Price differential of a change.
58.6. Cancelling leaves the customer owing nothing🔗
🔗open question
A cancellation never leaves the customer owing the airline money: the
amount due to the airline is no larger than the amount due by the airline,
when the forfeited amount is part of the old price.
Open question for the business. Under the reading that collects the whole
penalty, a penalty larger than the refundable value leaves the customer
owing the difference. The example penaltyAboveRefund shows it: a 1,000.00
order with 20.00 forfeited and a 1,000.00 penalty leaves 20.00 due to the
airline on a cancellation. Under the other reading the guarantee holds, but
the due amounts no longer net to the formula of ONE-201.5. Is a penalty
capped at the refundable value, or is the excess collected?
It checks acceptance criteria ONE-202.4 of requirement ONE-202, Amounts due to and by the airline.
58.7. Orders cancelled at once are closed🔗
🔗open question
An order cancelled at once has every item cancelled and is closed, under
every reading of the guide.
Open question for the business. A cancellation removes each service through
the delivery status table, and the table has no move to REMOVED from
REQUESTED or from UNABLE TO DELIVER, under any reading. A service the
airline has not yet confirmed therefore stays REQUESTED, and its item is not
cancelled. The example unpaidCancellationWhileRequested shows it. A
service UNABLE TO DELIVER, such as one on a flight the airline cancelled,
stays too, so cancelling that order never closes it. Under the readings that
refuse to cancel a service IN PROGRESS, or that allow delivery before
payment, a service IN PROGRESS or already DELIVERED stays as well. Can a
seller cancel a service the airline is still deciding on, or one the airline
cannot deliver, and what delivery status does it take?
It checks acceptance criteria ONE-203.2 of requirement ONE-203, Cancelling an order.
58.8. Cancellation offers stay within payments🔗
🔗open question
A cancellation offer never makes the amount due by the airline larger than
the payments received for the order.
Open question for the business. The offer is priced from the price of the
order's live items, as in the worked examples, and the payments received do
not enter it. A partly paid order is cancelled through an offer that returns
its whole price. The example partlyPaidCancellation shows it: a
1,000.00 order with 300.00 received gets an offer of 1,000.00 due by the
airline. Is the refundable amount capped at the payments received, and which
route applies when some items are paid and others are not?
It checks acceptance criteria ONE-203.4 of requirement ONE-203, Cancelling an order.
58.9. Transferred originals hold no value🔗
🔗open question
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?
It checks acceptance criteria ONE-204.5 of requirement ONE-204, Changing an order item.
58.10. Order balance after servicing🔗
🔗open question
A balanced order stays balanced when a paid change of one of its items is
made and its price differential settled, under every reading of the guide.
Open question for the business. After a change that keeps a service, the
original item still holds value (see ONE-204.5), so its price still counts as
live next to the new item's price. The example changeBalance shows it:
a 1,000.00 trip changed to a 900.00 trip keeping the outbound flight, with a
40.00 penalty and 120.00 forfeited, leaves 1,060.00 paid against 1,900.00 of
live items plus 160.00 recorded. The same change with nothing kept balances.
A request to keep value for later use, or a waived penalty above the
refundable value, breaks it too, for the reasons given under ONE-201.5.
Should the original item stop counting once the change is paid, and how does
a change accepted but not yet paid enter the balance?
It checks acceptance criteria ONE-205.3 of requirement ONE-205, Money recorded on an order.
58.11. Settled payments keep their status🔗
🔗open questionRules.OneOrder.Payment.recordOutcome_settled_final
(r : Rules.OneOrder.Payment.OutcomeReading)
(p : Rules.OneOrder.Payment.Transaction) (ref : String)
(s : Rules.OneOrder.Payment.PaymentStatus)
(h :
p.status = Rules.OneOrder.Payment.PaymentStatus.successful ∨
p.status = Rules.OneOrder.Payment.PaymentStatus.failed) :
(Rules.OneOrder.Payment.recordOutcome r p ref s).status = p.status Rules.OneOrder.Payment.recordOutcome_settled_final
(r :
Rules.OneOrder.Payment.OutcomeReading)
(p : Rules.OneOrder.Payment.Transaction)
(ref : String)
(s :
Rules.OneOrder.Payment.PaymentStatus)
(h :
p.status =
Rules.OneOrder.Payment.PaymentStatus.successful ∨
p.status =
Rules.OneOrder.Payment.PaymentStatus.failed) :
(Rules.OneOrder.Payment.recordOutcome r
p ref s).status =
p.status
A SUCCESSFUL or FAILED payment keeps its status whatever outcome the airline
later reports for one of its methods.
Open question for the business. The guide says a PENDING payment moves to
SUCCESSFUL or FAILED and does not say whether either is final. Under a reading
where a card chargeback turns a successful transaction into a failed one, a
SUCCESSFUL payment becomes FAILED; the example chargeback shows it.
Under a reading where a redirected payment completed after the airline marked
it failed is recorded, a FAILED payment becomes SUCCESSFUL; the example
lateRedirectCapture shows it. Can a SUCCESSFUL payment later fail, can
a FAILED payment later succeed, and what then happens to the order items it
covers?
It checks acceptance criteria ONE-303.3 of requirement ONE-303, Payment status and its moves.
58.12. Time limit on unpaid items🔗
🔗open questionRules.OneOrder.Payment.unpaid_item_removed_eventually
(m : Rules.OneOrder.Delivery.MoveReading)
(r : Rules.OneOrder.Payment.Removal)
(o : Rules.OneOrder.Payment.PayableOrder)
(pi : Rules.OneOrder.Payment.PayableItem) (hpi : pi ∈ o.items)
(hunpaid :
Rules.OneOrder.Payment.isPaid o.payments pi.item.id = false) :
∃ t,
∀ now ≥ t,
Rules.OneOrder.Payment.PayableItem.remove m r pi ∈
(Rules.OneOrder.Payment.expireUnpaid m r now o).items Rules.OneOrder.Payment.unpaid_item_removed_eventually
(m :
Rules.OneOrder.Delivery.MoveReading)
(r : Rules.OneOrder.Payment.Removal)
(o :
Rules.OneOrder.Payment.PayableOrder)
(pi :
Rules.OneOrder.Payment.PayableItem)
(hpi : pi ∈ o.items)
(hunpaid :
Rules.OneOrder.Payment.isPaid
o.payments pi.item.id =
false) :
∃ t,
∀ now ≥ t,
Rules.OneOrder.Payment.PayableItem.remove
m r pi ∈
(Rules.OneOrder.Payment.expireUnpaid
m r now o).items
An unpaid order item does not stay in the order indefinitely: from some
instant on, the time limit rule removes it.
Open question for the business. The rule removes an item only when its
payment time limit passes, and the guide lets an airline create an order item
without one. The ARMI guidance expects a limit on every unpaid item, while the
EASD guide says a missing limit only means the airline gave no advice. An item
without a limit is never removed and holds its services with nothing paid; the
example noTimeLimit shows it a year after the order was created. May
an unpaid order item exist without a payment time limit, and if so, may it stay
unpaid indefinitely?
It checks acceptance criteria ONE-306.5 of requirement ONE-306, Unpaid item at its time limit.
58.13. Removed items hold no value🔗
🔗open questionRules.OneOrder.Payment.removed_item_holds_no_value
(m : Rules.OneOrder.Delivery.MoveReading)
(v : Rules.OneOrder.ValueReading) (r : Rules.OneOrder.Payment.Removal)
(now : Rules.Core.Instant) (o : Rules.OneOrder.Payment.PayableOrder)
(pi : Rules.OneOrder.Payment.PayableItem) (hpi : pi ∈ o.items)
(hl : o.lapses now pi = true) :
Rules.OneOrder.OrderItem.isActive v
(Rules.OneOrder.Payment.PayableItem.remove m r pi).item =
false Rules.OneOrder.Payment.removed_item_holds_no_value
(m :
Rules.OneOrder.Delivery.MoveReading)
(v : Rules.OneOrder.ValueReading)
(r : Rules.OneOrder.Payment.Removal)
(now : Rules.Core.Instant)
(o :
Rules.OneOrder.Payment.PayableOrder)
(pi :
Rules.OneOrder.Payment.PayableItem)
(hpi : pi ∈ o.items)
(hl : o.lapses now pi = true) :
Rules.OneOrder.OrderItem.isActive v
(Rules.OneOrder.Payment.PayableItem.remove
m r pi).item =
false
An order item removed at its payment time limit holds no value: none of its
services holds value afterwards.
Open question for the business. The guide says such an item is removed and
names no resulting statuses. If its services become REMOVED, none holds value
under every reading of the guide. If they become EXPIRED, whether they hold
value is itself unsettled: under the cautious reading an expired service holds
value, so the removed item stays active and keeps its order opened. If they
become REMOVED HOLD VALUE, they hold value under every reading. The example
removalStatuses shows all three. Which delivery status does an item's
service take when its payment time limit passes unpaid?
It checks acceptance criteria ONE-306.6 of requirement ONE-306, Unpaid item at its time limit.
58.14. Every order holds a mandatory item🔗
🔗open question
Every accepted selection includes at least one item the offer marks
mandatory.
Open question for the business. The guidance asks for at least one mandatory
item in each offer and exempts a la carte offers. When an offer marks no item
mandatory, every selection of its items is accepted, so a seat can be ordered
without the flight it belongs to. The example seatWithoutFlight shows
it. Which selections are allowed from an offer that marks no item mandatory,
and may a seat or a bag be ordered without its flight?
It checks acceptance criteria ONE-401.4 of requirement ONE-401, Selecting items from an offer.
58.15. Order items match the selection🔗
🔗open questionRules.OneOrder.Creation.create_items_match_selection
(m : Rules.OneOrder.Creation.MultiOfferHandling)
(offers : List Rules.OneOrder.Creation.MarkedOffer)
(req : List Rules.OneOrder.Creation.Selection)
(now : Rules.Core.Instant) (orderId : String)
(ord : Rules.OneOrder.Order)
(h :
Rules.OneOrder.Creation.createOrder m offers req now orderId =
Except.ok ord) :
ord.items =
List.flatMap
(fun s ↦
List.map
(Rules.OneOrder.toOrderItem
(Rules.OneOrder.Creation.itemPrefix orderId s.offer))
(Rules.OneOrder.Creation.selectedFrom offers s))
req Rules.OneOrder.Creation.create_items_match_selection
(m :
Rules.OneOrder.Creation.MultiOfferHandling)
(offers :
List
Rules.OneOrder.Creation.MarkedOffer)
(req :
List
Rules.OneOrder.Creation.Selection)
(now : Rules.Core.Instant)
(orderId : String)
(ord : Rules.OneOrder.Order)
(h :
Rules.OneOrder.Creation.createOrder m
offers req now orderId =
Except.ok ord) :
ord.items =
List.flatMap
(fun s ↦
List.map
(Rules.OneOrder.toOrderItem
(Rules.OneOrder.Creation.itemPrefix
orderId s.offer))
(Rules.OneOrder.Creation.selectedFrom
offers s))
req
An accepted request becomes an order whose items are, for each selection
in turn, the items it selects from its offer and no others, under both
readings.
Open question for the business. The sources allow one request to select from
several offers and do not say what happens when one of them is rejected.
Under the reading where the selections that pass go ahead, the items selected
from a rejected offer are left out of the order. The example
oneOfferExpired shows it: the return flight selected from an expired
offer has no order item. Does a rejected offer reject the whole request, or
do the offers that pass go ahead?
It checks acceptance criteria ONE-402.1 of requirement ONE-402, Creating one order from several offers.
58.16. Order price is the sum of the selected items🔗
🔗open question
An order created from offers priced in one currency has a total in that
currency, the sum of the prices of the selected items, under both readings.
Open question for the business. Under the reading where the selections that
pass go ahead, the items selected from a rejected offer are left out, and the
order costs less than the items selected. The example oneOfferExpired
shows it: the selected items cost 780.00 EUR and the order 400.00 EUR. Does a
rejected offer reject the whole request, or do the offers that pass go
ahead?
It checks acceptance criteria ONE-402.2 of requirement ONE-402, Creating one order from several offers.
58.17. Atomic order creation🔗
🔗open questionRules.OneOrder.Creation.create_rejects_expired
(m : Rules.OneOrder.Creation.MultiOfferHandling)
(offers : List Rules.OneOrder.Creation.MarkedOffer)
(req : List Rules.OneOrder.Creation.Selection)
(now : Rules.Core.Instant) (orderId : String)
(s : Rules.OneOrder.Creation.Selection) (hs : s ∈ req)
(o : Rules.OneOrder.Creation.MarkedOffer)
(ho : List.find? (fun x ↦ x.offer.id == s.offer) offers = some o)
(hexp : now ≥ o.offer.expiresAt) :
∃ e,
Rules.OneOrder.Creation.createOrder m offers req now orderId =
Except.error e Rules.OneOrder.Creation.create_rejects_expired
(m :
Rules.OneOrder.Creation.MultiOfferHandling)
(offers :
List
Rules.OneOrder.Creation.MarkedOffer)
(req :
List
Rules.OneOrder.Creation.Selection)
(now : Rules.Core.Instant)
(orderId : String)
(s : Rules.OneOrder.Creation.Selection)
(hs : s ∈ req)
(o :
Rules.OneOrder.Creation.MarkedOffer)
(ho :
List.find?
(fun x ↦ x.offer.id == s.offer)
offers =
some o)
(hexp : now ≥ o.offer.expiresAt) :
∃ e,
Rules.OneOrder.Creation.createOrder m
offers req now orderId =
Except.error e
A request that names an offer which has expired at the instant of the
request is rejected as a whole, under both readings: no order is created.
Open question for the business. The sources allow one request to select from
several offers and do not say what happens when one of them has expired or
fails its checks. Under the reading where the selections that pass go ahead,
an order is created from the valid offer alone, and the customer holds half
of a trip chosen as a whole. The example oneOfferExpired shows it.
Does a rejected offer reject the whole request, or do the offers that pass go
ahead?
It checks acceptance criteria ONE-402.3 of requirement ONE-402, Creating one order from several offers.
58.18. Order total from item prices🔗
🔗open questionRules.OneOrder.Creation.create_single_currency
(m : Rules.OneOrder.Creation.MultiOfferHandling)
(offers : List Rules.OneOrder.Creation.MarkedOffer)
(req : List Rules.OneOrder.Creation.Selection)
(now : Rules.Core.Instant) (orderId : String)
(ord : Rules.OneOrder.Order)
(h :
Rules.OneOrder.Creation.createOrder m offers req now orderId =
Except.ok ord) :
∃ c, (Rules.OneOrder.Change.orderPrice ord c).isSome = true Rules.OneOrder.Creation.create_single_currency
(m :
Rules.OneOrder.Creation.MultiOfferHandling)
(offers :
List
Rules.OneOrder.Creation.MarkedOffer)
(req :
List
Rules.OneOrder.Creation.Selection)
(now : Rules.Core.Instant)
(orderId : String)
(ord : Rules.OneOrder.Order)
(h :
Rules.OneOrder.Creation.createOrder m
offers req now orderId =
Except.ok ord) :
∃ c,
(Rules.OneOrder.Change.orderPrice ord
c).isSome =
true
Every order created has a total price in a single currency, under both
readings.
Open question for the business. Each offer is checked for its own currency,
and a request may select from offers priced in different currencies. The
order then holds items in two currencies, and its item prices have no sum.
The example twoCurrencies shows it: a flight priced in EUR and a hotel
transfer priced in USD go into one order that has no total. May one order
hold items priced in more than one currency, and if so, what is its total?
It checks acceptance criteria ONE-402.5 of requirement ONE-402, Creating one order from several offers.
58.19. One order per offer🔗
🔗open questionRules.OneOrder.Creation.once_per_offer
(hd : Rules.OneOrder.Creation.RepeatHandling)
(m : Rules.OneOrder.Creation.MultiOfferHandling)
(book : List Rules.OneOrder.Creation.CreatedOrder)
(offers : List Rules.OneOrder.Creation.MarkedOffer)
(req : List Rules.OneOrder.Creation.Selection)
(now : Rules.Core.Instant) (orderId : String)
(ord : Rules.OneOrder.Order)
(book' : List Rules.OneOrder.Creation.CreatedOrder)
(hbook : Rules.OneOrder.Creation.OncePerOffer book)
(h :
Rules.OneOrder.Creation.createOnce hd m book offers req now
orderId =
Except.ok (ord, book')) :
Rules.OneOrder.Creation.OncePerOffer book' Rules.OneOrder.Creation.once_per_offer
(hd :
Rules.OneOrder.Creation.RepeatHandling)
(m :
Rules.OneOrder.Creation.MultiOfferHandling)
(book :
List
Rules.OneOrder.Creation.CreatedOrder)
(offers :
List
Rules.OneOrder.Creation.MarkedOffer)
(req :
List
Rules.OneOrder.Creation.Selection)
(now : Rules.Core.Instant)
(orderId : String)
(ord : Rules.OneOrder.Order)
(book' :
List
Rules.OneOrder.Creation.CreatedOrder)
(hbook :
Rules.OneOrder.Creation.OncePerOffer
book)
(h :
Rules.OneOrder.Creation.createOnce hd
m book offers req now orderId =
Except.ok (ord, book')) :
Rules.OneOrder.Creation.OncePerOffer
book'
No offer ever produces two orders: once an offer appears in a recorded
order, no request adds another order for it.
Open question for the business. The sources do not say that creating an
order uses up its offer. Under the reading where the airline creates another
order for a repeated request, a request sent again after a timeout gives the
customer a second order from the same offer. The example
repeatedRequest shows it. Does creating an order use up its offer, and
how does the airline recognize a request it has already answered?
It checks acceptance criteria ONE-403.4 of requirement ONE-403, Repeated create requests.
58.20. History rebuilds every version🔗
🔗open questionRules.OneOrder.Creation.history_rebuilds_current
(l : Rules.OneOrder.Creation.HistoryListing)
(o : Rules.OneOrder.Order)
(gs : List Rules.OneOrder.Creation.ChangeGroup) :
(Rules.OneOrder.Creation.orderHistory l
(Rules.OneOrder.Creation.OrderRecord.after o gs)).rebuild =
(Rules.OneOrder.Creation.OrderRecord.after o gs).current Rules.OneOrder.Creation.history_rebuilds_current
(l :
Rules.OneOrder.Creation.HistoryListing)
(o : Rules.OneOrder.Order)
(gs :
List
Rules.OneOrder.Creation.ChangeGroup) :
(Rules.OneOrder.Creation.orderHistory l
(Rules.OneOrder.Creation.OrderRecord.after
o gs)).rebuild =
(Rules.OneOrder.Creation.OrderRecord.after
o gs).current
Applying the change groups of an order's history to the order at version
1, in the order listed, gives the order as it is now, under both readings.
Open question for the business. The guide lists change groups oldest first,
each raising the version by one, while the capability page for order history
lists them newest first and says each lowers the version. Applied newest
first, a group that removes an item runs before the group that added it, and
the item comes back. The example newestFirstHistory shows it. In
which order does the history list its change groups, and does a history
requested from version v include the group that produced v?
It checks acceptance criteria ONE-404.5 of requirement ONE-404, Recording changes to an order.
58.21. Changes on a stale version are rejected🔗
🔗open questionRules.OneOrder.Creation.stale_rejected
(s : Rules.OneOrder.Creation.StaleHandling)
(r : Rules.OneOrder.Creation.OrderRecord) (v : ℕ)
(g : Rules.OneOrder.Creation.ChangeGroup) (hv : v ≠ r.version) :
∃ e,
Rules.OneOrder.Creation.requestChange s r (some v) g =
Except.error e Rules.OneOrder.Creation.stale_rejected
(s :
Rules.OneOrder.Creation.StaleHandling)
(r :
Rules.OneOrder.Creation.OrderRecord)
(v : ℕ)
(g :
Rules.OneOrder.Creation.ChangeGroup)
(hv : v ≠ r.version) :
∃ e,
Rules.OneOrder.Creation.requestChange
s r (some v) g =
Except.error e
A change that carries a version other than the order's current version is
rejected, under both readings.
Open question for the business. The guide lets the airline return an error
when the versions differ and does not require it. Under the reading where
the airline applies the change anyway, a seller who saw an older version
overwrites a change it never saw. The example twoSellersOneVersion
shows it. Does a version mismatch always reject the change, and may a change
be sent without a version?
It checks acceptance criteria ONE-405.3 of requirement ONE-405, Change against a stale version.
58.22. Orders holding value stay accessible🔗
🔗open question
An order is kept while it has an active item, under every reading and
every count of months.
Open question for the business. The resolution asks for 13 months from
creation and 13 months from first usage, and nothing after both have passed.
An item whose services are removed with their value held stays active for as
long as the customer does not use the value. The example
storedValueNeverUsed shows it: two years after creation the order still
holds value and no longer has to be kept. What are an open item and first
usage, and must an order that still holds value stay accessible?
It checks acceptance criteria ONE-406.4 of requirement ONE-406, Order retention.
58.23. Guaranteed prices only on offers that can be accepted🔗
🔗open question
An offer item's price is guaranteed only at instants at which the offer can
still be accepted.
Open question for the business. The guide says a price is guaranteed until its
time limit and does not say whether the limit's own instant is inside. An
offer is rejected as expired at its expiry instant. Under the reading that a
guarantee still holds at its instant, an item whose price guarantee ends at
the same instant as the offer has a guaranteed price at an instant when the
offer can no longer be accepted. The example guaranteeAtExpiry shows
it. Does a price guarantee still hold at the instant its time limit
names?
It checks acceptance criteria ONE-501.5 of requirement ONE-501, Price guarantee at an instant.
58.24. No order at a lapsed price🔗
🔗open questionRules.OneOrder.Offers.createOrder_price_guaranteed
(r : Rules.OneOrder.Offers.CreationReading)
(o : Rules.OneOrder.Offers.TimedOffer) (now : Rules.Core.Instant)
(orderId : String) (n : Rules.OneOrder.Offers.NewOrder)
(h : Rules.OneOrder.Offers.createOrder r o now orderId = Except.ok n)
(oi : Rules.OneOrder.Offers.TimedOfferItem) :
oi ∈ o.items →
Rules.OneOrder.Offers.TimedOffer.guaranteeLapsed r.guaranteeEnd o oi
now =
false Rules.OneOrder.Offers.createOrder_price_guaranteed
(r :
Rules.OneOrder.Offers.CreationReading)
(o : Rules.OneOrder.Offers.TimedOffer)
(now : Rules.Core.Instant)
(orderId : String)
(n : Rules.OneOrder.Offers.NewOrder)
(h :
Rules.OneOrder.Offers.createOrder r o
now orderId =
Except.ok n)
(oi :
Rules.OneOrder.Offers.TimedOfferItem) :
oi ∈ o.items →
Rules.OneOrder.Offers.TimedOffer.guaranteeLapsed
r.guaranteeEnd o oi now =
false
No order is created at the offered price while the price guarantee of one
of the offer's items has lapsed.
Open question for the business. The guide recommends repricing into a new
offer when a price guarantee has lapsed, and does not say what the airline
must do when the customer accepts the offer before it expires. Under the
reading that creates the order at the offered price, an offer whose
30 minute price guarantee lapsed is accepted at the offered price one minute
before the offer expires. The example lapsedGuaranteeAccepted shows
it. Is acceptance in this window refused, sent back for a new offer, or
honoured at the offered price?
It checks acceptance criteria ONE-502.4 of requirement ONE-502, Time limits of a new order.
58.25. No order item overdue at creation🔗
🔗open questionRules.OneOrder.Offers.createOrder_limit_not_before_creation
(r : Rules.OneOrder.Offers.CreationReading)
(o : Rules.OneOrder.Offers.TimedOffer) (now : Rules.Core.Instant)
(orderId : String) (n : Rules.OneOrder.Offers.NewOrder)
(h : Rules.OneOrder.Offers.createOrder r o now orderId = Except.ok n)
(ni : Rules.OneOrder.Offers.NewOrderItem) :
ni ∈ n.items →
∀ (t : Rules.Core.Instant), ni.paymentBy = some t → n.createdAt ≤ t Rules.OneOrder.Offers.createOrder_limit_not_before_creation
(r :
Rules.OneOrder.Offers.CreationReading)
(o : Rules.OneOrder.Offers.TimedOffer)
(now : Rules.Core.Instant)
(orderId : String)
(n : Rules.OneOrder.Offers.NewOrder)
(h :
Rules.OneOrder.Offers.createOrder r o
now orderId =
Except.ok n)
(ni :
Rules.OneOrder.Offers.NewOrderItem) :
ni ∈ n.items →
∀ (t : Rules.Core.Instant),
ni.paymentBy = some t →
n.createdAt ≤ t
No order item starts with a payment time limit before the order's
creation.
Open question for the business. An offer item may state its payment time limit
as a fixed date and time, and the guide does not say what happens when that
instant has passed by the time the order is created. The rule copies the
instant, so the order item is overdue the moment it exists. The example
fixedLimitBeforeCreation shows it. Is such an acceptance refused, or
does the order item get a new payment time limit?
It checks acceptance criteria ONE-502.5 of requirement ONE-502, Time limits of a new order.
58.26. Payment due at creation can be made🔗
🔗open questionRules.OneOrder.Offers.zero_duration_payable
(r : Rules.OneOrder.Offers.CreationReading)
(o : Rules.OneOrder.Offers.TimedOffer) (now : Rules.Core.Instant)
(orderId : String) (n : Rules.OneOrder.Offers.NewOrder)
(h : Rules.OneOrder.Offers.createOrder r o now orderId = Except.ok n)
(hz :
∀ oi ∈ o.items,
oi.limits.payWithin = some 0 ∧ oi.limits.payBy = none)
(p : Rules.OneOrder.Payment.Transaction) :
Rules.OneOrder.Payment.acceptPayment n.payable p n.createdAt ≠
Except.error Rules.OneOrder.Payment.PaymentRejection.timeLimitPassed Rules.OneOrder.Offers.zero_duration_payable
(r :
Rules.OneOrder.Offers.CreationReading)
(o : Rules.OneOrder.Offers.TimedOffer)
(now : Rules.Core.Instant)
(orderId : String)
(n : Rules.OneOrder.Offers.NewOrder)
(h :
Rules.OneOrder.Offers.createOrder r o
now orderId =
Except.ok n)
(hz :
∀ oi ∈ o.items,
oi.limits.payWithin = some 0 ∧
oi.limits.payBy = none)
(p :
Rules.OneOrder.Payment.Transaction) :
Rules.OneOrder.Payment.acceptPayment
n.payable p n.createdAt ≠
Except.error
Rules.OneOrder.Payment.PaymentRejection.timeLimitPassed
An order item whose offer item's payment time limit is a duration of zero
can be paid at the instant the order is created.
Open question for the business. The guide says a payment time limit of zero
means payment is due at order creation. The rule sets the order item's limit
to the creation instant, and the payment rule of ONE-304 rejects a payment
made at or after the limit, so no payment for the item is ever on time. The
example zeroDurationPayment shows it. Is a payment made at the
creation instant on time, or must it come with the request that creates the
order?
It checks acceptance criteria ONE-502.6 of requirement ONE-502, Time limits of a new order.
58.27. Every stage with rules has a rule in force🔗
🔗open questionRules.OneOrder.Offers.ruleInForce_covers_stage
(e : Rules.OneOrder.Offers.ExpiryReading)
(rules : List Rules.OneOrder.Offers.Restriction)
(j : Rules.OneOrder.Offers.Journey) (a : Rules.OneOrder.Offers.Action)
(now : Rules.Core.Instant)
(h : ∃ r ∈ rules, r.action = a ∧ r.stage = j.stageAt now) :
(Rules.OneOrder.Offers.ruleInForce e rules j a now).isSome = true Rules.OneOrder.Offers.ruleInForce_covers_stage
(e :
Rules.OneOrder.Offers.ExpiryReading)
(rules :
List
Rules.OneOrder.Offers.Restriction)
(j : Rules.OneOrder.Offers.Journey)
(a : Rules.OneOrder.Offers.Action)
(now : Rules.Core.Instant)
(h :
∃ r ∈ rules,
r.action = a ∧
r.stage = j.stageAt now) :
(Rules.OneOrder.Offers.ruleInForce e
rules j a now).isSome =
true
While a journey is in a stage for which an action has rules, a rule is in
force for that action.
Open question for the business. A rule starts at its effective date, and the
guide does not say what applies in a stage before its first rule starts, or,
when expiration dates end rules, in a gap before the next rule starts. A
journey paid before its first rule for the stage before departure starts has
no rule in force, under both readings; under the reading that expiration dates
end rules, a rule whose effective and expiration dates are equal is never in
force. The example noRuleInForce shows both. What applies to a change
or cancellation when no rule of the stage is in force?
It checks acceptance criteria ONE-503.5 of requirement ONE-503, Restriction rule in force.
58.28. Taxes on a non-refundable fare🔗
🔗open questionRules.OneOrder.Offers.cancel_returns_refundable_charges
(e : Rules.OneOrder.Offers.ExpiryReading)
(ff : Rules.OneOrder.Offers.FullOrFixed)
(rules : List Rules.OneOrder.Offers.Restriction)
(j : Rules.OneOrder.Offers.Journey) (now : Rules.Core.Instant)
(item : Rules.OneOrder.Offers.CancelledItem) (m : Rules.Core.Money)
(o : Bool)
(h :
Rules.OneOrder.Offers.cancellationRefund e ff rules j now item =
Rules.OneOrder.Offers.RefundDecision.refund m o) :
item.refundableCharges ≤ m.amount Rules.OneOrder.Offers.cancel_returns_refundable_charges
(e :
Rules.OneOrder.Offers.ExpiryReading)
(ff : Rules.OneOrder.Offers.FullOrFixed)
(rules :
List
Rules.OneOrder.Offers.Restriction)
(j : Rules.OneOrder.Offers.Journey)
(now : Rules.Core.Instant)
(item :
Rules.OneOrder.Offers.CancelledItem)
(m : Rules.Core.Money) (o : Bool)
(h :
Rules.OneOrder.Offers.cancellationRefund
e ff rules j now item =
Rules.OneOrder.Offers.RefundDecision.refund
m o) :
item.refundableCharges ≤ m.amount
A voluntary cancellation of an unused item returns at least the taxes, fees
and charges in its price that are flagged refundable.
Open question for the business. The guide gives each tax, fee and charge its
own refund flag and gives each offer item cancel rules, and never says how the
two combine. The rule returns what the cancel rule gives, so a rule that
forbids cancellation returns nothing, and a fixed refund can be less than the
refundable taxes. The examples nonRefundableFareTaxes and
fullMarkedWithAmount show both. Does a cancel rule that returns
nothing also keep the taxes flagged refundable, and does a no show change the
answer?
It checks acceptance criteria ONE-505.5 of requirement ONE-505, Refund owed on voluntary cancellation.
58.29. Price total from its parts🔗
🔗open questionRules.OneOrder.Offers.price_adds_excluded_lines
(x : Rules.OneOrder.Offers.ExcludedTax)
(p : Rules.OneOrder.Offers.PriceParts)
(t : Rules.OneOrder.Offers.PriceTotal)
(h : Rules.OneOrder.Offers.priceTotal x p = Except.ok t) :
t.excludedTax.amount = p.lineExcluded Rules.OneOrder.Offers.price_adds_excluded_lines
(x : Rules.OneOrder.Offers.ExcludedTax)
(p : Rules.OneOrder.Offers.PriceParts)
(t : Rules.OneOrder.Offers.PriceTotal)
(h :
Rules.OneOrder.Offers.priceTotal x p =
Except.ok t) :
t.excludedTax.amount = p.lineExcluded
A totalled price adds the tax of every consumption tax line marked as not
included in it.
Open question for the business. The guide's examples state both the tax lines
and a total of excluded tax, and one example marks every HST line as not
included while stating an excluded total of zero. Under the reading that
trusts the stated total, that tax is left out of the price's total. The
example excludedTaxReadings shows the two readings differ by the whole
tax. When a line marked as not included and the stated total of excluded tax
disagree, which one does the price's total follow?
It checks acceptance criteria ONE-506.6 of requirement ONE-506, Totalling a price from its parts.
58.30. Every ancillary reaches its flight🔗
🔗open question
An ancillary for the same passenger and segment as a flight service of the
order is counted as dependent on it, under either reading.
Open question for the business. Under the reference reading only an
ancillary that names its flight counts. In the seat worked example the seat
services name no flight service, so a seat for the passenger on the flight is
not a dependent of it, and a change to the flight reports no impact on the
seat. The example seatWithoutReference shows it. Which link defines
the dependency: a reference to the parent, or the shared passenger and
segment? And may an ancillary depend on another ancillary, such as a lounge
pass on a premium seat?
It checks acceptance criteria ONE-601.4 of requirement ONE-601, Dependent service and its parent.
58.31. Ancillary needs a flight service🔗
🔗open questionRules.OneOrder.Ancillaries.change_keeps_flights
(m : Rules.OneOrder.Delivery.MoveReading)
(related : Rules.OneOrder.Ancillaries.ServiceKind → Bool)
(d : Rules.OneOrder.Ancillaries.ServiceDetails)
(o o' : Rules.OneOrder.Order) (c : Rules.OneOrder.Change.ItemChange)
(h0 : Rules.OneOrder.Ancillaries.uncovered related d o = [])
(h : Rules.OneOrder.Change.changeItem m o c = Except.ok o') :
Rules.OneOrder.Ancillaries.uncovered related d o' = [] Rules.OneOrder.Ancillaries.change_keeps_flights
(m :
Rules.OneOrder.Delivery.MoveReading)
(related :
Rules.OneOrder.Ancillaries.ServiceKind →
Bool)
(d :
Rules.OneOrder.Ancillaries.ServiceDetails)
(o o' : Rules.OneOrder.Order)
(c : Rules.OneOrder.Change.ItemChange)
(h0 :
Rules.OneOrder.Ancillaries.uncovered
related d o =
[])
(h :
Rules.OneOrder.Change.changeItem m o
c =
Except.ok o') :
Rules.OneOrder.Ancillaries.uncovered
related d o' =
[]
When every live flight-related ancillary of an order has a live flight
service for its passenger and segment, a paid change to an order item keeps it
so.
Open question for the business. The guide states the rule when an ancillary
is bought. A change that moves a passenger's flight to another segment
cancels the old flight service and leaves the bag bought for it confirmed, on
a segment the passenger no longer flies. The example
bagLeftByFlightChange shows it. Does the rule hold for the life of the
order, and if so, what happens to the bag?
It checks acceptance criteria ONE-602.4 of requirement ONE-602, Adding services to an order.
58.32. No live dependent of a cancelled flight🔗
🔗open questionRules.OneOrder.Ancillaries.cancel_items_no_live_dependents
(m : Rules.OneOrder.Delivery.MoveReading)
(h : Rules.OneOrder.Ancillaries.DependentHandling)
(r : Rules.OneOrder.Ancillaries.LinkReading)
(d : Rules.OneOrder.Ancillaries.ServiceDetails)
(allows : String → Bool) (o o' : Rules.OneOrder.Order)
(named : List String)
(hok :
Rules.OneOrder.Ancillaries.cancelItems m h r d allows o named =
Except.ok o')
(f : Rules.OneOrder.Service)
(hf : f ∈ Rules.OneOrder.Ancillaries.namedFlights d o named)
(s : Rules.OneOrder.Service)
(hs : s ∈ Rules.OneOrder.Ancillaries.services o')
(hdep : Rules.OneOrder.Ancillaries.dependsOn r d f s = true) :
Rules.OneOrder.Delivery.isLive s = false Rules.OneOrder.Ancillaries.cancel_items_no_live_dependents
(m :
Rules.OneOrder.Delivery.MoveReading)
(h :
Rules.OneOrder.Ancillaries.DependentHandling)
(r :
Rules.OneOrder.Ancillaries.LinkReading)
(d :
Rules.OneOrder.Ancillaries.ServiceDetails)
(allows : String → Bool)
(o o' : Rules.OneOrder.Order)
(named : List String)
(hok :
Rules.OneOrder.Ancillaries.cancelItems
m h r d allows o named =
Except.ok o')
(f : Rules.OneOrder.Service)
(hf :
f ∈
Rules.OneOrder.Ancillaries.namedFlights
d o named)
(s : Rules.OneOrder.Service)
(hs :
s ∈
Rules.OneOrder.Ancillaries.services
o')
(hdep :
Rules.OneOrder.Ancillaries.dependsOn r
d f s =
true) :
Rules.OneOrder.Delivery.isLive s = false
After a seller cancels a flight, no live service depends on it.
Open question for the business. Under the reading where the dependents stay
as they are, a cancelled flight leaves its bag confirmed on a segment the
passenger no longer flies. The example cancelFlightWithBag shows it.
The other two readings keep the guarantee when every live service of the order
can be removed (cancel_items_no_live_dependents_of_not_leave). A bag
still REQUESTED from the airline cannot be: the delivery status table has no
move from REQUESTED to REMOVED, so it stays live under every reading.
Should cancelling a flight cancel its bag and seat, refuse until the seller
names them, or leave them in place, and what happens to one the airline has
not yet confirmed?
It checks acceptance criteria ONE-603.4 of requirement ONE-603, Cancelling a flight with ancillaries.
58.33. Dependents keep their own conditions🔗
🔗open question
A live service of an item whose conditions do not allow cancellation is in
the order afterwards as it was.
Open question for the business. Under the reading where dependents are
cancelled with their flight, cancelling a flight cancels the extra bag bought
for it, although the bag's conditions do not allow cancellation, as in the add
bag worked example. The example cancelFlightWithBag shows it. The
other two readings keep the guarantee
(cancel_items_respects_conditions_of_not_cancel_with). Whose
conditions govern a dependent cancelled with its flight, and its refund: the
dependent's own or the flight's?
It checks acceptance criteria ONE-603.5 of requirement ONE-603, Cancelling a flight with ancillaries.
58.34. A cancellable item can be cancelled🔗
🔗open questionRules.OneOrder.Ancillaries.cancel_items_allowed
(m : Rules.OneOrder.Delivery.MoveReading)
(h : Rules.OneOrder.Ancillaries.DependentHandling)
(r : Rules.OneOrder.Ancillaries.LinkReading)
(d : Rules.OneOrder.Ancillaries.ServiceDetails)
(allows : String → Bool) (o : Rules.OneOrder.Order)
(i : Rules.OneOrder.OrderItem) (hi : i ∈ o.items)
(ha : allows i.id = true) :
∃ named,
i.id ∈ named ∧
∃ o',
Rules.OneOrder.Ancillaries.cancelItems m h r d allows o named =
Except.ok o' Rules.OneOrder.Ancillaries.cancel_items_allowed
(m :
Rules.OneOrder.Delivery.MoveReading)
(h :
Rules.OneOrder.Ancillaries.DependentHandling)
(r :
Rules.OneOrder.Ancillaries.LinkReading)
(d :
Rules.OneOrder.Ancillaries.ServiceDetails)
(allows : String → Bool)
(o : Rules.OneOrder.Order)
(i : Rules.OneOrder.OrderItem)
(hi : i ∈ o.items)
(ha : allows i.id = true) :
∃ named,
i.id ∈ named ∧
∃ o',
Rules.OneOrder.Ancillaries.cancelItems
m h r d allows o named =
Except.ok o'
An order item whose conditions allow cancellation can be cancelled by some
request that names it.
Open question for the business. Under the reading where a cancellation is
refused until the seller names the dependents too, a flight whose extra bag
may not be cancelled can never be cancelled: naming the flight alone is
refused for the bag, and naming the bag too is refused by the bag's
conditions. The example refuseUntilNamedBlocks shows it. The other
two readings keep the guarantee (cancel_items_allowed_of_not_refuse).
Should a dependent's conditions be able to stop its flight from being
cancelled?
It checks acceptance criteria ONE-603.6 of requirement ONE-603, Cancelling a flight with ancillaries.
58.35. Moved seats on the new flight🔗
🔗open questionRules.OneOrder.Ancillaries.replace_no_seat_clash
(e :
Rules.OneOrder.Ancillaries.ServiceKind →
Rules.OneOrder.Ancillaries.DependentEffect)
(r : Rules.OneOrder.Ancillaries.LinkReading)
(d : Rules.OneOrder.Ancillaries.ServiceDetails)
(o : Rules.OneOrder.Order) (f : Rules.OneOrder.Service)
(newSeg : String)
(held : List Rules.OneOrder.Ancillaries.SeatAssignment)
(a : Rules.OneOrder.Ancillaries.SeatAssignment)
(ha :
a ∈
Rules.OneOrder.Ancillaries.movedSeats d
(Rules.OneOrder.Ancillaries.replaceFlight e r d o f newSeg))
(b : Rules.OneOrder.Ancillaries.SeatAssignment) (hb : b ∈ held)
(hseg : b.segment = a.segment) (hseat : b.seat = a.seat) :
b.passenger = a.passenger Rules.OneOrder.Ancillaries.replace_no_seat_clash
(e :
Rules.OneOrder.Ancillaries.ServiceKind →
Rules.OneOrder.Ancillaries.DependentEffect)
(r :
Rules.OneOrder.Ancillaries.LinkReading)
(d :
Rules.OneOrder.Ancillaries.ServiceDetails)
(o : Rules.OneOrder.Order)
(f : Rules.OneOrder.Service)
(newSeg : String)
(held :
List
Rules.OneOrder.Ancillaries.SeatAssignment)
(a :
Rules.OneOrder.Ancillaries.SeatAssignment)
(ha :
a ∈
Rules.OneOrder.Ancillaries.movedSeats
d
(Rules.OneOrder.Ancillaries.replaceFlight
e r d o f newSeg))
(b :
Rules.OneOrder.Ancillaries.SeatAssignment)
(hb : b ∈ held)
(hseg : b.segment = a.segment)
(hseat : b.seat = a.seat) :
b.passenger = a.passenger
No seat moved by a flight replacement lands on a seat another passenger
holds on the new flight.
Open question for the business. Under a reading where seats move with their
flight, a seat keeps its number on the new flight, and nothing checks the new
flight's seat map. A passenger's paid seat 12C moves to a flight on which
another passenger already holds 12C. The example seatMovedOntoTakenSeat
shows it. What happens to a seat when its flight is replaced: does it move,
and to which seat, or is it refunded, stored or reshopped?
It checks acceptance criteria ONE-604.4 of requirement ONE-604, Dependents when a flight changes.
58.36. One passenger per seat🔗
🔗open questionRules.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?
It checks acceptance criteria ONE-605.3 of requirement ONE-605, Choosing seats.
58.37. One seat per passenger per segment🔗
🔗open questionRules.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?
It checks acceptance criteria ONE-605.4 of requirement ONE-605, Choosing seats.
58.38. One order item per a-la-carte offer item🔗
🔗open question
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?
It checks acceptance criteria ONE-606.5 of requirement ONE-606, Price of an a-la-carte selection.
58.39. A removal returns no more than the bundle price🔗
🔗open question
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?
It checks acceptance criteria ONE-607.3 of requirement ONE-607, Value of one bundled service.
58.40. Removing a whole bundle returns its price🔗
🔗open question
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?
It checks acceptance criteria ONE-607.4 of requirement ONE-607, Value of one bundled service.
58.42. Notices are resolved before departure🔗
🔗open questionRules.OneOrder.AirlineChange.resolved_before_departure
(r : Rules.OneOrder.AirlineChange.FollowUpReading)
(n : Rules.OneOrder.AirlineChange.ChangeNotice)
(h : n.followUps ≠ []) :
∃ t < n.departure,
(Rules.OneOrder.AirlineChange.consequenceAt r n t).isSome = true Rules.OneOrder.AirlineChange.resolved_before_departure
(r :
Rules.OneOrder.AirlineChange.FollowUpReading)
(n :
Rules.OneOrder.AirlineChange.ChangeNotice)
(h : n.followUps ≠ []) :
∃ t < n.departure,
(Rules.OneOrder.AirlineChange.consequenceAt
r n t).isSome =
true
A notice that offers follow-up actions is resolved before the affected
flight departs, even if the seller never answers.
Open question for the business. The sources make both the time limit and the
consequence optional, and do not tie the time limit to the departure. A
notice that offers Cancel with neither, like the guide's Cancel example, never
lapses; a time limit set after the departure lapses too late. The example
noticesAtDeparture shows both still unresolved when the flight departs.
What applies when a follow-up action has no time limit or no consequence, and
must the time limit fall before the affected flight departs?
It checks acceptance criteria ONE-702.4 of requirement ONE-702, Consequence of a missed time limit.
58.43. Penalty when declining an airline change🔗
🔗open questionRules.OneOrder.AirlineChange.decline_cancel_no_penalty
(e : Rules.OneOrder.Change.ExcessPenalty)
(w : Rules.OneOrder.AirlineChange.DeclineFees)
(inv : Rules.OneOrder.AirlineChange.InvoluntaryReading)
(n : Rules.OneOrder.AirlineChange.ChangeNotice)
(affected : Rules.Core.Money)
(t : Rules.OneOrder.AirlineChange.DeclineTerms)
(d : Rules.OneOrder.Change.PriceDifferential)
(hinv : inv.involuntary n.reason = true)
(h :
Rules.OneOrder.AirlineChange.declineOffer e w inv n affected t
Rules.OneOrder.AirlineChange.Decline.cancel =
Except.ok d) :
d.penalty.amount = 0 Rules.OneOrder.AirlineChange.decline_cancel_no_penalty
(e :
Rules.OneOrder.Change.ExcessPenalty)
(w :
Rules.OneOrder.AirlineChange.DeclineFees)
(inv :
Rules.OneOrder.AirlineChange.InvoluntaryReading)
(n :
Rules.OneOrder.AirlineChange.ChangeNotice)
(affected : Rules.Core.Money)
(t :
Rules.OneOrder.AirlineChange.DeclineTerms)
(d :
Rules.OneOrder.Change.PriceDifferential)
(hinv : inv.involuntary n.reason = true)
(h :
Rules.OneOrder.AirlineChange.declineOffer
e w inv n affected t
Rules.OneOrder.AirlineChange.Decline.cancel =
Except.ok d) :
d.penalty.amount = 0
A customer who declines an involuntary change through Cancel, or whose
seller lets it lapse into Auto-cancellation, pays no cancellation penalty.
Open question for the business. The sources offer Cancel as an answer to an
airline change and never say whether the airline's fees apply; the
cancellation page leaves penalties to the airline. Under the reading that
applies the item's fees, the 50 EUR cancellation fee of the itinerary change
worked example is charged for leaving a change the airline made. The example
declineByCancel shows it. Do the airline's cancellation fees apply
when the customer declines a change the airline imposed?
It checks acceptance criteria ONE-703.4 of requirement ONE-703, Declining an airline change.
58.44. Price of reshopping after airline change🔗
🔗open questionRules.OneOrder.AirlineChange.decline_reshop_no_fee
(e : Rules.OneOrder.Change.ExcessPenalty)
(w : Rules.OneOrder.AirlineChange.DeclineFees)
(inv : Rules.OneOrder.AirlineChange.InvoluntaryReading)
(n : Rules.OneOrder.AirlineChange.ChangeNotice)
(affected : Rules.Core.Money)
(t : Rules.OneOrder.AirlineChange.DeclineTerms) (p : Rules.Core.Money)
(d : Rules.OneOrder.Change.PriceDifferential)
(hinv : inv.involuntary n.reason = true)
(h :
Rules.OneOrder.AirlineChange.declineOffer e w inv n affected t
(Rules.OneOrder.AirlineChange.Decline.reshop p) =
Except.ok d) :
d.penalty.amount = 0 Rules.OneOrder.AirlineChange.decline_reshop_no_fee
(e :
Rules.OneOrder.Change.ExcessPenalty)
(w :
Rules.OneOrder.AirlineChange.DeclineFees)
(inv :
Rules.OneOrder.AirlineChange.InvoluntaryReading)
(n :
Rules.OneOrder.AirlineChange.ChangeNotice)
(affected : Rules.Core.Money)
(t :
Rules.OneOrder.AirlineChange.DeclineTerms)
(p : Rules.Core.Money)
(d :
Rules.OneOrder.Change.PriceDifferential)
(hinv : inv.involuntary n.reason = true)
(h :
Rules.OneOrder.AirlineChange.declineOffer
e w inv n affected t
(Rules.OneOrder.AirlineChange.Decline.reshop
p) =
Except.ok d) :
d.penalty.amount = 0
A customer who declines an involuntary change through Reshop pays no change
fee.
Open question for the business. The sources say a reshop after an airline
change may or may not cost the customer more, and give no rule. Under the
reading that applies the item's fees, the 40 EUR change fee of the itinerary
change worked example is charged when the customer reshops away from flights
the airline moved. The example declineByReshop shows it. Do change
fees and fare differences apply when the customer reshops after an airline
change, and which alternatives must the airline offer?
It checks acceptance criteria ONE-703.5 of requirement ONE-703, Declining an airline change.
58.45. Refund for a cancelled flight🔗
🔗open question
When the airline cancels a flight of a paid order item and does not
re-accommodate the customer, the customer gets part of the item's price back.
Open question for the business. The flight cancellation worked example
offers no follow-up action and no refund, and no source says whether a flight
the airline cannot deliver entitles the customer to money back. Because the
price is set per order item, no source says how much of it belongs to one
flight either. Under the reading the worked example shows, a paid return trip
at 1,000.00 EUR whose inbound flight is cancelled gets nothing back. The
example cancelInboundFlight shows it. Is a refund owed when the
airline cancels a flight without re-accommodation, and how much of an item's
price belongs to that flight?
It checks acceptance criteria ONE-704.4 of requirement ONE-704, Cancelling a flight without re-accommodation.
58.46. Cancelled service in an active item🔗
🔗open question
After the airline cancels a flight, every order item that holds a
CANCELLED service is itself CANCELLED, provided this held before.
Open question for the business. The Order concept ties a CANCELLED service
to a cancelled order item, and the cancellation page treats cancelling some
services of an item as a change. The flight cancellation worked example
cancels one flight's services and leaves the item as it was. A return trip
whose inbound flight is cancelled keeps an active outbound flight, so the item
stays ACTIVE with CANCELLED services in it, under every reading. The example
cancelInboundFlight shows it. Should the airline replace the item, as
a change does, or may an active item hold cancelled services?
It checks acceptance criteria ONE-704.5 of requirement ONE-704, Cancelling a flight without re-accommodation.
58.47. No live service is left on a cancelled flight🔗
🔗open question
When the airline cancels a flight and does not re-accommodate the
customer, no live service is left on that flight.
Open question for the business. The flight's services are ended through the
delivery status table, and the table has no move to UNABLE TO DELIVER from
REQUESTED, IN PROGRESS or SUSPENDED, under any reading. A service the airline
has not yet confirmed therefore stays live on a flight that will not operate.
The example cancelFlightWhileRequested shows it. What delivery status
does a requested, in-progress or suspended service take when its flight is
cancelled?
It checks acceptance criteria ONE-704.6 of requirement ONE-704, Cancelling a flight without re-accommodation.
58.48. Original item kept while Accept is pending🔗
🔗open question
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?
It checks acceptance criteria ONE-705.4 of requirement ONE-705, Re-accommodation before the seller answers.
58.49. Paid status after re-accommodation🔗
🔗open question
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?
It checks acceptance criteria ONE-705.5 of requirement ONE-705, Re-accommodation before the seller answers.
58.50. Seller never pays for a refund🔗
🔗open questionRules.OneOrder.Accounting.refund_not_paid_by_seller
(rr : Rules.OneOrder.Accounting.RecallReading)
(r : Rules.OneOrder.Accounting.SellerRefund)
(hrefund : r.refund ≤ r.payment) (hcomm : r.commission ≤ r.payment) :
0 ≤ (Rules.OneOrder.Accounting.refundClearance rr r).amount
Rules.OneOrder.Accounting.refund_not_paid_by_seller
(rr :
Rules.OneOrder.Accounting.RecallReading)
(r :
Rules.OneOrder.Accounting.SellerRefund)
(hrefund : r.refund ≤ r.payment)
(hcomm : r.commission ≤ r.payment) :
0 ≤
(Rules.OneOrder.Accounting.refundClearance
rr r).amount
The clearance for a refund through the seller never has the seller paying
the ORA: its amount is never negative.
Open question for the business. Under the reading that recalls the
commission first paid in full on any refund, a partial refund smaller than
that commission gives a negative amount. The example refundClearances
shows it: a 5.00 refund of a 75.00 payment that carried 7.50 of commission
leaves the seller paying the ORA 2.50. Recalling no commission, or the share
that matches the share refunded, never does
(refund_clearance_nonneg_without_full_recall). How much commission
is recalled on a partial refund?
It checks acceptance criteria ONE-802.6 of requirement ONE-802, Net clearance amount.
58.51. One clearance per payment commitment🔗
🔗open questionRules.OneOrder.Accounting.one_clearance_per_payment
(r : Rules.OneOrder.Accounting.RepeatReading)
(cs : List Rules.OneOrder.Accounting.Clearance) :
(List.map (fun x ↦ x.commitment)
(Rules.OneOrder.Accounting.submitAll r [] cs)).Nodup
Rules.OneOrder.Accounting.one_clearance_per_payment
(r :
Rules.OneOrder.Accounting.RepeatReading)
(cs :
List
Rules.OneOrder.Accounting.Clearance) :
(List.map (fun x ↦ x.commitment)
(Rules.OneOrder.Accounting.submitAll
r [] cs)).Nodup
Every pair of an order ID and a payment ID has at most one accepted
clearance, whatever clearances the ORA sends.
Open question for the business. The Clearance Manager checks clearance data
signed by both parties only for a repeated clearance ID. Two signed
clearances for one payment with different clearance IDs are both accepted.
The example signedTwice shows it. May one payment have two signed
clearances with different clearance IDs?
It checks acceptance criteria ONE-803.4 of requirement ONE-803, Accepting a clearance.
58.52. Settled and unsettled clearance amounts🔗
🔗open questionRules.OneOrder.Accounting.clearance_amounts_accounted
(r : Rules.OneOrder.Accounting.SettlementReading) (agreed : ℕ)
(es : List Rules.OneOrder.Accounting.SettlementEvent) :
(Rules.OneOrder.Accounting.settleRun r
(Rules.OneOrder.Accounting.SettlementRecord.new agreed)
es).Accounted
Rules.OneOrder.Accounting.clearance_amounts_accounted
(r :
Rules.OneOrder.Accounting.SettlementReading)
(agreed : ℕ)
(es :
List
Rules.OneOrder.Accounting.SettlementEvent) :
(Rules.OneOrder.Accounting.settleRun r
(Rules.OneOrder.Accounting.SettlementRecord.new
agreed)
es).Accounted
Every part of a clearance's agreed amount stays settled and kept, still
unsettled, or written off, whatever happens to it.
Open question for the business. Under a reading where a clawed-back amount
does not count as unsettled again, a clawback takes money back from the payee
without adding it to what is owed, so that part of the agreed amount is
neither settled, unsettled nor written off. The example
clawedBackThenCollected shows it: a 300.00 clearance settled in full and
then clawed back by 100.00 keeps 200.00 settled, with nothing unsettled.
Does a clawed-back amount count as unsettled again, and can a later clearing
settle it?
It checks acceptance criteria ONE-804.5 of requirement ONE-804, Clearance status.
58.53. Net position per remittance date🔗
🔗open questionRules.OneOrder.Accounting.net_positions_sum_zero
(r : Rules.OneOrder.Accounting.EasyPayReading)
(cs : List Rules.OneOrder.Accounting.Clearance) (date : String)
(ps : List Rules.OneOrder.Accounting.Party) (hnd : ps.Nodup)
(hcover :
∀ c ∈ cs,
Rules.OneOrder.Accounting.Party.org c.payee ∈ ps ∧
∀ (q : Rules.OneOrder.Accounting.Party),
Rules.OneOrder.Accounting.netPayer r c = some q → q ∈ ps) :
(List.map (Rules.OneOrder.Accounting.netPosition r cs date) ps).sum =
0
Rules.OneOrder.Accounting.net_positions_sum_zero
(r :
Rules.OneOrder.Accounting.EasyPayReading)
(cs :
List
Rules.OneOrder.Accounting.Clearance)
(date : String)
(ps :
List Rules.OneOrder.Accounting.Party)
(hnd : ps.Nodup)
(hcover :
∀ c ∈ cs,
Rules.OneOrder.Accounting.Party.org
c.payee ∈
ps ∧
∀
(q :
Rules.OneOrder.Accounting.Party),
Rules.OneOrder.Accounting.netPayer
r c =
some q →
q ∈ ps) :
(List.map
(Rules.OneOrder.Accounting.netPosition
r cs date)
ps).sum =
0
The net positions of all parties on a remittance date sum to zero.
Open question for the business. Under the reading that leaves an EasyPay
clearance out of its payer's position and keeps it in the payee's, the
positions add up to the EasyPay amounts. The example easyPayNetting
shows it: a seller owing an airline 100.00 by settlement plan and 50.00 by
EasyPay is a remittance payer for 100.00, while the airline is a settlement
payee for 150.00. Does the EasyPay provider count as a party in the
netting?
It checks acceptance criteria ONE-805.5 of requirement ONE-805, Net position of a party.
58.54. Clearing totals are never negative🔗
🔗open questionRules.OneOrder.Accounting.payee_clearing_nonneg
(lines : List Rules.OneOrder.Accounting.ClearingLine) :
0 ≤
Rules.OneOrder.Accounting.clearingTotal
Rules.OneOrder.Accounting.ClearingTo.settlementPayee lines Rules.OneOrder.Accounting.payee_clearing_nonneg
(lines :
List
Rules.OneOrder.Accounting.ClearingLine) :
0 ≤
Rules.OneOrder.Accounting.clearingTotal
Rules.OneOrder.Accounting.ClearingTo.settlementPayee
lines
The total of a clearing to a settlement payee is never negative.
Open question for the business. A payee whose clawbacks in a clearing exceed
what it is due in that clearing gets a negative total, which a bank transfer to
the payee cannot carry. The example clawbackExceedsDue shows it: a
payee due 200.00 with 300.00 clawed back has a total of minus 100.00. Does the
payee then become a remittance payer, or is the clawback carried forward to a
later clearing?
It checks acceptance criteria ONE-806.3 of requirement ONE-806, Total of a clearing.
58.55. Whole payment allocated🔗
🔗open questionRules.OneOrder.Accounting.allocation_whole_payment
(a : Rules.OneOrder.Accounting.AllocationReading)
(rd : Rules.OneOrder.Accounting.Rounding) (paid : ℕ)
(os : List Rules.OneOrder.Accounting.Obligation)
(hshort : paid ≤ Rules.OneOrder.Accounting.totalOwed os) :
(Rules.OneOrder.Accounting.allocate a rd paid os).sum = paid Rules.OneOrder.Accounting.allocation_whole_payment
(a :
Rules.OneOrder.Accounting.AllocationReading)
(rd :
Rules.OneOrder.Accounting.Rounding)
(paid : ℕ)
(os :
List
Rules.OneOrder.Accounting.Obligation)
(hshort :
paid ≤
Rules.OneOrder.Accounting.totalOwed
os) :
(Rules.OneOrder.Accounting.allocate a rd
paid os).sum =
paid
A short payment is allocated in full and no more: the amounts settled add
up to what was paid.
Open question for the business. Under the Remittance of Funds page each
settlement payee's share has to be rounded to a minor unit, and the rounded
shares need not add up to the payment. The example threePayees shows
it: 100.00 split between three payees owed 100.00 each settles 99.99 when
shares are rounded down and 100.02 when they are rounded up. Under the
Transfer of Funds page the whole payment is allocated
(transfer_allocates_all). How is a proportional share rounded, and
who receives the remainder?
It checks acceptance criteria ONE-807.5 of requirement ONE-807, Allocating a short remittance.
58.56. One allocation for a short remittance🔗
🔗open questionRules.OneOrder.Accounting.one_allocation
(rd : Rules.OneOrder.Accounting.Rounding) (paid : ℕ)
(os : List Rules.OneOrder.Accounting.Obligation)
(hshort : paid < Rules.OneOrder.Accounting.totalOwed os) :
Rules.OneOrder.Accounting.allocate
Rules.OneOrder.Accounting.AllocationReading.proportional rd paid
os =
Rules.OneOrder.Accounting.allocate
Rules.OneOrder.Accounting.AllocationReading.oldestFirst rd paid os Rules.OneOrder.Accounting.one_allocation
(rd :
Rules.OneOrder.Accounting.Rounding)
(paid : ℕ)
(os :
List
Rules.OneOrder.Accounting.Obligation)
(hshort :
paid <
Rules.OneOrder.Accounting.totalOwed
os) :
Rules.OneOrder.Accounting.allocate
Rules.OneOrder.Accounting.AllocationReading.proportional
rd paid os =
Rules.OneOrder.Accounting.allocate
Rules.OneOrder.Accounting.AllocationReading.oldestFirst
rd paid os
A short payment settles each clearance for the same amount under either
source page.
Open question for the business. The Remittance of Funds page splits a short
payment across the settlement payees in proportion to what each is owed; the
Transfer of Funds page applies it to the payer's obligations in the order
they were recorded, whatever the payee. The example twoAirlines shows
them differ: a payer owing airline A 100.00 (older) and airline B 100.00
(newer) pays 100.00, and A and B receive 50.00 each under the first page and
100.00 and nothing under the second. Which allocation does the Clearance
Manager use?
It checks acceptance criteria ONE-807.6 of requirement ONE-807, Allocating a short remittance.
58.57. No liability left at a final status🔗
🔗open questionRules.OneOrder.Accounting.final_status_no_liability
(r : Rules.OneOrder.Accounting.RevenueReading)
(k : Rules.OneOrder.Accounting.CancelCheck)
(b b' : Rules.OneOrder.Accounting.ServiceBooks)
(e : Rules.OneOrder.Accounting.BookEvent)
(h : Rules.OneOrder.Accounting.bookStep r k b e = some b')
(hf : Rules.OneOrder.Delivery.isFinal b'.delivery = true) :
Rules.OneOrder.Accounting.ServiceBooks.liability r b' = 0 Rules.OneOrder.Accounting.final_status_no_liability
(r :
Rules.OneOrder.Accounting.RevenueReading)
(k :
Rules.OneOrder.Accounting.CancelCheck)
(b b' :
Rules.OneOrder.Accounting.ServiceBooks)
(e :
Rules.OneOrder.Accounting.BookEvent)
(h :
Rules.OneOrder.Accounting.bookStep r k
b e =
some b')
(hf :
Rules.OneOrder.Delivery.isFinal
b'.delivery =
true) :
Rules.OneOrder.Accounting.ServiceBooks.liability
r b' =
0
When a service reaches a final delivery status, none of the amount paid
for it is held as a liability.
Open question for the business. The sources do not say which final statuses
earn revenue. Under a reading that keeps the amount paid for a no-show as a
liability, or that does not recognize a penalty when a cancellation is
reported, money stays a liability on a service that will never change again.
The examples noShowTreatments and cancelWithPenalty show it.
For DELIVERED, NOT CLAIMED, EXPIRED and FAILED TO DELIVER, does the amount
paid earn revenue, go back as a refund or stay a liability, and when is a
penalty reported at cancellation recognized?
It checks acceptance criteria ONE-809.3 of requirement ONE-809, Accounting for paid services.
58.58. Money balance of an order🔗
🔗open questionRules.OneOrder.Accounting.order_books_balance
(r : Rules.OneOrder.Accounting.RevenueReading)
(k : Rules.OneOrder.Accounting.CancelCheck) (ids : List String)
(es : List (String × Rules.OneOrder.Accounting.BookEvent)) :
(Rules.OneOrder.Accounting.OrderBooks.totals r
(Rules.OneOrder.Accounting.OrderBooks.run r k
(List.map Rules.OneOrder.Accounting.ServiceBooks.new ids)
es)).Balanced
Rules.OneOrder.Accounting.order_books_balance
(r :
Rules.OneOrder.Accounting.RevenueReading)
(k :
Rules.OneOrder.Accounting.CancelCheck)
(ids : List String)
(es :
List
(String ×
Rules.OneOrder.Accounting.BookEvent)) :
(Rules.OneOrder.Accounting.OrderBooks.totals
r
(Rules.OneOrder.Accounting.OrderBooks.run
r k
(List.map
Rules.OneOrder.Accounting.ServiceBooks.new
ids)
es)).Balanced
Whatever accounting is told about an order's services, its payments equal
its refunds, plus the amount held as liability, plus the revenue recognized,
plus the forfeited amounts.
Open question for the business. Under the reading where accounting records a
cancellation as the airline sends it, a refund, penalty and forfeited amount
that do not add up to what was paid break the balance. The examples
goodwillRefund and cancelNotAddingUp show it: a goodwill refund
of 120.00 on a 100.00 flight leaves 100.00 paid against 120.00 refunded.
Where the airline checks the amounts, the balance holds
(order_books_balance_of_checked). Must the amounts of a cancellation
add up to what was paid, and if not, where does the difference go?
It checks acceptance criteria ONE-809.4 of requirement ONE-809, Accounting for paid services.
58.59. Refunds within payments🔗
🔗open questionRules.OneOrder.Accounting.refunds_within_payments
(r : Rules.OneOrder.Accounting.RevenueReading)
(k : Rules.OneOrder.Accounting.CancelCheck) (ids : List String)
(es : List (String × Rules.OneOrder.Accounting.BookEvent)) :
(Rules.OneOrder.Accounting.OrderBooks.totals r
(Rules.OneOrder.Accounting.OrderBooks.run r k
(List.map Rules.OneOrder.Accounting.ServiceBooks.new ids)
es)).refunded ≤
(Rules.OneOrder.Accounting.OrderBooks.totals r
(Rules.OneOrder.Accounting.OrderBooks.run r k
(List.map Rules.OneOrder.Accounting.ServiceBooks.new ids)
es)).paid
Rules.OneOrder.Accounting.refunds_within_payments
(r :
Rules.OneOrder.Accounting.RevenueReading)
(k :
Rules.OneOrder.Accounting.CancelCheck)
(ids : List String)
(es :
List
(String ×
Rules.OneOrder.Accounting.BookEvent)) :
(Rules.OneOrder.Accounting.OrderBooks.totals
r
(Rules.OneOrder.Accounting.OrderBooks.run
r k
(List.map
Rules.OneOrder.Accounting.ServiceBooks.new
ids)
es)).refunded ≤
(Rules.OneOrder.Accounting.OrderBooks.totals
r
(Rules.OneOrder.Accounting.OrderBooks.run
r k
(List.map
Rules.OneOrder.Accounting.ServiceBooks.new
ids)
es)).paid
Whatever accounting is told about an order's services, it never refunds
more than was paid.
Open question for the business. Under the reading where accounting records a
cancellation as the airline sends it, nothing stops a refund larger than what
was paid. The example goodwillRefund shows it: a goodwill refund of
120.00 on a flight paid at 100.00. Where the airline checks the amounts, a
refund never exceeds what was paid
(refunds_within_payments_of_checked). May a refund exceed what was
paid, for example as goodwill, and how is the excess accounted for?
It checks acceptance criteria ONE-809.5 of requirement ONE-809, Accounting for paid services.