# Solving the peg game with TLA+

# Introduction

In this post, I’ll use TLA+, which is a *formal specification language based on temporal logic*, to solve an old favorite of mine: the “Cracker Barrel peg game”.

# The Peg Game

This game is also formally known as triangular peg solitaire. And, according to Wikipedia, the game mechanics work as follows:

The standard game fills the entire board with pegs except for the central hole. The objective is, making valid moves, to empty the entire board except for a solitary peg in the central hole. A valid move is to jump a peg orthogonally over an adjacent peg into a hole two positions away and then to remove the jumped peg.

So, where does TLA+ come in?

# The TLA+ specification

In order to solve a problem with TLA+, what we really do is *specify* the rules of the system—a TLA+ “program” is called a *specification*. So, we’ll be specifying the rules of the peg game, and with TLA+ we do this using set theory and temporal logic.

Once we model/specify the game, we can ask TLA+ any question about the game we want, and it will answer it for us. For example: *“how many possible unique peg-game possibilities are there?”*, or *“is it possible to, after 12 moves, end a game with only the pegs (1,1) and (1,5) remaining?”*. The question we’ll be asking is *“what steps should we take to win?*.

Before we design our specification, let’s clarify some TLA+ fundamentals.

There are excellent TLA+ tutorials online but I’ll recap, really quick, the minimum you need to know to understand the specification I’ve provided.

TLA+ is based on temporal logic. To put it briefly, this means you are modelling the system as a cyclic graph of *states* using set theory, where each *state* is simply a mapping of variables to values, and states transition between each other according to mathematical functions based heavily on set theory.

For a minimal TLA+ specification, you should expect to define one or more variables, one or more functions, a special `Init`

function, and a special `Next`

function.

For example, in the diagram shown above, each node represents a state, and the edges represent transitions between states. To be exact, it could be described as follows:

```
VARIABLES x
Init == x=1
Next == (x'=x+5 ∨ x'=x*3)
```

To elaborate:

**Variables**: These have a single value at any given step, but may change from one step to the next (in accordance with the`Init`

and`Next`

functions). They’re defined in a single header, e.g.,`VARIABLES x, y, z, etc`

.**Functions**: These naturally close over all variables, can optionally take one or more arguments, and return a single value. (Defined using`==`

, e.g.,`f == x+y+z`

or`g(n) == x+n`

.): This is a`Init`

*special*function (which happens to be a predicate—a boolean function) which defines what the*initial state(s)*of the system are. Any set of (variable→value) mappings which causes this function to return`True`

will be included as an initial state. For example,`Init == x=1`

means the initial state(s) are any state(s) where`x`

equals`1`

—in this case there is only one state (`x=1`

) for which this resolves to`True`

, so there is only one initial state. (In contrast, if we would have used`Init == x*x=4`

, there would be two initial states:`x=-2`

and`x=2`

.): This is a`Next`

*special*function/predicate which, given any state, defines what the*next state(s)*of the system are. The`'`

suffix should be read as “next state of”. For example,`Next == x'=x+1`

means the next state(s) are those where the next value of`x`

is the previous value of`x`

plus`1`

. In the example given above,`Next == (x'=x+5 ∨ x'=x*3)`

means the next state(s) are those where the next value of`x`

is the previous value of`x`

plus`5`

,*or*, where the next value of`x`

is the previous value of`x`

times`3`

. (Note how there can be a varying number of`Init`

and`Next`

states!)

Now that we’ve clarified some TLA+ fundamentals, let’s get back to ~~coding~~ specifying the peg game!

Again, we need to model the peg game according to the rules we described earlier. First, we’ll refer to each hole as a “spot”, and give each spot a number (well, an ordered pair of numbers). This means we have this list of all possible “Spots”. We’ll need to tell TLA+ that.

We can define a function named `Spots`

, which returns the entire list of spots, like so:

```
Spots == { <<x,y>> \in {1,2,3,4,5}\X{1,2,3,4,5} : x+y<=6 }
```

…or, alternatively…

```
Spots == { <<x,y>> ∈ {1,2,3,4,5}⨯{1,2,3,4,5} : x+y<=6 }
```

This can be read as “`Spots`

