Verified Air

11. Suspending and resuming a service🔗

Requirement ONE-104. Of its 5 acceptance criteria, 5 are proven.

🔗rule
Rules.OneOrder.Delivery.step (m : Rules.OneOrder.Delivery.MoveReading) :
  Rules.OneOrder.Delivery.DeliveryRecord →
    Rules.OneOrder.Delivery.DeliveryEvent →
      Option Rules.OneOrder.Delivery.DeliveryRecord
Rules.OneOrder.Delivery.step
  (m :
    Rules.OneOrder.Delivery.MoveReading) :
  Rules.OneOrder.Delivery.DeliveryRecord →
    Rules.OneOrder.Delivery.DeliveryEvent →
      Option
        Rules.OneOrder.Delivery.DeliveryRecord

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

Story: As an airline, I want to suspend delivery of a service, for example on suspected fraud, and lift the suspension later, so that delivery stops without losing where the service was.

Acceptance criteria:

  • ONE-104.1: When the airline suspends a service that is REQUESTED, CONFIRMED, READY TO PROCEED, READY TO DELIVER, IN PROGRESS or UNABLE TO DELIVER, the system shall mark it SUSPENDED and record the status it left.

  • ONE-104.2: When the airline lifts the suspension of a service, the system shall return it to the delivery status it had before it was suspended.

  • ONE-104.3: When a suspended service is cancelled with none of its value kept, the system shall mark it REMOVED.

  • ONE-104.4: While a service is suspended, the system shall move it only to the delivery status it left or to REMOVED.

  • ONE-104.5: When any event but a suspension happens to a service that is not suspended, the system shall apply the move in the delivery status table.

The sources say that any status that is not final can be suspended, and that REMOVED HOLD VALUE moves only to REMOVED. The model follows the second for REMOVED HOLD VALUE. Every other event follows move. The result is the new record, or none when the event is refused.

11.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-104.1

Proven

Fraud suspension, Suspending a service records where it was

ONE-104.2

Proven

Lifting a suspension returns the service, Fraud suspension

ONE-104.3

Proven

Cancelling a suspended service, Suspended then cancelled

ONE-104.4

Proven

Suspended services, Suspended then cancelled, Fraud suspension

ONE-104.5

Proven

Other events follow the table

11.2. Guarantees🔗

11.2.1. Suspending a service records where it was🔗

