さて、スタートAlloy中、頂いたテクニカルな質問のうち1つに、当日うまく答えられませんでした(すいません… orz)。
ちゃんと考え直したので(^^; ここに書いておきます。(thx to @masahiro_sakaiさん)
質問
以下のようなシグネチャ宣言があったとする。
sig A { r: B one -> one C }
ここで、Bのスコープを1にすると、任意の a: A から得られる a.r が全部同じになってしまう。
たとえば、以下のようなコマンドで反例が出ない。
check { all disj a1, a2: A | a1.r = a2.r } for 3 but 1 B
たとえば a1.r は空で、a2.r は空でないような可能性があるように思うが、なぜないのか?
回答
まず、シグネチャのフィールドにある関係は、次のように解釈されます。(Alloy本 p.261)
…したがって、例えば
sig S {f: e}という宣言によって導入される制約は、(fを通常の変数とした場合の)fが式eの部分集合であるという制約ではなく、以下のような制約になる。
all this: S | this.f in e
よって、先ほどのシグネチャA内のフィールドrの宣言は、
all a: A | a.r in B one -> one C
という制約だと解釈されます。(thisはaに置き換えました)
更に、関係の中の多重度についてですが、(Alloy本 p. 76)
多重度は単なる省略記法であり、標準的な制約に置き換えることができる。以下の多重度制約は、
r: A m -> n B以下のように書き換えることができる。
all a: A | n a.r all b: B | m r.b
とあります。コロンは in と読み替えても意味的には同じです。
ということで、先ほどの制約式を、更に展開すると
all a: A | all b: B | one b.(a.r) all a: A | all c: C | one (a.r).c
となります。
なので、Bのスコープが1だと、B、C ともに空で a.r が常に空になるか、B、C ともにサイズ1で、aによらず a.r が存在して一意に定まるか、いずれかになります。
追記
続きを書きました → シグネチャのフィールドにある関係の多重度 続き - たけをの日記@天竺から帰ってきたよ