1

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

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

4

2 回答 2

1

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

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

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

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

于 2021-02-18T19:35:37.443 回答
-1

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

于 2021-01-21T17:26:57.757 回答