// 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;