带有外部系统假设的TLA+规范

Question

我正在为一个工作中的项目试用TLA+。我想证明，尽管对数据的内部结构做了一些更改，使用相同键获取数据还是会返回相同的数据。为此，我想将外部系统建模为一个黑匣子，其响应具有特定的属性。例如：

CONSTANT ValidKeys
CONSTANT DataPoints
CONSTANT FETCH(_)

\* Incorrect use of ASSUME, but for illustrative purposes.
ASSUME ValidKeys \in SUBSET DOMAIN FETCH(ValidKeys)
ASSUME \forall key in ValidKeys:
  LET fetched == Fetch(ValidKeys)[key]
  IN fetched \in Seq(DataPoints)

然后，我想编写我自己的系统，其中TLA+将根据指定的假设推断行为。这有可能吗？

Answer 1

是的，但更好的是--特别是如果你想要使用TLA+模型检查器，它是工具箱的一部分--直接使用不确定性，而不是依赖于使用常量和假设的公理化规范，这些参数和假设要求您在模型检查时提供特定的实例，这可能不是您想要的。

你可以这样做：

CONSTANT ValidKey
CONSTANT DataPoint

VARIABLE x

Fetch(key) == key \in ValidKey /\ x' \in Seq(DataPoint)

这基本上是说，Fetch是一些返回一个DataPoint序列的操作，但是您不知道哪个操作，这并不重要。现在，在检查您的系统时，将由Fetch检查所有可能的响应(因为Seq是无界的，当模型检查时，您将需要使用某个操作符覆盖它，该操作符描述一个不超过给定长度的有界序列)。

如果希望Fetch总是对相同的键“返回”相同的结果，则可以执行不同的操作：

CONSTANTS ValidKey, DataPoint
VARIABLE fetch

Init == fetch \in [ValidKey -> Seq(DataPoint)] /\ ...

Next == UNCHANGED fetch /\ ...

它表示fetch是某种未知的函数，具有所需的类型。TLC同样会检查规范中的所有可能的fetch函数。