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 については別記事で書こうと思います.
参考
非公式ドキュメントですが,基本的にはここを参照しています.
コメント