mdp
const int M = 5;
const int MAX_MONEY = 100;
const int STAGES = 10;
const double p_win = 0.7;
const double p_jackpot = 0.05;
module game
m:[0..MAX_MONEY] init M;
s:[1..STAGES+1] init 1;
[zero] (s < STAGES) -> (s'=min(s+1, STAGES)) & (m'=m);
[one] m > 0 & (s < STAGES)-> p_win:(s'=min(s+1, STAGES)) & (m'=min(m+1, MAX_MONEY)) + p_jackpot: (s'=min(s+1, STAGES)) & (m'=min(m+10, MAX_MONEY)) + (1-(p_win+p_jackpot)): (s'=min(s+1, STAGES)) & (m'=max(m-1,0));
[two] m > 1 & (s < STAGES)-> p_win:(s'=min(s+1, STAGES)) & (m'=min(m+2, MAX_MONEY)) + p_jackpot: (s'=min(s+1, STAGES)) & (m'=min(m+2*10, MAX_MONEY)) + (1-(p_win+p_jackpot)): (s'=min(s+1, STAGES)) & (m'=max(m-2,0));
[three] m > 2 & (s < STAGES)-> p_win:(s'=min(s+1, STAGES)) & (m'=min(m+3, MAX_MONEY)) + p_jackpot: (s'=min(s+1, STAGES)) & (m'=min(m+3*10, MAX_MONEY)) + (1-(p_win+p_jackpot)): (s'=min(s+1, STAGES)) & (m'=max(m-3,0));
[four] m > 3 & (s < STAGES)-> p_win:(s'=min(s+1, STAGES)) & (m'=min(m+4, MAX_MONEY)) + p_jackpot: (s'=min(s+1, STAGES)) & (m'=min(m+4*10, MAX_MONEY)) + (1-(p_win+p_jackpot)): (s'=min(s+1, STAGES)) & (m'=max(m-4,0));
[five] m > 4 & (s < STAGES)-> p_win:(s'=min(s+1, STAGES)) & (m'=min(m+5, MAX_MONEY)) + p_jackpot: (s'=min(s+1, STAGES)) & (m'=min(m+5*10, MAX_MONEY)) + (1-(p_win+p_jackpot)): (s'=min(s+1, STAGES)) & (m'=max(m-5,0));
[end] s=(STAGES) -> (s'=s+1);
endmodule
label "goal" = (s=STAGES+1);
label "obs" = (m=0);
rewards
[end] s=STAGES : MAX_MONEY-m;
endrewards