0

我正在编写一个简单的客户端-服务器交互规范来学习 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")

在模型检查时，我遇到了一个这样的反例：Init -> (Query -> Unauthorized -> Authorize -> Expire)，括号中的部分无限重复。我的第一个想法是对OKstep 提出强烈的公平要求。然而，问题是在这种情况下，OK步骤从未启用。

我可以添加诸如[]<><<OK>>_vars（其内容为“最终OK发生的情况总是如此”）之类的内容，但这感觉像是在作弊，并且从我收集到的内容中，使用任意时间公式指定活跃度——而不是弱公平或强公平——是不受欢迎的。

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

4

1 回答 1

1

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

我找到了这个恰当命名的线程如何在无限次重试后测试进程最终成功？，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如果它继续无限期地启用，它将继续发生，因此系统不会在消息交换过程中停止。

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

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

第五是缺少的：它首先解决了OK从未启用的情况，因为会话在Query可能发生之前就过期了。

  1. 如果这种情况反复Query发生，并且会话同时有效，它最终会发生。
于 2020-03-22T12:15:11.190 回答