指定活动，因此在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步骤提出严格的公平性要求。但是问题是在这种情况下OK步骤从未启用。

我可以添加诸如[]<><<OK>>_vars之类的内容（它的意思是“总是会最终出现OK”），但这感觉像是在作弊，并且从我收集的内容中，使用任意时间公式指定了生命力-而不是弱点或强烈的公平感-被皱眉了。

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

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的尝试中。

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

第四是我的直觉：它解决了进行查询然后会话期满的情况。

4. 如果反复启用OK（可能发生），则最终会发生。

还有第五个遗漏之处：它修复了最初从不启用OK的情况，因为会话在Query发生之前就已过期。

5. 如果反复发生Query且会话在同一时间有效的情况，则最终会发生。