Lamport thinks anonymous subexpressions were a mistake and should be removed from the language. Given that these specs are "example" TLA+ specs, it perhaps makes sense to keep them from being examples of things you should not use. There are a few specs in this repo which use anonymous subexpressions:
|
(***************************************************************************) |
|
(* TLC only tells you if an invariant is violated, not what part is *) |
|
(* violated. To help locate an error, it's useful to give TLC the *) |
|
(* conjuncts of an invariant as separate invariants to check. *) |
|
(***************************************************************************) |
|
Inv1 == Inv!1 |
|
Inv2 == Inv!2 |
|
Inv3 == Inv!3 |
|
Inv4 == Inv!4 |
|
MCInv == /\ AllSafeAtZero!: |
|
/\ ChoosableThm!: |
|
/\ OneValuePerBallot => OneVote |
|
/\ VotesSafeImpliesConsistency!: |
|
/\ ShowsSafety!: |
This one uses labels, thus is not anonymous, although for the same purpose of addressing specific conjuncts in a conjunction list:
|
<1>2. ~ Inv!P2 BY tcolor = "white" DEF Inv |
|
<1>3. ~ Inv!P1 BY <1>1 DEF Inv |
|
<1>. QED |
|
<2>1. Inv!P0 BY Inv, <1>2, <1>3 DEF Inv |
The byzpaxos specs use many conjunction list subaddresses, nested even!
|
<1>2. \A self : leader(self) <=> NextDef!2!2!(self) |
|
BY DEF leader, Phase1a, Phase1c |
|
<1>3. \A self : facceptor(self) <=> NextDef!2!3!(self) |
|
PROVE acceptor(self) <=> TLANext!1!(self) |
|
BY <1>2, BallotAssump DEF acceptor, ProcSet, Phase1b, Phase2b |
|
<1>3. ASSUME NEW self \in Ballot |
|
PROVE leader(self) <=> TLANext!2!(self) |
Lamport thinks anonymous subexpressions were a mistake and should be removed from the language. Given that these specs are "example" TLA+ specs, it perhaps makes sense to keep them from being examples of things you should not use. There are a few specs in this repo which use anonymous subexpressions:
Examples/specifications/Paxos/MCPaxos.tla
Lines 53 to 61 in aaf4954
Examples/specifications/Paxos/MCVoting.tla
Lines 41 to 45 in aaf4954
This one uses labels, thus is not anonymous, although for the same purpose of addressing specific conjuncts in a conjunction list:
Examples/specifications/ewd840/EWD840_proof.tla
Lines 72 to 75 in aaf4954
The byzpaxos specs use many conjunction list subaddresses, nested even!
Examples/specifications/byzpaxos/BPConProof.tla
Lines 586 to 588 in aaf4954
Examples/specifications/byzpaxos/PConProof.tla
Lines 432 to 435 in aaf4954
Examples/specifications/byzpaxos/VoteProof.tla
Line 353 in aaf4954