贋金パズルの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

fakecoin2.als

sig Coin {}

pred test[s, left, right, eq, lt, gt : set Coin] {
  no left & right
  #left = #right
  eq = s - (left + right)
  lt = s & left
  gt = s & right
}

pred final[s : set Coin] { lone s }

pred solve {
  some l, r, eq, lt, gt,
       eq_l, eq_r, eq_eq, eq_lt, eq_gt,
       lt_l, lt_r, lt_eq, lt_lt, lt_gt,
       gt_l, gt_r, gt_eq, gt_lt, gt_gt
       : set Coin {
    test[Coin, l, r, eq, lt, gt]
    test[eq, eq_l, eq_r,  eq_eq, eq_lt, eq_gt]
    test[lt, lt_l, lt_r,  lt_eq, lt_lt, lt_gt]
    test[gt, gt_l, gt_r,  gt_eq, gt_lt, gt_gt]
    final[eq_eq]
    final[eq_lt]
    final[eq_gt]
    final[lt_eq]
    final[lt_lt]
    final[lt_gt]
    final[gt_eq]
    final[gt_lt]
    final[gt_gt]
  }
}

run solve for 5 int, exactly 8 Coin

fakecoin3.als

sig Coin {}

sig State {
  disj left, right : set Coin, 
  eq, lt, gt : lone State,
  candidates : set Coin,
} {
  not this in this.^(@eq+@lt+@gt)
  not lone candidates => {
    #left = #right
    eq.@candidates = candidates - left - right
    lt.@candidates = candidates & left
    gt.@candidates = candidates & right

    -- optimization
    one eq
    one lt
    one gt
    some left
    left in candidates or right in candidates
  }
}

pred solve {
  one root : State {
    root.candidates = Coin
    no root.(eq+lt+gt).(eq+lt+gt).(eq+lt+gt) -- optimization
  }
}

run solve for 1 int, 13 State, exactly 9 Coin