У меня есть модуль 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".
Как я могу решить эту ошибку?