Problem Set 4: Creating Life

Due Tuesday, October 28, 2008, 11:59 pm.

For this problem set, you are to turn in an overview document covering Part 2. The overview document should be composed as described in Overview Requirements. As with the previous problem set it is your job to convince us that your code works, by describing your implementation and by presenting a testing strategy, test cases, and results.

You may work on this problem set with a partner. We strongly recommend discussing, critiquing, and agreeing on specifications before doing any implementation. You can also bring specs to office hours to get feedback. When critiquing a spec, think about the spec both from the standpoint of the client who is going to use the spec, and the developer who must implement it. It is also a good idea to discuss and agree on abstraction functions and rep invariants for your data structures. You will also need to think about how to divide your program into modules.

We will be holding 20-minute design review meetings during October 19–22. Your group is expected to meet with one of the TAs or the instructor during their office hours, or with consultants during consulting hours. A signup schedule is available on CMS. You should be able to explain your design in about 10 minutes, leaving 10 minutes for questions. It's a good idea to practice your presentation ahead of time so you use your time effectively.

In your design review, plan to talk about at least:

How you will divide the program into modules, and why.
Specifications for any modules you define.
What representations (and invariants over them) you will use.
Any other interesting issues you foresee.

Watch here for a summary of any updates or corrections.

10/19: Fixed instructions for making a new top-level in linux.
10/21: Switched from arrow keys to 'w','s','a','d' for panning.

Part 1: Written Problems

