Search code examples
tla+

Choosing one item from a symmetric set

I have a TLA+ spec akin to the following:

CONSTANT Items
VARIABLE item

And I'd like Items to be symmetric, and to select a single element from Items and store it into item.

I've been using item = CHOOSE x \in Items: TRUE, but I learned that this breaks symmetry on Items: TLC will always select the first item from the set.

I'd like to select a single item in a way that preserves symmetry, to allow TLC to explore all states. I don't care which item we select -- only that it is one, and that it is from Items. (Later, I need item to be \in Items.

While I'd prefer item to be a single element, it would also be okay for item to be a set of cardinality 1, so later I can check for \subseteq Items.

It was recommended to me to replace CHOOSE with {x \in Items: TRUE} to preserve symmetry and have the result be \subseteq Items, but this does not constrain the resulting set to cardinality 1.

Is there a way to ask TLA+ to give me a single item, or a set of cardinality 1, from a symmetric set of values?

Solution

  • I learned a bit more about TLA+/TLC since posting the question, and here's my answer:

    To simply select an element from a symmetry set in the initial predicate:

    item \in Items

    or in an action:

    item' \in Items

    If you want to select an item that matches a predicate, as you can specify with CHOOSE, then this is the alternative:

    item \in {x \in Items: P(x)}

    This'll form a subset of Items that match the predicate, then select a single element of those.

    Here's some data that shows the difference between this syntax and CHOOSE. Consider this module:

    ----------------------------- MODULE ChooseDemo -----------------------------
CONSTANT Items
VARIABLE item

TypeInvariant == item \in Items

Init == item = CHOOSE x \in Items: TRUE

Next == item' \in {x \in Items: x /= item}
=============================================================================

    When Items has three items:

    • NOT a symmetry set: TLC finds 1 initial state and a total of 7 (3 distinct) states.
    • symmetry set: TLC finds 1 initial state and a total of 3 (1 distinct) states.

    Now consider this module:

    --------------------------- MODULE SetFormingDemo ---------------------------
CONSTANT Items
VARIABLE item

TypeInvariant == item \in Items

Init == item \in {x \in Items: TRUE}

Next == item' \in {x \in Items: x /= item}
=============================================================================

    When Items has three items:

    • NOT a symmetry set: TLC finds 3 (3 distinct) initial states and a total of 9 (3 distinct) states.
    • symmetry set: TLC finds 3 (1 distinct) initial state and a total of 5 (1 distinct) states.

    Hence, by using the set-forming syntax, TLC finds more states than it did with CHOOSE.