Alloyで論理パズルを解いてみる その3

7人の写真.als

//問題:
//男の子3人(与之助、一平、大介)、
//女の子4人(めぐみ、ゆかり、まどか、みゆき)
//の7人の園児が並んで写真を撮ることになった。
//このうちの4人が次のような注文をつけた。
//
// 与之助 「両隣は女の子がいい」
// 一平   「女の子の隣はいや」
// めぐみ 「ゆかりの隣がいい」
// まどか 「右端がいい」
//
//これらの注文がすべて叶ったとすると、左端にいたのは誰？
//
// 出典: 新作論理パズル77 小野田 博一
enum 性別 {男の子, 女の子}

abstract sig 園児 {
   の性別: one 性別,
   の右隣: lone 園児,
   の左隣: lone 園児	 
}

fact 左端 {
   one c: 園児 | (no c.の左隣 && one c.の右隣 )
}

fact 右端 {
   one c: 園児 | (one c.の左隣 && no c.の右隣)
}

fact 自分は自分の隣になれない {
   no c: 園児 | c = c.の左隣
   no c: 園児 | c = c.の右隣
}

fact 隣の人の隣は自分 {
   all c: 園児 | one c.の左隣 => c.の左隣.の右隣 = c
   all c: 園児 | one c.の右隣 => c.の右隣.の左隣 = c
}

fact 同じ人が両隣にいることはない {
   all c: 園児 | c.の左隣 != c.の右隣
}

fact 全員横一列に並んでいる { //循環しない
   no c: 園児 | c in c.^の左隣
   no c: 園児 | c in c.^の右隣
}

one sig 与之助, 一平, 大介 extends 園児 {}
{ の性別 = 男の子}

one sig めぐみ, ゆかり, まどか, みゆき extends 園児 {}
{ の性別 = 女の子}

fact 与之助の要求 {
   one 与之助.の左隣
   one 与之助.の右隣
   all c: {与之助.の左隣 + 与之助.の右隣} | c.の性別 = 女の子
}

fact 一平の要求 {
   all c: {一平.の左隣 + 一平.の右隣} | c.の性別 = 男の子
}

fact めぐみの要求 {
   ゆかり in {めぐみ.の左隣 + めぐみ.の右隣}
}

fact まどかの要求 {
   no まどか.の右隣
}

pred show {}
run show

util/orderingを使えば、もちっと楽に書けるのかな？