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

я пробовал

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

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

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

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

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


configuration constants tla+ tlc model-checking
person luvieere    schedule 21.05.2010    source источник

Ответы (3)


arrow_upward
2
arrow_downward

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

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

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

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

person lasaro    schedule 17.02.2011

arrow_upward
1
arrow_downward

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

person Hovercouch    schedule 01.02.2018

arrow_upward
1
arrow_downward

Оказывается, для этого нужен отдельный .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 не обрабатывает <- в конфигурации.

person Dmitry Petukhov    schedule 02.05.2020