0

我知道决策树和不变量是什么（如果这是正确的术语）。使用的所有其他定义（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
4

1 回答 1

1

请参阅此示例，该示例显示如何使用 ASSUME 断言一些简单的数学/常数公式：https ://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/SimpleMath/SimpleMath.tla

于 2020-05-20T03:28:40.547 回答