PlusCal
概要
PlusCal は逐次処理をモデル化することを目的に設計された仕様記述言語。TLA+ 用の逐次処理向け DSL と言ったところで TLA+ から多くの構文や演算子を流用しているが、ステートマシンの設計をモデル化することを意図して仕様化された TLA+ と比べてパラダイムは大きく異なっている。
PlusCal の仕様は TLA+ のブロックコメント部分に記述する (HTML 内に CSS や JavaScript を記述する感覚に似ている)。PlusCal で記述された仕様は最終的に TLA+ にトランスパイルされてモデルチェックが行われる。
---- MODULE モジュール名 ----
(* --algorithm algorithm_name
begin
skip; \* ここに逐次実行のステップを記述する。
end algorithm; *)
====
hello, world の実行例
この記事では TLA+ と同様に Visual Studio Code (vscode) を使用して PlusCal の実行を行う。環境構築は環境設定と TLC の実行の通り vscode と TLA+ 拡張機能をインストールするだけである。
まず最初に簡単な hello, world を実行してみよう。vscode で以下のような内容の HelloWorld.tla
ファイルを作成する。
---- MODULE HelloWorld ----
EXTENDS TLC
(* --algorithm HelloWorld
begin
PRINT:
print "hello, world";
end algorithm; *)
====
最初に知っておくべき基本的な注意点:
- 構文の境界: PlusCal としての構文は
algorithm [モジュール名]
からend algorithm;
までの間で、それより外は TLA+ の構文である。 - モジュール名の統一: ファイル名の
[モジュール名].tla
と TLA+ 構文のMODULE [モジュール名]
、PlusCal 構文のalgorithm [モジュール名]
は全て同じ[モジュール名]
を使用しなければならない。この例での[モジュール名]
とは HelloWorld のこと。 - EXTENDS: PlusCal のコードから TLA+ の機能を使用するときは TLA+ 構文で
EXTENDS
を指定する。EXTENDS
の機能的な意味は Java や Python の import と同じで識別子を解決する。この例では HelloWorld モジュール内でprint
という機能を使用するためにTLC
モジュールをEXTENDS
している。
CTRL+Shift+P を押して "TLA+: Parse module" を選択すると以下の様な TLA+ のコードにトランスパイルされる。トランスパイル結果を見ると PlusCal のコード中の end algorithm; *)
から ====
の間に TLA+ のコードが挿入されていることがわかる (翻訳前の完全な状態は HelloWorld.old
に保存されている)。また同時に HelloWorld.cfg
も生成される。
---- MODULE HelloWorld ----
EXTENDS TLC
(* --algorithm HelloWorld
begin
PRINT:
print "hello, world";
end algorithm; *)
\* BEGIN TRANSLATION (chksum(pcal) = "cd711785" /\ chksum(tla) = "bd4f6bd0")
VARIABLE pc
vars == << pc >>
Init == /\ pc = "PRINT"
PRINT == /\ pc = "PRINT"
/\ PrintT("hello, world")
/\ pc' = "Done"
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars
Next == PRINT
\/ Terminating
Spec == Init /\ [][Next]_vars
Termination == <>(pc = "Done")
\* END TRANSLATION
====
SPECIFICATION Spec
\* Add statements after this line.
この記事では生成される TLA+ 表記の仕様や *.cfg
については特に説明しない。
次に EXPLORER ペインで HelloWorld.tla
ファイルを右クリックして (Fig 1) "Check model with TLC" を選択するとモデルチェックが実行されて結果が表示される (Fig 2)。
TLC での実行結果は単に hello, world を逐次実行したのとまったく同じに見えるかもしれない。これは hello, world の仕様が条件分岐もループも持たず、また状態変数や境界値条件の複合のような性質もないことから、唯一の実行経路が実行可能であればモデルチェックが完了するためである。
参考文献
- Leslie Lamport (2009) The PlusCal Algorithm Language
- Leslie Lamport (1997) The Operators of TLA+