tla+ - 使用 VS Code 时如何在 TLA+ 配置文件中设置常量？

Question

我正在使用 VS Code 和 vscode-tlaplus 插件而不是 TLA+ 工具箱来学习 TLA+。现在我有了这个 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"}

所以，定义一个 CONSTANT 似乎没用。

我做错了什么，还是这是预期的行为？

谢谢

Answer 1

这是预期的行为。 TLC 仅支持非常特定的 TLA+ 表达式作为分配给 CFG 文件中常量的值。我同意如果支持更强大的表达式会很好。
这通常按惯例处理:您有一个“好的副本”SpecName.tla TLA+ 规范不能直接通过 TLC 进行模型检查，第二个 MCSpecName.tla TLA+ 规范首先覆盖各种定义以使其可模型检查，并定义常量值。因此，在您的情况下，您将拥有:
测试.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 .这实际上是一个很好的约定，让您可以自由地编写“好的副本”规范以更准确地反射(reflect)现实，而不是遵循模型检查器的奇思妙想。例如，在您的良好副本规范中，您可能有 now定义当前时间的变量；它可以是 Real-valued，并在每个 Tick 之后以任意正 Real 值前进行动。在您的 MC 规范中，您将覆盖 now和 Tick使用 Naturals 的一些子集。