Как я могу установить КОНСТАНТЫ в файле конфигурации TLA + при использовании VS Code?

Я изучаю TLA +, используя VS Code и плагин vscode-tlaplus вместо TLA + Toolbox. Теперь у меня есть файл TLA, в котором я определяю некоторые константы:

---- MODULE test ----
EXTENDS TLC, Integers, Sequences

CONSTANTS Capacity, Items, ValueRange, SizeRange

ItemParams == [size: SizeRange, value: ValueRange]
ItemSets == [Items -> ItemParams]
===

Я хотел бы указать в файле cfg следующее:

SPECIFICATION Spec

CONSTANTS
    SizeRange = 1..4
    ValueRange = 0..3
    Capacity = 7
    Items = {"a", "b", "c"}

Но это вызывает следующую ошибку:

TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a tlc2.tool.ConfigFileException
:
TLC found an error in the configuration file at line 5
It was expecting = or <-, but did not find it.

Пока я нашел только этот обходной путь:

.tla

---- MODULE test ----
EXTENDS TLC, Integers, Sequences

CONSTANTS Capacity, Items, ValueRange, SizeRange

ConstSizeRange == 1..4
ConstValueRange == 0..3

ItemParams == [size: SizeRange, value: ValueRange]
ItemSets == [Items -> ItemParams]
====

.cfg

SPECIFICATION Spec

CONSTANTS
    SizeRange <- ConstSizeRange
    ValueRange <- ConstValueRange
    Capacity = 7
    Items = {"a", "b", "c"}

Таким образом, определение КОНСТАНТЫ кажется бесполезным.

Я что-то делаю не так, или это ожидаемое поведение?

Спасибо


tla+
person Nicholas    schedule 29.11.2019    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Это ожидаемое поведение. TLC поддерживает только очень специфические выражения TLA + в качестве значений, присвоенных константам в файле CFG. Я согласен, было бы неплохо, если бы поддерживались более мощные выражения.

Обычно это делается по соглашению: у вас есть одна хорошая копия SpecName.tla TLA + spec, которая не может быть напрямую проверена моделью TLC, и вторая MCSpecName.tla TLA + spec, которая переопределяет различные определения в первой, чтобы сделать ее проверяемой моделью, плюс определяет постоянные значения . Итак, в вашем случае у вас будет:

Test.tla:

---- MODULE Test ----
EXTENDS TLC, Integers, Sequences

CONSTANTS Capacity, Items, ValueRange, SizeRange

ConstSizeRange == 1..4
ConstValueRange == 0..3

ItemParams == [size: SizeRange, value: ValueRange]
ItemSets == [Items -> ItemParams]
====

MCTest.tla:

---- MODULE MCTest ----
EXTENDS Test

ConstSizeRange == 1..4

ConstValueRange == 0..3

====

MCTest.cfg:

SPECIFICATION Spec

CONSTANTS
    SizeRange <- ConstSizeRange
    ValueRange <- ConstValueRange
    Capacity = 7
    Items = {"a", "b", "c"}

Вы можете увидеть это соглашение, используемое в примерах TLA +, таких как Paxos. . На самом деле это довольно хорошее соглашение, позволяющее вам написать свою хорошую копию спецификации, чтобы более точно отражать реальность, а не подчиняться прихотям проверщика моделей. Например, в вашей хорошей спецификации копирования у вас может быть переменная now, которая определяет текущее время; он может иметь действительное значение и увеличиваться на произвольное положительное вещественное значение после каждого Tick действия. В спецификации MC вы должны переопределить now и Tick, чтобы использовать некоторое подмножество Naturals.

person ahelwer    schedule 15.11.2020