// maximum probability player 1 eventually wins a rounds
<<player1>> Pmax=? [Fc "win1" ]

// maximum probability player 2 wins a round first
<<player2>> Pmax=? [ !"win1" U "win2" ]

const int K;

// max expected payoff over K rounds
// when K=1 have a single round, i.e. the matrix game
<<player1>>R{"utility"}max=?[C<=K*2]