Выбор одного элемента из симметричного набора

Question

У меня есть спецификация TLA+ сродни следующему:

CONSTANT Items
VARIABLE item

И я бы хотел Items быть симметричным, и выбрать один элемент из Items и сохранить его в item,

Я использую item = CHOOSE x \in Items: TRUE, но я узнал, что это нарушает симметрию Предметов: TLC всегда выбирает первый элемент из набора.

Я хотел бы выбрать один элемент таким образом, чтобы сохранить симметрию, чтобы позволить TLC исследовать все состояния. Мне все равно, какой предмет мы выбираем - только то, что он один, и что он из Items, (Позже мне нужно item быть \in Items,

Хотя я бы предпочел item быть единым элементом, было бы также хорошо для item быть набором мощности 1, поэтому позже я могу проверить \subseteq Items,

Мне порекомендовали заменить CHOOSE с {x \in Items: TRUE} сохранить симметрию и иметь результат \subseteq Items, но это не ограничивает результирующий набор в количество элементов 1.

Есть ли способ попросить TLA+ дать мне один элемент или набор мощности 1 из симметричного набора значений?

Answer 1

Я узнал немного больше о TLA+/TLC с момента публикации вопроса, и вот мой ответ:

Чтобы просто выбрать элемент из набора симметрии в исходном предикате:

item \in Items

или в действии:

item' \in Items

Если вы хотите выбрать элемент, который соответствует предикату, как вы можете указать с помощью CHOOSE, то это альтернатива:

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

Это сформирует подмножество элементов, которые соответствуют предикату, а затем выберет один из них.

Вот некоторые данные, которые показывают разницу между этим синтаксисом и CHOOSE. Рассмотрим этот модуль:

----------------------------- 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}
=============================================================================

когда Items имеет три предмета:

• НЕ набор симметрии: TLC находит 1 начальное состояние и всего 7 (3 различных) состояния.
• набор симметрии: TLC находит 1 начальное состояние и всего 3 (1 различных) состояния.

Теперь рассмотрим этот модуль:

--------------------------- 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}
=============================================================================

когда Items имеет три предмета:

• НЕ набор симметрии: TLC находит 3 (3 различных) начальных состояния и всего 9 (3 различных) состояния.
• набор симметрии: TLC находит 3 (1 отдельное) начальное состояние и всего 5 (1 отдельное) состояние.

Следовательно, используя синтаксис формирования множеств, TLC находит больше состояний, чем он делал с CHOOSE.