2013-07-09

モデリング検査ツール Alloy Analyzer を使いたい！のエントリ。第四回目です。

今回は Many to Many をモデリングしてみます。
映画エンティティと出演者エンティティの関係づけ。

通常、RDB上で実現される Many to Many は、中間テーブルを使いますね。
こんな感じ。

これをAlloyで表現すると、以下のようになりました。

Many to Many with 中間テーブル

module movies_and_actors
sig Movie {
  mv_act: set MoviesActors
}
sig Actor {
  act_mv: set MoviesActors
}
sig MoviesActors {
  actor: one Actor,
  movie: one Movie
}
fact { 
  // 反転（対応）関係
  Movie <: mv_act = ~(MoviesActors <: movie)
  Actor <: act_mv = ~(MoviesActors <: actor)
  // 中間テーブルが作り出す関連は、互いに素（ふたつのカラムによるユニーク制約）
  all disj ms, ms': MoviesActors | ms.(movie + actor) != ms'.(movie + actor)
}
run {} for 5

描画されたダイアグラムを見てみましょう。

期待通りの Many to Many になっているようです。

この、中間テーブル上でのユニーク制約を実現する fact

all disj ms, ms': MoviesActors | ms.(movie + actor) != ms'.(movie + actor)

を、自然言語で表現すると
「どの異なる2つのMoviesActorsインスタンスをとっても、
そのインスタンスの持つ movie と actor の組み合わせは、同値ではない。」
ってところかな。
このfactはかなり試行錯誤しました。が、最終的には、わりと一般的な書き方になっているし、間違ってないと思うんですが、どうでしょうか。

なお、このままだと、Actor と Movie を直接辿ることができないので、
中間テーブルをスキップするショートカット・パスを書き足してみます。

module movies_and_actors
sig Movie {
  actors: set Actor,
  mv_act: set MoviesActors
} {
  // ショートカット 
  actors = mv_act.actor 
}
sig Actor {
  movies: set Movie,
  act_mv: set MoviesActors
} { 
  // ショートカット 
  movies = act_mv.movie 
}
sig MoviesActors {
  actor: one Actor,
  movie: one Movie
}
fact { 
  // 反転（対応）関係
  Movie <: mv_act = ~(MoviesActors <: movie)
  Actor <: act_mv = ~(MoviesActors <: actor)
  // 中間テーブルが作り出す関連は、互いに素（ふたつのカラムによるユニーク制約）
  all disj ms, ms': MoviesActors | ms.(movie + actor) != ms'.(movie + actor)
}
run {}