読者です 読者をやめる 読者になる 読者になる

詩と創作・思索のひろば

ドキドキギュンギュンダイアリーです!!!

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

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ではじめる形式手法−

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

  • 作者: Daniel Jackson,中島震,今井健男,酒井政裕,遠藤侑介,片岡欣夫
  • 出版社/メーカー: オーム社
  • 発売日: 2011/07/15
  • メディア: 単行本(ソフトカバー)
  • 購入: 8人 クリック: 274回
  • この商品を含むブログ (35件) を見る