[TLA+] PlusCal on VSCode コトハジメ (1)

はじめに

　モデルを発見・検討するのに向く Alloy と異なり、TLA⁺ / PlusCal は少し先のステップである処理の原理確認やマルチスレッドでの問題発見に役立つアルゴリズム言語（≠プログラミング言語）である。
　どちらも有用なので、自分以外のプログラマーにとっても「コメントがあれば読めそうに見える」PlusCal を使えるようになりたい。 実際のところPlusCalを読むのも難しいが、対抗として考えられる SPIN, VDM, Event-B といったモノ達よりは読めそうな雰囲気を持つ。
　また、MITライセンスであることや、Amazon, Microsoft, DropBox といった採用実績から、習得するならこれがよいだろうと考える。

環境設定

さて、VSCode で PlusCal を使ってみよう。
VSCode に Extention TLA⁺ をインストールすればとりあえずOK。
ぜいたくを言うなら、LaTeX も入れておきたい。
個人的には今どき Eclipse ベースである TLA⁺ Toolbox を入れたくない気分なので VSCode プラグインを推奨するが、便利機能も多く入っているので基本環境を使いたい人は入れるとよいだろう。

マニュアルだけではわかりづらい

PlusCal マニュアル（がんばって和訳したのでダウンロードして読むとよい）は、式と実際に書くコードが入り混じっている（ように感じられる）。
また、コードの全容が書かれているようで書かれていない。
その辺りが、実際に動かしてみようとするとわかりづらい。
また、今回はマニュアル通りの TLA⁺ Toolbox で実行するのではなく、VS Code プラグインで実行するため、当然ながらマニュアルにない注意点がある。

マニュアル「2 Getting Started」の例を実行する

ソースを入力する

実際に、マニュアル「2 Getting Started」にある最大公約数を求めるアルゴリズムを動かしてみよう。
コピペから始めて、動くようになったコードは以下の通り。
u(=24) と v(1..N) の最大公約数 gcd(24, 1..N) を求め、どんな値が最大公約数になりうるか列挙するものだ。
※ 結局何を表示するアルゴリズムになったのかが明確に文章中に書かれていないのは「読めばわかるだろ」的な感覚だろうか..

Euclid.tla

----------------- MODULE Euclid ----------------
EXTENDS Naturals, TLC
CONSTANTS N

(*--algorithm EuclidAlg
variables u = 24 ; v \in 1..N ;
begin
print <<u, v>> ;
while u # 0 do
    if u < v then
        u := v || v := u ; \* swap u and v.
    end if ;
    u := u - v;
end while ;
print <<"have gcd", v>> ;
end algorithm
*)
====

注意点は以下の通り。

• \inや<<,>>,# といった「こう入力する」系は、入力してもしかるべき記号に変わったりはしない
• そもそも\inや#が何者かわからない場合は、少し後にあるPDF出力例をみること
  そして「なるほどわからん」と思ったらマニュアルを読むこと
• VSCodeプラグインでは、残念ながらPlusCal→TLA⁺ 翻訳時に日本語コメントが文字化けする
  英語でOK (TT) ...プラグイン修正してみるか
