指定活性，以便 TLA+ 中不会发生循环

Question

我正在编写一个简单的客户端-服务器交互规范来学习 TLA+：

-------------------------------- MODULE Bar --------------------------------
VARIABLES
    sessionOK, \* if session is OK or expired
    msg        \* message currently on the wire

vars == <<msg, sessionOK>>

TypeOK ==
    /\ sessionOK \in {TRUE, FALSE}
    /\ msg \in {
         "Query",
         "OK",
         "Unauthorized",
         "null"
       }

Init ==
    /\ msg = "null"
    /\ sessionOK = FALSE

Query ==
    /\ msg \in {"null", "OK"}
    /\ msg' = "Query"
    /\ UNCHANGED <<sessionOK>>

OK ==
    /\ msg = "Query"
    /\ sessionOK = TRUE
    /\ msg' = "OK"
    /\ UNCHANGED <<sessionOK>>

Unauthorized ==
    /\ msg = "Query"
    /\ sessionOK = FALSE
    /\ msg' = "Unauthorized"
    /\ UNCHANGED <<sessionOK>>

Authorize ==
    /\ msg = "Unauthorized"
    /\ msg' = "null"
    /\ sessionOK' = TRUE

Expire ==
    /\ sessionOK = TRUE
    /\ sessionOK' = FALSE
    /\ UNCHANGED <<msg>>

Next ==
    \/ Query
    \/ Unauthorized
    \/ OK
    \/ Authorize
    \/ Expire

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

=============================================================================

正如您所希望看到的那样，客户端可以运行对服务器进行一些查询，如果会话正常，它将获得结果，否则它会收到一条消息，需要授权然后重试.会话随时可能过期。

我想确保客户端最终会得到一个结果，所以我在属性中添加了这一行：

(msg = "Query") ~> (msg = "OK")

在模型检查时，我遇到了这样一个反例：初始化 -> （查询 -> 未授权 -> 授权 -> 过期），括号中的部分无限期地重复。我的第一个想法是对 OK step 提出强烈的公平性要求。然而，问题出在这种情况下 OK 步骤从未启用。

我可以添加诸如 []<><<OK>>_vars（读作 "it's always the case that eventually OK occurs"）之类的东西，但这感觉就像作弊，而且从我收集的信息来看，使用任意时间公式指定活跃度——而不是弱或强的公平性-- 不赞成。

如何使用弱公平性或强公平性来保证查询最终会得到响应？或者我的模型不好？我没主意了...

Answer 1

我正在回答我自己的问题。如果有人认为他们有更好的答案，请分享。

我发现了这个名字恰如其分的话题 How to test a process eventually succeeds after indefinite number of retries?，其中 Leslie Lamport 自己指出，我们可以只对一个动作和其他一些公式的结合断言公平。在我们的场景中 Spec 看起来像这样：

Spec ==
    /\ Init
    /\ [][Next]_vars
    /\ WF_vars(Next)
    /\ SF_vars(OK)
    /\ SF_vars(Query /\ (sessionOK = TRUE))

现在，这些公式中的每一个是什么意思？前三个非常明显，并且包含在我定义 Spec.

的尝试中

Init 在行为的第一个状态为真。
Next 对于行为的每一步都是正确的（允许口吃）。
Next 如果无限期地继续启用，将继续发生，因此系统不会在消息交换的过程中停止。

第四个是我的直觉：它修复了进行查询然后会话过期的情况。

如果 OK 被重复启用（可能发生）那么它最终会发生。

第五个是缺失的：它修复了 OK 一开始从未启用的情况，因为会话在 Query 可能发生之前就过期了。

如果重复出现Query的情况，并且session同时有效，最终还是会发生。

指定活性，以便 TLA+ 中不会发生循环

Specifying liveness so a cycle doesn't happen in TLA+

tla+