贋金パズルのAlloyモデル

fakecoin.als

sig Coin {}

abstract sig State {
  candidates : set Coin,
}

sig Branch extends State {
  left, right : set Coin, 
  eq, lt, gt : State
}
fact {
  all b : Branch {
    not b in b.^(eq+lt+gt)
    no b.left & b.right
    #b.left = #b.right
    b.eq.candidates = b.candidates - (b.left + b.right)
    b.lt.candidates = b.candidates & b.left
    b.gt.candidates = b.candidates & b.right
  }
}

sig Leaf extends State { }
{ lone candidates }

pred solve {
  one root : State {
    root.candidates = Coin
    State in root.*(eq+lt+gt)
  } 
}
run solve for 5 int, 4 Branch, 9 Leaf,  exactly 8 Coin

gistfile2.txt