Jack Vanlightly Vanlightly
This file contains hidden or 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 TwoCounters ---------------------------- | |
| EXTENDS Integers | |
| CONSTANT C, Limit | |
| VARIABLES counter | |
| Init == | |
| counter = [c \in C |-> 0] | |
| Next == |
Vanlightly
/ stats_10q_10a.cfg
Created
July 24, 2020 14:33
This file contains hidden or 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
| \* MV CONSTANT declarations | |
| CONSTANTS | |
| a1 = a1 | |
| a2 = a2 | |
| a3 = a3 | |
| a4 = a4 | |
| a5 = a5 | |
| a6 = a6 | |
| a7 = a7 | |
| a8 = a8 |
Vanlightly
/ rebalancing_with_tlcgetset_inv.tla
Created
July 23, 2020 15:03
This file contains hidden or 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 rabbit_leaderless_rebalancing ------------------- | |
| EXTENDS TLC, Sequences, Integers, FiniteSets, Naturals | |
| CONSTANTS Q, \* set of queues, e.g. { q1, q2, q3, q4, q5 } | |
| A \* set of apps, e.g. { a1, a2, a3 } | |
| (* | |
| Models an algorithm that balances the consumption of group of Q queues over a group of | |
| A applications, using the Single Active Consumer (SAC) feature of RabbitMQ. |
Vanlightly
/ rebalancing_with_tlcgetset.tla
Created
July 22, 2020 19:33
This file contains hidden or 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 rabbit_leaderless_rebalancing ------------------- | |
| EXTENDS TLC, Sequences, Integers, FiniteSets, Naturals | |
| CONSTANTS Q, \* set of queues, e.g. { q1, q2, q3, q4, q5 } | |
| A \* set of apps, e.g. { a1, a2, a3 } | |
| (* | |
| Models an algorithm that balances the consumption of group of Q queues over a group of | |
| A applications, using the Single Active Consumer (SAC) feature of RabbitMQ. |
Vanlightly
/ rabbit_leaderless_rebalancing.tla
Last active
July 22, 2020 22:03
An algorithm for coooperating RabbitMQ clients to balance consumption over a group of Sing-Active-Consumer queues
This file contains hidden or 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 rabbit_leaderless_rebalancing ------------------- | |
| EXTENDS TLC, Sequences, Integers, FiniteSets, Naturals | |
| CONSTANTS Q, \* set of queues, e.g. { q1, q2, q3, q4, q5 } | |
| A \* set of apps, e.g. { a1, a2, a3 } | |
| (* | |
| Models an algorithm that balances the consumption of group of Q queues over a group of | |
| A applications, using the Single Active Consumer (SAC) feature of RabbitMQ. |
NewerOlder