Introduction to Modeling (Part 2, Transitions)

The livecode is here.

Logistics

The first lab starts today! The starter model is a variant of the livecode that we produced in class. It also contains a possible version of the move predicate we started writing.

Please keep Forge updated. You'll want to update it for the lab, today.

Project Showcase

Here are a few examples of the sort of thing you'll be able to model in Forge. Of course, these don't cover all possibilities! But they should give you an idea of what you might aim for.

Games and Puzzles

Uno™
(Noah Atanda, Madison Lease, and Priyanka Solanky)

Texas Hold 'em
(Matthew Boranian and Austin Lang)

Triple Triad
(Nick Bottone, Sebastien Jean-Pierre, and Robert Murray)

Programming Language Concepts

Rust Lifetimes and Borrowing
(Thomas Castleman and Ria Rajesh)

Security Concepts

Cryptographic Protocols
(Abigail Siegel and Mia Santomauro)

Networks and Distributed Systems

Network Reachability
(Tim Nelson and Pamela Zave, for the Formal Methods Summer School)

Where We Left Off

Last time, we started running Forge to get instances that contained well formed tic-tac-toe boards.

Modeling More Concepts: Starting Boards, Turns, and Winning

Starting Boards

What would it mean to be a starting state in a game? The board is empty:

pred starting[s: Board] {
  all row, col: Int | 
    no s.board[row][col]
}

Turns

How do we tell when it's a given player's turn? It's X's turn when there are the same number of each mark on the board:

pred XTurn[s: Board] {
  #{row, col: Int | s.board[row][col] = X} =
  #{row, col: Int | s.board[row][col] = O}
}

The {row, col: Int | ...} syntax means a set comprehension, and describes the set of row-column pairs where the board contains X (or O). The # operator gives the size of these sets, which we then compare.

Question: Is it enough to say that OTurn is the negation of XTurn?

No! At least not in the model as currently written. If you're curious to see why, run the model and look at the instances produced. Instead, we need to say something like this:

pred OTurn[s: Board] {
  #{row, col: Int | s.board[row][col] = X} =
  add[#{row, col: Int | s.board[row][col] = O}, 1]
}

Forge supports arithmetic operations on integers like add. While it doesn't matter for this model yet, addition (and other operations) can overflow according to 2's complement arithmetic. For example, if we're working with 4-bit integers, then add[7,1] will be -8. You can experiment with this in the visualizer's evaluator, which we'll be using a lot after the initial modeling tour is done.

(Warning: don't try to use + for addition in Forge! Use add; we'll explain why later.)

Winning the Game

What does it mean to win? A player has won on a given board if:

• they have placed their mark in all 3 columns of a row;
• they have placed their mark in all 3 rows of a column; or
• they have placed their mark in all 3 squares of a diagonal.

We'll express this in a winner predicate that takes the current board and a player name. Let's also define a couple helper predicates along the way:

pred winRow[s: Board, p: Player] {
  -- note we cannot use `all` here because there are more Ints  
  some row: Int | {
    s.board[row][0] = p
    s.board[row][1] = p
    s.board[row][2] = p
  }
}

pred winCol[s: Board, p: Player] {
  some column: Int | {
    s.board[0][column] = p
    s.board[1][column] = p
    s.board[2][column] = p
  }      
}

pred winner[s: Board, p: Player] {
  winRow[s, p]
  or
  winCol[s, p]
  or 
  {
    s.board[0][0] = p
    s.board[1][1] = p
    s.board[2][2] = p
  }
  or
  {
    s.board[0][2] = p
    s.board[1][1] = p
    s.board[2][0] = p
  }  
}

We now have a fairly complete model for a single tic-tac-toe board. Before we progress to games, let's decide how to fix the issue we saw above, where our model allowed for boards where a player has moved too often.

Should we add something like OTurn[s] or XTurn[s] to our wellformedness predicate? If we then enforced wellformedness for all boards, that would indeed exclude such instances---but at some risk, depending on how we intend to use the wellformed predicate. There are a few answers...

• If we were generating valid boards, a cheating state might well be spurious, or at least undesirable. In that case, we might prevent such states in wellformed and rule it out.
• If we were generating (not necessarily valid) boards, being able to see a cheating state might be useful. In that case, we'd leave it out of wellformed.
• If we're interested in verification, e.g., we are asking whether the game of Tic-Tac-Toe enables ever reaching a cheating board, we shouldn't add not cheating to wellformed---at least, not so long as we're enforcing wellformed, or else Forge will never find us a counterexample!

IMPORTANT: In that last setting, notice the similarity between this issue and what we do in property-based testing. Here, we're forced to distinguish between what a reasonable board is (analogous to the generator's output in PBT) and what a reasonable behavior is (analogous to the validity predicate in PBT). One narrows the scope of possible worlds to avoid true "garbage"; the other checks whether the system behaves as expected in one of those worlds.

