```// Simple dice game

smg

// Players
player P1 [toss1], [again1], [done1], [loop] endplayer
player P2 [toss2], [again2], [done2] endplayer

// Max number of throws per player
const int N;

module player1

// Local state:
s1 : [0..2] init 0;
// Loop counter
i : [0..N] init 0;
// Die value
x : [0..6] init 0;

// Throw die
[toss1] s1=0 -> 1/6:(x'=1)&(s1'=1) + 1/6:(x'=2)&(s1'=1) + 1/6:(x'=3)&(s1'=1)
+ 1/6:(x'=4)&(s1'=1) + 1/6:(x'=5)&(s1'=1) + 1/6:(x'=6)&(s1'=1);
// Decide whether to accept the die value
[again1] s1=1 & i<N-1 -> (i'=i+1)&(s1'=0);
[done1] s1=1 & i<N-1 -> (i'=i+1)&(s1'=2);
// No more throws allowed
[done1] s1=1 & i=N-1 -> (i'=i+1)&(s1'=2);
// Finished: loop
[loop] s1=2 -> true;

endmodule

module player2

// Local state:
s2 : [0..4] init 0;
// Die value
y : [0..6] init 0;
// Loop counter
j : [0..N] init 0;

// Start game (once player 1 is done)
[done1] s2=0 ->(s2'=1);
// Throw die
[toss2] s2=1 -> 1/6:(y'=1)&(s2'=2) + 1/6:(y'=2)&(s2'=2) + 1/6:(y'=3)&(s2'=2)
+ 1/6:(y'=4)&(s2'=2) + 1/6:(y'=5)&(s2'=2) + 1/6:(y'=6)&(s2'=2);
// Decide whether to accept the die value
[again2] s2=2 & j<i-1 -> (j'=j+1)&(s2'=2);
[done2] s2=2 & j<i-1 -> (s2'=3);
// No more throws allowed
[done2] s2=2 & j>=i-1 -> (s2'=3);
// Finished: loop
[loop] s2=3 -> true;

endmodule

// Labels
formula done = s1=2 & s2=3;
label "done" = done;
label "p1win" = done & x>y;
label "p2win" = done & x<=y;
//label "draw" = done & x=y;
```