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)

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

ご覧のとおり、クライアントはサーバーに対してクエリを実行できます。セッションが OK の場合は結果が返されます。それ以外の場合は、承認してから再試行する必要があるというメッセージが表示されます。セッションはいつでも期限切れになる可能性があります。

クライアントが最終的に結果を取得できるようにしたいので、次の行をプロパティに追加しました。

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

モデルのチェック時に、次のような反例に直面しています: Init -> (Query -> Unauthorized -> Authorize -> Expire) で、括弧内の部分が無限に繰り返されます。私が最初に考えたのは、ステップに強い公平性を要求することでしたOK。ただし、問題はこのシナリオのOKステップが有効にならないことです。

[]<><<OK>>_vars（「最終的に発生するのは常にそうである」と読みます）のようなことを追加できますOKが、これは不正行為のように感じられ、収集したものから、任意の一時的な式を使用してライブ性を指定すること、および弱い公平性または強い公平性ではありません.

弱い公平性または強い公平性を使用して、クエリが最終的に応答を受け取ることを保証するにはどうすればよいですか? それとも私のモデルが悪いのでしょうか？私はアイデアがありません...

4

1 に答える 1

1

私は自分の質問に答えています。誰かがより良い答えを持っていると思う場合は、共有してください。

この適切な名前のスレッドを見つけましたプロセスをテストする方法は、無期限の再試行後に最終的に成功しますか? 、レスリー・ランポート自身が指摘するところでは、アクションと他の公式の結合について公平性を主張することができます. このシナリオSpecでは、次のようになります。

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

では、これらの式はそれぞれ何を意味するのでしょうか? 最初の 3 つは非常に明白であり、定義しようとする私の試みに含まれていましたSpec。

  1. Init動作の最初の状態で真です。
  2. Next動作のすべてのステップに当てはまります (吃音は許可されています)。
  3. Next無期限に有効にし続けると発生し続けるため、メッセージ交換の途中でシステムが停止することはありません。

4 つ目は私の直感でした。これにより、クエリが作成された後、セッションが期限切れになる状況が修正されます。

  1. 繰り返し有効にするOKと (発生する可能性があります)、最終的には発生します。

そして 5 番目に欠けていたOKのは、セッションが発生する前に期限切れになったため、そもそも有効にならなかった状況を修正するQueryことです。

  1. 発生する可能性のあるケースが繰り返しQuery発生し、同時にセッションが有効である場合、最終的には発生します。
于 2020-03-22T12:15:11.190 に答える