在 TLA+ 中表达“随机”行为外部 API

如何解决在 TLA+ 中表达“随机”行为外部 API

在我的模块中，我试图表示外部 API 的行为（可能以 200 HTTP 状态或 4XX/5XX HTTP 状态响应；这意味着它有 2 种可能的状态相对于我的系统=> 成功或失败）。

简而言之，我应该如何描述我的系统使用的外部 API，并且它应该根据 API 的响应（成功或失败）做出可预测的反应？（我多久收到一次成功/失败的回复；我不知道，这是“随机的”）

解决方法

这个问题在语言新手中很常见。 TLA+ 没有任何内置方式来表示系统执行更有可能采取一条路径而不是另一条路径 - 在您的情况下，API 是否返回错误。没关系，因为通常您编写 TLA+ 规范以确保您的系统在所有可能的执行跟踪下正常运行。所以 API 错误的可能性将被表达为一个简单的分离：

APIResult ==
    \/ retVal' = "SomeHappyPathValue"
    \/ retVal' = "Error"

新人觉得这很奇怪，因为在他们看来，错误路径应该比快乐路径“不太可能”发生，而这个规范似乎说它们同样可能发生。但这是基于对模型检查器（通常）如何工作的误解：它不会模拟尝试查找错误的随机跟踪，而是对所有可能的执行跟踪进行广度优先搜索，尝试找到一个状态违反了不变量。因此，一个执行跟踪比另一个“更有可能”的想法对模型检查器没有任何意义，因为它与它检查的东西无关。

请注意，实际上可以在如上所述的模拟模式下运行模型检查器，但通常只有在您的状态空间如此巨大以至于无法进行全面探索时才会这样做。

TLA+ 邮件列表上的一个帖子回答了这个问题：http://discuss.tlapl.us/msg04033.html