formal-methods - 形式的な方法 : []<> TLA で無限に頻繁に (常に最終的に)

Question

TLA での私の理解では、最終的なアクション (<>) は、次の状態でスタッターが発生することを許可していません。では、次の状態変数は、無限に頻繁 ([]<>) の場合、吃音を許可しないということですか?

気象条件の例を挙げると、無限に多くの場合、最終的には年に何日も雨が降る (いつ起こるかはわかりません) と説明できますが、雨が降った日の後に天気は晴れでなければなりませんか?

無限に対する私の理解は正しいですか？私が間違っている場合は修正してください。

ありがとうございました。