Last active
May 10, 2023 00:47
-
-
Save cfm/ae17ed1a69370b73921d9e36e458d792 to your computer and use it in GitHub Desktop.
two-party Lamport clock with definitive leader
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
| states/ | |
| *.dot* | |
| *.out* | |
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
| SPECIFICATION Spec | |
| CONSTANT MAX = 3 |
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
| 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) | |
| ==== |
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
| DOT=$(wildcard *.dot) | |
| PNG=$(DOT:.dot=.dot.png) | |
| .PHONY: all | |
| all: $(PNG) | |
| %.dot.png: %.dot Makefile | |
| dot -Tpng $< > $@ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment