3. Delivery transitions🔗

Requirement OO-002. Of its 5 acceptance criteria, 1 is proven and 4 are checked by examples only.

rule

Rules.OfferOrder.step :
  Rules.OfferOrder.DeliveryState →
    Rules.OfferOrder.DeliveryEvent →
      Option Rules.OfferOrder.DeliveryState
Rules.OfferOrder.step :
  Rules.OfferOrder.DeliveryState →
    Rules.OfferOrder.DeliveryEvent →
      Option
        Rules.OfferOrder.DeliveryState

EARS: 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.

Story: As an operations agent, I want a service's delivery state to change only along the allowed transitions, so that a delivered service is never cancelled and a service is never refunded before it is cancelled.

Acceptance criteria:

OO-002.1: When a ready service is delivered, the system shall mark it delivered.
OO-002.2: When a ready service is cancelled, the system shall mark it cancelled.
OO-002.3: When a cancelled service is refunded, the system shall mark it refunded.
OO-002.4: If a delivered service is cancelled, then the system shall refuse the event.
OO-002.5: If any other event is applied to a service, then the system shall refuse the event.

The result is the new state, or none when the event is not allowed in the current state.

3.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
OO-002.1	Example only	Delivery walk, Transition table
OO-002.2	Example only	Transition table
OO-002.3	Example only	Transition table
OO-002.4	Proven	Delivery walk, Delivered services cannot be cancelled, Transition table
OO-002.5	Example only	Transition table

3.2. Delivery state diagram🔗

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

3.3. Try it🔗

Choose the inputs and see what the rule decides.

Try the rule

State Event

Loading the rule...

The answer comes from the Rust function step, compiled to WebAssembly and running in your browser. Lean proves that this function computes what the model computes, for every input (Verify/RustRules.lean). The few lines that pass your choices to it are not part of the proof.

3.4. Guarantees🔗

3.4.1. Delivered services cannot be cancelled🔗

guarantee

Rules.OfferOrder.delivered_not_cancellable :
  Rules.OfferOrder.step Rules.OfferOrder.DeliveryState.delivered
        Rules.OfferOrder.DeliveryEvent.cancel =
      none ∧
    ∀ (e : Rules.OfferOrder.DeliveryEvent),
      Rules.OfferOrder.step Rules.OfferOrder.DeliveryState.delivered e ≠
        some Rules.OfferOrder.DeliveryState.cancelled
Rules.OfferOrder.delivered_not_cancellable :
  Rules.OfferOrder.step
        Rules.OfferOrder.DeliveryState.delivered
        Rules.OfferOrder.DeliveryEvent.cancel =
      none ∧
    ∀
      (e :
        Rules.OfferOrder.DeliveryEvent),
      Rules.OfferOrder.step
          Rules.OfferOrder.DeliveryState.delivered
          e ≠
        some
          Rules.OfferOrder.DeliveryState.cancelled

A delivered service can never be cancelled: the cancel event is refused in the delivered state, and no event moves a delivered service to cancelled.

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

Checks acceptance criteria OO-002.4.

3.5. Examples🔗

3.5.1. Delivery walk🔗

example

Rules.OfferOrder.deliveryWalk : Rules.OfferOrder.DeliveryWalk
Rules.OfferOrder.deliveryWalk :
  Rules.OfferOrder.DeliveryWalk

Given a flight that is ready for delivery.

When the passenger flies, and someone then tries to cancel the flight.

Then the flight is delivered, and the cancel is refused.

What Lean computed:

After deliver: delivered
After cancel: none

Checks acceptance criteria OO-002.1, OO-002.4.

3.5.2. Transition table🔗

example

Rules.OfferOrder.transitionTable : List Rules.OfferOrder.Transition
Rules.OfferOrder.transitionTable :
  List Rules.OfferOrder.Transition

Given each of the four delivery states.

When each of the three delivery events is applied to it.

Then deliver and cancel move a ready service, refund moves a cancelled service, and every other event is refused. The review document draws this table as the delivery state diagram.

What Lean computed:

Before	Event	After
ready	deliver	delivered
ready	cancel	cancelled
ready	refund	none
delivered	deliver	none
delivered	cancel	none
delivered	refund	none
cancelled	deliver	none
cancelled	cancel	none
cancelled	refund	refunded
refunded	deliver	none
refunded	cancel	none
refunded	refund	none

Checks acceptance criteria OO-002.1, OO-002.2, OO-002.3, OO-002.4, OO-002.5.