Propositional Logic
Prove the following statements using only the inference rules provided in Lecture 12: Natural Deduction (don't use any of the tautologies).
1. A ∧ ¬B ⇒ ¬(A ⇒ B)
2. (A ⇒ C) ∧ (B ∧ ¬C) ⇒ ¬A
3. (¬A ∨ B) ⇔ (A ⇒ B)
Predicate Logic
Prove the following statements using the inference rules for propositional logic in Lecture 11: Natural Deduction and the rules for quantifiers in Lecture 12. Note that p, q are names of predicates.
1. ¬∃x. ⊥
2. (∀x. p(x) ⇒ q(x)) ⇒ ((∀x. p(x)) ⇒ (∀x. q(x)))
3. (∀x. p(x)) ⇒ (¬∃x.¬p(x))
Program verification
Suppose we have a function max with the following spec:
```
(* Requires: ⊤
 * Returns: r = max(x,y) where (r=x∨r=y) ∧ r≥x ∧ r≥y *)
```
Now we implement a function that takes the maximum of three numbers as follows:
```
(* Requires: ⊤
 * Returns: max3(x,y,z) = r
 *    where (r=x ∨ r=y ∨ r=z) ∧ r≥x ∧ r≥y ∧ r≥z *)
let max3(x,y,z) =
  if x <= y then max(y,z) else max(x,z)
```
1. Write a partial correctness assertion whose meaning is that max3 satisfies its spec.
2. Use the Hoare logic rules to build as much of a proof as possible without proving any predicate logic formulas.
3. Give proofs for the remaining predicate logic proof obligations, using predicate logic. For this part, you may use tautologies or other standard axioms you like. The following axioms may be useful:
  - ∀x.x≤x (reflexivity)
  - ∀x.∀y.x≤y ⇔ y≥x (defn of ≥)
  - ∀x.∀y.x≤y ∧ y≥x ⇒ x=y (anti-symmetry)
  - ∀x.∀y.∀z. x≤y ∧ y≤z ⇒ x≤z (transitivity)

Part 2: Conway's Game of Life

The second part of this problem set involves implementing Conway's Game of Life in OCaml.

Rules of the Game

If a cell is dead and it has exactly 3 live neighbors, it becomes live.
If a cell is dead and has any other number of live neighbors, it stays dead.
If a cell is alive and has either 2 or 3 live neighbors, it stays alive.
If a cell is alive and has any other number of live neighbors, it dies.

It might help to play around with the system in any one of many available implementations online to obtain a better grasp of the consequences of these rules.

All state transitions occur across the entire board at the same time. That is, if we consider the current state of the game to be represented as the state of each cell on the board, then the next state of the game is one in which the above transition function is applied once to each cell simultaneously. We call this board transition a tick. One can imagine a slight variation on this game in which live cells also contain an RGB color represented as a 3-tuple of integers, each between 0 and 255. To support color, the transition rules given above are slightly modified. When a live cell is kept alive by its 2 or 3 neighbors, its color remains unchanged. However, when a dead cell is brought to life by its three neighbors, its color is computed from the average color of those neighbors. The evolve_color function computes the new color of the cell, given the average color of the neighbors.

Your Task

Your main task is to implement a GameOfLife module incorporating the rules above. As discussed in greater detail below, we've given you a functional interface to OCaml's graphics libraries that allows you to display and modify the state of your game in a GUI. The way you use your functions to update the GUI is intrinsically tied to your design, and you should consider this carefully when defining the state for GameOfLife. The GAMEOFLIFE interface is left up to you, but we do expect you to write it.

Your implementation should incorporate a few key clarifications. The game's universe is square, with a power-of-2 number of cells in each dimension. Cells occur at integer coordinates in this space. The lower left cell is (0,0) and the upper right is (2ⁿ - 1, 2^ⁿ - 1) for board size n. However, the GUI is always centered between cells. Thus, if the window was centered on cell (x,y), the view would be centered on cell (x+0.5, y+0.5).

The viewing window is always centered between cells, so we cannot zoom indefinitely. Because the viewing window is limited to 512 × 512 pixels, it does not make sense to zoom in further than zoom 8. When the level of zoom is such that each viewing window pixel represents several cells in the game of life, the color of the cell in the GUI should be based on the average color of all cells that fall within that window pixel, including dead cells, which are black (0,0,0).

The game board may be very large, so your representation should allow for efficient zooming at powers of two as described above and accommodate very large boards as long as they are sparsely populated; your implementation should handle sparse populations on board sizes as large as 2²⁴×2²⁴ efficiently. To assure this, run time must not grow linearly with the size of the board. Be sure that you have a good understanding of what is required for all parts of the assignment before you design the state representation.

Graphics

We are providing a module Graph, which provides functionality for computer graphics and graphical user interfaces. It has the following signature:

This module requires the use of two libraries that are not automatically loaded into OCaml: graphics.cma, and unix.cma. To load these libraries into the top level environment, run the following commands before compiling the code:

#load "graphics.cma";;
#load "unix.cma";;

We are distributing a top-level OCaml environment that has these libraries pre-loaded called ocamlg. You're code must compile on this environment without any #load commands. If you are using Emacs, you can use this top-level environment while developing; when it asks which top-level environment to load, point Emacs to the directory containing ocamlg. For ease, you may dump ocamlg into the default directory. On Windows, this is: C:\Program Files\Objective Caml\bin.

Note that this environment is a Windows binary. If you are running a linux/mac, you can create your own top level environment with the following command:

ocamlmktop -o ocamlg "graphics.cma" "unix.cma"

GUI

You are required to implement a module GUI. It should have the following two functions implemented, as well as any other function you see fit:

(* loadPattern s loads the game defined in file s *)
loadPattern: string -> unit

(* startNew creates a new, empty game of life *)
startNew: unit -> unit

Both of these functions should open a 512 by 512 pixel window, and the game should start running (as opposed to being paused). You are required to implement a function loadPattern, allowing games to be loaded based on a state description in a file.

A correctly formatted file has a first line that gives the size n of the board. After that, it contains a series of lines describing rows of the state of the game near the origin (0,0). Each line contains a sequence of the characters ".", "r", "g", or "b". The character "." means that there is a dead cell. The characters "r", "g", and "b" represent cells that are initially alive, with colors red (255, 0, 0), green (0, 255, 0), or blue (0,0,255). The program should check that all lines have the same length. The described cells are loaded so that the loaded pattern is centered on the position (2^n-1,2^n-1) as nearly as possible. For example, here is the format for a red vertical blinker in a 2³×2³ board:

3
.r.
.r.
.r.

Loading this should create an 8x8 board, with red cells alive at positions (4,3), (4,4), and (4,5). On the next step, it will change to a horizontal blinker.

Interacting with the Game

Besides updating the game board in accordance with the rules of the game of life, you are also required to provide the following functionality in your program:

Pausing: Pressing the space bar on the keyboard should cause toggle whether the simulation is paused or running. When the game is in a pause, pressing 't' on the keyboard should cause one simulated tick. (Hint: when the game is paused, it will save energy to sleep for some small amount of time (for example, 1/60 second) between checks for new key presses.)
Interactive panning: Pressing ~~arrow keys~~ 'w','s','a', or 'd' should scroll the current view up a height equal to one-quarter of the visible game board.
Mouse editing: When the game is paused, the user should be able to click and drag the mouse across the game board. Any cell that the mouse clicks on (or clicks and drags over) that is dead should be set alive, with a random color.
Interactive zoom: Pressing the period ('.') key on the keyboard should cause the current view to zoom in one level. Pressing the comma (',') on the keyboard should cause the current view to zoom out.

Karma

The following features can be implemented for good karma:

Autozoom: Pressing 'a' on the keyboard toggles autozoom mode. In this mode, the game automatically and continuously adjusts pan and zoom settings to keep the view zoomed in as much as possible while keeping every live cell in view. Can you implement this without unnecessary panning?
Smooth panning and zoom: Instead of simply panning by a fixed number of cells at a time, allow for smooth movement of the board one pixel at a time while the panning keys are held down. When the view is zoomed, this means cells may overlap the window boundary. (NOTE: if this is correctly implemented, you do not have to implementing the panning by 1/4 of the visible board.) Similarly, instead of zooming in and out by factors of two, allow for a continuous range of values, zooming in or out at a rate of 100% per second. The function Unix.gettimeofday(), which gives the current time, may be useful for this.

Other features:

Files to Submit

Please submit the following files:

Part 1:

Submit a file called part1.txt or part1.pdf, containing answers to the questions in part 1.

Part 2:

Submit all the files you worked on for your Game of Life implementation. Please note: you do not have to submit graph.mli or graph.ml; we will be using the implementations we provided. You should submit a file for this part called part2.zip, which contains:

gameOfLife: You should submit gameOfLife.ml and gameOfLife.mli. The latter file contains your specification for the game of life. The latter file contains your implementation.
gui.ml: You should submit a file called gui.ml. This file should contain a module called GUI, as described above.
Other files: You may include any other files as necessary. If you choose to include other files, please create a file called others.txt that lists the files you have submitted and explained their purpose.