Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
贋金パズルのAlloyモデル
// 失敗版
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
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
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment