Search code examples
alloy

Lock Challenge in Alloy

I would like to solve the following lock challenge using Alloy.

My main issue is how to model the integers representing the digit keys.

I created a quick draft:

sig Digit, Position{}

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

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

In this context, could you please:

  • tell me if Alloy seems to you suitable to solve this kind of problem?
  • give me some pointers regarding the way I could model the key digits (without using Ints)?

Thank you.

enter image description here

Solution

  • Yes, I think Alloy is suitable for this kind of problem.

    Regarding digits, you don't need integers at all: in fact, it is a bit irrelevant for this particular purpose if they are digits or any set of 10 different identifiers (no arithmetic is performed with them). You can use singleton signatures to declare the digits, all extending signature Digit, which should be marked as abstract. Something like:

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

    A similar strategy can be used to declare the three different positions of the lock. And btw since you have exactly one lock you can also declare Lock as singleton signature.