# Fun with Alloy Model Checker

###
david karapetyan
*Updated on *
・4 min read

I'm trying to learn how to use and leverage the Alloy model checker in my day job and side projects but there doesn't seem to be much material in the way of basic examples for beginners. So to fill in those gaps here's the classic SEND + MORE = MONEY cryptarithmetic puzzle expressed as an Alloy model.

First we need to specify the objects we will be working with

```
// Non-negative numbers
abstract sig Num { val: Int } { val >= 0 && val <= 9 }
// Digits in SEND + MORE = MONEY
one sig S, E, N, D, M, O, R, Y extends Num { }
```

The objects we are working with are digits so we enumerate the digits and specify that there is only one instance of each digit (`one sig ...`

). We also specify that the value of each digit must be between 0 and 9 (`... { val >= 0 && val <= 9 }`

).

Next we specify a basic fact about the digits all being different

```
// Digits must all be different
fact {
all m, n : Num | m != n => n.val != m.val
}
```

There are also predicates and functions and we will get to those shortly. If we translate the above into plain english then we get the following statement: for every `m`

and `n`

that are numbers if `m`

does not equal `n`

then `m`

and `n`

must have different values.

That's pretty much it for the statement of the problem. With the basic specification in place we can now start expressing the constraints.

To specify `SEND + MORE = MONEY`

I'm going to define a function so that I don't have to type as much when expressing the constraints

```
// Function for computing the sum and the carry at the same time
fun sumCarry(a: Num, b: Num): (Int -> Int) {
let s = a.val + b.val |
s -> (s > 9 => 1 else 0)
}
```

The syntax is a little weird if you are used to programming languages. In Alloy `->`

means tuple. So in the above function we are computing the sum and carry and then returning it as a tuple. In more programmer friendly notation the above function could be written in pseudo code as

```
function sumCarry(a, b): (Int, Int) {
return (a + b, (a + b > 9) ? 1 : 0)
}
```

Now we can express the constraints of the puzzle

```
// Constraints for SEND + MORE = MONEY
fact {
M.val > 0
let YSumCarry = sumCarry[D, E],
ESumCarry = sumCarry[N, R],
NSumCarry = sumCarry[E, O],
OSumCarry = sumCarry[S, M] |
Y.val = rem[YSumCarry.univ, 10] &&
E.val = rem[plus[ESumCarry.univ, univ.YSumCarry], 10] &&
N.val = rem[plus[NSumCarry.univ, univ.ESumCarry], 10] &&
O.val = rem[plus[OSumCarry.univ, univ.NSumCarry], 10] &&
M.val = univ.OSumCarry
}
```

It's a little bit long but hopefully it should be obvious what is going on. We express the constraints of the sum in terms of the digits and then we specify what the values of the digits should be in terms of the sums and carries. Sit with it for a bit and it will make sense. It took me a while to understand why this works and if you are used to thinking imperatively then meditating on the above will help rewire your neurons to think more declaratively. It might help to try to translate the constraint into english. Here is a hint: it is the basic algorithm for doing sums that everyone learns in grade school.

The one part I probably have to explain is `univ.A`

and `A.univ`

syntax. Our `sumCarry`

functions returns a tuple of `(sum, carry)`

and we want to extract the first and second components of that tuple. Alloy has a weird way of expressing that using `univ`

which is the set of all atoms and is a keyword built into the language so it can't be reduced to other primitives in the language. By joining the universal set with our tuple we get the first and second components of the tuple we got from the function. The first component is `A.univ`

because joins in Alloy throw away the element being joined, i.e. `(a, b).(b, c) == (a, c)`

, and if the tuple only had 2 elements to begin with then joining with `univ`

leaves us with 1 element. By symmetry the the second element is `univ.A`

.

Everything up until this point has been setting up the constraints and in order to get a solution we must "run" the model for a predicate so we are going to use an empty predicate which from what I gathered is usually called "show"

```
pred show { }
run show for 5 Int
```

Again some more weird syntax here. That 5 in front of `Int`

specifies the bit width, which is another way of saying our signed integers have 5 bits (think about why 4 bits would not be enough when working with signed integers).

So everything all together now

```
// SEND + MORE = MONEY
// Non-negative numbers
abstract sig Num { val: Int } { val >= 0 && val <= 9 }
// Digits
one sig S, E, N, D, M, O, R, Y extends Num { }
// Digits must all be different and in 0..9
fact {
all m, n : Num | m != n => n.val != m.val
}
// Function for computing the sum and the carry at the same time
fun sumCarry(a: Num, b: Num): (Int -> Int) {
let s = a.val + b.val |
s -> (s > 9 => 1 else 0)
}
// Constraints for SEND + MORE = MONEY
fact {
M.val > 0
let YSumCarry = sumCarry[D, E],
ESumCarry = sumCarry[N, R],
NSumCarry = sumCarry[E, O],
OSumCarry = sumCarry[S, M] |
Y.val = rem[YSumCarry.univ, 10] &&
E.val = rem[plus[ESumCarry.univ, univ.YSumCarry], 10] &&
N.val = rem[plus[NSumCarry.univ, univ.ESumCarry], 10] &&
O.val = rem[plus[OSumCarry.univ, univ.NSumCarry], 10] &&
M.val = univ.OSumCarry
}
pred show { }
run show for 5 Int
```

Running the example and getting the solution is left as an exercise for the reader.

Wow, I did not know Alloy. This is a nice example, I'm learning a bit with it! Thanks!

Cool. Glad you like it. I wrote up a few more after I wrote this one: dev.to/davidk01/solving-8-queens-p..., dev.to/davidk01/some-more-fun-with....