在 TLA+ 中表达 "random" 行为（外部 API）

Question

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

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

Answer 1

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

Answer 2

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

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

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

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

在 TLA+ 中表达 "random" 行为（外部 API）

Expressing a "random" behaviour (external API) in TLA+

methods

specifications

tla+