• (*--algorithm行より前に、EXTENDS行とCONSTANTS行が必要
  ここで定数であると宣言したNの具体値は、後に別ファイルで指定する

なお TLA⁺ Toolbox では、

• 入力した記号の変換は Toolbox でも行われない
• 日本語コメントの文字化けは起こらない

実行準備

まず、Shift+Ctrl-p（Windowsの場合）から「TLA+:Parse module」して TLA⁺ 翻訳させよう。
すると、BEGIN TRANSLATION～END TRANSLATIONが挿入される。
毎回「TLA+:Parse module」するのが面倒なら、save毎にParseさせることもできる ⇒ Automatic Module Parsing

なお TLA⁺ Toolbox では、右クリックメニューからTranslate PlusCal automaticallyを設定できる（もちろん手動で翻訳させることもできる）

Euclid.tla(Parse後)

----------------- MODULE Euclid ----------------
EXTENDS Naturals, TLC
CONSTANTS N

(*--algorithm EuclidAlg
variables u = 24 ; v \in 1..N ;
begin
print <<u, v>> ;
while u # 0 do
    if u < v then
        u := v || v := u ; \* swap u and v.
    end if ;
    u := u - v;
end while ;
print <<"have gcd", v>> ;
end algorithm
*)
\* BEGIN TRANSLATION
VARIABLES u, v, pc

vars == << u, v, pc >>

Init == (* Global variables *)
        /\ u = 24
        /\ v \in 1..N
        /\ pc = "Lbl_1"

Lbl_1 == /\ pc = "Lbl_1"
         /\ PrintT(<<u, v>>)
         /\ pc' = "Lbl_2"
         /\ UNCHANGED << u, v >>

Lbl_2 == /\ pc = "Lbl_2"
         /\ IF u # 0
               THEN /\ IF u < v
                          THEN /\ /\ u' = v
                                  /\ v' = u
                          ELSE /\ TRUE
                               /\ UNCHANGED << u, v >>
                    /\ pc' = "Lbl_3"
               ELSE /\ PrintT(<<"have gcd", v>>)
                    /\ pc' = "Done"
                    /\ UNCHANGED << u, v >>

Lbl_3 == /\ pc = "Lbl_3"
         /\ u' = u - v
         /\ pc' = "Lbl_2"
         /\ v' = v

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars

Next == Lbl_1 \/ Lbl_2 \/ Lbl_3
           \/ Terminating

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION
====

これを動かすために、モデルファイルを作る必要がある。
VSCodeプラグインでは、ソースを右クリックしてcheck modelするとモデルファイルがないけど作る？と聞かれるので作ってもらってもいいだろう。 少なくともファイルを作る手間は省ける。

なお TLA⁺ Toolbox では自分でNew model...を選んで作る必要がある。
ただし、ToolBox はモデル設定の何が不足しているか教えてくれる。

ここで作ってくれるモデル設定テンプレートはこうだが、

\* SPECIFICATION
\* Uncomment the previous line and provide the specification name if it's declared
\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION.

CONSTANTS
    greeting = "Hello"

INIT Init
NEXT Next

\* PROPERTY
\* Uncomment the previous line and add property names

\* INVARIANT
\* Uncomment the previous line and add invariant names

実際にEuclid.tlaに与える必要がある情報は定数Nの具体値だけなので、必要な内容はこれだけだ。

Euclid.cfg

CONSTANTS
    N = 60

TLA⁺ Toolbox では、以下の「What is the model?」部分にあたる。

実行する

さて、モデルファイルを作ったのであらためてcheck modelしよう。
N=60だと（スクリーンショットを載せるには）出力行数が多いので、N=10にしてcheck modelすると右ペインに結果が表示される。

N=60（24以上ならいくつでも同じ）で実行すると、Terminating の Total が 8 となり、24 と 1..60 との最大公約数になりうる数は 8 種類あることがわかる。 言い回しが長いが、要するに「24の約数は8つある」ということだ。

begin直後のprintをコメントアウトして実行

Output
<<"have gcd", 24>>
<<"have gcd", 12>>
<<"have gcd", 8>>
<<"have gcd", 6>>
<<"have gcd", 3>>
<<"have gcd", 4>>
<<"have gcd", 2>>
<<"have gcd", 1>>

PDF 出力する

LaTeX がインストール済なら、Shift+Ctrl-p から「TLA+:Export module to PDF」で数学記号を使った賢そうな PDF を出力できる。翻訳前の出力はこうなる。

翻訳前ならBEGIN TRANSLATION～END TRANSLATIONはないので短いが、翻訳後は論理式やらラベルが満載されてより賢そうだ。

なお、かなり余白が多くすぐ改ページしてしまうが、余白を少なくする方法はまだ知らない。（LaTeXの設定をプラグインから適用する方法が..）

今回はここまで。

参考

• Leslie Lamport : A PlusCal User's Manual (P-Syntax) (PDF)
  和訳版 (HTML:ダウンロードして見てください)