TLA+による簡単な状態遷移表現とfairnessの導入

対象読者

TLA+のツール導入もある程度の文法理解も終わった方。
注意：ネット記事上で大半を占めるPlusCalでの記述ではありません。

課題

以下の状態遷移図にて、最終的にS3に到達するかを検証します。

構造表現

sがステートでact[ABC]がエッジです。

VARIABLE s

Invariants == s \in {"S1", "S2", "S3"}
Init == /\ s = "S1"

actA == /\ s = "S1"
        /\ s' = "S2"

actB == /\ s = "S2"
        /\ s' = "S1"

actC == /\ s = "S2"
        /\ s' = "S3" 

挙動表現

とりあえず以下とします。
これはfairnessに関する問題をはらんでいます。

Next == \/ /\ actA
        \/ /\ actB
        \/ /\ actC
Spec == /\ Init
        /\ [][Next]_<<s>>

modelには以下のように記述します。

実行してみましょう。

実行：Stutteringによるエラー

以下のエラーとなりました。

Stutteringと書いてあります。これはNextが実行されない状態が延々とループしていることを意味します。上記エラーではS1で停滞しています。
これはSpecの

[Next]_<<s>>

が

Next\/(s'=s)

と同値でありこれらはNextが実行されずsが変化しないことを許容していることが原因です。

このような停滞は貴方のモデル検証にて懸念するべきことでは無いかもしれませんが、別なケースでは多いに懸念に値するものです。別な記事にてかければと思います。
とりあえずこの記事では、停滞は起こらないと仮定したいとして、以下のエラー回避を行います。

問題回避：WFの導入

Specに以下ADDコメントで示されている行を追加します。

Spec == /\ Init
        /\ [][Next]_<<s>>
        /\ WF_<<s>>(Next)   \* ADD

WFはWeakFairnessの略です。Nextがいずれ実行されることを保証します。

これで目的の検証はできるでしょうか。
実行してみましょう。

実行：ループによるエラー

Back to State 1とあるように、S2後にS1に戻っています。すなわちS1-S2間をループしています。

WFにてNextの実行を保証したとしても、このループが回る限り永遠に最終目的であるs3への到達は出来ません。この状態は即ちact[AB]の実行が早すぎてactCが実行されないというものであり、これもSttutteringと同様あるケースでは懸念とする状況ですが、今回は対象外として回避を行います。

問題回避：SFの導入

以下のように追記します。

Spec == /\ Init
        /\ [][Next]_<<s>>
        /\ WF_<<s>>(Next)   
        /\ SF_<<s>>(actC)   \* ADD

SFはStrongFairnessの略です。actCがある時点から永久に実行不可にならないのであれば、いずれ実行されることを保証します。

実行してみましょう

実行：エラー無し

正常終了出来たかと思います。

最終コード

------------------------------- MODULE States -------------------------------
VARIABLE s

Invariants == s \in {"S1", "S2", "S3"}
Init == /\ s = "S1"

actA == /\ s = "S1"
        /\ s' = "S2"

actB == /\ s = "S2"
        /\ s' = "S1"

actC == /\ s = "S2"
        /\ s' = "S3" 

Next == \/ /\ actA
        \/ /\ actB
        \/ /\ actC

Spec == /\ Init
        /\ [][Next]_<<s>>
        /\ WF_<<s>>(Next)   
        /\ SF_<<s>>(actC)
        

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