12. Ending a service from another area🔗

Requirement ONE-105. Of its 3 acceptance criteria, 3 are proven.

rule

Rules.OneOrder.Delivery.endWith
  (m : Rules.OneOrder.Delivery.MoveReading)
  (e : Rules.OneOrder.Delivery.DeliveryEvent)
  (st : Rules.OneOrder.ServiceStatus) (s : Rules.OneOrder.Service) :
  Rules.OneOrder.Service
Rules.OneOrder.Delivery.endWith
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (e :
    Rules.OneOrder.Delivery.DeliveryEvent)
  (st : Rules.OneOrder.ServiceStatus)
  (s : Rules.OneOrder.Service) :
  Rules.OneOrder.Service

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

Story: As a revenue accountant, I want every area to move a service's delivery status by the same table, so that a final status I was told about never changes afterwards.

Acceptance criteria:

ONE-105.1: When a rule ends a service with an event that the delivery status table allows from the service's delivery status, the system shall give the service the rule's service status and the delivery status the table gives.
ONE-105.2: If the delivery status table refuses a rule's event for a service's delivery status, then the system shall leave the service as it was.
ONE-105.3: The system shall move a service's delivery status only along a move of the delivery status table, whichever area changes it.

The rules that end services call this one: cancelling an unpaid order and changing an order item, cancelling order items and removing services from a bundle, the airline cancelling a flight, and an unpaid item reaching its payment time limit. A successful payment moves a CONFIRMED service to READY TO PROCEED, a move of the table. Accounting keeps its own record of the final status it is told about and changes no service. The result is the service afterwards.

12.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-105.1	Proven	End with allowed
ONE-105.2	Proven	Change after outbound flown, Cancel flight while requested, End with refused
ONE-105.3	Proven	Every area moves delivery statuses along the table

12.2. Guarantees🔗

12.2.1. End with allowed🔗

guarantee

Rules.OneOrder.Delivery.endWith_allowed
  (m : Rules.OneOrder.Delivery.MoveReading)
  (e : Rules.OneOrder.Delivery.DeliveryEvent)
  (st : Rules.OneOrder.ServiceStatus) (s : Rules.OneOrder.Service)
  (d : Rules.OneOrder.DeliveryStatus)
  (h : Rules.OneOrder.Delivery.nextDelivery m e s = some d) :
  Rules.OneOrder.Delivery.endWith m e st s =
    { id := s.id, passenger := s.passenger, segment := s.segment,
      status := st, delivery := d }
Rules.OneOrder.Delivery.endWith_allowed
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (e :
    Rules.OneOrder.Delivery.DeliveryEvent)
  (st : Rules.OneOrder.ServiceStatus)
  (s : Rules.OneOrder.Service)
  (d : Rules.OneOrder.DeliveryStatus)
  (h :
    Rules.OneOrder.Delivery.nextDelivery m
        e s =
      some d) :
  Rules.OneOrder.Delivery.endWith m e st
      s =
    { id := s.id,
      passenger := s.passenger,
      segment := s.segment, status := st,
      delivery := d }

When the delivery status table allows a rule's event from a service's delivery status, the service takes the rule's service status and the delivery status the table gives, under every reading.

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

Checks acceptance criteria ONE-105.1.

12.2.2. End with refused🔗

guarantee

Rules.OneOrder.Delivery.endWith_refused
  (m : Rules.OneOrder.Delivery.MoveReading)
  (e : Rules.OneOrder.Delivery.DeliveryEvent)
  (st : Rules.OneOrder.ServiceStatus) (s : Rules.OneOrder.Service)
  (h : Rules.OneOrder.Delivery.nextDelivery m e s = none) :
  Rules.OneOrder.Delivery.endWith m e st s = s
Rules.OneOrder.Delivery.endWith_refused
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (e :
    Rules.OneOrder.Delivery.DeliveryEvent)
  (st : Rules.OneOrder.ServiceStatus)
  (s : Rules.OneOrder.Service)
  (h :
    Rules.OneOrder.Delivery.nextDelivery m
        e s =
      none) :
  Rules.OneOrder.Delivery.endWith m e st
      s =
    s

When the delivery status table refuses a rule's event for a service's delivery status, the service is left as it was, under every reading.

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

Checks acceptance criteria ONE-105.2.

12.2.3. Every area moves delivery statuses along the table🔗

guarantee

