合金中的锁挑战

Question

我想用下列锁定挑战解决合金问题。

我的主要问题是如何建模表示数字键的整数。

我创建了一个快速草稿：

sig Digit, Position{}

sig Lock {
 d: Digit one -> lone Position
}

run {} for exactly 1 Lock, exactly 3 Position, 10 Digit

在这方面，请你：

• 告诉我合金在你看来是否适合解决这类问题？
• 请给我一些提示，说明我可以如何建模密钥位(而不使用Ints)？

谢谢。

​

​

Answer 1

是的，我认为合金适合这种问题。

关于数字，您根本不需要整数:实际上，如果它们是数字或由10个不同标识符组成的任何一组(不对它们执行算术)，则与此特定用途有点无关。您可以使用单例签名来声明数字，所有扩展签名Digit都应该标记为abstract。类似于：

abstract sig Digit {}
one sig Zero, One, ..., Nine extends Digit {}

可以使用类似的策略来声明锁的三个不同位置。另外，由于您只有一个锁，所以也可以声明Lock为单例签名。

Answer 2

一个简单的开始方式，你并不总是需要sig的解决方案。找到的解决方案可能不是预期的解决方案，但这是因为需求含糊不清，采取了一条捷径。

pred lock[ a,b,c : Int ] {
    a=6 || b=8 || c= 2
    a in 1+4 || b in 6+4 || c in 6+1
    a in 0+6 || b in 2+6 || c in 2+0
    a != 7 && b != 3 && c != 8
    a = 7 || b=8 || c=0 
}

run lock for 6 int

在文本视图中查找答案。

我们讨论了合金列表，我想用一个更易读的版本来修改我的解决方案：

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    { # (Int.lck & (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 6 Int

Answer 3

我这个拼图的框架是：

enum Digit { N0,N1,N2,N3,N4,N5,N6,N7,N8,N9 }
one sig Code {a,b,c:Digit}

pred hint(h1,h2,h3:Digit, matched,wellPlaced:Int) {
    matched = #(XXXX)        // fix XXXX
    wellPlaced = #(XXXX)     // fix XXXX
}

fact {
    hint[N6,N8,N2, 1,1]
    hint[N6,N1,N4, 1,0]
    hint[N2,N0,N6, 2,0]
    hint[N7,N3,N8, 0,0]
    hint[N7,N8,N0, 1,0]
}

run {}