ブランチが実行されていることを確認してください。

Question

プログラムは、STARTからLEFTまたはRIGHTブランチに分岐できます。 LEFTブランチの実行パスとRIGHTブランチのもう一つの実行パスがあることを確認する方法はありますか？完全一般場合

------------------------------ MODULE WFBranch ------------------------------ 

VARIABLE state 

START == "start" 
LEFT == "left" 
RIGHT == "right" 

Init == state = START 

Next == 
    \/ /\ state = START 
     /\ \/ state' = LEFT 
      \/ state' = RIGHT 
    \/ /\ state \in {LEFT, RIGHT} 
     /\ state' = START 

Spec == 
    /\ Init 
    /\ [][Next]_<<state>> 
    /\ WF_<<state>>(Next) \* Avoid stuttering at start 

(* 
This passes, but it does not ensure that there exist different paths covering both 
branches - e.g. state might never be LEFT. 
*) 
CheckEventualStates == \/ (state = START) ~> (state = RIGHT) 
         \/ (state = START) ~> (state = LEFT) 

============================================================================= 

Answer 1

、すべての状態のために、少なくとも一つの行動が最終的に到達したことを確認する方法はありません。これは、TLA +が線形時間論理に基づいているためです。これは、複数の異なる動作間に保持されるプロパティを表現する手段を持たないためです。

場合によっては、の特定のケースに応じて、あなたが作ることができるサブセットがあります。たとえば、私たちは、その後、あなたがENABLED FTRは、「指定システム」8.4弱い公正で説明されて

CheckEventualStates == 
    /\ <>(ENABLED Left) 
    /\ <>(ENABLED Right)