TLC не может справиться с этим соединением спецификации
У меня есть модуль TLA+, который в итоге выглядит следующим образом:
--- MODULE Group ---
CONSTANTS People
VARIABLES members
Join(person) == ...
Leave(person) == ...
Init == members \subseteq People
Next == \E p \in People :
\/ Join(p)
\/ Leave(p)
====================
Когда я пытаюсь проверить модель с помощью TLC, я получаю следующую ошибку:
TLC бросил неожиданное исключение. Вероятно, это было вызвано ошибкой в спецификации или модели. Посмотрите Пользовательский Выход или Консоль TLC для подсказок к тому, что случилось. Исключением является исключение java.lang.RuntimeException: TLC не может обработать этот конъюнкт спецификации: строка X, столбец Y и строка Z, столбец T модуля Group
... указывая на все содержание Next,
Я верю своему Next хорошо написано, потому что вот пример модели, которая имеет очень похожий Next к моему: https://github.com/tlaplus/Examples/blob/master/specifications/aba-asyn-byz/aba_asyn_byz.tla#L110
Кроме того, в разделе 14.2.2 "Уточняющих систем Лесли Лампорта" говорится:
TLC может оценивать многозначное выражение, только если это выражение равно конечному множеству [...]. TLC будет оценивать выражения следующих форм, только если он может перечислять множество S:
и предоставляет пример "существует такой x в S, что p ".
Как я могу решить эту ошибку?
0 ответов
Проблема была с моим использованием \subseteq в Init, как ответили здесь: \ in работает, в то время как \subseteq выдает ошибку "идентификатор не определен"