Modeling Token Buckets in PlusCal and TLA+

8 points by ahelwer