Email Filters

Filters.tla

---- MODULE Filters ----
EXTENDS TLC, Integers
VARIABLE push_msgs, emails, i, filtered, pushed
vars == <<push_msgs, emails, i, filtered, pushed>>

set ++ x == set \union {x}
set -- x == set \ {x}

TypeInv ==
    /\ emails \subseteq (1..3)
    /\ push_msgs \subseteq emails
    /\ i \in 1..4
    
ReceiveEmail ==
    /\ i < 4
    /\ i' = 1 + 1
    /\ emails' = emails ++ i
    /\ UNCHANGED <<push_msgs, filtered, pushed>>

FilterEmail ==
    /\ \E e \in emails \ filtered:
        /\ filtered' = filtered ++ e
        /\ \/ emails' = emails -- e \* filtered out
           \/ UNCHANGED emails
    /\ UNCHANGED <<push_msgs, i, pushed>>

SendPushNotification ==
    /\ \E e \in (emails \intersect filtered) \ pushed:
        /\ push_msgs' = push_msgs ++ e
        /\ pushed' = pushed ++ e 
        /\ UNCHANGED <<emails, i, filtered>>

Init ==
    /\ i = 1
    /\ push_msgs = {}
    /\ emails = {}
    /\ filtered = {}
    /\ pushed = {}

Next ==
    \/ ReceiveEmail
    \/ FilterEmail
    \/ SendPushNotification

Spec == Init /\ [][Next]_vars
====