equals the set of all (x,y) combinations where x∈{1,2,3,4,5}, y∈{1,2,3,4,5}, and x+y<=6”. This is just a shorter way of writing `Spots == [(1,1),(1,2),(1,3),(1,4),(1,5),(2,1),(2,2),(2,3),(2,4),(3,1),(3,2),(3,3),(4,1),(4,2),(5,1)]`

.

`Spots`

doesn’t change from turn to turn. Though we’ve defined it as a function, you can think of it as constant. But not all of our values are constant: in *any* turn-based game, there is always the concept of a *current state*, which changes after each turn. And in our game, the current state is fairly simple: it can be summarized by the subset of `Spots`

which have currently have pegs. Since this state will change from turn to turn, we’ll put it in a TLA+ *variable*. We can simply create a single variable, called `state`

:

```
VARIABLES state
```

(Please be aware that, in general, “the state” refers collectively to the current values of all variables. But, in this case, we only have one single variable, so we’ve simply named it `state`

, but we could have named it, for example, `activepegs`

.)

According to the official peg game rules, the initial state of the board will be when all `Spots`

are filled except for `(3,2)`

.

We can declare that with the following:

```
Init == (state = Spots \ { <<3,2>> })
```

(Note that `A \ B`

denotes logical relative complement, i.e., “all elements in the set A but not B”.)

As I explained earlier, `Init`

is a special function in TLA+, and is called the *initial state function* (or *initial state predicate*). It may be confusing that I’m setting `Init`

“equal” the result of another equation, so I’ll offer a different perspective: with this line, don’t think of it as “defining” or “assigning” the `Init`

condition to this expression, think of it as *constraining* the initial possible values of all of our variables. In our case, we happen have a single variable, and we happen to be locking it down to one single value.

Now that we’ve defined the initial state of the game, we’ll need to talk about how to move pegs around. For example, during our first move from the starting state, we only have two ways to get to the next state:

- Move
`(1,2)`

up-right to`(3,2)`

, or - Move
`(4,1)`

up-left to`(3,2)`

I already explained how “next states” work, but I’ll say it again: in TLA+, we model state changes by *specifying the mathematical relationship between the current state of our variables (in this case, just state) and the next state of our variables (state')*. Remember that TLA+ will recognize the

`'`

suffix of `state'`

to mean “the next value of state”.Formally, we can specify what constitutes a valid next state with the `Next`

condition:

This probably looks intimidating. A quick guide to the symbols:

`<<x,y>>`

means “the ordered pair`(x,y)`

”`∃ e ∈ s : p`

means “there exists an element`e`

from the set`s`

where`p`

is true”`∧`

means “and”`∨`

means “or”

Also, I’ve snuck in several (related) functions (not defined yet) which really boil down to following two, except all in different directions:

`CanJumpUpRight(x,y)`

will true if, in the board’s current`state`

, there is a peg at position`(x,y)`

, and it’s allowed to jump*up-right*according to the peg game rules.`JumpUpRight(x,y)`

will return the set of pegs which*will*be left on the board if we*do*choose to jump*up-right*from the current`state`

. (Note that it doesn’t actually*do*anything, because it’s just a function!)

And if we fully translate the above definition of `Next`

to english, it reads:

A next

`state`

(`state'`

) is a valid next move from the current`state`

if and only if there exists some`(x,y)`

spot in the current`state`

which CAN jump in some direction (UpRight, DownLeft, etc.) , and also, the next state is the result of jumping in that direction.

Here are the complete definitions of each “CanJump” and “Jump” function:

The game is now mostly specified, but we yet defined yet what it means to “win”. We’ll want to define a function that returns true if the current `state`

is in a winning position. For this game, it’s pretty simple: if there’s only one peg left, we’ve won:

```
Win == Cardinality(state) = 1
```

(The `Cardinality`

function is a built-in TLA+ function which counts how many elements are in a set.)

To “ask” TLA+ to find a winning state, we can use the TLA+ toolbox’s “model checker”:

What I’ve done here is asked TLA+, “Please verify that there are no winning states; i.e., for all states, `Win`

is always `False`

.” It found that this is false, and gave evidence.

The complete source code can be found on GitHub.

(Note that, if you read the source code, you’ll notice that I’ve added additional variables: `xx`

, `yy`

, and `dd`

. This is essentially a hack to get TLA+ to print out the entire history of states, rather than just the final, winning state. There are probably better ways to do this, but this works!)