stackoverflow（および google group alloytools）より。
簡単なパズルですが、条件に合うものがいくつあるか数える練習として役立つかもしれません。
..と思っていたら、意外に深い。
問題
英語のまま画像直リンですが
リスト
One とか Two とかなので、数をどう数えるか。
そして問題とコードを照らし合わせやすいこと。
その２つに気を使ってみました。
＃4/2追記：同値を含むケースを正しく判定できるようにしたら少し読みづらくなってしまった..（修正理由は「自分で書いてみた方へ」を参照）
// https://stackoverflow.com/questions/60951163/lock-challenge-in-alloy
one sig Lock {code1,code2,code3:Int} {
code1+code2+code3 in 0+1+2+3+4+5+6+7+8+9
}
enum Marker { C1,C2,C3 }
pred hint[c1,c2,c3, matched,wellPlaced : Int] {
let codeDigits = Lock.(code1+code2+code3) |
matched = #(
(c1 in codeDigits => C1 else none) +
(c2 in codeDigits => C2 else none) +
(c3 in codeDigits => C3 else none)
)
wellPlaced = #(
(c1=Lock.code1 => C1 else none) +
(c2=Lock.code2 => C2 else none) +
(c3=Lock.code3 => C3 else none)
)
}
run {
hint[6,8,2, 1,1]
hint[6,1,4, 1,0]
hint[2,0,6, 2,0]
hint[7,3,8, 0,0]
hint[7,8,0, 1,0]
} for 5 int
結果
┌─────────┬─────┬─────┬─────┐
│this/Lock│code1│code2│code3│
├─────────┼─────┼─────┼─────┤
│Lock⁰ │0 │4 │2 │
└─────────┴─────┴─────┴─────┘
別の解法
Peter Kriens 氏の解を少し（correct[]の同値ケース対応だけ）修正させてもらって紹介します。
忘れていた視点や、私がこれまで得られなかった書き方などが満載された、さすがエキスパートと思わされるショートコードでした。
let sq[a,b,c] = 0->a + 1->b + 2->c
let digit = { n : Int | n>=0 and n <10 }
fun correct[ lck : seq digit, a, b, c : digit ] : Int { # (lck.~(sq[a,b,c])) }
fun wellPlaced[ lck : seq digit, a, b, c : digit ] : Int { # (lck & sq[a,b,c]) }
pred lock[ a, b, c : digit ] {
let lck = sq[a,b,c] {
1 = correct[ lck, 6,8,2] and 1 = wellPlaced[ lck, 6,8,2]
1 = correct[ lck, 6,1,4] and 0 = wellPlaced[ lck, 6,1,4]
2 = correct[ lck, 2,0,6] and 0 = wellPlaced[ lck, 2,0,6]
0 = correct[ lck, 7,3,8]
1 = correct[ lck, 7,8,0] and 0 = wellPlaced[ lck, 7,8,0]
}
}
run lock for 5 Int
sigを使わない例なので、結果はTextViewで見ます。
---INSTANCE---
integers={-16, -15, -14, -13, -12, -11, -10, -9, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15}
univ={-1, -10, -11, -12, -13, -14, -15, -16, -2, -3, -4, -5, -6, -7, -8, -9, 0, 1, 10, 11, 12, 13, 14, 15, 2, 3, 4, 5, 6, 7, 8, 9, Univ$0}
Int={-1, -10, -11, -12, -13, -14, -15, -16, -2, -3, -4, -5, -6, -7, -8, -9, 0, 1, 10, 11, 12, 13, 14, 15, 2, 3, 4, 5, 6, 7, 8, 9}
seq/Int={0, 1, 2, 3}
String={}
none={}
this/Univ={Univ$0}
skolem $lock_a={0}
skolem $lock_b={4}
skolem $lock_c={2}
自分で書いてみた方へ
この問題の正解(0,4,2)を導き出して「よしこれで完成」と思ったら、その解法が汎用的なものか確認してみましょう。
ここにもう一つ別の錠があります。
同じやり方で解けないとしたら、その解法は十分とは言えないかもしれません。
- Hint1: (1,2,3) - Nothing is correct.
- Hint2: (4,5,6) - Nothing is correct.
- Hint3: (7,8,9) - One number is correct but wrong placed.
- Hint4: (9,0,0) - All numbers are correct, with one well placed.
補足
TLA+など他の形式手法でもハマりやすいところですが、今回の correct[] のように「マッチするのは何件か」を数えたいとき集合を使いがちです。
しかし集合は同値を複数持たないので、例えば正解が (4,1,2) のところに (1,1,1) を入れた場合に集合でマッチさせようとすると{1,2,4} AND {1} = {1}で１件という結果になってしまいます。
＃英語の感覚に自信がないけれど、(5,5,5)に(5,5,5)と入力しても "One number is correct and (all) well placed." と数えるのは正しくなさそうに思う。
普通のプログラミング言語なら配列や正規表現を使うところを、Alloyでどう記述したらいいか、いい練習になりました。
参考
- stackoverflow : Lock Challenge in Alloy