CODEWITHSUNDEEP
model-checkingtla+
Dominykas Mostauskis
Dominykas Mostauskis

Reputation: 8125

How to check if a decision tree satisfies an invariant?

I know the decision tree and what the invariant is (if that's the right term). All the other definitions used (UsingTor, UsingProxy, etc. can be anything). How can I use TLA+ to check if every leaf of the decision tree satisfies the invariant?

I would know how to do this if the decision tree was a sequence of states: I'd check if it always ends up in a state satisfying this invariant. Not sure how to do this though.

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

Upvotes: 0

Views: 67

Answers (1)

M.K.
M.K.

Reputation: 354

See this example that shows how to use ASSUME to assert some simple mathematical/constant formulas: https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/SimpleMath/SimpleMath.tla

Upvotes: 1

Related Questions