const k; // number of rounds // module to count the rounds module rounds rounds : [0..k+1]; [] rounds<=k -> (rounds'=rounds+1); [] rounds=k+1 -> true; endmodule rewards "utility1" // utility of player 1 [r1,p2] true : -1; [r1,s2] true : 1; [p1,r2] true : 1; [p1,s2] true : -1; [s1,p2] true : 1; [s1,r2] true : -1; endrewards rewards "utility2" // utility of player 2 [r1,p2] true : 1; [r1,s2] true : -1; [p1,r2] true : -1; [p1,s2] true : 1; [s1,p2] true : -1; [s1,r2] true : 1; endrewards