Vanlightly

------------------- 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

------------------- 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

------------------- 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

\* MV CONSTANT declarations
CONSTANTS
a1 = a1
a2 = a2
a3 = a3
a4 = a4
a5 = a5
a6 = a6
a7 = a7
a8 = a8

Vanlightly

---------------------------- MODULE TwoCounters ----------------------------
EXTENDS Integers

CONSTANT C, Limit
VARIABLES counter

Init == 
    counter = [c \in C |-> 0]
    
Next ==

Vanlightly

----------------------------- MODULE JumpyClock -----------------------------
EXTENDS Naturals

VARIABLES hour, minute, second

Init ==
    /\ hour = 0
    /\ minute = 0
    /\ second = 0

Vanlightly

------------------------------- MODULE Clock -------------------------------
EXTENDS Naturals


VARIABLES hour, minute, second

Init ==
    /\ hour = 0
    /\ minute = 0
    /\ second = 0

Vanlightly

CONSTANTS NodeCount
VARIABLES running,
          peer_status
Nodes == 1..NodeCount

Vanlightly

--------------------------- MODULE gossa_v2 ---------------------------
(*
To hit the liveness property of stuttering while still not
converged, comment out the actions Die and CorrectlyDetectDeadNode
in the Next state formula.
*)


EXTENDS Naturals

Vanlightly

--------------------------- MODULE gossa_v3 ---------------------------

(*
To see how a state constraint can break liveness try running this spec
twice with:
- NodeCount=2:
- Use the LivenessSpec temporal formula.
- Uncomment the line '/\ generation[source] < 4' in Gossip.
  This line adds an artificial rule that will prevent convergence.
Run 1: