どのように特定の状態をアサートすると、TLA +に変数を持つ別の状態になりますか？

Question

申し訳ありませんが、タイトルは少しわかりません。私は1つの要求を追加する労働者のセット、および別のセットや労働者にそれらを満たすとOutcomesへの書き込みを持って

variables Requests = {}, Outcomes = {}; 

：私は2つのセットを定義してTLA +スペックを持っています。各リクエストには固有のIdがあり、一致するOutcomeエントリにも含まれます。

Requestsセットに追加されたリクエストは、最終的にOutcomesセットの同じIdの構造と一致することを保証したいと思います。私は、 "リードする"、~>、演算子を使ってこれをしようとしていましたが、Idの一致部分を解決する方法を見つけることができません。

私は単純に何かしようとしました：

RequestsAreFulfilled == \E req \in Requests: TRUE 
         ~> \E outcome \in Outcomes : outcome.id = req.id 

をしかし、これは明らかにreq以来、第二の式で定義されていません破ります。私は、2番目の表現の行に沿って何かを考えました。「次に、すべてのリクエストアイテムが結果アイテムと一致する状態がありますが、システムは決して終了しないので動作しません。 Requestsが設定されているので、は常に追いついています。

リクエストが最終的に同じIDの結果と一致すると主張する方法は何ですか？

Answer 1

TLCには、非定型セットの生存特性が証明されています。有限の固定されたIDを持つ固定されたケースから始めましょう。次に、関係を指定することができます。

\A id \in Ids: (\E r \in req: r.id = id) ~> (\E o \in out: o.id = id) 

この場合、構造が分かりやすく、共有関係をよりよく表現できるため、構造を使用する方がよいでしょう。

requested = [i \in Ids |-> FALSE]; 
processed = [i \in Ids |-> FALSE]; 

\A id \in Ids: requested[i] ~> processed[i] 

または

messages = [i \in Ids |-> [requested |-> FALSE, processed |-> FALSE]] 
\A id \in Ids: 
    LET m == messages[i] 
    IN m.requested ~> m.processed 

あなたがメッセージの無限の数をしたい場合、TLCは、ライブネスチェックを処理するために取得するための一つの方法は、「リサイクル」の完成メッセージをするためのロジックを追加するidの固定セットを使用することです - requestedとprocessedの両方をFALSEに設定します。次に、常時演算子[]<>を使用して、これを表現することができます。

\A id \in Ids: []<>(requested[i] => processed[i])