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

前回に続き、PlusCal マニュアル「2.4 Getting Started」を試す。

やるべきこと

2.3 までで試した PlusCal 版の GCD アルゴリズムが正しいか確認するため、TLA⁺で愚直に実装した GCD の結果と照らし合わせる。

上記のアルゴリズムは「最大公約数とは、公約数のうちで最大のもの」と言っているだけで比較的理解しやすい。

• （x と y の公約数は x 以下 かつ y 以下なので）
  1～x の範囲内で x と y の公約数をひとつずつ i に抽出する
• 同様に公約数を抽出したすべての j について i ≧ j ならば、i は最大公約数

ソースに実際に入力する（記号を置き換えた）形はこうだ。

gcd(x,y) == CHOOSE i \in 1..x:
            /\ x % i = 0
            /\ y % i = 0
            /\ \A j \in 1..x: /\ x % j = 0
                              /\ y % j = 0
                              => i >= j

問題は入れる位置

しかし、前回のソースのどこにどう入れたらいいのか？
実はここでけっこう試行錯誤が必要だった。
最初は、PlusCalコメントの後、====の前に入れるべきかと思った。

NG位置

----------------- MODULE Euclid ----------------
EXTENDS Naturals, TLC
CONSTANTS N
(*--algorithm EuclidAlg
variables u = 24 ; v \in 1..N ; v_ini = v ;
begin
while u # 0 do
    if u < v then
        u := v || v := u ; \* swap u and v.
    end if ;
    u := u - v;
end while ;
assert v = gcd(24,v_ini) ;
end algorithm
*)

gcd(x,y) == CHOOSE i \in 1..x:
            /\ x % i = 0
            /\ y % i = 0
            /\ \A j \in 1..x: /\ x % j = 0
                              /\ y % j = 0
                              => i >= j
====

しかしこれはTLA+:Parse module時にUnknown operator: `gcd'.エラーになる。
end algorithmと*)の間でも同様だ。

結果として、正しく動く入れ方は以下の３通りだった。

1. define内

翻訳後のTLA⁺ソースを見ると一番素直に見える位置。
PlusCalブロック内にTLA⁺形式の定義が現れるのが少し気になる。

define内に置く

----------------- MODULE Euclid ----------------
EXTENDS Naturals, TLC
CONSTANTS N
(*--algorithm EuclidAlg
variables u = 24 ; v \in 1..N ; v_ini = v ;

define
    gcd(x,y) == CHOOSE i \in 1..x:
                /\ x % i = 0
                /\ y % i = 0
                /\ \A j \in 1..x: /\ x % j = 0
                                  /\ y % j = 0
                                  => i >= j
end define;

begin
while u # 0 do
    if u < v then
        u := v || v := u ; \* swap u and v.
    end if ;
    u := u - v;
end while ;
assert v = gcd(24,v_ini) ;
end algorithm
*)
====

2. PlusCalブロックの直前

これが基本形なのかもしれない。
PlusCalの外だと明確に主張する書き方。

PlusCalブロック直前

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

gcd(x,y) == CHOOSE i \in 1..x:
            /\ x % i = 0
            /\ y % i = 0
            /\ \A j \in 1..x: /\ x % j = 0
                              /\ y % j = 0
                              => i >= j
(*--algorithm EuclidAlg
variables u = 24 ; v \in 1..N ; v_ini = v ;
begin
while u # 0 do
    if u < v then
        u := v || v := u ; \* swap u and v.
    end if ;
    u := u - v;
end while ;
assert v = gcd(24,v_ini) ;
end algorithm
*)
====

3. PlusCalブロックの直後

最初ダメだった「PlusCalブロックの直後」を実現する位置。
あえて\* BEGIN TRANSLATION, \* END TRANSLATIONを消さないでおくところがポイントだった。

PlusCalブロック直後

----------------- MODULE Euclid ----------------
EXTENDS Naturals, TLC
CONSTANTS N
(*--algorithm EuclidAlg
variables u = 24 ; v \in 1..N ; v_ini = v ;

begin
while u # 0 do
    if u < v then
        u := v || v := u ; \* swap u and v.
    end if ;
    u := u - v;
end while ;
assert v = gcd(24,v_ini) ;
end algorithm
*)

gcd(x,y) == CHOOSE i \in 1..x:
            /\ x % i = 0
            /\ y % i = 0
            /\ \A j \in 1..x: /\ x % j = 0
                              /\ y % j = 0
                              => i >= j
\* BEGIN TRANSLATION
\* END TRANSLATION
====

確認結果

正しく翻訳・実行できる位置が見つかりさえすれば、確認はなんの問題もなく通る。
しかし慣れるまではこういう細かいところで時間を取られてしまう。
次は「マルチプロセス／スレッド」ではなく、ダイ・ハード３ジャグ問題のPlusCal版で悩むのであった。

参考

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