Name unnamed ASSUMEs in three example specifications

Give the existing top-level `ASSUME` blocks a name so that downstream
TLAPS proofs can cite them by reference instead of restating the
conjuncts.  The conjuncts themselves are preserved verbatim, so the
specifications and their TLC checks are unchanged.

Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Author: lemmy

specifications/CigaretteSmokers/CigaretteSmokers.tla

@@ -14,7 +14,8 @@ VARIABLE smokers, dealer
 (* {matches, paper, tobacco}. 'Offers' is a subset of subsets of           *)
 (* ingredients, each missing just one ingredient                           *)
 (***************************************************************************)
-ASSUME /\ Offers \subseteq (SUBSET Ingredients)
+ASSUME OffersAssumption ==
+       /\ Offers \subseteq (SUBSET Ingredients)
        /\ \A n \in Offers : Cardinality(n) = Cardinality(Ingredients) - 1
 
 (***************************************************************************)

specifications/CoffeeCan/CoffeeCan.tla

@@ -39,7 +39,7 @@ EXTENDS Naturals
 
 CONSTANT MaxBeanCount
 
-ASSUME MaxBeanCount \in Nat /\ MaxBeanCount >= 1
+ASSUME MaxBeanFact == MaxBeanCount \in Nat /\ MaxBeanCount >= 1
 
 VARIABLES can
 

specifications/PaxosHowToWinATuringAward/Voting.tla

@@ -25,7 +25,8 @@ CONSTANTS Value, Acceptor, Quorum
 (* element (an acceptor) in common.  Think of a quorum as a set consisting *)
 (* of a majority (more than half) of the acceptors.                        *)
 (***************************************************************************)
-ASSUME /\ \A Q \in Quorum : Q \subseteq Acceptor
+ASSUME QuorumAssumption ==
+       /\ \A Q \in Quorum : Q \subseteq Acceptor
        /\ \A Q1, Q2 \in Quorum : Q1 \cap Q2 /= {} 
 
 (***************************************************************************)

specifications/allocator/SchedulingAllocator.tla

@@ -18,7 +18,7 @@ CONSTANTS
   Clients,     \* set of all clients
   Resources    \* set of all resources
 
-ASSUME
+ASSUME SchedulingAllocatorAssumptions ==
   IsFiniteSet(Resources)
 
 VARIABLES

specifications/ewd687a/EWD687a.tla

@@ -123,7 +123,8 @@ OutEdges(p) == {e \in Edges : e[1] = p}
 (* something that was not stated explicitly: that a process can't send     *)
 (* messages to itself, so an edge joins two different processes.           *)
 (***************************************************************************)
-ASSUME  /\ \* Every edge is a pair of distinct processes
+ASSUME EdgeFacts ==
+        /\ \* Every edge is a pair of distinct processes
            \A e \in Edges :
              /\ (e \in Procs \X Procs)
              /\ (e[1] # e[2])

specifications/spanning/spanning.tla

@@ -1,7 +1,7 @@
 ------------------------------ MODULE spanning ------------------------------
 EXTENDS Integers
 CONSTANTS Proc, NoPrnt, root, nbrs
-ASSUME NoPrnt \notin Proc /\ nbrs \subseteq Proc \times Proc
+ASSUME NoPrntFact == NoPrnt \notin Proc /\ nbrs \subseteq Proc \times Proc
 VARIABLES prnt, rpt, msg
 vars == <<prnt, rpt, msg>> 
 

specifications/transaction_commit/PaxosCommit.tla

@@ -44,7 +44,7 @@ CONSTANT RM,             \* The set of resource managers.
          Majority,       \* The set of majorities of acceptors
          Ballot          \* The set of ballot numbers
 
-ASSUME  \* We assume these properties of the declared constants.
+ASSUME PaxosCommitAssumptions ==  \* We assume these properties of the declared constants.
   /\ Ballot \subseteq Nat
   /\ 0 \in Ballot
   /\ Majority \subseteq SUBSET Acceptor