Как я могу назначить последовательности константам в разделе CONSTANTS файла конфигурации TLA +?

Question

я пробовал

CONSTANTS seq = <<5,6,7>>

но TLC выдает синтаксическую ошибку:

Ошибка: TLC обнаружил ошибку в файл конфигурации в строке 1. Это было ожидал = или <- и не нашел его. </p>

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

Итак ... что мне нужно сделать, чтобы назначить последовательность?

Answer 1

Вы не можете напрямую назначить константу в файле TLA +. Если вы используете панель инструментов, напишите CONSTANTS seq, затем в модель добавьте нужный кортеж в качестве обычного назначения.

Answer 2

Я не помню, чтобы когда-либо сталкивался с этой проблемой, и мой TLC слишком ржавый, чтобы попытаться дать вам ответ из первых рук (я только что перезапустил использование панели инструментов TLA +).

Однако из приведенного ниже поста я полагаю, что вы не можете создавать экземпляры констант с последовательностями через файлы конфигурации TLC.

http://bbpress.tlaplus.net/topic/creating-a-sequence-from-a-set

Даже при том, что вопросстар, оставив ответ может помочь будущим TLAers.