8. Moves between delivery statuses🔗

Requirement ONE-101. Of its 5 acceptance criteria, 3 are proven, 1 is checked by examples only and 1 is open.

rule

Rules.OneOrder.Delivery.move (m : Rules.OneOrder.Delivery.MoveReading) :
  Rules.OneOrder.DeliveryStatus →
    Rules.OneOrder.Delivery.DeliveryEvent →
      Option Rules.OneOrder.DeliveryStatus
Rules.OneOrder.Delivery.move
  (m :
    Rules.OneOrder.Delivery.MoveReading) :
  Rules.OneOrder.DeliveryStatus →
    Rules.OneOrder.Delivery.DeliveryEvent →
      Option Rules.OneOrder.DeliveryStatus

EARS: When an event happens to a service, the system shall move its delivery status only along the moves in the delivery status table.

Story: As an airline, I want a service's delivery status to change only along the moves the standard describes, so that a service is delivered only once it is paid for and each status means the same to every party.

Acceptance criteria:

ONE-101.1: When the airline confirms a REQUESTED service, the system shall mark it CONFIRMED.
ONE-101.2: When payment for a CONFIRMED service succeeds, the system shall mark it READY TO PROCEED.
ONE-101.3: When a service that is READY TO PROCEED, READY TO DELIVER or IN PROGRESS is delivered, the system shall mark it DELIVERED.
ONE-101.4: If payment for a service has not succeeded, then the system shall keep it out of READY TO PROCEED, READY TO DELIVER, IN PROGRESS and DELIVERED.
ONE-101.6: If an event has no move from the service's delivery status in the table, then the system shall refuse it.

The table, read from the status definitions, the ORDSTS guidance and the worked examples: REQUESTED goes to CONFIRMED; CONFIRMED goes to READY TO PROCEED on payment; READY TO PROCEED goes to READY TO DELIVER, IN PROGRESS or DELIVERED; READY TO DELIVER goes to IN PROGRESS or DELIVERED; IN PROGRESS goes to DELIVERED. The ways a service ends without delivery are in endService, and suspension is in step. Delivery from CONFIRMED and the return from UNABLE TO DELIVER to READY TO PROCEED are left to the reading. The result is the new status, or none when the event is refused.

8.1. How each acceptance criterion is checked🔗

A criterion is proven when a guarantee below proves it for every input, and example only when only examples check it.

Criterion	Status	Checked by
ONE-101.1	Proven	Confirming a requested service
ONE-101.2	Proven	Payment readies a confirmed service, Paid flight delivered
ONE-101.3	Proven	Delivering a paid service, Paid flight delivered
ONE-101.4	Open	Payment before delivery starts, Unpaid after force majeure, Delivered before payment
ONE-101.6	Example only	Undecided moves, Move table

8.2. Delivery state diagram🔗

The build runs every state and event through the model in the example Rules.OneOrder.Delivery.moveTable and draws the moves the rule allows. Any event without an arrow is refused.

8.3. Guarantees🔗

8.3.1. Confirming a requested service🔗

guarantee

Rules.OneOrder.Delivery.confirm_marks_confirmed
  (m : Rules.OneOrder.Delivery.MoveReading) :
  Rules.OneOrder.Delivery.move m Rules.OneOrder.DeliveryStatus.requested
      Rules.OneOrder.Delivery.DeliveryEvent.confirm =
    some Rules.OneOrder.DeliveryStatus.confirmed
Rules.OneOrder.Delivery.confirm_marks_confirmed
  (m :
    Rules.OneOrder.Delivery.MoveReading) :
  Rules.OneOrder.Delivery.move m
      Rules.OneOrder.DeliveryStatus.requested
      Rules.OneOrder.Delivery.DeliveryEvent.confirm =
    some
      Rules.OneOrder.DeliveryStatus.confirmed

A REQUESTED service the airline confirms becomes CONFIRMED, under every reading.

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

Checks acceptance criteria ONE-101.1.

8.3.2. Payment readies a confirmed service🔗

guarantee

Rules.OneOrder.Delivery.pay_marks_ready
  (m : Rules.OneOrder.Delivery.MoveReading) :
  Rules.OneOrder.Delivery.move m Rules.OneOrder.DeliveryStatus.confirmed
      Rules.OneOrder.Delivery.DeliveryEvent.pay =
    some Rules.OneOrder.DeliveryStatus.readyToProceed
