Formally modeled Dreidel for no good reason

Dec. 12, 2023, 2:14 p.m.

I can mathematically prove the game’s not fun.

New blog post

Notes on Every Strangeloop 2023 Talk I Attended. Would have been out earlier but I was busy and sick. Patreon is here.

I formally modeled Dreidel for no good reason

It’s the sixth night of Channukah and I’m thinking about dreidels:

On Channukah we use dreidels to play the game dreidel:

1. Every player starts with N pieces (usually chocolate coins). This is usually 10-15 pieces per player.
2. At the beginning of the game, and whenever the pot is empty, every play antes one coin into the pot.

3. Turns consist of spinning the dreidel. Outcomes are:

   • נ (Nun): nothing happens.
   • ה (Hey): player takes half the pot, rounded up.
   • ג (Gimmel): player takes the whole pot, everybody antes.
   • ש (Shin): player adds one of their coins to the pot.

4. If a player ever has zero coins, they are eliminated. Play continues until only one player remains, or (much more likely) everybody gets bored.

Traditionally this game is played by kids, as it’s an excellent way to convince them that gambling is boring as all hell. In 2015 Ben Blatt simulated the game and found that for P=4 and N=10, the average game will take 860 spins to finish.

But this was based on a mere 50,000 simulated games! We can do better than a mere simulation. We can mathematically model the game and get exact numbers. So we’re busting out PRISM.

Modeling Dreidel in PRISM

PRISM is a probabilistic model checker. You create a model of a probabilistic system, like queueing workers or a gambling game, and PRISM can give you exact probabilities of various events happening. I’ve written two blog posts on PRISM:

• Probabilistic Modeling with PRISM
• Two workers are quadratically better than one

If you read those blog posts, you’ll quickly learn that I really do not like PRISM. The problem is that it is incredibly limited language. It doesn’t have strings, or arrays, or functions. This makes generalizing or abstracting things virtually impossible, and you’re going to be hardcoding a lot of stuff. Despite all that, I keep finding excuses to use PRISM anyway. I’ve got an enormous number of small PRISM tricks I will never share with anyone because nobody else will ever use PRISM. Maybe there’s a grad student who needs them, I dunno.

I’m not going to go through the entire model, you can see it here. Just some highlights:

formula Players = 4; //Players
formula maxval = M*Players;
formula done = (p1=0) | (p2=0) | (p3=0) | (p4=0);

Since I can’t abstract over anything, I can’t make a general model that works for P players, so instead I hardcode in 4 players. Also, properly modeling “playing until one player is left” would have been a nightmare, so instead I’m just modeling until one player is eliminated.

    [spin] ((pot != 0) & !done & (turn = 1)) ->
      0.25: (p1' = p1-1) & (pot' = min(pot+1, maxval)) & (turn' = 2) //shin
    + 0.25: (turn' = 2) //nun
    + 0.25: (p1' = min(p1+halfpot,maxval)) & (pot' = pot-halfpot) & (turn' = 2) // hay
    + 0.25: (p1' = min(p1+pot,maxval)) & (pot' = 0) & (turn' = 2); //gimmel

This is the core of a PRISM spec: a set of conditions for this to happen, a set of weighted outcomes, and the updates for each outcome. Though it’s mathematically impossible for a shin to make the pot have more than maxval coins, whatever model checking algorithm PRISM uses couldn’t tell that, so I had to manually cap it with (pot' = min(pot+1, maxval)). I spent a lot of time on this spec coddling the model checker.

Also notice that I had to hardcode that this is all for player one (p1). This means that I have to write this action three more times:

    [spin] ((pot != 0) & !done & (turn = 2)) ->
      0.25: (p2' = p2-1) & (pot' = min(pot+1, maxval)) & (turn' = 3)
    + 0.25: (turn' = 3)
    // etc etc etc

All of the actions are guarded on pot!=0. When it’s empty, we instead have an ante action:

    [ante] (pot = 0) & !done -> (pot'=pot+4) & (p1' = p1-1) & (p2' = p2-1) & (p3' = p3-1) & (p4' = p4-1);

Since this means not all actions will be spins, I added a reward to track just the spins:

rewards "num_spins"
    [spin] true : 1;
endrewards

Querying the system

So why bother with all this when the Python would be like ten lines? The reason is that once you’ve gone through all the work of modeling something in PRISM, you get a powerful querying system to learn properties of the model. First, let’s just find the expected value (weighted average) for the number of spins to knock out one player:

$ ./prism dreidel.prism -const M=10 -pf 'R=? [C]'    

Value in the initial state: 63.71149441710945
Time for model checking: 174.563 seconds.

So if we have four players, and each player starts with 10 coins, it’ll take on average 64 spins to knock a single player out. I stopwatched a dreidel and it takes about 8 seconds for a spin, so you’re looking at about nine minutes of watching a top spin before someone gets to leave the table.

Of course that’s only the likeliest outcome. I can also get the cumulative probability like this:

const C0;
P=? [F<=C0 done]

That returns the probability that within C0 steps of starting, done is Finally true. Note this is total model checking steps and includes antes too. While I can run this from the command line, it's nicer to see in the GUI.

Those are still pretty easy to find from a regular simulation, so let's try a more complex property. What's the probability that the game ends because a player rolled a Shin, as opposed to an ante?

prism dreidel.prism 
  -pf "P=? [F (pot != 0 & !done & (X done))]" 
  -const M=6:4:10 
  -exportresults stdout

M       Result
6       0.2944666679018678
10      0.2930102532933088

(Don't forget to check the probability it ends because of an ante!)

What's the probability that the first player will have 75% of all pieces in the game, and still lose?

-pf "P=? [F (p1=maxval-M & (F p1=0))]"
-const M=5:5:15 
-exportresults stdout
M       Result
6       1.1876357695852015E-10
10      1.0185162507865054E-8
15      4.902270837317093E-8

It's extraordinarily unlikely but becomes less extraordinarily likely when you start with more coins. And again we're just modeling until one player runs out of coins, so the odds are slightly (slightly) higher than this.

Finally, the chance the pot maxes out at C0 coins:

-pf 'P=? [(F pot=C0) & (G pot <= C0)]'
-const M=10,C0=0:1:20

Was this worth it?

Ugh no I hate PRISM

But also I think I figured out a different approach to modeling this that would better handle adding players and running until just one player is left. Maybe that'll be a blog post for next Channukah!

End of Year Administrative Stuff

Next week will be the last newsletter of the year. Quick updates on this year's projects:

• Logic for Programmers: Haven't made any progress on it for a while, but a friend has kindly offered to help edit and keep me to a schedule, so I'm more optimistic for the next year.

• Why programming languages doesn't have graph types: Done with interviews, writing an outline!

I want to write a new formal methods talk for next year, which would focus on the general history and idea of formal specification instead of just pitching TLA+ as a product. If you know any conference people who'd be interested, put me in touch!

If you're reading this on the web, you can subscribe here. Updates are 6x a month. My main website is here.