Dreidel modeling

dreidel.prism

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