This is a spec for the Coffee Can problem, a math problem usually attributed to David Gries in his 1987 book The Science of Programming. However, on page 301 section 23.2 of the same book Gries attributes the problem to a 1979 letter by Edsger W. Dijkstra, who himself credits the problem to his colleague Carel S. Scholten.
The problem as presented on page 165 of The Science of Programming:
A coffee can contains some black beans and white beans. The following process is to be repeated as long as possible:
Randomly select two beans from the can. If they are the same color, throw them out, but put another black bean in. (Enough extra black beans are available to do this.) If they are different colors, place the white one back into the can and throw the black one away.
Execution of this process reduces the number of beans in the can by one. Repetition of this process must terminate with exactly one bean in the can, for then two beans cannot be selected. The question is: what, if anything, can be said about the color of the final bean based on the number of white beans and the number of black beans initially in the can?
We model this problem in TLA⁺ with a focus on two things: 1. Validate a monotonic decrease in number of beans at each step 2. Identify a loop/inductive invariant 3. Form a hypothesis about the final bean and modelcheck it
Finite modelchecking can only check our properties for a finite number of beans, while we want to show that it holds for all Natural numbers. TLA⁺'s built-in proof language can be used for this purpose, although such a proof is not currently included in this spec.