PlusCALを試してみよう
世の中で話題沸騰のTLA+およびPlusCAL、僕も試してみようかな、と思い立った。
お、ぐぐっても日本人試してないじゃん。というか、記事書いてないじゃん。
一番乗り！っていうだけのノリです、すみません。仕事でバリバリ使えたらかっこいいんですが、今のところただの勉強。
TLAってなんだろう、という方は、このペーパーを読むとぐっとくると思います。
http://research.microsoft.com/en-us/um/people/lamport/tla/amazon.html
さてさて、空前のTLAブームにもかかわらず、本家のWebはたいそうショボイ。
http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html
ドキュメント類も、全部「適当に汲みとってよ」みたいなのが多くて最初からつまずきそうですが、まあ、そんなもんでしょう。
参考にしているドキュメント
いまのところ、TLA+ 本体よりもPlusCALのほうがとっつきやすそうなので、これを読んでいる。
http://research.microsoft.com/en-us/um/people/lamport/tla/c-manual.pdf
でも、結局TLA+を理解しないとダメな予感。
ツールをインストールしてみる。
最初にダウンロードしたのはなんかTLA TOOLBOXというもの。Linux版はeclipseのプラグインとかだったんだけど、よくわからん。Mac版は展開してtoolboxってのをダブルクリックしたら開発環境みたいなのが立ち上がった。キタコレ。でも、古い人間にはよくわからんです。はやく実際のコード書きたいんです。
と、思ってたらもっとローテクなのが有りました。
http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html
このツールを展開したら、
export CLASSPATH=~/installed_directory
とかにして、
java pcal.trans test.tla
とかすればいいはず。
はじめてのTLA
さてさて、写経の時間です。これからやることは、PlusCal記法で書いたコードをtlaに変換してもらう、ということで、ふむふむ、じゃあ、PlusCal用のファイルを作って、と。拡張子はなんだろう？って思ってたわけですよ。でも、そうではないみたい。ようは、tlaファイルにPlusCalのコードをコメントとして埋め込むと、それをTLAに変換してくれる、という話でした。そして、変換は元ファイルを直接書き換えるというかなり思い切ったことをしてきます。（元ファイルは.oldとして残る）
以下、上記 c-manualからの写経です。私に著作権はないです。その辺の作法知らないけどスルーしてください。
---- MODULE test ----
EXTENDS Naturals, TLC
CONSTANT N
(*
--algorithm test {
variables u = 24 ; v \in 1 .. N ;
{ print <<u, v>>;
while (u # 0)
{ if (u < v) { u:= v || v:= u};
u:= u - v };
print <<"have gcd", v>>; }}
*)これを、test.tlaとして、いざ、java pcal.trans test.tla を実行。
成功（、するまでに、試行錯誤があった。）
ざっくりいうと、24と 1からNまでの自然数の最大公約数を求めるプログラム、ということだ。
さて、このアルゴリズムが正しいかを検証する。
java tcl2.TLC test.tla でいいのかな？
あれ、エラー。（１回目）
最初のエラーは、上記コードのCONSTANT がCONTSTANTになってたからだった。なんと、そこは変換では無視される。タイポを直して再チャレンジ。
またエラー。Nがなんだかわかりません。コンフィグファイルを設定してください。と言われて、おう、そうだよね、
test.cfgってファイルが勝手に作られてるし、ここでN指定しないと、そりゃだめだよね、とおもったものの、コンフィグファイルの
記法がわからん。。。 試行錯誤で、CONSTANT N = 12; であることがわかった。これで、1から12まで数と24の最大公約数を計算する際の状態を全て求めてチェックしてくれる。
ふむふむできた。これだけではなんの意味もないが、もう少しそれっぽいのも試してみる予定。
