Crossing the river with TLA+

The pretty-printed version of the spec is here: https://github.com/lorin/tla-boat/blob/master/boat.pdf

The idea is that the algorithm is defined as non-deterministic (the `with` clauses nondeterministically chooses any "safe" configuration of the boat and cross the river with it), and the model-checker is then asked, is it true that no possible execution (a sequence of steps) solves the puzzle? The model checker then finds an execution that violates this assertion, and that is the solution (or one possible solution) to the puzzle.