Created
October 28, 2022 17:13
-
-
Save hwayne/ba8bc6fc362e56027a38e57e64c1a2c8 to your computer and use it in GitHub Desktop.
Email Filters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ---- 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 | |
| ==== |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment