TLA+
\( \def\ldef{≜} \) \( \def\globally{□} \) \( \def\eventually{◇} \) \( \def\openleftarrowplus{\overset{+}{⇾}} \) \( \def\equalv{⫤} \)

PlusCal

Takami Torao TLC2 #PlusCal #TLA+
  • このエントリーをはてなブックマークに追加

概要

PlusCal は逐次処理をモデル化することを目的に設計された仕様記述言語。TLA+ 用の逐次処理向け DSL と言ったところで TLA+ から多くの構文や演算子を流用しているが、ステートマシンの設計をモデル化することを意図して仕様化された TLA+ と比べてパラダイムは大きく異なっている。

PlusCal の仕様は TLA+ のブロックコメント部分に記述する (HTML 内に CSS や JavaScript を記述する感覚に似ている)。PlusCal で記述された仕様は最終的に TLA+ にトランスパイルされてモデルチェックが行われる。

---- MODULE モジュール名 ----
(* --algorithm algorithm_name
begin
  skip; \* ここに逐次実行のステップを記述する。
end algorithm; *)
====
  1. 概要
  2. hello, world の実行例
  3. 参考文献

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; *)
====

最初に知っておくべき基本的な注意点:

  1. 構文の境界: PlusCal としての構文は algorithm [モジュール名] から end algorithm; までの間で、それより外は TLA+ の構文である。
  2. モジュール名の統一: ファイル名の [モジュール名].tla と TLA+ 構文の MODULE [モジュール名]、PlusCal 構文の algorithm [モジュール名] は全て同じ [モジュール名] を使用しなければならない。この例での [モジュール名] とは HelloWorld のこと。
  3. 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)。

Fig 1. コンテキストメニューに表示されている "Check model with TLC" を選択するとモデルのチェックが行われる。
Fig 2. TLC の実行結果。

TLC での実行結果は単に hello, world を逐次実行したのとまったく同じに見えるかもしれない。これは hello, world の仕様が条件分岐もループも持たず、また状態変数や境界値条件の複合のような性質もないことから、唯一の実行経路が実行可能であればモデルチェックが完了するためである。

PlusCal: 制御構造

自動販売機を例に PlusCal の基本的な制御構造を説明する。実行環境のセットアップは PlusCal を参照。

2021年2月22日(Mon) TLC2 #PlusCal #TLA+

参考文献

  1. Leslie Lamport (2009) The PlusCal Algorithm Language
  2. Leslie Lamport (1997) The Operators of TLA+
↑ページの先頭
F