Alloy Analyzer でOrphan Removal（を、もういちど。）

Alloy Analyzer Alloy for RDB

前回、写真共有サービスを想定して、@OneToMany(orphanRemoval=true) な
エンティティ群を定義してみました。その書き直し版です。

前回は、「状態をあらわすsig」を、書くと言っておきながら、
操作対象のインスタンス（=削除するUserとPhoto）のことだけを考えていました。
しかし、本来「状態」とは、操作対象でないインスタンスも含めて
（=RDBでいうと、関係するテーブルのレコードぜんぶ）表現していないと
いけないのでは思い直し、書き直しました。

module orphanRemoval
/* 基本のエンティティ ======================================================= */
sig User {
  photos: set Photo
}
sig Photo {
  owner: one User
}
// 所有者のいないPhotoは無い
fact {
  photos = ~owner
}
/* 状態管理用エンティティ =================================================== */
/*
■User削除前
*/
one sig PhotoRel_RightS {
  u: set User,
  p: some Photo,
  rel: p -> u
} {
  rel = p <: owner
}
fact {
  // ※このsigのフィールドはすべてのインスタンスを扱っていること
  all everyUser:User, everyPhoto:Photo, s:PhotoRel_RightS | 
    (everyUser in s.u) && (everyPhoto in s.p)
}
/*
■UserのPhotoだけ削除完了
*/ 
one sig PhotoRel_OrphanRemovedS { 
  delUser: set User,
  u'': set User,
  p'': some Photo,
  rel'': p'' some -> (u'' - delUser)
} { 
  rel'' = p'' <: owner
  // ※Photoを限定：deluserのphotsは無い。
  p'' = (u'' - delUser).photos
}
fact {
  all 
    before:PhotoRel_RightS, 
    process:PhotoRel_OrphanRemovedS, 
    after:PhotoRel_AllRemovedS | 
      // ※delUserを限定
      process.delUser = before.u - after.u' && 
        // ※Userを限定
        (process.u'' = before.u) 
}
/*
■User/Photo削除後
*/
one sig PhotoRel_AllRemovedS {
  u': some User,
  p': some Photo,
  rel': p' -> u'
} {
  rel' = p' <: owner
  // ※Photoを限定
  p' = u'.photos
}
fact {
  // ※Userを限定：削除されたUserが必ず存在すること
  all before:PhotoRel_RightS, after:PhotoRel_AllRemovedS | 
    (before.u - after.u') != none
}

エンティティの sigと、状態を表す sig 、そして、それらにまつわる fact はこんな感じです。
状態を表す sig は、より厳密になったと思います。

そして、削除の振る舞いの表現は、以下のようにしました。
各状態が持つ、Photo -> User 型フィールド同士を比較すればいいはずです。

/* 振る舞いの表現 =========================================================== */
/*
▼各状態のrelを比較して判定。
*/
pred deleteUser(
  rightS: PhotoRel_RightS, 
  orphanRemovedS: PhotoRel_OrphanRemovedS, 
  allRemovedS: PhotoRel_AllRemovedS, 
  userDeleted: User
) {
  after_OrphanRemoved[rightS, orphanRemovedS] and
  after_AllRemoved[rightS, allRemovedS, userDeleted]
}
pred after_OrphanRemoved(
  rightS'': PhotoRel_RightS, 
  orphanRemovedS'': PhotoRel_OrphanRemovedS
) {
  rightS''.rel - orphanRemovedS''.rel'' = orphanRemovedS''.delUser.photos <: owner
}
pred after_AllRemoved(
  rightS': PhotoRel_RightS, 
  allRemovedS': PhotoRel_AllRemovedS,
  userDeleted': User
) {
  rightS'.rel - allRemovedS'.rel' = userDeleted'.photos <: owner
}

/* 振る舞いのcheck ========================================================== */
check deleteUser {
  all user: User, 
    rightS: PhotoRel_RightS, 
    orphanRemovedS: PhotoRel_OrphanRemovedS, 	
    allRemovedS: PhotoRel_AllRemovedS | 
      // ※削除するUserを事後条件から特定 
      // TODO: これの else はどう表現するべきなのか？
      user = rightS.u - allRemovedS.u implies
        deleteUser[rightS, orphanRemovedS, allRemovedS, user]
}

事前状態 PhotoRel_RightS にも、事後状態 PhotoRel_AllRemovedS にも、
削除する（した）Userを特定する情報がありません。
それが正しいのかどうかわからないんですが、結果的にそうなりました。
この問題は、両者の差分（rightS.u - allRemovedS.u）をとることで、簡単に解決できるわけですが、
プログラマーの思考には、なんかしっくりこないやり方です。
事後の状態にあわせて引数を定義する・・・？
じゃあその定義外の引数については、どう考えたらいいんだろう？
あるいは、この定義に合わない「状態」（の組み合わせ）のほうを、除外していることになるんだろうか。
でもそれだったら、factで表現すべきだよな・・・？

そして前回同様、「状態をあらわすsig」の記述には手こずりました。
「状態」と、ひとくちに言っても、そこには、エンティティと/フィールドと/制約/
の三者が絡むという複雑さがあるので、alloyの要領に慣れないうちは、
このように手こずるんだと思います。ただ、正しく書ければ、それがビジュアルに
検証できるというありがたさがあるので、それを信じて今後も頑張る。

それにしても、たった一対のOneToMany（OneToOne）を表現するだけでもこの記述量とは・・・
とてもじゃありませんが、一般的なWEB＋RDBのシステム開発現場で、
普段づかい出来るような代物ではありません。

これらの一連の制約の記述、自動生成できないかな。DSL的に。
alloy言語そのものを拡張するか、あるいは、
alloy4eclipse のように、IDEのプラットフォームに乗っかって、
コードスニペットとして自動生成するツールを作るか、、、

面倒なものに手を出してしまった。。。