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

密猟者.als

//問題:
//天然記念物であるノグチゲラの生息する森で不審な4人の男を見つけた。
//野生保護官の質問に対して4人は以下のように答えた。
//
// 赤シャツの男 「私たちは密猟をしているのではありません」
// 灰シャツの男 「私たちは銃を持っていません」
// 青シャツの男 「私たちはノグチゲラが何か知りません」
// 白シャツの男 「灰シャツの男の言ってることはウソです」
//
// 4人の中で本当のことを言ってるのは一人だけだった。
// 4人は密猟者か？
//
// 出典: 新作論理パズル77 小野田 博一
enum 目的 {密猟ではない, 密猟である}
enum 発言の真偽 {嘘, 本当}
enum 銃の所持 {持っている, 持っていない}
enum ノグチゲラの知識 {知っている, 知らない}

abstract sig 不審な男 {
  の目的: one 目的,
  の発言が: one 発言の真偽,
  は銃を: one 銃の所持,
  はノグチゲラを: one ノグチゲラの知識
}

one sig 赤シャツ, 灰シャツ, 青シャツ, 白シャツ extends 不審な男 {}

fact 目的は全員一緒 {
   all p, p': 不審な男 | p.の目的 = p'.の目的
}

fact 本当のことを言ってるのはひとりだけ {
  one p: 不審な男 | p.の発言が = 本当
}

fact 赤シャツの発言 {
  赤シャツ.の発言が = 本当 <=> (all p: 不審な男 | p.の目的 = 密猟ではない)	
}

fact 灰シャツの発言 {
  灰シャツ.の発言が = 本当 <=> (all p: 不審な男 | p.は銃を = 持っていない)
}

fact 青シャツの発言 {
  青シャツ.の発言が = 本当 <=> (all p: 不審な男 | p.はノグチゲラを = 知らない)
}

fact 白シャツの発言 {
  白シャツ.の発言が = 本当 <=> (灰シャツ.の発言が = 嘘)
}

//assert 密猟者ではない {
//  all p: 不審な男 | p.の目的 = 密猟ではない
//}
//check 密猟者ではない

assert 密猟者だ {
  all p: 不審な男 | p.の目的 = 密猟である
}
check 密猟者だ