diff options
| author | Tor Brede Vekterli <vekterli@yahooinc.com> | 2023-08-24 13:42:31 +0200 |
|---|---|---|
| committer | Tor Brede Vekterli <vekterli@yahooinc.com> | 2023-08-24 13:42:31 +0200 |
| commit | f8a19f304a9cb70ea18d5bf541aeb5496d05bbf7 (patch) | |
| tree | 7edb5868516ed7f3897d1bace8ccbc3d54ff1ba1 /storage/specs | |
| parent | f37ad506b56dffd8002eb9334d0811e788dade01 (diff) | |
Simplify spec SeqToSet definition
A sequence of length n is defined as a function whose domain is
equal to 1..n (note: 1-indexing), so just use the domain directly
instead of manually constructing the range.
Diffstat (limited to 'storage/specs')
| -rw-r--r-- | storage/specs/bucketinfo/bucketinfo.tla | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/storage/specs/bucketinfo/bucketinfo.tla b/storage/specs/bucketinfo/bucketinfo.tla index 8224ff6a4f1..8ce604a029c 100644 --- a/storage/specs/bucketinfo/bucketinfo.tla +++ b/storage/specs/bucketinfo/bucketinfo.tla @@ -61,7 +61,7 @@ variables messages = {}; \* model messages as unordered set to test reordering "for free" define - SeqToSet(s) == {s[i]: i \in 1..Len(s)} + SeqToSet(s) == {s[i]: i \in DOMAIN s} HasMessage(t, d) == \E m \in messages: (m.type = t /\ m.dest = d) @@ -368,11 +368,11 @@ end process; end algorithm;*) -\* BEGIN TRANSLATION (chksum(pcal) = "7a179595" /\ chksum(tla) = "2d89f470") +\* BEGIN TRANSLATION (chksum(pcal) = "7a26a2a5" /\ chksum(tla) = "379d6205") VARIABLES proposedMuts, publishedStates, storEpoch, messages (* define statement *) -SeqToSet(s) == {s[i]: i \in 1..Len(s)} +SeqToSet(s) == {s[i]: i \in DOMAIN s} HasMessage(t, d) == \E m \in messages: (m.type = t /\ m.dest = d) |