Alloy で形式手法を始めてみた！～関係式の多重度編～
関係式とは？
シグネチャ同士のつながり関係を表す条件式を関係式といいます．
これもある種のフィールドとして扱います．
フィールドについてはこちらで説明しています．
多項関係
シグネチャは，フィールドとして多項関係を持つことが可能です．
多項関係は "->" で記述します．多項関係ですから，"->" は直積を表します．
sig Password {}
sig Machine {}
one sig Person {
Unlock: Password -> Machine
}これを実行すると，下の図のように，Person がどの Password でどの Machine を Unlock できるかの図が表示されます（Unlock が空のものも表示されるので，表示されるまで Next し続けます）．
この場合，Unlock は {(Password0, Machine1), (Password1, Machine0)} を表しています．
更にいうと，Unlock は各 Person に対して二項関係 Password -> Machine を定義しているわけですから，Unlock は正確には "Person -> (Password -> Machine)" であると考えられます．
したがって，シグネチャのフィールドも多項関係です．
こちらの例を再度見てみましょう．
sig Father {}
sig Mother {}
sig Child {
father: Father
, mother: Mother
}結局これも，father は Child -> Father という関係を，mother は Child -> Mother という関係を定義していたということです．
陽に -> を使うかどうかということですね．
多項関係の重複度
-> 演算子にも重複度（set, one, lone, some）をつけて多項関係に制限をつけられますので，解説していきます．
文法的には，
// A, B はシグネチャ，m, n は重複度，rel は多項関係
rel: A m -> n Bという書き方をします．意味合いとしては，「A の各インスタンスは B のインスタンス n（個）に対応し，B の各インスタンスは A のインスタンス m（個）に対応する」ということです．詳しく見ていきましょう．
ただし，m, n には set, one, lone, some の 4 通りずつが入りますから，16 通り解説することになります．大変ですが，見ていきましょう．ただし，基本的には以下のことを押さえておけば大体わかります．
set は，写り先または写し元が 0 個以上
これは，set の説明で見たとおりです．図で表すと，以下のようになります．
なお，set は省略可能です．逆に言えば，m や n を指定しなければ，set として扱われます．
one は，写り先または写し元が 1 個
これは，one の説明で見たとおりです．図で表すと，以下のようになります．
lone は，写り先または写し元が 0 または 1 個
これは，one の説明で見たとおりです．図で表すと，以下のようになります．
some は，写り先または写し元が 1 個以上
これは，some の説明で見たとおりです．図で表すと，以下のようになります．
以下の説明は，これらの組み合わせに過ぎません．
結局は，"相手が hoge 個対応する" ということを押さえておけば OK です．
A set -> set B
A のインスタンスに対応する B のインスタンスがあるかもしれないし，複数あるかもしれない状況です．
つまり，制約がないということです．
言い換えると，A のインスタンスの集合と B のインスタンスの集合の直積の部分集合です．
A set -> one B
A の各インスタンスにちょうど 1 個の B のインスタンスが対応します．
言い換えると，A から B への関数です．
矢印でいうと，A のどのインスタンスからも矢印がちょうど 1 本出ている状況です．
A set -> lone B
A の各インスタンスに 1 個以下の B のインスタンスが対応します．
言い換えると，A から B への部分関数です．
矢印でいうと，A のどのインスタンスからも矢印が 1 本以下出ている状況です．
A set -> some B
A の各インスタンスに 1 個以上の B のインスタンスが対応します．
矢印でいうと，A のどのインスタンスからも矢印が 1 本以上出ている状況です．
A one -> set B
A の各インスタンスに対応する B のインスタンスがあるかもしれないし，複数あるかもしれない状況です．
逆に，B のインスタンスに対してちょうど 1 個の A のインスタンスが対応します．
言い換えると，B から A への写像の逆像です．
矢印でいうと，B のどのインスタンスもちょうど 1 本の矢印が入ってくるということです．
A one -> one B
A の各インスタンスにちょうど 1 個の B のインスタンスが対応し，
B の各インスタンスにちょうど 1 個の A のインスタンスが対応します．
言い換えると，A から B への全単射です．
当然，A のインスタンスの個数と B のインスタンスの個数が同じである必要があります．
矢印でいうと，A のどのインスタンスからもちょうど 1 個の矢印が出ていて，
B のどのインスタンスにもちょうど 1 個の矢印が入ってくる状況です．
A one -> lone B
A の各インスタンスに 1 個以下の B のインスタンスが対応し，
B の各インスタンスにちょうど 1 個の A のインスタンスが対応します．
言い換えると，B から A への単射の逆像です．
矢印でいうと，A のどのインスタンスからも 1 本以下の矢印が出ていて，B のどのインスタンスにも矢印が入ってくる状況です．
A one -> some B
A の各インスタンスに 1 個以上の B のインスタンスが対応し，
B の各インスタンスにちょうど 1 個の A のインスタンスが対応します．
言い換えると，B から A への全射の逆像です．
矢印でいうと，A のどのインスタンスからも 1 本以上矢印が出ていて，B にはちょうど 1 個の矢印が入ってくる状況です．
A lone -> set B
A の各インスタンスに対応する B のインスタンスがあるかもしれず，
B の各インスタンスに A のインスタンスが 1 個以下対応する状況です．
言い換えると，B から A への部分関数の逆像です．
矢印でいうと，B のどのインスタンスも 1 本以下の矢印が入っている状況です．
A lone -> one B
A の各インスタンスに対応する B のインスタンスがちょうど 1 個対応し，
B の各インスタンスに対応する A のインスタンスが 1 個以下対応する状況です．
言い換えると，A から B への単射です．
矢印でいうと，A のどのインスタンスからもちょうど 1 本の矢印が出ていて，
B のどのインスタンスにも 1 本以下の矢印が入っている状況です．
A lone -> lone B
A の各インスタンスに 1 個以下の B のインスタンスが対応し，
B の各インスタンスに対応する A のインスタンスが 1 個以下対応する状況です．
言い換えると，A から B への単射な部分関数です．
矢印でいうと，A, B のどのインスタンスもちょうど 1 個の矢印に対応している状況です．
学校内のカップルみたいな感じですね．
A lone -> some B
A の各インスタンスに 1 個以上の B のインスタンスが対応し，
B の各インスタンスに対応する A のインスタンスが 1 個以下対応する状況です．
言い換えると，B から A への全射な部分関数の逆像です．
A some -> set B
A の各インスタンスに対応する B のインスタンスがあるかもしれず，
B の各インスタンスに対応する A のインスタンスが 1 個以上対応する状況です．
言い換えると，A から B への全射な部分関数です．
A some -> one B
A の各インスタンスに対応する B のインスタンスがちょうど 1 個対応し，
B の各インスタンスに対応する A のインスタンスが 1 個以上対応する状況です．
言い換えると，A から B への全射です．
A some -> lone B
A の各インスタンスに対応する B のインスタンスが 1 個以下対応し，
B の各インスタンスに対応する A のインスタンスが 1 個以上対応する状況です．
言い換えると，A から B への全射な部分関数です．
A some -> some B
A の各インスタンスに対応する B のインスタンスが 1 個以上対応し，
B の各インスタンスに対応する A のインスタンスが 1 個以上対応する状況です．
言い換えると，A と B のタプルの集合のうち，A の全てのインスタンス，B の全てのインスタンスが含まれているものです．
判定表
実際に仕様を記述するときには，自分で重複度を書かないといけません．
関係 r: A m -> n B をどのように書けばいいかの判定方法は，以下のようになります．
n の決定
m の決定
最後に
すぐ忘れてしまいますが，よくよく考えるとそこまで難しくはないですね，
判定表は，サボりな自分用です……．
(A m -> n B) -> C については別記事で書こうと思います．
参考
非公式ドキュメントですが，基本的にはここを参照しています．
コメント