Created
December 5, 2024 11:42
-
-
Save Vanlightly/b6b01539471cf9614eb328d02cf61bbb to your computer and use it in GitHub Desktop.
Symmetry in TLA+
This file contains 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 CountersNodes ----------------------------- | |
| EXTENDS Integers, FiniteSets, TLC | |
| CONSTANTS Counters, \* e.g. {c1, c2} | |
| Nodes \* e.g. {n1, n2} | |
| VARIABLES counter, | |
| node | |
| Inc(n, c) == | |
| /\ counter[c] < 2 | |
| /\ node' = [node EXCEPT ![n] = @ + 1] | |
| /\ counter' = [counter EXCEPT ![c] = @ + 1] | |
| Init == | |
| /\ counter = [c \in Counters |-> 0] | |
| /\ node = [n \in Nodes |-> 0] | |
| Next == | |
| \E n \in Nodes, c \in Counters : | |
| Inc(n, c) | |
| ============================================================================= |
This file contains 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 PerNodeCounter ----------------------------- | |
| EXTENDS Integers, FiniteSets, TLC | |
| CONSTANTS Counters, | |
| Nodes | |
| VARIABLES counter, | |
| node, | |
| ok, | |
| mapping | |
| Inc(n, c) == | |
| /\ counter[c] < 2 | |
| /\ mapping[n] = c | |
| /\ node' = [node EXCEPT ![n] = @ + 1] | |
| /\ ok' = [ok EXCEPT ![n] = TRUE] | |
| /\ counter' = [counter EXCEPT ![c] = @ + 1] | |
| /\ UNCHANGED <<mapping>> | |
| Fail(n, c) == | |
| /\ counter[c] < 2 | |
| /\ mapping[n] = c | |
| /\ ok' = [ok EXCEPT ![n] = FALSE] | |
| /\ UNCHANGED <<mapping, node, counter>> | |
| Init == | |
| /\ counter = [c \in Counters |-> 0] | |
| /\ node = [n \in Nodes |-> 0] | |
| /\ ok = [n \in Nodes |-> TRUE] | |
| /\ mapping = CHOOSE m \in [Nodes -> Counters] : | |
| \A c \in Counters : | |
| \E n \in Nodes : c = m[n] | |
| Next == | |
| \E n \in Nodes, c \in Counters : | |
| \/ Inc(n, c) | |
| \/ Fail(n, c) | |
| ============================================================================= |
This file contains 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 | |
| CONSTANTS Counters \* e.g. {c1, c2} | |
| VARIABLES counters | |
| Inc(c) == | |
| /\ counters[c] < 2 | |
| /\ counters' = [counters EXCEPT ![c] = @ + 1] | |
| Init == | |
| counters = [c \in Counters |-> 0] | |
| Next == | |
| \E c \in Counters : | |
| Inc(c) | |
| ============================================================================= |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment