Alloy をコマンドラインから実行できるツールを書いた

先日触れた Alloy は、エントリの最後に書いたようにインクリメンタルなモデリングを行うためのものだけど、基本的に提供されているインターフェイスが GUI なのが少し不便だった。全てのコマンドを実行するショートカットキーがなく、メニューから選ばなくてはならないので、新しく加えた制約がそれまで成立していたアサーションを壊しはしないかチェックするのがけっこう面倒であった。

http://motemen.hatenablog.com/entry/2016/06/alloy-oauth2-modeling

こういうのは自動化すべきであった。で、Alloy が Java の API を提供している ことに気がついたのは件のエントリを書いた日のことだった……。

すぐには使いたい場面はなくなってしまったのだけど、この API を使ってコマンドラインツールを書くことにした。Alloy の jar の中にはソースコードが同梱されていたので、edu/mit/csail/sdg/alloy4whole/ExampleUsingTheAPI.java なんかを参考にしたら簡単だった。

勉強がてら Kotlin と Gradle を使って書いた。

https://github.com/motemen/kt-alloy-cli

git clone して ./gradlew distTar すると、Alloy の jar をダウンロードした上でアプリをコンパイルし、./build/distributions/kt-alloy-cli.tar に成果物をまとめて出力する。これをどこかに展開し、alloy-run のようなコマンドから参照すればよい:

#!/bin/bash
exec path/to/bin/kt-alloy-cli "$@"

引数として Alloy で書かれたソースコードを与えると、ファイル中のすべてのコマンドを順に実行する。run の場合充足例が見つかれば ok、check の場合反例が見つからなければ ok。

% alloy-run oauth2/oauth2.als
1..3
ok 1 - Run show for 6 but 1 AuthorizationServer, 1 Client
ok 2 - Run allUserAgentsAreEventuallyAuthorized for 6 but exactly 1 AuthorizationServer, exactly 1 Client, 2 UserAgent
not ok 3 - Check userAgentsAreProperlyAuthorized for 6 but exactly 1 AuthorizationServer, exactly 1 Client, 2 UserAgent

オプション引数に -V を与えると、反例が見つかった場合、GUI を開いてインスタンスを提示してくれる。

出力は TAP 互換になっているので Perl の prove からも使える。

% prove --exec=alloy-run oauth2/oauth2.als
oauth2/oauth2.als .. Failed 1/3 subtests

Test Summary Report
-------------------
oauth2/oauth2.als (Wstat: 0 Tests: 3 Failed: 1)
  Failed test:  3
Files=1, Tests=3,  3 wallclock secs ( 0.01 usr  0.01 sys +  6.06 cusr  0.25 csys =  6.33 CPU)
Result: FAIL

どうぞご利用ください。

抽象によるソフトウェア設計−Alloyではじめる形式手法−