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

Question

Я пробовал

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

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

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

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

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

Answer 1

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

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

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

Несмотря на то, что вопрос старый, оставление ответа может помочь будущим TLAers.

Answer 2

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

Answer 3

Получается, что нужен отдельный .tlaфайл для этого. Предположим, у вас есть "Main.tla" в качестве исходного файла. Вы хотитеMyConst иметь ценность <<1,2,3>>. Набор инструментов TLA+ создаетMC.tla где ставит константы:

---- MODULE MC ----
EXTENDS Main, TLC

const_uniq12345 = <<1,2,3>>
====

в MC.cfg, будет линия

CONSTANT MyConst <- const_uniq12345

Обратите внимание, что MyConst = const_uniq12345 не будет работать - если вы используете = вместо того <-, MyConst будет содержать модельное значение const_uniq12345 вместо того <<1, 2, 3>>

Я использовал https://github.com/hwayne/tlacli, чтобы иметь возможность запускать TLC из командной строки (панель инструментов TLA имеет ужасный UX), и я смог предоставить константу кортежа с помощью дополнительных.tlaфайл вроде этого. Я использовал значащее имя вместоconst_uniq12345тоже конечно. Пришлось позвонитьjava -cp /path/to/tla2tools.jar ... вручную, хотя (получил полную команду, используя --show-script вариант tlacli), потому что в настоящее время tlacli не справляется <- в конфиге.