7

我正在使用 VS Code 和 vscode-tlaplus 插件而不是 TLA+ Toolbox 来学习 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 似乎没用。

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

谢谢

4

1 回答 1

5

这是预期的行为。TLC 仅支持非常特定的 TLA+ 表达式作为分配给 CFG 文件中常量的值。我同意如果支持更强大的表达式会很好。

这通常按惯例处理：您有一个“好副本” SpecName.tlaTLA+ 规范，它不能直接由 TLC 模型检查，第二个MCSpecName.tlaTLA+ 规范覆盖第一个中的各种定义以使其可模型检查，并定义常量值. 因此，在您的情况下，您将拥有：

测试.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它可以是 Real-valued，并在每次操作后以任意正 Real 值前进。在您的 MC 规范中，您将覆盖now并Tick使用 Naturals 的某些子集。

于 2020-11-15T14:23:24.540 回答