金星人の男と火星人の女は常に本当のことだけを云い、金星人の女と火星人の男は常に嘘を吐く。一発で男か女かを見分けることのできる、「はい」か「いいえ」で答えられる質問は何か？

marsandvenus.als

module marsandvenus

enum 惑星 {火星, 金星}
enum 男か女 {男, 女}
enum 真理値 {真, 偽}

sig 質問 {
	評価: 人間 -> one 真理値
}

abstract sig 人間 {
  性別: 男か女,
  出身: 惑星,
	回答: 質問 -> one 真理値
} {
	all q : 質問 |
		((性別 = 男 and 出身 = 金星) or (性別 = 女 and 出身 = 火星)) <=> 回答[q] = q.評価[this]
}

one sig 金星人の男 extends 人間 {} {
	性別 in 男
	出身 in 金星
}

one sig 金星人の女 extends 人間 {} {
	性別 in 女
	出身 in 金星
}

one sig 火星人の男 extends 人間 {} {
	性別 in 男
	出身 in 火星
}

one sig 火星人の女 extends 人間 {} {
	性別 in 女
	出身 in 火星
}

pred 女性発見器(何か: 質問) {
	all 誰か: 人間 | 誰か.性別 in 女 <=> (誰か.回答[何か] = 真)
}

run 女性発見器