Lab 3: Chomp
Getting Started
A modified research version of Alloy, called Amalgam, will be required for the lab. The tool behaves just like Alloy (except the Next button is renamed to the Diff button), other than some features you will explore in part 2. To run Amalgam, simply open a terminal and type the following command. If you have issues running the command, please ask for assistance.
> amalgam [your banner ID]
We ask you to provide your ID so that we can examine your data across multiple labs. Amalgam will hash this ID to anonymize it before saving data for study purposes. The data collected will be used to improve the course and the Alloy features you're seeing today, and will not affect your grade in any way.
Part 1
Chomp Gameplay
For Alton Brown’s newest twist in Cutthroat Kitchen, players have to bid for the right to make two of their opponents play a little game Alton likes to call Chomp.
Chomp is a game for two players, played over a candy bar of mostly chocolate. The candy bar is a grid of chocolate squares, but final square has been replaced with soap.
In each turn, a player picks a set of rows or a set of columns of the candy bar to take, and the candy bar for the following turn is whatever remains. In alternating turns, players one and two choose rows or columns to take such that their opponent is left with the soap (thereby losing the game), and must make use of it in their dish.
Chomp State
An aspiring contender decides to prepare by modeling the game of Chomp in Alloy. They hope that doing so will let them reason about the game and potential winning strategies. They've completed most of their model themselves, and are asking you to help them finish it during this lab session.
The following declarations define the state of Chomp. Nothing is undefined in this snippet:
open util/ordering[Board]
// Chomp has two players: P1 and P2
abstract sig Player {}
one sig P1, P2 extends Player {}
// The chomp board has 2 dimensions: rows and columns
abstract sig Dimension {}
one sig Rows, Cols extends Dimension {}
// Each dimension has a set of indices (row 1, row 2, …)
sig Index {}
// A chomp board consists of:
abstract sig Board {
inplay : Dimension -> set Index, -- the rows/columns not taken yet
turn : one Player, -- the player taking a turn
chomp : lone Dimension -- the player’s choice (rows/columns but not both)
}
// A playable chomp board has at least one square (the soap) left
pred playable[b: Board] { some b.inplay[Rows] and some b.inplay[Cols] }
Add these declarations to your model. Read them carefully to make sure you understand how the Chomp game and board works.
Chomp Events
The following declarations define the events of Chomp. Notice that the contender has left out part of the definition. Your first task is to help them fill in the blank.
// Player one starts off the game with a playable (non-empty) board
fact FirstBoard { playable[first] and first.turn = P1 }
/* If there are squares to take, a player must make a move
If a player makes a move, there must be squares to take */
fact DefiniteGameplay { all b:Board | playable[b] iff some b.chomp }
/* All gameplay progress (events) are stated as a relationship between
a game board and it’s successor (except for last, which has no successor!) */
fact NextBoard { all b:Board-last | {
-- alternating turns
b.next.turn != b.turn
-- the game board always stays the same, or gets smaller
b.next.inplay in b.inplay
-- if the board is playable, and there’s a move:
some b.chomp implies {
-- a player can take rows, but not columns:
b.chomp in Rows implies {
b.inplay[Rows] not in b.next.inplay[Rows]
b.inplay[Cols] in b.next.inplay[Cols]
}
-- a player can take columns, but not rows:
b.chomp in Cols implies {
/* FILL */
}
}
-- if there is no move (unplayable), the board stays the same
no b.chomp implies b.inplay in b.next.inplay
}}
// the winner does not take the soap, which results in an unplayable board
pred winner[p: Player] { some b: Board | playable[b] and not playable[b.next] and b.turn != p }
Add these declarations to your model and complete the FILL. Run the spec without further constraints and view an instance or two. Remember that you can simplify the visualization by changing the theme or using a projection! We suggest projecting over Board, and making the field inplay show as attribute, not as arc, if the edges are hard to read.
Sanity Checking
It's often useful to put "sanity checks" in your spec, to make sure things work according to plan.
pred twoCanWin {
-- an instance where player 2 wins
/* FILL */
}
run twoCanWin for 10 Board, 5 Index, 5 Int
pred canFinishEarly {
-- an instance with more than one unplayable board
/* FILL */
}
run canFinishEarly for 10 Board, 5 Index, 5 Int
Add these definitions to the contender's model. Complete the sanity check definitions and run them to make sure their definitions so far look okay.
A winning strategy!!!
After a great deal of experimentation, the contender believes that, if player One moves first in the game, they can can always win by ensuring that the board they pass onto player Two is square. However, they aren't quite sure how to express that strategy in Alloy...
// for playable boards of this player’s turn
pred WinningStrategy[p: Player] { all b:Board | playable[b] and b.turn = p implies {
-- if there are more rows than columns
b.inplay[Rows] not in b.inplay[Cols] implies {
-- return a square board
/* FILL */
}
-- if there are more columns than rows
b.inplay[Cols] not in b.inplay[Rows] implies {
-- return a square board
/* FILL */
}
-- if there are equal rows and columns
b.inplay[Cols] = b.inplay[Rows] implies {
-- take only one row or column
{ one b.inplay[Cols]-b.next.inplay[Cols]
no b.inplay[Rows]-b.next.inplay[Rows] }
or { one b.inplay[Rows]-b.next.inplay[Rows]
no b.inplay[Cols]-b.next.inplay[Cols] }
}
}}
pred P1StrategyWins { WinningStrategy[P1] implies winner[P1] }
run P1StrategyWorks { P1StrategyWins } for 10 Board, 5 Index, 5 Int
check P1StrategyFails { P1StrategyWins } for 10 Board, 5 Index, 5 Int
Add these definitions to your model, fill in Player One's supposed winning strategy, and run the check. Did this pass? If it did, does that mean the strategy is correct? What might have gone wrong?
Scoping out the Problem
Let's check P1StrategyFails under larger bounds: Board to 20, Index to 10, Int to 10. Is Alloy able to still quickly check the assertion? (If it takes more than a minute, go ahead and click the Stop button.) If Alloy is slow here, maybe there is another tool we'll be seeing soon that handles this kind of problem much better. c:
Part 2
Please run through the following (brief) tutorial on Amalgam's "maximal" mode:
https://docs.google.com/document/d/1q0ufe1pQlJHGYi-YQemRNPUp4zoEuwgpBp9GOKRPYe8/edit?usp=sharing
Then make certain that "show me only maximal models" mode is enabled in the options menu before continuing. You can check and change this in the options menu.
Let's investigate the circumstances under which player 1's winning strategy fails. Please copy and paste the following definitions into the end of your Alloy lab file:
pred StartingBoard { /* FILL */ }
pred PlayerTwo { /* FILL */ }
pred reason { WinningStrategy[P1] and StartingBoard and PlayerTwo }
check reasonImpliesP1StrategyFails { reason implies (not P1StrategyWins) } for 10 Board, 5 Index, 5 Int
check P1StrategyFailsImpliesReason { (not P1StrategyWins) implies reason } for 10 Board, 5 Index, 5 Int
You can run P1StrategyWorks to ask Alloy for examples where player 1’s strategy works, and P1StrategyFails to ask for situations where player 1’s strategy fails.
By exploring both sets of instances, see if you can characterize the situations where player 1’s strategy fails. Fill in the two description predicates so that it returns true only for those instances. We are asking you to describe the instances, not just negate the body of the P1StrategyWins predicate. What might be true about an instance that causes player 1’s strategy to fail? We have hinted that it might be about the StartingBoard; fill your hypothesis in here. If the second player needs to do anything special to win, please fill that in in PlayerTwo.
Use the evaluator to form your hypothesis: your description should be true in instances where player 1’s strategy fails, and false in instances where player 1’s strategy works. To check your hypothesis, run the reasonImpliesP1StrategyFails and P1StrategyFailsImpliesReason predicates. Keep adapting your reason until the two validation predicates pass. In terms of the figure, your goal is to have reason and P1StrategyFails completely overlap. Too tight of a description will leave some instances of P1StrategyFails out of the overlap (P1StrategyFailsImpliesReason will fail). Too loose of a description will leave some instances of reason out of the overlap (reasonImpliesP1StrategyFails will fail).
Do not be discouraged! This is a challenging task, and you will receive full credit for an honest attempt. If you run low on time, please proceed to the next part.
Part 3
Exit Amalgam. You will see your anonymous ID printed on the command line.
Please fill out the following exit survey, and show the completion page to a TA: