Alloyガール3

Alloyガール1、Alloyガール2の続き。

JS: あれれ？おかしいな？
僕: ん、どうしたの？
JS: Alloyちゃんはこの2つ等価だって言ってたけど出てくるものが違うよ？

sig StateManager {
	state: set State
}

sig State {}

run {
	one StateManager
}

one sig StateManager {
	state: set State
}

sig State {}

run {}

僕: え？あ、ホントだね。最初に出てくるものが違うね。でも全部出すと同じだ。
JS: ぜんぶ？？
僕: あー、そうか、説明してなかったか。「Next」ボタンを押すと次の解が出るんだよ。
JS: あ、てきとうに1つ選んで教えてくれるのかと思ってた。
Alloy: そんな適当なことするわけがないじゃない。私はスコープ内の解を全部出しているのよ。
JS: スコープ？
僕: あ、それも説明してなかった。Alloyさんの発想は「構成要素の数が少ないモデルを全部検証すれば大体のバグが発見できるはず」なんだけど、
Alloy: 「各要素いくつまでの範囲で検証するか」がスコープよ
僕: (セリフ取られた…) で「run {}」は「各要素3つまでの範囲で探索」になってる。
Alloy: run {} for 3と等価。
JS: なるほどー。for 3 ってのは3つ以下って意味なのね？ちょうど3つにしたい時は？
Alloy: そう書けばいいじゃない。
僕: exactlyを使うんだよね。あと、全部ちょうど3つにするとStateManagerが1個って制約に反するからStateだけに指定しなきゃ。

one sig StateManager {
	state: set State
}

sig State {}

run {
} for exactly 3 State

次回予告

JS: Stateが3つの例だけが出るようになったー
僕: うんうん、よかったね
JS: でもー、なんかStateManagerにつながってないStateがあるけど、いいのかな
僕: あー、なるほど。それは…と説明したいところだが保健室に行かなきゃいけないんで続きは帰ってきてから！