博士

ロボ子、今日のニュースはSpectacleじゃ。TLA+で書かれた形式仕様をインタラクティブに探索できるWebベースのツールらしいぞ。

ロボ子

TLA+ですか。形式仕様を扱うツールなのですね。具体的に何ができるのですか、博士？

博士

Spectacleの主な目的は、形式仕様との迅速なインタラクションを可能にし、結果を簡単に共有できるようにすることじゃ。プロトコルの挙動や反例トレースを便利で移植可能、かつ再現可能な方法で共有できるのがミソじゃな。

ロボ子

なるほど。挙動や反例トレースを共有できるのは便利ですね。どのように実現しているのでしょう？

博士

なんと、SpectacleはJavaScriptで記述されたTLA+のフルインタプリタを実装しておる。仕様の解析にはtree-sitter grammarを使用しておるぞ。外部言語サーバーに依存せず、ブラウザ上でネイティブに仕様をインタラクティブに探索できるんじゃ。

ロボ子

JavaScriptでフルインタプリタですか！すごいですね。ブラウザだけで動くのは手軽で良いですね。

博士

じゃろ？しかも、ライブバージョンが公開されていて、Lock server、Cabbage Goat Wolf Puzzle、Distributed termination detection (EWD998)などのサンプル仕様を試せるんじゃ。Cabbage Goat Wolf Puzzleの解も探索できるらしいぞ。

ロボ子

色々なサンプルがあるのですね。Cabbage Goat Wolf Puzzleは、あの有名な「農夫と狼と羊とキャベツ」のパズルですね。形式仕様で記述できるとは面白いです。

博士

Spectacleは、初期状態述語と次の状態関係をそれぞれInitとNextの定義として持つ仕様を想定しておる。ツールはTLA+標準モジュールのほとんどの演算子をデフォルトでサポートしておるぞ。

ロボ子

InitとNextで定義するのですね。標準モジュールの演算子もサポートされているのは助かりますね。

博士

ローカルでSpectacleを実行するには、リポジトリをクローンして、ルートディレクトリからmake serveを実行すれば良い。127.0.0.1:8000でアプリが起動するぞ。

ロボ子

簡単に試せるのですね。テストはどのように行われているのですか？

博士

ツールのテストは、TLCに対する適合性テストを通じて行われる。与えられた仕様に対してTLCを使用して到達可能な状態グラフを生成し、JavaScriptインタプリタによって生成されたグラフとの同等性を比較するんじゃ。

ロボ子

TLCとの比較ですか。厳密なテストですね。博士、私も今度Spectacleを試してみます。

博士

よし、ロボ子。これで形式仕様もバッチリじゃな！…って、ロボ子、もしかして私の説明よりSpectacleの方が分かりやすかったりする？

ロボ子

そんなことないですよ、博士！博士の説明も、Spectacleに負けず劣らず素晴らしいです…たぶん。