Formally modeling dreidel, the sequel • Buttondown

December 18, 2024

2 model 2 dreidel

Channukah’s next week and that means my favorite pastime, complaining about how Dreidel is a bad game. Last year I formally modeled it in PRISM to prove the game’s not fun. But because I limited the model to only a small case, I couldn’t prove the game was truly bad.

It’s time to finish the job.

The Story so far

You can read the last year’s newsletter here but here are the high-level notes.

The Game of 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.
   • ה (He): 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.

If you don’t have a dreidel, you can instead use a four-sided die, but for the authentic experience you should wait eight seconds before looking at your roll.

PRISM

PRISM is a probabilistic modeling language, meaning you can encode a system with random chances of doing things and it can answer questions like “on average, how many spins does it take before one player loses” (64, for 4 players/10 coins) and “what’s the more likely to knock the first player out, shin or ante” (ante is 2.4x more likely). You can see last year’s model here.

The problem with PRISM is that it is absurdly inexpressive: it’s a thin abstraction for writing giant stochastic matrices and lacks basic affordances like lists or functions. I had to hardcode every possible roll for every player. This meant last year’s model had two limits. First, it only handles four players, and I would have to write a new model for three or five players. Second, I made the game end as soon as one player lost:

formula done = (p1=0) | (p2=0) | (p3=0) | (p4=0);

To fix both of these things, I thought I’d have to treat PRISM as a compilation target, writing a program that took a player count and output the corresponding model. But then December got super busy and I ran out of time to write a program. Instead, I stuck with four hardcoded players and extended the old model to run until victory.

The new model

These are all changes to last year’s model.

First, instead of running until one player is out of money, we run until three players are out of money.

- formula done = (p1=0) | (p2=0) | (p3=0) | (p4=0);
+ formula done = 
+  ((p1=0) & (p2=0) & (p3=0)) |
+  ((p1=0) & (p2=0) & (p4=0)) |
+  ((p1=0) & (p3=0) & (p4=0)) |
+  ((p2=0) & (p3=0) & (p4=0));

Next, we change the ante formula. Instead of adding four coins to the pot and subtracting a coin from each player, we add one coin for each player left. min(p1, 1) is 1 if player 1 is still in the game, and 0 otherwise.

+ formula ante_left = min(p1, 1) + min(p2, 1) + min(p3, 1) + min(p4, 1);

We also have to make sure anteing doesn’t end a player with negative money.

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

Finally, we have to add logic for a player being “out”. Instead of moving to the next player after each turn, we move to the next player still in the game. Also, if someone starts their turn without any coins (f.ex if they just anted their last coin), we just skip their turn.

+ formula p1n = (p2 > 0 ? 2 : p3 > 0 ? 3 : 4);

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

We make similar changes for all of the other players. You can see the final model here.

Querying the model

So now we have a full game of Dreidel that runs until the player ends. And now, finally, we can see the average number of spins a 4 player game will last.

./prism dreidel.prism -const M=10 -pf 'R=? [F done]' 

In English: each player starts with ten coins. R=? means “expected value of the ‘reward'”, where ‘reward’ in this case means number of spins. [F done] weights the reward over all behaviors that reach (“Finally”) the done state.

Result: 760.5607582661091
Time for model checking: 384.17 seconds.

So there’s the number: 760 spins. ^{At 8 seconds a spin, that’s almost two hours for one game.}

…Jesus, look at that runtime. Six minutes to test one query.

PRISM has over a hundred settings that affect model checking, with descriptions like “Pareto curve threshold” and “Use Backwards Pseudo SOR”. After looking through them all, I found this perfect combination of configurations that gets the runtime to a more manageable level:

./prism dreidel.prism 
    -const M=10 
    -pf 'R=? [F done]' 
+   -heuristic speed

Result: 760.816255997373
Time for model checking: 13.44 seconds.

Yes, that’s a literal “make it faster” flag.

Anyway, that’s only the “average” number of spins, weighted across all games. Dreidel has a very long tail. To find that out, we’ll use a variation on our query:

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

P=? is the Probability something happens. F <=C0 done means we Finally reach state done in at most C0 steps. By passing in different values of C0 we can get a sense of how long a game takes. Since “steps” includes passes and antes, this will overestimate the length of the game. But antes take time too and it should only “pass” on a player once per player, so this should still be a good metric for game length.

./prism dreidel.prism 
    -const M=10 
    -const C0=1000:1000:5000
    -pf 'const C0; P=? [F <=C0 done]' 
    -heuristic speed

C0      Result
1000    0.6259953274918795
2000    0.9098575028069353
3000    0.9783122218576754
4000    0.994782069562932
5000    0.9987446018004976

A full 10% of games don’t finish in 2000 steps, and 2% pass the 3000 step barrier. At 8 seconds a roll/ante, 3000 steps is over six hours.

Dreidel is a bad game.

More fun properties

As a sanity check, let’s confirm last year’s result, that it takes an average of 64ish spins before one player is out. In that model, we just needed to get the total reward. Now we instead want to get the reward until the first state where any of the players have zero coins.

./prism dreidel.prism 
    -const M=10 
    -pf 'R=? [F (p1=0 | p2=0 | p3=0 | p4=0)]' 
    -heuristic speed

Result: 63.71310116083396
Time for model checking: 2.017 seconds.

Yep, looks good. With our new model we can also get the average point where two players are out and two players are left. PRISM’s lack of abstraction makes expressing the condition directly a little painful, but we can cheat and look for the first state where ante_left <= 2.

./prism dreidel.prism 
    -const M=10 
    -pf 'R=? [F (ante_left <= 2)]' 
    -heuristic speed

Result: 181.92839196680023

It takes twice as long to eliminate the second player as it takes to eliminate the first, and the remaining two players have to go for another 600 spins.

Dreidel is a bad game.

The future

There’s two things I want to do next with this model. The first is script up something that can generate the PRISM model for me, so I can easily adjust the number of players to 3 or 5. The second is that PRISM has a filter-query feature I don’t understand but I think it could be used for things like “if a player gets 75% of the pot, what’s the probability they lose anyway”. Otherwise you have to write wonky queries like (P =? [F p1 = 30 & (F p1 = 0)]) / (P =? [F p1 = 0]). ^{But I’m out of time again, so this saga will have to conclude next year.}

I’m also faced with the terrible revelation that I might be the biggest non-academic user of PRISM.

Logic for Programmers Khanukah Sale

Still going on! You can get LFP for 40% off here from now until the end of Xannukkah (Jan 2).

I’m in the Raku Advent Calendar!

My piece is called counting up concurrencies. It’s about using Raku to do some combinatorics! Read the rest of the blog too, it’s great

If you’re reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.