Rules.OneOrder.Delivery.pay_marks_ready
  (m :
    Rules.OneOrder.Delivery.MoveReading) :
  Rules.OneOrder.Delivery.move m
      Rules.OneOrder.DeliveryStatus.confirmed
      Rules.OneOrder.Delivery.DeliveryEvent.pay =
    some
      Rules.OneOrder.DeliveryStatus.readyToProceed

A CONFIRMED service whose payment succeeds becomes READY TO PROCEED, under every reading.

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

Checks acceptance criteria ONE-101.2.

8.3.3. Delivering a paid service🔗

guarantee

Rules.OneOrder.Delivery.deliver_marks_delivered
  (m : Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (hs :
    s = Rules.OneOrder.DeliveryStatus.readyToProceed ∨
      s = Rules.OneOrder.DeliveryStatus.readyToDeliver ∨
        s = Rules.OneOrder.DeliveryStatus.inProgress) :
  Rules.OneOrder.Delivery.move m s
      Rules.OneOrder.Delivery.DeliveryEvent.deliver =
    some Rules.OneOrder.DeliveryStatus.delivered
Rules.OneOrder.Delivery.deliver_marks_delivered
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (hs :
    s =
        Rules.OneOrder.DeliveryStatus.readyToProceed ∨
      s =
          Rules.OneOrder.DeliveryStatus.readyToDeliver ∨
        s =
          Rules.OneOrder.DeliveryStatus.inProgress) :
  Rules.OneOrder.Delivery.move m s
      Rules.OneOrder.Delivery.DeliveryEvent.deliver =
    some
      Rules.OneOrder.DeliveryStatus.delivered

A service that is READY TO PROCEED, READY TO DELIVER or IN PROGRESS becomes DELIVERED when it is delivered, under every reading. READY TO DELIVER and IN PROGRESS may be skipped.

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

Checks acceptance criteria ONE-101.3.

8.3.4. Payment before delivery starts🔗

guarantee

Rules.OneOrder.Delivery.paid_before_delivery
  (m : Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (es : List Rules.OneOrder.Delivery.DeliveryEvent)
  (hs :
    s = Rules.OneOrder.DeliveryStatus.requested ∨
      s = Rules.OneOrder.DeliveryStatus.confirmed)
  (hpay :
    Rules.OneOrder.Delivery.paymentSucceeds m
        { status := s, suspendedFrom := none } es =
      false) :
  (Rules.OneOrder.Delivery.run m { status := s, suspendedFrom := none }
        es).status ∉
    [Rules.OneOrder.DeliveryStatus.readyToProceed,
      Rules.OneOrder.DeliveryStatus.readyToDeliver,
      Rules.OneOrder.DeliveryStatus.inProgress,
      Rules.OneOrder.DeliveryStatus.delivered]
Rules.OneOrder.Delivery.paid_before_delivery
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (es :
    List
      Rules.OneOrder.Delivery.DeliveryEvent)
  (hs :
    s =
        Rules.OneOrder.DeliveryStatus.requested ∨
      s =
        Rules.OneOrder.DeliveryStatus.confirmed)
  (hpay :
    Rules.OneOrder.Delivery.paymentSucceeds
        m
        { status := s,
          suspendedFrom := none }
        es =
      false) :
  (Rules.OneOrder.Delivery.run m
        { status := s,
          suspendedFrom := none }
        es).status ∉
    [Rules.OneOrder.DeliveryStatus.readyToProceed,
      Rules.OneOrder.DeliveryStatus.readyToDeliver,
      Rules.OneOrder.DeliveryStatus.inProgress,
      Rules.OneOrder.DeliveryStatus.delivered]

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?

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

Checks acceptance criteria ONE-101.4.

8.4. Examples🔗

8.4.1. Paid flight delivered🔗

example

Rules.OneOrder.Delivery.paidFlightDelivered :
  Rules.OneOrder.Delivery.Walk
Rules.OneOrder.Delivery.paidFlightDelivered :
  Rules.OneOrder.Delivery.Walk

Given a flight service that is CONFIRMED and waiting for payment.

When payment succeeds, and then the passenger flies and the provider reports the flight delivered.

Then the flight is READY TO PROCEED and then DELIVERED under both readings. It skips READY TO DELIVER and IN PROGRESS, as the services in the Order Closing worked example do.

What Lean computed:

Strict: ready to proceed, delivered
Loose: ready to proceed, delivered

Checks acceptance criteria ONE-101.2, ONE-101.3.

8.4.2. Delivered before payment🔗

example

Rules.OneOrder.Delivery.deliveredBeforePayment :
  Rules.OneOrder.Delivery.Walk
Rules.OneOrder.Delivery.deliveredBeforePayment :
  Rules.OneOrder.Delivery.Walk

Given a bag service that is CONFIRMED, with no payment yet.

When the provider reports the bag delivered.

Then under the strict reading the report is refused and the bag stays CONFIRMED. Under the loose reading the bag is DELIVERED though nobody paid for it.

What Lean computed:

Strict: confirmed
Loose: delivered

Checks acceptance criteria ONE-101.4.

8.4.3. Unpaid after force majeure🔗

example

Rules.OneOrder.Delivery.unpaidAfterForceMajeure :
  Rules.OneOrder.Delivery.Walk
Rules.OneOrder.Delivery.unpaidAfterForceMajeure :
  Rules.OneOrder.Delivery.Walk

Given a flight service that is CONFIRMED, with no payment yet.

When a force majeure event prevents delivery, the constraint then lifts, and the passenger flies.

Then under the strict reading the flight stays UNABLE TO DELIVER. Under the loose reading it returns to READY TO PROCEED when the constraint lifts and is then DELIVERED, though nobody paid for it.

What Lean computed:

Strict: unable to deliver, unable to deliver, unable to deliver
Loose: unable to deliver, ready to proceed, delivered

Checks acceptance criteria ONE-101.4.

8.4.4. Move table🔗

example

Rules.OneOrder.Delivery.moveTable : List Rules.OneOrder.Delivery.Move
Rules.OneOrder.Delivery.moveTable :
  List Rules.OneOrder.Delivery.Move

Given each delivery status, under the strict reading, where every move the sources leave undecided is refused.

When each event other than a suspension happens to a service in it.

Then these 28 moves are allowed, and every other event is refused. The review document draws them as the delivery state diagram. Suspension is covered by the rule for suspended services.

What Lean computed:

Before	Event	After
requested	confirm	confirmed
confirmed	pay	ready to proceed
confirmed	remove	removed
confirmed	remove hold value	removed hold value
confirmed	expire	expired
confirmed	not claimed	not claimed
confirmed	unable	unable to deliver
confirmed	fail	failed to deliver
ready to proceed	prepare	ready to deliver
ready to proceed	start	in progress
ready to proceed	deliver	delivered
ready to proceed	remove	removed
ready to proceed	remove hold value	removed hold value
ready to proceed	expire	expired
ready to proceed	not claimed	not claimed
ready to proceed	unable	unable to deliver
ready to proceed	fail	failed to deliver
ready to deliver	start	in progress
ready to deliver	deliver	delivered
ready to deliver	remove	removed
ready to deliver	remove hold value	removed hold value
ready to deliver	expire	expired
ready to deliver	not claimed	not claimed
ready to deliver	unable	unable to deliver
ready to deliver	fail	failed to deliver
in progress	deliver	delivered
in progress	fail	failed to deliver
removed hold value	release value	removed

Checks acceptance criteria ONE-101.6.

8.4.5. Undecided moves🔗

example

Rules.OneOrder.Delivery.undecidedMoves :
  List Rules.OneOrder.Delivery.UndecidedMove
Rules.OneOrder.Delivery.undecidedMoves :
  List
    Rules.OneOrder.Delivery.UndecidedMove

Given each delivery status and each event.

When the event happens to a service in the status, under the strict reading and under the loose reading.

Then seven moves are allowed under the loose reading and refused under the strict one: delivery of a CONFIRMED service before payment, the cancellation or NOT CLAIMED end of a service IN PROGRESS, and the return of an UNABLE TO DELIVER service to READY TO PROCEED.

What Lean computed:

Status	Event	Moves to
confirmed	prepare	ready to deliver
confirmed	start	in progress
confirmed	deliver	delivered
in progress	remove	removed
in progress	remove hold value	removed hold value
in progress	not claimed	not claimed
unable to deliver	constraint lifted	ready to proceed

Checks acceptance criteria ONE-101.6.

8.5. Open question🔗

The guarantee Payment before delivery starts is open: the example Delivered before payment, Unpaid after force majeure shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.