1 Offer acceptance
This blueprint covers one slice of the Offer and Order domain: an offer with priced items and an expiry, the order created when the offer is accepted, payments against the order, and refunds against payments. Each node in this chapter is a Lean declaration. A green node is defined or proven in Lean; an uncolored theorem is open. The next chapter adds candidate rules from IATA’s public ONE Order material that have no Lean yet.
The review document, under review/ on the site, shows the same declarations with their docstrings, the examples the build computes, and the open question for the Offer/Order team.
1.1 Core concepts
The currencies the slice prices offers in, as ISO 4217 codes: USD, EUR and GBP.
An amount of money is a non-negative whole number of minor units (cents, pence) in one currency.
Two amounts add only when they are in the same currency. A mixed-currency sum has no result, so it is a visible failure rather than a silent conversion.
A point in time, as whole seconds since the Unix epoch. All times are UTC.
A traveller named on an offer or order.
Whoever makes a request. A placeholder for the Identity namespace.
Data sensitivity levels, ordered public, internal, confidential, restricted. A placeholder for the Data Governance namespace.
Every classification level is at least as sensitive as public.
By comparing ranks: public has rank 0.
1.2 Offers and orders
One priced product inside an offer for one passenger: a flight, a bag, a seat. It corresponds to a ONE Order OfferItem.
A set of priced items the airline offers a customer, valid until it expires, with every price in one currency.
Where a purchased service is in its life: ready, delivered, cancelled, or refunded.
Something that happens to a purchased service: deliver, cancel, or refund.
One purchased service inside an order, created from one offer item.
A customer’s purchase: the items of one accepted offer, the total price, and when it was created.
Why an offer could not be accepted: it expired, it is empty, or its items are priced in more than one currency.
When a customer accepts an offer, the system creates an order only if the offer has not expired, contains at least one item, and prices every item in the offer’s currency. The order’s price is the sum of the item prices.
The only allowed transitions are ready to delivered, ready to cancelled, and cancelled to refunded. Every other event is refused.
When an offer is accepted, the order’s price is exactly the sum of the offer’s item prices.
Unfold the acceptance decision; in the only branch that creates an order, the price is defined as that sum.
An offer accepted at or after its expiry instant is rejected as expired.
The expiry check is the first check the decision makes.
The cancel event is refused for a delivered service, and no event moves a delivered service to cancelled.
Check each of the three events.
1.3 Payments and refunds
Money received from the customer against an order.
Money returned to the customer against one payment.
The total received in an order’s payments, and the total returned in refunds against those payments.
A refund is accepted against a payment only if the refund amount does not exceed that payment’s amount. The check looks at one refund at a time.
If every refund was accepted against one of the order’s payments, the total refunded does not exceed the total paid.
Counterexample: two refunds of 60.00 against one payment of 100.00 are each accepted and together return 120.00.
Open point: does the limit apply per refund, cumulatively per payment, or cumulatively per order, and is a refund above the amount paid ever allowed, for example as a goodwill credit?
Not proven. The counterexample above shows the statement is false for the rule as written.
1.4 EARS requirements
Each requirement below is the EARS statement in a rule’s Lean docstring. The status and the proving theorems are computed by the build.
|
ID |
EARS statement |
Declaration |
Proven by |
|
ONE-001 |
When a customer accepts an offer, the system shall create an order with one order item for each offer item and one service for each passenger and flight segment of that item. |
accept |
accept_item_per_offer_item, accept_services_per_passenger_segment, accept_item_ids_unique, accept_rejects_expired, guaranteed_while_acceptable_of_exclusive, createOrder_toOrder, accept_order_opened, guaranteed_while_acceptable (open) |
|
ONE-002 |
The system shall give each order item the status active, cancelled or closed from the service and delivery statuses of its services. |
itemStatuses |
item_active_iff, change_original_cancelled (open), accept_pending_keeps_original (open), item_cancelled_iff, accept_pending_keeps_original_of_acceptance, cancel_flight_cancelled_items (open), cancelled_at_once_closed (open), item_has_one_status (open), item_closed_iff |
|
ONE-003 |
The system shall mark an order opened while any of its services holds value, and closed once all its items are closed or cancelled and all its services are delivered or removed. |
orderStatuses |
order_opened_iff, order_closed_iff, closed_order_refuses_events, cancelled_at_once_closed (open), all_final_order_closed (open), accept_order_opened, order_opened_or_closed (open) |
|
ONE-101 |
When an event happens to a service, the system shall move its delivery status only along the moves in the delivery status table. |
move |
pay_marks_ready, pilot_step_within_table, confirm_marks_confirmed, no_show_marks_not_claimed, deliver_marks_delivered, fail_marks_failed, unable_marks_unable, expire_marks_expired, cancel_removes, step_follows_table |
|
ONE-102 |
When a service is cancelled, expires, is not claimed or cannot be delivered, the system shall move it to the delivery status that records why. |
endService |
none |
|
ONE-103 |
The system shall treat DELIVERED, REMOVED, EXPIRED, NOT CLAIMED and FAILED TO DELIVER as final delivery statuses, which no event leaves. |
isFinal |
liability_until_final, final_reachable, all_final_order_closed (open), final_status_no_liability (open), final_refuses_all |
|
ONE-104 |
When the airline suspends a service, the system shall record the delivery status it left and return it only to that status or remove it. |
step |
suspended_cancel_removes, held_value_only_released, resume_returns, closed_order_refuses_events, suspended_moves_back_or_removed, final_refuses_all, suspend_records_status, step_follows_table |
|
ONE-105 |
When a rule in any area ends a service, the system shall move the service’s delivery status only along a move of the delivery status table. |
endWith |
endWith_cancelled_not_live, endWith_follows, follows_ite_endWith, endWith_refused, endWith_allowed |
|
ONE-201 |
When the airline prices a change or cancellation of order items, the system shall state the amount due to the airline, the amount due by the airline and a type code that names the outcome. |
priceDifferential |
respend_reusable, differential_collects_iff, differential_pays_iff, priceDifferential_ok, change_keeps_balance (open), change_net_is_fee_plus_difference, differential_rejects_mixed_currency, priceDifferential_prices, differential_nets (open) |
|
ONE-202 |
When a change or cancellation carries a penalty, the system shall either net the penalty against the price difference or charge it separately. |
dueAmounts |
separate_penalty_added, net_same_either_way, netted_single_amount, due_amounts_net_of_collect, cancel_not_owing (open), cancel_not_owing_of_waive |
|
ONE-203 |
When a seller asks to cancel an order, the system shall cancel it at once if no payment has been received for it, and otherwise only through a cancellation offer. |
requestCancellation |
paid_needs_offer, offer_within_payments (open), unpaid_cancelled_at_once, cancelled_at_once_closed (open), offer_priced_from_live_items |
|
ONE-204 |
When a seller has accepted and paid a change to an order item, the system shall add a new item with the services the change keeps and cancel the services it does not keep. |
changeItem |
change_original_cancelled (open), notify_at_notice, change_item_refs_unique, change_keeps_balance (open), change_marks_transferred, changeItem_moves, change_keeps_services, change_cancels_others, delivery_moves_follow_table, change_keeps_flights (open), changeItem_ok |
|
ONE-205 |
When a seller settles a change or cancellation offer, the system shall record on the order what the customer paid, what the airline returned, the penalty and the forfeited amount. |
settle |
change_keeps_balance (open), settle_records_penalty, settle_adds_payments |
|
ONE-301 |
The system shall give a payment the status FAILED if it has no payment method or the transaction of any of its payment methods failed, SUCCESSFUL if all of them succeeded, and PENDING otherwise. |
status |
status_pending_iff, status_failed_iff, status_successful_iff, isPaid_iff, status_without_method, applyOutcome_unsuccessful, expireUnpaid_fails_pending, applyOutcome_ready, recordOutcome_final_of_reading, applyOutcome_no_time_limit, recordOutcome_settled_final (open) |
|
ONE-302 |
The system shall count an order item paid once a SUCCESSFUL payment covers it. |
isPaid |
expireUnpaid_keeps_paid, expireUnpaid_removes, isPaid_iff, expireUnpaid_fails_pending, unpaid_item_removed_eventually (open) |
|
ONE-303 |
When the airline reports the outcome of a payment method’s transaction, the system shall record it as the transaction’s status if the move from the recorded status is allowed. |
recordOutcome |
recordOutcome_pending, recordOutcome_final_of_reading, recordOutcome_other_methods, recordOutcome_settled_final (open) |
|
ONE-304 |
When a seller pays for order items, the system shall accept the payment only if it is made before the items’ payment time limits and its requested amounts add up to their price, and shall charge each payment method its requested amount plus its surcharge. |
acceptPayment |
acceptPayment_rejects_without_method, zero_duration_payable (open), acceptPayment_total, acceptPayment_commitment_zero, acceptPayment_requested_eq_price, acceptPayment_rejects_after_time_limit, acceptPayment_charges |
|
ONE-305 |
When a payment becomes SUCCESSFUL, the system shall move every CONFIRMED service of the order items it covers to READY TO PROCEED and remove their payment time limits. |
applyOutcome |
applyOutcome_moves, applyOutcome_uncovered, applyOutcome_unsuccessful, applyOutcome_ready, delivery_moves_follow_table, failed_method_pays_nothing, applyOutcome_no_time_limit |
|
ONE-306 |
When an order item’s payment time limit passes with no SUCCESSFUL payment covering it, the system shall remove the item and mark FAILED every PENDING payment that covers it. |
expireUnpaid |
expireUnpaid_moves, expireUnpaid_keeps_paid, expireUnpaid_removes, expireUnpaid_fails_pending, expireUnpaid_keeps_before_limit, delivery_moves_follow_table, unpaid_item_removed_eventually (open) |
|
ONE-401 |
When a seller selects items from an offer, the system shall accept the selection only if it names items the offer holds and includes every item the offer marks mandatory. |
selectItems |
selectItems_ok, select_rejects_unknown, select_takes_named_items, select_includes_mandatory_of_marked, select_includes_mandatory (open), select_rejects_missing_mandatory |
|
ONE-402 |
When a seller sends a create request with selections from one or more offers, the system shall check each selection and create one order from them, or reject the request. |
createOrder |
create_items_match_selection (open), create_once_records, create_rejects_expired_of_wholeRequest, create_rejects_empty, create_single_currency (open), create_items_match_selection_of_wholeRequest, create_price_eq_sum_of_wholeRequest, createOrder_ok, create_price_eq_sum (open), create_rejects_expired (open) |
|
ONE-403 |
When a seller sends a create request, the system shall create the order and record the offers it came from, unless an offer it names has already produced an order. |
createOnce |
create_once_records, repeat_rejected, once_per_offer (open), once_per_offer_of_ne, repeat_returns_existing |
|
ONE-404 |
When the airline applies a group of changes to an order, the system shall raise the order’s version by one and record the group in the order’s history. |
recordChanges |
foldl_recordChanges, no_version_applied, record_raises_version, current_version_applied |
|
ONE-405 |
When a seller sends a change request, the system shall compare the order version the request carries, if any, with the order’s current version before applying the change. |
requestChange |
stale_rejected (open), no_version_applied, stale_rejected_of_reject, current_version_applied |
|
ONE-406 |
The system shall keep an order accessible for 13 months from its creation and for 13 months from its first usage while it has an active item, and for 7 days after every item has reached a final status. |
mustKeep |
keep_after_final, keep_from_creation, keep_while_active (open), keep_from_first_use |
|
ONE-501 |
While no order has been created from an offer, the system shall treat an offer item’s price and inventory as guaranteed only until both the item’s guarantee time limit and the offer’s expiry. |
guaranteesAt |
guarantees_end_by_expiry, no_limit_no_guarantee, guaranteed_while_acceptable_of_exclusive, price_guaranteed_before, guaranteed_while_acceptable (open), inventory_guaranteed_before |
|
ONE-502 |
When a customer accepts an offer whose items carry time limits, the system shall create the order as ONE-001 does and give each order item its payment time limit and price guarantee from its offer item. |
createOrder |
zero_duration_payable (open), createOrder_ok, createOrder_toOrder, createOrder_price_guaranteed (open), createOrder_keeps_guarantee, createOrder_guaranteed_of_reprice, createOrder_limit_not_before_creation (open), createOrder_fixed, createOrder_duration |
|
ONE-503 |
When a change or cancellation is asked for at an instant, the system shall take as the rule in force the rule for that action and the journey’s current stage with the latest effective date not after that instant. |
ruleInForce |
ruleInForce_latest, ruleInForce_stage, ruleInForce_covers_stage (open), change_refused, cancel_to_original_form, change_no_fee, cancel_fixed_refund, cancel_forbidden_nothing, cancel_full_refund, ruleInForce_not_expired, change_fee_is_penalty, ruleInForce_started |
|
ONE-504 |
When a customer asks for a voluntary change, the system shall refuse it if the rule in force forbids it, and otherwise quote it with the rule’s fee as the penalty. |
voluntaryChange |
change_net_is_fee_plus_difference, change_refused, change_no_fee, change_fee_is_penalty |
|
ONE-505 |
When a customer cancels an unused order item voluntarily, the system shall return what the cancel rule in force gives: nothing if it forbids cancellation, and otherwise a full or a fixed refund. |
cancellationRefund |
cancel_returns_refundable_charges (open), cancel_to_original_form, cancel_fixed_refund, cancel_forbidden_nothing, cancel_full_refund |
|
ONE-506 |
When an airline states a price with its parts, the system shall total the price as its base amount plus its surcharges, fees, taxes and the consumption tax not included in it. |
priceTotal |
price_adds_excluded_lines (open), price_rejects_large_discount, price_adds_excluded_lines_of_lines, price_tax_total, price_base, price_rejects_mixed_currency, price_total_from_parts |
|
ONE-601 |
The system shall count as dependent on a flight service the ancillary services of the order that the link between dependent and parent ties to it. |
dependents |
dependents_by_reference, replace_moves, dependents_cover_of_passenger_segment, dependents_cover (open), dependent_not_flight, replace_effect_by_kind, replace_states_each_dependent, dependents_by_passenger_segment |
|
ONE-602 |
When a seller adds services to an order, the system shall accept the request only if every flight-related ancillary in it has a live flight service for its passenger and segment, in the order or in the request. |
addServices |
add_accepts_unrelated, add_appends, add_refuses_without_flight |
|
ONE-603 |
When a seller cancels order items, the system shall cancel every live service of the items named and treat the services that depend on a cancelled flight as the reading says. |
cancelItems |
cancel_items_no_live_dependents_of_not_leave, cancel_items_respects_conditions_of_not_cancel_with, cancel_items_respects_conditions (open), cancelItems_ok, cancel_items_allowed_of_not_refuse, cancelItems_moves, cancel_items_keeps_others, cancel_items_allowed (open), cancelItems_ok_conditions, delivery_moves_follow_table, cancel_items_refuses_not_cancellable, cancel_items_named, cancel_items_no_live_dependents (open) |
|
ONE-604 |
When a flight service is replaced by a flight on another segment, the system shall state for each live service that depends on it the effect the reading gives for its kind. |
replaceFlight |
replace_no_seat_clash (open), replace_moves, replace_effect_by_kind, replace_states_each_dependent |
|
ONE-605 |
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. |
chooseSeats |
choose_seats_refuses_unavailable, choose_seats_one_passenger_per_seat (open), choose_seats_items, choose_seats_one_seat_per_passenger (open) |
|
ONE-606 |
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. |
chooseAlaCarte |
alacarte_item_price, alacarte_refuses_ineligible, chooseAlaCarte_ok, alacarte_total, alacarte_one_item (open), alacarte_item_per_passenger_segment |
|
ONE-607 |
When a seller removes services from a bundle, the system shall cancel them and return their share of the bundle price under the reading. |
removeFromBundle |
removeFromBundle_moves, bundle_return_le_price (open), bundle_returns_shares, bundle_removes, removeFromBundle_ok, bundle_return_all (open), delivery_moves_follow_table |
|
ONE-701 |
When an airline change notice offers follow-up actions, the system shall keep them pending until the seller answers with one of them or a consequence of inaction applies. |
resolve |
resolve_acknowledge_only, resolve_unanswered, resolve_answers, resolve_answered_sound, resolve_answered_of_answeredBy, contact_airline_answers_of_recorded, contact_airline_answers (open) |
|
ONE-702 |
When a time limit of a change notice passes and the seller has not answered, the system shall apply the consequence of inaction of the follow-up action whose time limit passed first. |
consequenceAt |
resolve_unanswered, before_limits_no_consequence, resolve_answers, resolve_answered_sound, no_limit_no_consequence, contact_airline_answers_of_recorded, contact_airline_answers (open), resolved_before_departure (open), lapse_applies_earliest |
|
ONE-703 |
When a customer declines an airline change through Cancel or Reshop, the system shall price it as a cancellation or change of the affected order items, with the airline’s cancellation or change fee as the penalty. |
declineOffer |
decline_reshop_no_fee_of_waived, decline_reshop_prices, decline_cancel_no_penalty_of_waived, decline_reshop_no_fee (open), decline_cancel_no_penalty (open), decline_cancel_prices |
|
ONE-704 |
When the airline cancels a flight and does not re-accommodate the customer, the system shall cancel every live service on that flight with delivery status UNABLE TO DELIVER. |
cancelFlight |
cancel_flight_leaves_no_live (open), cancel_flight_keeps_others, cancel_flight_cancelled_items (open), cancel_flight_refunds (open), cancel_flight_marks, cancelFlight_moves, cancel_flight_refund_le_price, delivery_moves_follow_table, cancel_flight_keeps_items |
|
ONE-705 |
When the airline moves a customer to other flights, the system shall replace the affected order item with a new item at the same price, holding a service for each passenger on each new flight. |
notifyChange |
reaccommodated_paid (open), accept_pending_keeps_original (open), notify_at_notice, accept_pending_keeps_original_of_acceptance, notifyChange_moves, delivery_moves_follow_table, notify_new_item, notify_at_acceptance |
|
ONE-801 |
The system shall owe the seller of an order item the total of the item’s commissions, each a fixed amount or a percentage of a stated base amount. |
commissionOwed |
commission_total, commission_mixed_currency |
|
ONE-802 |
When a payment commitment is made, the system shall state the clearances between the ORA and the seller for it, with their net clearance amounts. |
clearancesFor |
airline_collected, seller_collected_netted, seller_collected_separate |
|
ONE-803 |
When the ORA sends a clearance, the system shall accept it unless it repeats a clearance already accepted, and record only accepted clearances. |
submit |
submit_keeps_distinct, repeated_id_rejected, repeated_unsigned_rejected, accepted_recorded |
|
ONE-804 |
When the ORA cancels a clearance or the Clearance Manager settles, claws back or writes off money on it, the system shall move the clearance’s status and amounts as the clearance statuses describe. |
settleStep |
settle_all, settle_part, write_off_removes_unsettled, cancel_marks_cancelled, settleStep_accounted |
|
ONE-805 |
When the Clearance Manager nets the clearances for a remittance date, the system shall make each party a settlement payee or a remittance payer for its net position. |
settlementRole |
positive_position_payee, negative_position_payer |
|
ONE-806 |
When the Clearance Manager sends a clearing, the system shall make its total, and the bank transfer for it, the amounts settled less the amounts clawed back. |
clearingTotal |
payee_clearing_nonneg (open), payee_clearing_total, payer_clearing_leaves_out_easyPay |
|
ONE-807 |
When a remittance payer pays short and the Clearance Manager has no credit line, the system shall split what was paid across the payer’s clearances. |
allocate |
allocation_oldest_first_per_payee, proportional_share_settled, allocation_whole_payment (open), one_allocation (open), transfer_oldest_first, transfer_allocates_all, allocation_within_owed |
|
ONE-808 |
If a service provider bills the ORA for a service before it has been delivered or consumed, then the system shall refuse the bill unless a bilateral agreement allows earlier billing. |
acceptBill |
bill_refused_other_provider, bill_refused_unless_consumed, delivered_bill_accepted |
|
ONE-809 |
The system shall hold the amount paid for a service as a liability until the service reaches a final delivery status, and only then recognize it as revenue. |
bookStep |
cancel_must_add_up, final_status_no_liability (open), bookStep_balanced_of_checked |
|
OO-001 |
When a customer accepts an offer, the system shall create an order only if the offer has not expired and contains at least one item. |
accept |
accept_rejects_expired, accept_price_eq_sum |
|
OO-002 |
When a delivery event is applied to a service, the system shall allow only the transitions ready to delivered, ready to cancelled, cancelled to refunded. |
step |
pilot_step_within_table, delivered_not_cancellable |
|
OO-003 |
When a refund is requested against a payment, the system shall accept it only if the refund amount does not exceed that payment’s amount. |
acceptRefund |
refunds_le_payments (open) |