---------------------------- MODULE AtomicPayment ----------------------------
EXTENDS CostAlgebra
CONSTANTS InitialFunds, BaseCost, Increases, Reductions, LateUse
VARIABLES available, paid, pending, declined

vars == <<available, paid, pending, declined>>
EmptyModifiers == <<>>
Cost == ModifiedCost(BaseCost, Increases, Reductions)
Ready == ~paid /\ ~pending /\ ~declined

Init == /\ available = InitialFunds
        /\ paid = FALSE
        /\ pending = FALSE
        /\ declined = FALSE

\* LateUse=TRUE is a deliberately defective test variant, never ordinary policy.
Pay == /\ Ready
       /\ available >= Cost
       /\ available' = available - Cost
       /\ paid' = ~LateUse
       /\ pending' = TRUE
       /\ UNCHANGED declined

Complete == /\ pending
            /\ paid' = TRUE
            /\ pending' = FALSE
            /\ UNCHANGED <<available, declined>>

Decline == /\ Ready
           /\ declined' = TRUE
           /\ UNCHANGED <<available, paid, pending>>

Next == Pay \/ Complete \/ Decline
Spec == Init /\ [][Next]_vars /\ WF_vars(Complete)

TypeOK == /\ available \in Nat
          /\ paid \in BOOLEAN
          /\ pending \in BOOLEAN
          /\ declined \in BOOLEAN
UseRecorded == pending => paid
PaymentIsExact == paid => available = InitialFunds - Cost
DeclineIsUnpaid == declined => (~paid /\ ~pending /\ available = InitialFunds)
AdmissionMatchesWallet == Ready => ((ENABLED Pay) <=> available >= Cost)
NoDoublePayment == paid => ~ENABLED Pay
Completion == [](pending => <>~pending)
=============================================================================