カロタンパズル in Alloy

kalotan.als

abstract sig カロタン {
  性別: 男か女か,
  発言1: Prop,
  発言2: lone Prop
}
{
  // 男なら常に真実を語る
  性別 in 男性 => 発言1.真偽 in ホント and (some 発言2 =>発言2.真偽 in ホント)
  // 女はどっちかホントでどっちかがウソ
  else some 発言2 => 発言1.真偽 != 発言2.真偽
}
enum 男か女か { 男性, 女性 }

one sig キビ extends カロタン {}
{
  // 自分を男といったか、女といったかのどちらか
  発言1 in キビは男の子 + キビは女の子
  no 発言2
}
one sig 親A extends カロタン {}
{
  発言1 in キビは男の子と言っている
  no 発言2
}
one sig 親B extends カロタン {}
{
  発言1 in キビは女の子
  some 発言2
  発言2 in キビはウソをついている
}

fact 親の性別はたぶん別々 {
  親A.性別 != 親B.性別
}

/** 皆さんの発言（命題）*/
abstract sig Prop {
  真偽: ホントかウソか
}
enum ホントかウソか { ウソ, ホント }

one sig キビは男の子 extends Prop {}
{
  真偽 in ホント <=> キビ.性別 in 男性
}

one sig キビは女の子 extends Prop {}
{
 真偽 in ホント <=> キビ.性別 in 女性
}

one sig キビは男の子と言っている extends Prop {}
{
  真偽 in ホント <=> キビ.発言1 in キビは男の子
}
one sig キビはウソをついている extends Prop {}
{
  真偽 in ホント <=> キビ.発言1.@真偽 in ウソ
}

run {  }