------------------------------ MODULE payment ------------------------------
EXTENDS Integers, TLC

CONSTANT CreditCards

(* --fair algorithm payment

variables
  valid = CreditCards,
  purchases = {},
  processed = {},
  failed = {}

define
    allPurchasesValid == \A purchase \in purchases : purchase \in valid
end define



fair process time = "invalidate"
begin Invalidate:
  await valid /= {};
  with c \in valid do
    valid := valid \ {c}
  end with
end process

fair process user \in CreditCards
begin
  Check:
    if self \notin failed /\ self \in valid then
      purchases := purchases \cup {self}
    elsif self \notin valid then
      valid := valid \cup {self};
      if self \in failed then purchases := purchases \cup {self} end if
    end if;
  goto Check
end process

fair process payment = "processpay"
begin Process:
  await purchases /= {};
  with p \in purchases do
    purchases := purchases \ {p};
    if p \in valid then
      processed := processed \cup {p}
    else
      failed := failed \cup {p}
    end if
  end with;
  NextPurchase:
  processed := {};
  goto Process
end process

end algorithm *)
\* BEGIN TRANSLATION
VARIABLES valid, purchases, processed, failed, pc

(* define statement *)
allPurchasesValid == \A purchase \in purchases : purchase \in valid


vars == << valid, purchases, processed, failed, pc >>

ProcSet == {"invalidate"} \cup (CreditCards) \cup {"processpay"}

Init == (* Global variables *)
        /\ valid = CreditCards
        /\ purchases = {}
        /\ processed = {}
        /\ failed = {}
        /\ pc = [self \in ProcSet |-> CASE self = "invalidate" -> "Invalidate"
                                        [] self \in CreditCards -> "Check"
                                        [] self = "processpay" -> "Process"]

Invalidate == /\ pc["invalidate"] = "Invalidate"
              /\ valid /= {}
              /\ \E c \in valid:
                   valid' = valid \ {c}
              /\ pc' = [pc EXCEPT !["invalidate"] = "Done"]
              /\ UNCHANGED << purchases, processed, failed >>

time == Invalidate

Check(self) == /\ pc[self] = "Check"
               /\ IF self \notin failed /\ self \in valid
                     THEN /\ purchases' = (purchases \cup {self})
                          /\ valid' = valid
                     ELSE /\ IF self \notin valid
                                THEN /\ valid' = (valid \cup {self})
                                     /\ IF self \in failed
                                           THEN /\ purchases' = (purchases \cup {self})
                                           ELSE /\ TRUE
                                                /\ UNCHANGED purchases
                                ELSE /\ TRUE
                                     /\ UNCHANGED << valid, purchases >>
               /\ pc' = [pc EXCEPT ![self] = "Check"]
               /\ UNCHANGED << processed, failed >>

user(self) == Check(self)

Process == /\ pc["processpay"] = "Process"
           /\ purchases /= {}
           /\ \E p \in purchases:
                /\ purchases' = purchases \ {p}
                /\ IF p \in valid
                      THEN /\ processed' = (processed \cup {p})
                           /\ UNCHANGED failed
                      ELSE /\ failed' = (failed \cup {p})
                           /\ UNCHANGED processed
           /\ pc' = [pc EXCEPT !["processpay"] = "NextPurchase"]
           /\ valid' = valid

NextPurchase == /\ pc["processpay"] = "NextPurchase"
                /\ processed' = {}
                /\ pc' = [pc EXCEPT !["processpay"] = "Process"]
                /\ UNCHANGED << valid, purchases, failed >>

payment == Process \/ NextPurchase

Next == time \/ payment
           \/ (\E self \in CreditCards: user(self))
           \/ (* Disjunct to prevent deadlock on termination *)
              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == /\ Init /\ [][Next]_vars
        /\ WF_vars(Next)
        /\ WF_vars(time)
        /\ \A self \in CreditCards : WF_vars(user(self))
        /\ WF_vars(payment)

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION



=============================================================================
\* Modification History
\* Last modified Sun Jan 20 22:34:58 EET 2019 by Harald
\* Created Wed Jan 16 22:41:36 EET 2019 by Harald