[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Christian Spann <cspanns....@xxxxxxxxx>*Date*: Wed, 18 Sep 2013 06:28:58 -0700 (PDT)

Hello, Whilst playing around with tlaplus and trying to learn how to specify consensus algorithms I stepped across the refinement example by Leslie Lamport ("Mechanically Checked Safety Proof of a Byzantine Paxos Algorithm") found here: http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html In the very basic Consensus.tla I stepped over an Axiom regarding the SingletonCardinality of sets (i guess). As I am very inadept with tla / pluscal I address my question to this group instead of adressing it directly to Mr. Lamport. As far as I understand it, the axiom: AXIOM SingletonCardinality == \A e : IsFiniteSet({e}) /\ (Cardinality({e}) = 1) always evaluates to true, as {e} is always a set with a single entry, "e". I guess the axiom would be correct if one would spare the {} brackets in both cases. Obviously the following test would then fail: SingleCardinalityTest == \A e \in SUBSET {"a", "b", "c"} : IsFiniteSet({e}) /\ (Cardinality({e}) = 1) as the SUBSET operator also produces {"a","b"} and alike. So did I find a typo here or is the behaviour intended? Best regards, Christian Spann

**Follow-Ups**:**Re: [tlaplus] Regarding the SingletonCardinality Axiom in Consensus.tla***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] TLAPS 1.2.1 released** - Next by Date:
**Re: [tlaplus] Regarding the SingletonCardinality Axiom in Consensus.tla** - Previous by thread:
**Re: [tlaplus] Re: TLAPS 1.2.1 released** - Next by thread:
**Re: [tlaplus] Regarding the SingletonCardinality Axiom in Consensus.tla** - Index(es):