1

我正在为一个工作项目尝试 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+ 将根据指定的假设推断行为。那可能吗？

4

1 回答 1

3

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

你可以这样做：

CONSTANT ValidKey
CONSTANT DataPoint

VARIABLE x

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

这基本上是说这Fetch是一些返回DataPoints序列的操作，但你不知道是哪个，没关系。现在，在检查您的系统时，将检查所有可能的响应Fetch（因为Seq是无界的，在模型检查时，您需要使用一些操作符来覆盖它，该操作符描述了一个给定长度的有界序列）。

如果您想Fetch始终为同一个键“返回”相同的结果，您可以做一些不同的事情：

CONSTANTS ValidKey, DataPoint
VARIABLE fetch

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

Next == UNCHANGED fetch /\ ...

这表示这fetch是所需类型的一些未知功能。TLC 将类似地检查所有可能fetch功能的规范。

于 2017-10-24T08:44:35.363 回答