問題タブ [tla+]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
tla+ - TLA+ でサイクルが発生しないように liveness を指定する
私は、TLA+ を学習するための単純なクライアント サーバー インタラクションの仕様を書いています。
ご覧のとおり、クライアントはサーバーに対してクエリを実行できます。セッションが OK の場合は結果が返されます。それ以外の場合は、承認してから再試行する必要があるというメッセージが表示されます。セッションはいつでも期限切れになる可能性があります。
クライアントが最終的に結果を取得できるようにしたいので、次の行をプロパティに追加しました。
モデルのチェック時に、次のような反例に直面しています: Init -> (Query -> Unauthorized -> Authorize -> Expire) で、括弧内の部分が無限に繰り返されます。私が最初に考えたのは、ステップに強い公平性を要求することでしたOK。ただし、問題はこのシナリオのOKステップが有効にならないことです。
[]<><<OK>>_vars（「最終的に発生するのは常にそうである」と読みます）のようなことを追加できますOKが、これは不正行為のように感じられ、収集したものから、任意の一時的な式を使用してライブ性を指定すること、および弱い公平性または強い公平性ではありません.
弱い公平性または強い公平性を使用して、クエリが最終的に応答を受け取ることを保証するにはどうすればよいですか? それとも私のモデルが悪いのでしょうか？私はアイデアがありません...