Formally modeling dreidel, the sequel • Buttondown

December 18, 2024

2 Model 2 Gyro

Next week is Hanukkah, which means my favorite pastime, how about complaining top It was a bad game. Last year I formally modeled it as prism To prove that this game is not fun. But because I restricted the model to a small case, I can’t prove that the game is really Bad.

It’s time to get the job done.

story so far

You can read last year’s newsletter here But here are advanced instructions.

Beyblade game

1. Each player starts with N pieces (usually chocolate coins). Usually 10-15 pieces per player.
2. At the beginning of the game, one coin is put into the pot each time the pot is empty.

3. Rotation involves spinning a top. turn out:

   • נ(Nun): Nothing happened.
   • ה(He): The player takes half of the pot, rounded up.
   • ג (Gimmel): The player takes the entire pot and everyone places a bet.
   • ש (Shin): The player adds a coin to the pot.

4. If a player has zero gold coins, they are eliminated. The game continues until only one player remains.

If you don’t have a top, you can use a four-sided die, but for a realistic experience you should wait eight seconds before looking at your die.

prism

prism is a probabilistic modeling language, which means you can code the system with the chance of doing something randomly, and it can answer questions like “On average, how many spins does a player lose?” (64, for 4 player/10 coins) and “Which is more likely to knock out the first player, shin or ante” (ante is 2.4 times more likely). You can check out last year’s model here.

The problem with PRISM is that it’s sorely lacking in expressive power: it’s just a weak abstraction for a writing giant. random matrix And lacks basic functionality like lists or functions. I have to hardcode every possible dice for each player. That means last year’s model had two limitations. First, it could only handle four players, and I had to write a new model for three to five players. Secondly, I let the game end as soon as I have a player lost:

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

In order to solve these two problems, I think I have to treat PRISM as a compilation target and write a program to count the number of players and output the corresponding model. But then December got really busy and I didn’t have time to program. Instead, I stuck with four hard-coded players and extended the old model to run until victory.

new model

These are all changes last year’s model.

First, instead of running until one player runs out of money, we run until three players run 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 one coin from each player, we add one coin to each remaining player. min(p1, 1) 1 if player 1 is still in the game, 0 otherwise.

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

We also have to ensure that the ante does not result in players receiving 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 the logic for players to be “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 (for example, if they just dropped their last coin), we 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’ve made similar changes to all other players. You can see the final model here.

Query model

Now we have a complete Dreidel game that runs until the player ends. And now, at lastwe can see the average number of spins a 4-player game lasts.

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

In English: Each player starts with ten coins. R=? Represents “the expected value of ‘reward'”, where “reward” in this case means the number of spins. [F done] Reward weighting for all achieved behaviors (“Ffinally”) done state.

Result: 760.5607582661091
Time for model checking: 384.17 seconds.

The numbers are: 760 spins. ^{8 seconds per revolution, almost two hours one game.}

…OMG, look at that run time. Test a query in six minutes.

PRISM has more than a hundred settings that affect model checking, including descriptions such as “Pareto Curve Threshold” and “Use Backward Pseudo SOR”. After looking through all of them, I found this perfect combination of configurations to get 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” sign.

Regardless, this is just the weighted “average” number of spins across all games. The top has a very long tail. To find the answer, we’ll use a variation of the query:

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

P=? yes phosphorusSomething happened. F <=C0 done means us FFinally reached the state done at most C0 step. By passing in different values C0 We can get an idea of ​​how long a match takes. Since “steps” include passes and antes, this overestimates the length of the game. But the ante also takes time, and each player can only “pass” the player once, so this should still be a good measure of 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

Fully 10% of games failed to complete the 2000 step mark, and 2% passed the 3000 step barrier. 8 seconds roll/bet, 3000 moves over six hours.

Beyblade is a terrible game.

More fun attributes

As a sanity check, let’s confirm last year’s results, which were that it took an average of around 64 spins before a player was eliminated. In this model, we only need to obtain the total reward. Now we want to get the reward until the first state where any player has 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.

Yes, it looks good. With our new model, we also get the average number of runs scored with two players out and two players left. PRISM’s lack of abstraction makes expressing conditions directly a bit of a pain, but we can cheat and look for the first state 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 does to eliminate the first player, and the remaining two players must play another 600 spins.

Beyblade is a terrible game.

future

Next I want to do two things with this model. The first is to write some scripts that generate PRISM models for me so that I can easily adjust the number of players to 3 or 5. Filter query Function I don’t understand, but I think It can be used for things like “If a player gets 75% of the pot, what is the chance they will lose?” Otherwise you have to write weird queries like this (P =? [F p1 = 30 & (F p1 = 0)]) / (P =? [F p1 = 0]). ^{But I ran out of time, so the saga must end next year.}

I’m also faced with a scary fact: I am probably PRISM’s largest non-academic user.

Programmer’s Logic Hanukkah Promotion

Still going on! you can get Lithium phosphate for 40% discount here From now until the end of Xannukkah (January 2).

I’m in the Raku Advent Calendar!

My work is called Calculate the number of concurrency. It’s about using Raku to do some combinatorial math! Also read the rest of the blog, it’s great

If you’re reading this online, you can subscribe here. Updated once a week. My main website is here.

my new book, Programmer’s Logichas now entered the early access stage! get it here.