I am trying to model the David Gries’ Coffee Can Problem in TLA+, and I am stuck at this part :
"What can you say about the color of the final remaining bean as a function of the numbers of black and white beans originally in the can?"
I don't know how to approach this. Could you please provide some advice or some hints? (a methodology is also welcome)
This is my code in TLA+ :
------------------------------ MODULE CanBean ------------------------------
EXTENDS Naturals, FiniteSets, Sequences
\* filter <- 2 | max_can <- 5
CONSTANT filter, max_can
VARIABLES picked, Can, Whites, Blacks
vars == <<picked, Can, Whites, Blacks>>
IsBlack(i) == i % filter = 0
IsWhite(i) == i % filter /= 0
GetWhite(a,b) == IF IsWhite(a) THEN a ELSE b
GetBlack(a,b) == IF IsBlack(a) THEN a ELSE b
AreBothWhite(a,b) == IsWhite(a) /\ IsWhite(b)
Pick == /\ picked = <<>>
/\ \E a,b \in Can : a/= b /\ picked' = <<a,b>>
/\ UNCHANGED <<Whites, Blacks, Can>>
Process == /\ picked /= <<>>
/\ LET a == picked[1] b == picked[2] IN
/\ \/ AreBothWhite(a,b) /\ Whites' = Whites \ {a,b} /\ \E m \in Nat \cap Can : Blacks' = Blacks \cup { filter * m }
\/ ~AreBothWhite(a,b) /\ Blacks' = Blacks \ { GetBlack(a,b) } /\ UNCHANGED Whites
/\ picked' = <<>>
/\ Can' = Blacks' \cup Whites'
Terminating == /\ Cardinality(Can) = 1
/\ UNCHANGED vars
TypeInvariantOK == /\ \A n \in Can : n \in Nat
/\ LET length == Len(picked)
IN length = 2 \/ length = 0
Init == /\ picked = <<>>
/\ Can = 1..max_can
/\ Blacks = { n \in Can : n % filter = 0 }
/\ Whites = { n \in Can : n % filter /= 0 }
Next == Pick \/ Process \/ Terminating
=============================================================================
\* Modification History
\* Last modified Sun Feb 21 14:53:34 CET 2021
\* Created Sat Feb 20 19:50:01 CET 2021
It should first be noted David Gries sources the coffee can problem to a fall 1979 letter written by Dijkstra, who himself heard of the problem from his colleague Carel Scholten (ref: The Science of Programming by David Gries, page 301 section 23.2).
I've written a simplified TLA+ spec you might find useful:
---------------------------- MODULE CoffeeCan -------------------------------
EXTENDS Naturals
VARIABLES can
Can == [black : Nat, white : Nat]
\* Initialize can so it contains at least one bean.
Init == can \in {c \in Can : c.black + c.white >= 1}
BeanCount == can.black + can.white
PickSameColorBlack ==
/\ BeanCount > 1
/\ can.black >= 2
/\ can' = [can EXCEPT !.black = @ - 1]
PickSameColorWhite ==
/\ BeanCount > 1
/\ can.white >= 2
/\ can' = [can EXCEPT !.black = @ + 1, !.white = @ - 2]
PickDifferentColor ==
/\ BeanCount > 1
/\ can.black >= 1
/\ can.white >= 1
/\ can' = [can EXCEPT !.black = @ - 1]
Termination ==
/\ BeanCount = 1
/\ UNCHANGED can
Next ==
\/ PickSameColorWhite
\/ PickSameColorBlack
\/ PickDifferentColor
\/ Termination
MonotonicDecrease == [][BeanCount > 1 => BeanCount' < BeanCount]_<<can>>
EventuallyTerminates == <>(ENABLED Termination)
Spec ==
/\ Init
/\ [][Next]_<<can>>
/\ WF_<<can>>(Next)
THEOREM Spec =>
/\ MonotonicDecrease
/\ EventuallyTerminates
=============================================================================
You can modelcheck it by overriding the definition of Nat.
As you've noticed, it's easy to see from this spec that the number of beans decreases monotonically (which can be verified with the MonotonicDecrease temporal property) thus the process must terminate within a finite number of steps. The second problem seems to involve probability, thus it is not a great fit for TLA+. TLC does have the ability to simulate basic random systems in TLA+, but this is too limited to directly encode the answer to question two as a system invariant. There's a formal specification language called PRISM created to deal with probabilistic systems, although its language is much less ergonomic than TLA+.
Edit: I wrote a PRISM spec for this problem and found something very interesting - we don't have to deal with probability at all! Here's the spec - the seemingly superfluous usage of min() and max() is because PRISM is very picky about updates not taking variables out of bounds, even if the probability of that update being taken is 0:
dtmc
const int MAX_BEAN = 20;
formula total = black + white;
formula p_two_black = (black/total)*(max(0,black-1)/(total-1));
formula p_two_white = (white/total)*(max(0,white-1)/(total-1));
formula p_different = 1.0 - p_two_black - p_two_white;
init
total >= 1 & total <= MAX_BEAN
endinit
module CoffeeCan
black : [0..(2*MAX_BEAN)];
white : [0..MAX_BEAN];
[] total > 1 ->
p_two_black : (black' = max(0, black - 1))
+ p_two_white : (black' = min(2*MAX_BEAN, black + 1)) & (white' = max(0, white - 2))
+ p_different : (black' = max(0, black - 1));
[] total = 1 -> true;
endmodule
After plugging in some test initial values I used PRISM to check the following formula, which basically asks "what is the probability that we terminate with a single white bean?":
P=?[F black = 0 & white = 1]
Do you know what I found? When you start out with an even number of white beans the probability is zero, and when you start out with an odd number of white beans the probability is one! We can encode this assertion as properties which PRISM will verify are true:
P>=1 [mod(white, 2) = 1 => (F black = 0 & white = 1)]
P>=1 [mod(white, 2) = 0 => (F black = 1 & white = 0)]
In retrospect this is obvious, because the number of white beans only ever decreases by two. So if you start out with an even number of white beans you will terminate with zero white beans, and if you start out with an odd number of white beans you will terminate with a single white bean. You can add this temporal property to the above TLA+ model to check this:
WhiteBeanTermination ==
IF can.white % 2 = 0
THEN <>(can.black = 1 /\ can.white = 0)
ELSE <>(can.black = 0 /\ can.white = 1)