!Alloy
なんか西尾さんがすげー楽しそうにAlloyを語っているのに僕には何もわからないのでなんか悔しい。

僕も楽しみたい。


SATソルバーのラッパだとかそんなことを聞いたので、いつか何かの役に立つかもしれないしね（あまり期待していない。）
{{embed https://twitter.com/#!/nishio/status/189005312756420608}}

参考： http://d.hatena.ne.jp/nishiohirokazu/20120409/1333979323

ってそもそもAlloyってどうやって入れるんだろうか？

探してみる
- http://alloy.mit.edu/alloy/
-- http://alloy.mit.edu/alloy/download.html

これか jarだから落としたら動きそう。

alloy4.jarをおっことす（4.1MBくらい）

あとは実行するだけか。
僕のメインPCはLinuxなので最寄りのコマンドラインから…

>>
$ java -jar alloy4.jar 
<<
よし ウインドウが出てきた 4.1.10 か。

フォントがダサいが… まぁいいか

http://d.hatena.ne.jp/nishiohirokazu/20120409/1333928800
Alloyガール1を参考にプログラム？してみる

!Alloyガール1おさらい
実行ってのはツールバーの Executeでいいのかな？…

>>
There are no commands to execute.
<<
よしよし
まだrunを書いてないからこれでよし。

>>
sig StateManager {
	state: State
}

sig State {}

run {}
<<

こうかな？（まるうつし）
>>
Executing "Run run$1"
   Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   116 vars. 15 primary vars. 165 clauses. 108ms.
   . found. Predicate is consistent. 33ms.
<<

なんか動いたな。

GUIで出すのは「Show」ボタンだな
おおおでた！  →

{{twitpic 97r9p3}}

よし これでAlloyガール1追っかけ終了だな。

とりあえずすげー敷居が低いな。
ビジネスロジックの検証とかがこういうのでできるようになると未来だと思うんだよねー


!Alloyガール2おさらい
もう少しやってみよう

おや？ そういえばこの条件を満たす答えはたくさんあるきがする…。
この画面の「Next」をクリック？ すると次の解が出るのか…。 の割にはなにか制限がかかっているような気がする。 あとでしらべるか。

あとStateManagerとつながっていないStateが出てくる解があるがそれは… それでいいのか？

>>
one sig StateManager {
	state: some State
}

sig State {}

run {}
<<
これの何個目かの解がブログのものと一致するな。



!このwikiの不満
画像を上げれるようにしたい。 twitpicに上げて参照とかどんだけー