\ in работает, в то время как \ subseteq выдает ошибку «неопределенный идентификатор»

Question

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

------------------------------ MODULE Group ------------------------------
CONSTANTS People
VARIABLES members

Init == members \subseteq People

Next == members' = members

Group == Init /\ [][Next]_members

=============================================================================

(я упростил эту спецификацию до такой степени, что она не делает ничего полезного.)

Когда я пытаюсь запустить ее через TLC, яполучить следующую ошибку:

При оценке элементы идентификатора либо не определены, либо не являются оператором.

Ошибка указывает на строку Init.

Когда я изменяю строку Init на:

Init == members \in People

, она корректно подтверждается.

Я хочу, чтобы прежние функциональные возможности, потому что я имею в виду, что members - это набор людей, а не один человек.

В соответствии с разделом 16.1.6 Спецификации Лесли Лампорта Системы , «TLA + предоставляет следующие операторы на наборах:» и перечисляет оба \in и \subseteq.

Почему TLA + не позволяет мне использовать \subseteq?

Answer 1

Хотя это допустимое выражение TLA +, TLC может присваивать значения следующего состояния только переменной x с помощью операторов x' = e или x' \in S.Смотрите раздел 14.2.6 для деталей.Это относится и к первоначальному назначению.В вашем случае вы, вероятно, хотите members \in SUBSET People.