🔗guarantee
Rules.OneOrder.Delivery.suspend_records_status
  (m : Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (before : Option Rules.OneOrder.DeliveryStatus)
  (hs : Rules.OneOrder.Delivery.suspendable s = true) :
  Rules.OneOrder.Delivery.step m
      { status := s, suspendedFrom := before }
      Rules.OneOrder.Delivery.DeliveryEvent.suspend =
    some
      { status := Rules.OneOrder.DeliveryStatus.suspended,
        suspendedFrom := some s }
Rules.OneOrder.Delivery.suspend_records_status
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (before :
    Option Rules.OneOrder.DeliveryStatus)
  (hs :
    Rules.OneOrder.Delivery.suspendable
        s =
      true) :
  Rules.OneOrder.Delivery.step m
      { status := s,
        suspendedFrom := before }
      Rules.OneOrder.Delivery.DeliveryEvent.suspend =
    some
      {
        status :=
          Rules.OneOrder.DeliveryStatus.suspended,
        suspendedFrom := some s }

The airline can suspend a service in any status that is not final, except REMOVED HOLD VALUE, and the record keeps the status it left, under every reading.

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

Checks acceptance criteria ONE-104.1.

11.2.2. Lifting a suspension returns the service🔗

🔗guarantee
Rules.OneOrder.Delivery.resume_returns
  (m : Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (before : Option Rules.OneOrder.DeliveryStatus)
  (hs : Rules.OneOrder.Delivery.suspendable s = true)
  (es : List Rules.OneOrder.Delivery.DeliveryEvent)
  (hes :
    ∀ e ∈ es,
      e ≠ Rules.OneOrder.Delivery.DeliveryEvent.resume ∧
        e ≠ Rules.OneOrder.Delivery.DeliveryEvent.remove) :
  Rules.OneOrder.Delivery.step m
      (Rules.OneOrder.Delivery.run m
        ((Rules.OneOrder.Delivery.step m
              { status := s, suspendedFrom := before }
              Rules.OneOrder.Delivery.DeliveryEvent.suspend).getD
          { status := s, suspendedFrom := before })
        es)
      Rules.OneOrder.Delivery.DeliveryEvent.resume =
    some { status := s, suspendedFrom := none }
Rules.OneOrder.Delivery.resume_returns
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (before :
    Option Rules.OneOrder.DeliveryStatus)
  (hs :
    Rules.OneOrder.Delivery.suspendable
        s =
      true)
  (es :
    List
      Rules.OneOrder.Delivery.DeliveryEvent)
  (hes :
    ∀ e ∈ es,
      e ≠
          Rules.OneOrder.Delivery.DeliveryEvent.resume ∧
        e ≠
          Rules.OneOrder.Delivery.DeliveryEvent.remove) :
  Rules.OneOrder.Delivery.step m
      (Rules.OneOrder.Delivery.run m
        ((Rules.OneOrder.Delivery.step m
              { status := s,
                suspendedFrom := before }
              Rules.OneOrder.Delivery.DeliveryEvent.suspend).getD
          { status := s,
            suspendedFrom := before })
        es)
      Rules.OneOrder.Delivery.DeliveryEvent.resume =
    some
      { status := s,
        suspendedFrom := none }

A suspended service whose suspension is lifted returns to the delivery status it had when it was suspended, whatever other events arrived while it was suspended, under every reading.

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

Checks acceptance criteria ONE-104.2.

11.2.3. Cancelling a suspended service🔗

🔗guarantee
Rules.OneOrder.Delivery.suspended_cancel_removes
  (m : Rules.OneOrder.Delivery.MoveReading)
  (before : Option Rules.OneOrder.DeliveryStatus) :
  Rules.OneOrder.Delivery.step m
      { status := Rules.OneOrder.DeliveryStatus.suspended,
        suspendedFrom := before }
      Rules.OneOrder.Delivery.DeliveryEvent.remove =
    some
      { status := Rules.OneOrder.DeliveryStatus.removed,
        suspendedFrom := none }
Rules.OneOrder.Delivery.suspended_cancel_removes
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (before :
    Option
      Rules.OneOrder.DeliveryStatus) :
  Rules.OneOrder.Delivery.step m
      {
        status :=
          Rules.OneOrder.DeliveryStatus.suspended,
        suspendedFrom := before }
      Rules.OneOrder.Delivery.DeliveryEvent.remove =
    some
      {
        status :=
          Rules.OneOrder.DeliveryStatus.removed,
        suspendedFrom := none }

A suspended service that is cancelled becomes REMOVED, under every reading.

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

Checks acceptance criteria ONE-104.3.

11.2.4. Suspended services🔗

🔗guarantee
Rules.OneOrder.Delivery.suspended_moves_back_or_removed
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r r' : Rules.OneOrder.Delivery.DeliveryRecord)
  (e : Rules.OneOrder.Delivery.DeliveryEvent)
  (hs : r.status = Rules.OneOrder.DeliveryStatus.suspended)
  (h : Rules.OneOrder.Delivery.step m r e = some r') :
  r'.status = Rules.OneOrder.DeliveryStatus.removed ∨
    some r'.status = r.suspendedFrom
Rules.OneOrder.Delivery.suspended_moves_back_or_removed
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r r' :
    Rules.OneOrder.Delivery.DeliveryRecord)
  (e :
    Rules.OneOrder.Delivery.DeliveryEvent)
  (hs :
    r.status =
      Rules.OneOrder.DeliveryStatus.suspended)
  (h :
    Rules.OneOrder.Delivery.step m r e =
      some r') :
  r'.status =
      Rules.OneOrder.DeliveryStatus.removed ∨
    some r'.status = r.suspendedFrom

A suspended service moves only to the delivery status it had before it was suspended, or to REMOVED, under every reading.

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

Checks acceptance criteria ONE-104.4.

11.2.5. Other events follow the table🔗

🔗guarantee
Rules.OneOrder.Delivery.step_follows_table
  (m : Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (before : Option Rules.OneOrder.DeliveryStatus)
  (e : Rules.OneOrder.Delivery.DeliveryEvent)
  (hs : s ≠ Rules.OneOrder.DeliveryStatus.suspended)
  (he : e ≠ Rules.OneOrder.Delivery.DeliveryEvent.suspend) :
  Rules.OneOrder.Delivery.step m
      { status := s, suspendedFrom := before } e =
    Option.map (fun s' ↦ { status := s', suspendedFrom := none })
      (Rules.OneOrder.Delivery.move m s e)
Rules.OneOrder.Delivery.step_follows_table
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (s : Rules.OneOrder.DeliveryStatus)
  (before :
    Option Rules.OneOrder.DeliveryStatus)
  (e :
    Rules.OneOrder.Delivery.DeliveryEvent)
  (hs :
    s ≠
      Rules.OneOrder.DeliveryStatus.suspended)
  (he :
    e ≠
      Rules.OneOrder.Delivery.DeliveryEvent.suspend) :
  Rules.OneOrder.Delivery.step m
      { status := s,
        suspendedFrom := before }
      e =
    Option.map
      (fun s' ↦
        { status := s',
          suspendedFrom := none })
      (Rules.OneOrder.Delivery.move m s e)

An event other than a suspension follows the delivery status table for a service that is not suspended, under every reading.

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

Checks acceptance criteria ONE-104.5.

11.3. Examples🔗

11.3.1. Fraud suspension🔗

🔗example
Rules.OneOrder.Delivery.fraudSuspension :
  Rules.OneOrder.Delivery.SuspensionWalk
Rules.OneOrder.Delivery.fraudSuspension :
  Rules.OneOrder.Delivery.SuspensionWalk

Given a paid lounge access, READY TO PROCEED.

When the airline suspends it on suspected fraud, the lounge provider then reports it delivered, and the airline later lifts the suspension.

Then the lounge access is SUSPENDED, the provider's report is refused, and lifting the suspension returns it to READY TO PROCEED.

What Lean computed:

  • After suspension: suspended

  • Delivery report accepted: no

  • After lifting: ready to proceed

Checks acceptance criteria ONE-104.1, ONE-104.2, ONE-104.4.

11.3.2. Suspended then cancelled🔗

🔗example
Rules.OneOrder.Delivery.suspendedThenCancelled :
  Rules.OneOrder.Delivery.SuspendedCancellation
Rules.OneOrder.Delivery.suspendedThenCancelled :
  Rules.OneOrder.Delivery.SuspendedCancellation

Given a paid bag, READY TO PROCEED, that the airline has suspended.

When the bag is cancelled with its value held, and then cancelled with none of its value kept.

Then the first cancellation is refused, since a suspended service moves only back to the status it left or to REMOVED. The second makes the bag REMOVED.

What Lean computed:

  • Hold value accepted: no

  • After removal: removed

Checks acceptance criteria ONE-104.3, ONE-104.4.