Rules.OneOrder.delivery_moves_follow_table
  (m : Rules.OneOrder.Delivery.MoveReading) :
  (∀ (o : Rules.OneOrder.Order),
      Rules.OneOrder.Delivery.MovesAlongTable m
        (Rules.OneOrder.orderServices o)
        (Rules.OneOrder.orderServices
          (Rules.OneOrder.Change.cancelDirect m o))) ∧
    (∀ (o o' : Rules.OneOrder.Order)
        (c : Rules.OneOrder.Change.ItemChange),
        Rules.OneOrder.Change.changeItem m o c = Except.ok o' →
          Rules.OneOrder.Delivery.MovesAlongTable m
            (Rules.OneOrder.orderServices o)
            (List.flatMap (fun x ↦ x.services)
              (List.take o.items.length o'.items))) ∧
      (∀ (a : Rules.OneOrder.AirlineChange.ApplyAt)
          (vo vo' : Rules.OneOrder.AirlineChange.VersionedOrder)
          (c : Rules.OneOrder.AirlineChange.Reaccommodation),
          Rules.OneOrder.AirlineChange.notifyChange m a vo c =
              Except.ok vo' →
            Rules.OneOrder.Delivery.MovesAlongTable m
              (Rules.OneOrder.orderServices vo.order)
              (List.flatMap (fun x ↦ x.services)
                (List.take vo.order.items.length vo'.order.items))) ∧
        (∀ (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),
            Rules.OneOrder.Ancillaries.cancelItems m h r d allows o
                  named =
                Except.ok o' →
              Rules.OneOrder.Delivery.MovesAlongTable m
                (Rules.OneOrder.orderServices o)
                (Rules.OneOrder.orderServices o')) ∧
          (∀ (sh : Rules.OneOrder.Ancillaries.BundleShare)
              (o o' : Rules.OneOrder.Order) (item : String)
              (ids : List String) (x : Rules.Core.Money),
              Rules.OneOrder.Ancillaries.removeFromBundle m sh o item
                    ids =
                  Except.ok (o', x) →
                Rules.OneOrder.Delivery.MovesAlongTable m
                  (Rules.OneOrder.orderServices o)
                  (Rules.OneOrder.orderServices o')) ∧
            (∀ (r : Rules.OneOrder.AirlineChange.FlightRefund)
                (seg : String) (o : Rules.OneOrder.Order),
                Rules.OneOrder.Delivery.MovesAlongTable m
                  (Rules.OneOrder.orderServices o)
                  (Rules.OneOrder.orderServices
                    (Rules.OneOrder.AirlineChange.cancelFlight m r seg
                        o).order)) ∧
              (∀ (r : Rules.OneOrder.Payment.Removal)
                  (now : Rules.Core.Instant)
                  (o : Rules.OneOrder.Payment.PayableOrder),
                  Rules.OneOrder.Delivery.MovesAlongTable m
                    (Rules.OneOrder.payableServices o.items)
                    (Rules.OneOrder.payableServices
                      (Rules.OneOrder.Payment.expireUnpaid m r now
                          o).items)) ∧
                ∀ (p : Rules.OneOrder.Payment.Transaction)
                  (items : List Rules.OneOrder.Payment.PayableItem),
                  Rules.OneOrder.Delivery.MovesAlongTable m
                    (Rules.OneOrder.payableServices items)
                    (Rules.OneOrder.payableServices
                      (Rules.OneOrder.Payment.applyOutcome p items))
Rules.OneOrder.delivery_moves_follow_table
  (m :
    Rules.OneOrder.Delivery.MoveReading) :
  (∀ (o : Rules.OneOrder.Order),
      Rules.OneOrder.Delivery.MovesAlongTable
        m (Rules.OneOrder.orderServices o)
        (Rules.OneOrder.orderServices
          (Rules.OneOrder.Change.cancelDirect
            m o))) ∧
    (∀ (o o' : Rules.OneOrder.Order)
        (c :
          Rules.OneOrder.Change.ItemChange),
        Rules.OneOrder.Change.changeItem m
              o c =
            Except.ok o' →
          Rules.OneOrder.Delivery.MovesAlongTable
            m
            (Rules.OneOrder.orderServices
              o)
            (List.flatMap
              (fun x ↦ x.services)
              (List.take o.items.length
                o'.items))) ∧
      (∀
          (a :
            Rules.OneOrder.AirlineChange.ApplyAt)
          (vo vo' :
            Rules.OneOrder.AirlineChange.VersionedOrder)
          (c :
            Rules.OneOrder.AirlineChange.Reaccommodation),
          Rules.OneOrder.AirlineChange.notifyChange
                m a vo c =
              Except.ok vo' →
            Rules.OneOrder.Delivery.MovesAlongTable
              m
              (Rules.OneOrder.orderServices
                vo.order)
              (List.flatMap
                (fun x ↦ x.services)
                (List.take
                  vo.order.items.length
                  vo'.order.items))) ∧
        (∀
            (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),
            Rules.OneOrder.Ancillaries.cancelItems
                  m h r d allows o named =
                Except.ok o' →
              Rules.OneOrder.Delivery.MovesAlongTable
                m
                (Rules.OneOrder.orderServices
                  o)
                (Rules.OneOrder.orderServices
                  o')) ∧
          (∀
              (sh :
                Rules.OneOrder.Ancillaries.BundleShare)
              (o o' :
                Rules.OneOrder.Order)
              (item : String)
              (ids : List String)
              (x : Rules.Core.Money),
              Rules.OneOrder.Ancillaries.removeFromBundle
                    m sh o item ids =
                  Except.ok (o', x) →
                Rules.OneOrder.Delivery.MovesAlongTable
                  m
                  (Rules.OneOrder.orderServices
                    o)
                  (Rules.OneOrder.orderServices
                    o')) ∧
            (∀
                (r :
                  Rules.OneOrder.AirlineChange.FlightRefund)
                (seg : String)
                (o :
                  Rules.OneOrder.Order),
                Rules.OneOrder.Delivery.MovesAlongTable
                  m
                  (Rules.OneOrder.orderServices
                    o)
                  (Rules.OneOrder.orderServices
                    (Rules.OneOrder.AirlineChange.cancelFlight
                        m r seg
                        o).order)) ∧
              (∀
                  (r :
                    Rules.OneOrder.Payment.Removal)
                  (now :
                    Rules.Core.Instant)
                  (o :
                    Rules.OneOrder.Payment.PayableOrder),
                  Rules.OneOrder.Delivery.MovesAlongTable
                    m
                    (Rules.OneOrder.payableServices
                      o.items)
                    (Rules.OneOrder.payableServices
                      (Rules.OneOrder.Payment.expireUnpaid
                          m r now
                          o).items)) ∧
                ∀
                  (p :
                    Rules.OneOrder.Payment.Transaction)
                  (items :
                    List
                      Rules.OneOrder.Payment.PayableItem),
                  Rules.OneOrder.Delivery.MovesAlongTable
                    m
                    (Rules.OneOrder.payableServices
                      items)
                    (Rules.OneOrder.payableServices
                      (Rules.OneOrder.Payment.applyOutcome
                        p items))

Every rule outside the Delivery area that changes a service's delivery status moves it only along a move of the delivery status table, keeping its reference, under every reading of the sources: cancelling an unpaid order, changing an order item, an airline change, cancelling order items, removing services from a bundle, the airline cancelling a flight, removing unpaid items at their payment time limit, and a successful payment.

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

Checks acceptance criteria ONE-105.3.

12.3. Examples🔗

12.3.1. Cancel flight while requested🔗

example

Rules.OneOrder.AirlineChange.cancelFlightWhileRequested :
  Rules.OneOrder.AirlineChange.FlightCancelled
Rules.OneOrder.AirlineChange.cancelFlightWhileRequested :
  Rules.OneOrder.AirlineChange.FlightCancelled

Given the paid return trip at 1,000.00 EUR, with its bag on the inbound flight still REQUESTED from the airline.

When the airline cancels the inbound flight and does not move the customer to another one.

Then the inbound flight is CANCELLED with delivery status UNABLE TO DELIVER. The bag stays REQUESTED, and live, on a flight that will not operate, because the delivery status table has no move from REQUESTED to UNABLE TO DELIVER.

What Lean computed:

Item: ORDITM-1
Price: 1000.00 EUR
Services: see the table below.
Cautious: active
Strict: active
Refund as shown: 0.00 EUR
Refund by flight: 500.00 EUR

Services:

Service	Segment	Status	Delivery
SVC-OUT	SEG-OUT	confirmed	ready to proceed
SVC-IN	SEG-IN	cancelled	unable to deliver
BAG-IN	SEG-IN	requested	requested

Checks acceptance criteria ONE-704.1, ONE-704.6, ONE-105.2.

12.3.2. Change after outbound flown🔗

example

Rules.OneOrder.Change.changeAfterOutboundFlown :
  Except Rules.OneOrder.Change.ChangeRejection
    Rules.OneOrder.Change.ChangedOrder
Rules.OneOrder.Change.changeAfterOutboundFlown :
  Except
    Rules.OneOrder.Change.ChangeRejection
    Rules.OneOrder.Change.ChangedOrder

Given the trip order with its outbound flight already flown, so DELIVERED, and its inbound flight ready to proceed.

When the seller accepts and pays a change that keeps no service and puts a new inbound flight in a new item at 900.00 EUR.

Then the inbound service is cancelled and removed. The outbound service stays DELIVERED, because the delivery status table lets no event move a delivered service.

What Lean computed:

Accepted. The result:

Items: see the table below.
Services: see the table below.

Items:

Item	Price	Cautious	Strict
ORDITM-1	1000.00 EUR	closed	closed
ORDITM-2	900.00 EUR	active	active

Services:

Item	Service	Status	Delivery
ORDITM-1	SVC-OUT	confirmed	delivered
ORDITM-1	SVC-IN	cancelled	removed
ORDITM-2	SVC-IN-2	confirmed	ready to proceed

Checks acceptance criteria ONE-204.3, ONE-105.2.