Vanlightly

\* Model parameters
CONSTANTS
    p1 = p1
    TxnLogPartitions = {p1}
    tp1 = tp1
    TopicPartitions = {p1}
    b1 = b1
    b2 = b2
    Brokers = {b1, b2}
    c1 = c1

Vanlightly

role Pong:
    action Init:
        self.response = None

    atomic action ReceivePing:
        recv_msg = any network[self.ID]
        send_msg = "hi " + recv_msg.name

        # Cache the first response and then always send that
        if self.response == None:

Vanlightly

----------------------------- MODULE CountersNodes -----------------------------

EXTENDS Integers, FiniteSets, TLC

CONSTANTS Counters, \* e.g. {c1, c2}
          Nodes     \* e.g. {n1, n2}
          
VARIABLES counter,
          node
          

Vanlightly

A cost analysis can be quite a large undertaking but also extremely valuable. How far one takes it depends on the time available and the value of the analysis.

There are different levels of detail/accuracy (in order of cheapest and easiest, to most effort/hardest):
* Use back of the napkin math, based on prior experience, to cost the infrastructure needed.
* Use modeling (spreadsheets or simple programs that simulate the workloads and hardware), with some assumptions from prior experience, to cost the infrastructure needed.
* Use synthetic benchmarking to cost infrastructure needed. This requires deploying OSS components and running perf tests.

I typically go for the modeling approach if the workload is low variance in hardware demands and I have a lot of experience with the workload, else it's benchmarking. The benchmarking doesn't need to be super comprehensive, but enough to get some confidence in the sizing needed to handle some common workloads.

The way I would generally tackle this is in two parts:

Vanlightly

--------------------------- MODULE gossa_v4 ---------------------------

(*
This version uses enabling conditions to limit the state space
while preserving the ability of TLC to effectively check
the liveness properties.
The constant MaxGeneration defines the inclusive maximum 
generation value that can be reached by any given node. The
limit is applied on Start because even though this is a recovery
action, it doesn't affect the lone liveness property of this

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:

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

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

Vanlightly

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


VARIABLES hour, minute, second

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

Vanlightly

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

VARIABLES hour, minute, second

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