Skip to content

Remove subexpressions from examples? #200

@ahelwer

Description

@ahelwer

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)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions