two-party Lamport clock with definitive leader

.gitignore

states/

*.dot*
*.out*

LamportClock.cfg

SPECIFICATION Spec
CONSTANT MAX = 3

LamportClock.tla

Two-party Lamport clock with definitive leader.

---- MODULE LamportClock ----
EXTENDS Integers, TLC
CONSTANTS MAX
VARIABLES Server, Client
vars == <<Server, Client>>

Max(a,b) ==
    IF a > b THEN a ELSE b

Init ==
    /\ Server = 0
    /\ Client = 0

ServerUpdates ==
    /\ Server < MAX
    /\ Server' = Server + 1
    /\ UNCHANGED Client

ClientSends ==
    /\ Client < MAX
    /\ Client' = Client + 1
    \* Client sends = Server receives:
    /\ Server' = Max(Client + 1, Server) + 1

ClientReceives ==
    /\ Server > Client
    /\ Client' = Max(Client, Server) + 1
    /\ UNCHANGED Server

Next ==
    \/ ServerUpdates
    \/ ClientSends
    \/ ClientReceives

Spec ==
    /\ Init
    /\ [][Next]_vars
    /\ WF_vars(Next)

====

LamportClock.tla.dot.png

Makefile

DOT=$(wildcard *.dot)
PNG=$(DOT:.dot=.dot.png)

.PHONY: all

all: $(PNG)

%.dot.png: %.dot Makefile
	dot -Tpng $< > $@