Regarding the SingletonCardinality Axiom in Consensus.tla

[Christian Spann <cspanns....@xxxxxxxxx>]

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