Выбор одного элемента из симметричного набора - PullRequest
Новая
       39

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

0 голосов
/ 16 февраля 2019

У меня есть спецификация 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 из симметричного набора значений?

1 Ответ

0 голосов
/ 19 февраля 2019

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

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

item \in Items

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

item' \in Items

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

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

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

Вот некоторые данные, которые показывают разницу между этим синтаксисом и 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.

...