Dreidel modeling

01-dreidel.prism

// dreidel model I wrote in 2023.
// see https://buttondown.com/hillelwayne/archive/i-formally-modeled-dreidel-for-no-good-reason/
dtmc

const int M; //starting money
formula Players = 4; //Players
formula maxval = M*Players;
formula done = (p1=0) | (p2=0) | (p3=0) | (p4=0);
formula halfpot = ceil(pot/2);

module dreidel
    p1 : [0..maxval] init M;
    p2 : [0..maxval] init M;
    p3 : [0..maxval] init M;
    p4 : [0..maxval] init M;
    pot: [0..maxval] init 0;
    turn: [1..4] init 1;

    [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
    
    [spin] ((pot != 0) & !done & (turn = 2)) ->
      0.25: (p2' = p2-1) & (pot' = min(pot+1, maxval)) & (turn' = 3) //shin
    + 0.25: (turn' = 3) //nun
    + 0.25: (p2' = min(p2+halfpot, maxval)) & (pot' = pot-halfpot) & (turn' = 3) // hay
    + 0.25: (p2' = min(p2+pot, maxval)) & (pot' = 0) & (turn' = 3); //gimmel

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

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

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

    [done] done -> true;
endmodule

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

02-dreidel.prism

// dreidel model I wrote in 2024.
// see https://buttondown.com/hillelwayne/archive/formally-modeling-dreidel-the-sequel/
dtmc

const int M; //starting money
formula Players = 4; //Players
formula maxval = M*Players;
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));

formula halfpot = ceil(pot/2);
formula ante_left = min(p1, 1) + min(p2, 1) + min(p3, 1) + min(p4, 1);

formula p1n = (p2 > 0 ? 2 : p3 > 0 ? 3 : 4);
formula p2n = (p3 > 0 ? 3 : p4 > 0 ? 4 : 1);
formula p3n = (p4 > 0 ? 4 : p1 > 0 ? 1 : 2);
formula p4n = (p1 > 0 ? 1 : p2 > 0 ? 2 : 3);

module dreidel
    p1 : [0..maxval] init M;
    p2 : [0..maxval] init M;
    p3 : [0..maxval] init M;
    p4 : [0..maxval] init M;
    pot: [0..maxval] init 0;
    turn: [1..4] init 1;

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

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

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

    [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));

    [done] done -> true;
endmodule

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