Re: [tlaplus] Checking if a set is a singleton

Note that Cardinality(S) is well-defined only for a finite set S. The semantics of TLA+ doesn’t specify if Cardinality(Nat) = 0, Cardinality(Nat) = 42 or Cardinality(Nat) = "foobar". That doesn’t matter much for model checking where variables cannot take on infinite sets anyway, but it may be a concern for theorem proving. In particular, the backend provers used by TLAPS don’t provide automation for reasoning about Cardinality.

Stephan

On 21 Jan 2026, at 23:36, Mathew Kuthur James <mathewkj2048@xxxxxxxxx> wrote:

Hi,

In TLA+, given a set S, I understand that it's better to write S = {} than writing Cardinality(S) = 0. Is there a similar method to check if S is a singleton set, that beats using Cardinality(S) = 1? I am considering using singleton(S) == (\A x \in S : \A y \in S : x = y) /\ (S \= {})

In general, is the Cardinality function costly in terms of model-checking performance, such that there are performance gains by using set comprehension for checking if a set is a singleton or empty (readability concerns aside)? What sort of test would I need to run to observe the performance gap, if one exists?

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/9a03af10-86d8-44bf-8c39-677d9b02e5d5n%40googlegroups.com.