alloy exercise for a puzzle

puzzle_1.alloy

enum Cap { Black, White }

abstract sig Children {
  cap:    one Cap,
  visible: set Children
  }

one sig A extends Children {} {
  visible = none
  cap = Black
  }
one sig B extends Children {} {
  visible = none
  cap = White
  }
one sig C extends Children {} {
  visible = B
  cap = Black
  }
one sig D extends Children {} {
  visible = B + C
  cap = White
  }

fact {
  #cap.Black = 2 and #cap.White = 2
  }

pred CanAnswer(c: Children) {
  #(c.visible :>cap.Black) = 2 or #(c.visible :> cap.White) = 2
  }

run {
  no c: Children | CanAnswer [c]
}

puzzle_2.alloy

// 帽子の色
enum Cap { Black, White }

abstract sig Children {
  cap:    one Cap,        // かぶっている帽子の色
  visible: set Children   // 見える他の子供
  }

// A, B, C, D の条件
one sig A extends Children {} {
  visible = none
  cap = Black
  }
one sig B extends Children {} {
  visible = none
  cap = White
  }
one sig C extends Children {} {
  visible = B
  cap = Black
  }
one sig D extends Children {} {
  visible = B + C
  cap = White
  }

fact {
  #cap.Black = 2 and #cap.White = 2
  }

// c の帽子の色の合計のいずれかが num なら真
pred CountCapNumber (c: Children, num: Int) {
  #c :> cap.Black = num or #c :> cap.White = num
  }

// 前をみた瞬間に答えられるか
pred すぐに回答できる (c: Children) {
  CountCapNumber [c.visible, 2]
  }

// 他の子の回答(ができないこと)を待って答えられるか
pred 少しして回答できる (c: Children) {
  // すぐに回答する子はいない
  no a: Children | すぐに回答できる [a]
  // 答えられない誰かが自分を見ているなら、共通して見える子の帽子の色が
  // 1=(2-1)なら回答できる
  some a: Children | c in a.visible and CountCapNumber [c.visible & a.visible, 1]
  }

pred 回答できる {
  some c: Children |
    すぐに回答できる [c] or 少しして回答できる [c]
  }

run 回答できる