model-checking - 決定木が不変条件を満たしているかどうかを確認する方法は?

Question

私は決定木と不変条件が何であるかを知っています (それが正しい用語であれば)。使用される他のすべての定義 ( UsingTor、UsingProxyなどは何でもかまいません)。TLA+ を使用して、ディシジョン ツリーのすべての葉が不変条件を満たしているかどうかを確認するにはどうすればよいですか?

決定木が状態のシーケンスである場合、これを行う方法を知っています。この不変条件を満たす状態になるかどうかを常に確認します。ただし、これを行う方法がわかりません。

Invariant ==
    /\ UsingTor => UsingProxy
    /\ UsingProxy => UsingTor
    /\ UsingProxy => UsingBlockingClient
    /\ UsingBlockingClient => UsingProxy
    /\ ToldToUseLocalBitcoinNode => ~ConfiguredToIgnoreLocalBtc
    /\ ConfiguredToIgnoreLocalBtc => ~ToldToUseLocalBitcoinNode
    /\ ToldToUseLocalBitcoinNode => ~UsingProxy
    /\ ~ToldToUseLocalBitcoinNode => DisableUseOfLocalBtcNode

DecisionTree ==
    \/ /\ UsingProxy
       /\ \/ /\ ConfiguredToIgnoreLocalBtc
             /\ UsingBlockingClient
          \/ /\ ~ConfiguredToIgnoreLocalBtc
             /\ UsingBlockingClient
             /\ UsingProxy
       /\ ~ToldToUseLocalBitcoinNode => DisableUseOfLocalBtcNode
    \/ /\ ~UsingProxy
       /\ ~UsingTor
       /\ ~UsingBlockingClient