Skip to content

Parenthesize SUBSET and UNION where precedence is unspecified. #252

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
lemmy merged 1 commit into from
Nov 5, 2026
Merged

Parenthesize SUBSET and UNION where precedence is unspecified. #252

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions specifications/KeyValueStore/KVsnap.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ START: \* Start the transaction
tx := tx \union {self};
snapshotStore := store; \* take my snapshot of store

with (rk \in SUBSET Key \ { {} }; wk \in SUBSET Key \ { {} }) {
with (rk \in (SUBSET Key) \ { {} }; wk \in (SUBSET Key) \ { {} }) {
read_keys := rk; \* select a random read-key-set from possible read-keys
write_keys := wk; \* select a random write-key-set from possible write-keys
};
Expand Down Expand Up @@ -79,7 +79,7 @@ COMMIT: \* Commit the transaction to the database if there is no conflict
}
*)

\* BEGIN TRANSLATION (chksum(pcal) = "1adfcb46" /\ chksum(tla) = "5b28617f")
\* BEGIN TRANSLATION (chksum(pcal) = "be9e3fd6" /\ chksum(tla) = "d93ee94d")
VARIABLES store, tx, missed, pc, snapshotStore, read_keys, write_keys, ops

vars == << store, tx, missed, pc, snapshotStore, read_keys, write_keys, ops
Expand All @@ -101,8 +101,8 @@ Init == (* Global variables *)
START(self) == /\ pc[self] = "START"
/\ tx' = (tx \union {self})
/\ snapshotStore' = [snapshotStore EXCEPT ![self] = store]
/\ \E rk \in SUBSET Key \ { {} }:
\E wk \in SUBSET Key \ { {} }:
/\ \E rk \in (SUBSET Key) \ { {} }:
\E wk \in (SUBSET Key) \ { {} }:
/\ read_keys' = [read_keys EXCEPT ![self] = rk]
/\ write_keys' = [write_keys EXCEPT ![self] = wk]
/\ pc' = [pc EXCEPT ![self] = "READ"]
Expand Down
8 changes: 4 additions & 4 deletions specifications/LevelChecking/LevelSpec.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -983,9 +983,9 @@
{i \in paramNums : /\ IsOpParam(i)
/\ Node[subst.subWith[i]].ref \in
OpDefNodeId}
IN UNION {Sub(lc) : lc \in rcd.levelConstraints}
IN (UNION {Sub(lc) : lc \in rcd.levelConstraints})
\cup
UNION { {LC(i, alp) : alp \in SubALP(i)} : i \in OpDefParams },
(UNION { {LC(i, alp) : alp \in SubALP(i)} : i \in OpDefParams }),

argLevelConstraints |->
(******************************************************************)
Expand Down Expand Up @@ -1046,9 +1046,9 @@
(* SubParamALP(i). *)
(*************************************************************)

IN UNION {Sub(alc) : alc \in rcd.argLevelConstraints}
IN (UNION {Sub(alc) : alc \in rcd.argLevelConstraints})
\cup
UNION {ALCSet(i) : i \in paramNums},
(UNION {ALCSet(i) : i \in paramNums}),

argLevelParams |->
(******************************************************************)
Expand Down
8 changes: 4 additions & 4 deletions specifications/allocator/AllocatorImplementation.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -166,11 +166,11 @@ Invariant == \** a lower-level invariant
/\ \A c \in Clients :
/\ Cardinality(RequestsInTransit(c)) <= 1
/\ requests[c] = unsat[c]
\cup UNION RequestsInTransit(c)
\cup UNION AllocsInTransit(c)
\cup (UNION RequestsInTransit(c))
\cup (UNION AllocsInTransit(c))
/\ alloc[c] = holding[c]
\cup UNION AllocsInTransit(c)
\cup UNION ReturnsInTransit(c)
\cup (UNION AllocsInTransit(c))
\cup (UNION ReturnsInTransit(c))

(* correctness properties in terms of clients' variables *)
ResourceMutex ==
Expand Down
Loading