-
Notifications
You must be signed in to change notification settings - Fork 214
Description
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
| (***************************************************************************) | |
| (* 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 |
Examples/specifications/Paxos/MCVoting.tla
Lines 41 to 45 in aaf4954
| 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:
Examples/specifications/ewd840/EWD840_proof.tla
Lines 72 to 75 in aaf4954
| <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!
Examples/specifications/byzpaxos/BPConProof.tla
Lines 586 to 588 in aaf4954
| <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) |
Examples/specifications/byzpaxos/PConProof.tla
Lines 432 to 435 in aaf4954
| 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) |
| PROVE SafeLemma!2 |