We'll come back to this later, when we've modeled full games. For now, let's separate our goal into a new predicate called balanced, and add it to our run command above:

pred balanced[s: Board] {
  XTurn[s] or OTurn[s]
}
run { some b: Board | wellformed[b] and balanced[b]} 

To view instances for this new run command, select the Execute menu and then Run run$2.

If we click the "Next" button a few times, we see that not all is well: we're getting boards where wellformed is violated (e.g., entries at negative rows, or multiple moves in one square).

We're getting this because of how the run was phrased. We said to find an instance where some board was well-formed and valid, not one where all boards were. By default, Forge will find instances with up to 4 Boards. So we can fix the problem either by telling Forge to find instances with only 1 Board:

run { some b: Board | wellformed[b] and balanced[b]} 
for exactly 1 Board

or by saying that all boards must be well-formed and balanced:

run { all b: Board | wellformed[b] and balanced[b]} 

Practice with run

Let's try some variant run commands (inspired by live questions in class).

No Boards

Is it possible for an instance with no boards to still satisfy constraints like these?

run {    
     all b: Board | {
         -- X has won, and the board looks OK
         wellformed[b]
         winner[b, X]
         balanced[b]    
     }
 }

Adding More

We can add more constraints if we have a more focused idea of what we want Forge to find. For example, this addition also requires that X moved in the middle of the board:

run {    
     all b: Board | {
         -- X has won, and the board looks OK
         wellformed[b]
         winner[b, X]
         balanced[b]
         -- X started in the middle
         b.board[1][1] = X
     }
 } for exactly 2 Board

Notice that, because we said exactly 2 Board here, Forge must find instances containing 2 tic-tac-toe boards, and both of them must satisfy the constraints: wellformedness, X moving in the middle, etc.

By the way: not also works. So you could ask for a board where X hasn't won by adding not winner[b, X].

You also have implies and iff (if and only if), although you can still do something like comparing two predicates without iff (try, e.g., asking for instances where A and not B holds).

From Boards to Games

What do you think a game of tic-tac-toe looks like? How should we model the moves between board states?

A game of tic-tac-toe is a sequence of steps in this graph, starting from the empty board. Let's model it.

First, what does a move look like? A player puts their mark at a specific location. In Alloy, we'll represent this using a transition predicate: a predicate that says when it's legal for one state to evolve into another. We'll often call these the pre-state and post-state of the transition:

pred move[pre: Board, row: Int, col: Int, p: Player, post: Board] {
  // ...
}

What constraints should we add? It's useful to divide the contents of such a predicate into:

• a guard, which allows the move only if the pre-state is suitable; and
• an action, which defines what is in the post-state based on the pre-state and the move parameters.

For the guard, in order for the move to be valid, it must hold that in the pre-state:

• nobody has already moved at the target location; and
• it's the moving player's turn.

For the action:

• the new board is the same as the old, except for the addition of the player's mark at the target location.

Now we can fill in the predicate. Let's try something like this:

pred move[pre: Board, row: Int, col: Int, p: Player, post: Board] {
  -- guard:
  no pre.board[row][col]   -- nobody's moved there yet
  p = X implies XTurn[pre] -- appropriate turn
  p = O implies OTurn[pre]  
  
  -- action:
  post.board[row][col] = p
  all row2: Int, col2: Int | (row!=row2 and col!=col2) implies {        
     post.board[row2][col2] = pre.board[row2][col2]     
  }  
}

There are many ways to write this predicate. However, we're going to stick with this form because it calls out an important point. Suppose we had only written post.board[row][col] = p for the action, without the all on the next following lines. Those added lines, which we'll call a frame condition, say that all other squares remain unchanged; without them, the contents of any other square might change in any way. Leaving them out would be what's called an underconstraint bug: the predicate would be too weak to accurately describe moves in tic-tac-toe.

Exercise: comment out the 3 frame-condition lines and run the model. Do you see moves where the other 8 squares change arbitrarily?

Exercise: could there be a bug in this predicate? (Hint: run Forge and find out!)