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

Question

我正在为一个工作项目试用 TLA+。我想证明使用相同的密钥获取数据将 return 相同的数据，尽管对数据的内部结构进行了一些更改。为此，我想将外部系统建模为一个黑盒子，其响应具有某些属性。例如：

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

是的，但最好是——尤其是如果你想使用 TLC，工具箱中的 TLA+ 模型检查器——直接使用非确定性，而不是依赖于使用常量和假设的公理规范，这需要你在模型检查时提供一个特定实例，这可能不是你想要的。

你可以这样做：

CONSTANT ValidKey
CONSTANT DataPoint

VARIABLE x

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

这基本上是说 Fetch 是 returns 一系列 DataPoint 的某种操作，但您不知道是哪个，这无关紧要。现在，当检查你的系统时，它会被 Fetch 检查 all 可能的响应（因为 Seq 是无界的，当模型检查时，你需要重写它与一些描述给定长度的有界序列的运算符。

如果您希望Fetch 始终"return" 相同的键得到相同的结果，您可以做一些不同的事情：

CONSTANTS ValidKey, DataPoint
VARIABLE fetch

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

Next == UNCHANGED fetch /\ ...

表示 fetch 是所需类型的一些未知函数。 TLC 将同样检查所有可能的 fetch 函数的规范。

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

TLA+ Spec with assumptions about external systems

tla+