const int k;

// all users maximise the expected reward before their battery becomes empty
<<user1:user2:user3>>{NE,SW}max=? (R{"r1"}[F e1=0] + R{"r2"}[F e2=0] + R{"r3"}[F e3=0])
<<user1:user2:user3>>{NE,FR}max=? (R{"r1"}[F e1=0] + R{"r2"}[F e2=0] + R{"r3"}[F e3=0])
<<user1:user2:user3>>{CE,SW}max=? (R{"r1"}[F e1=0] + R{"r2"}[F e2=0] + R{"r3"}[F e3=0])
<<user1:user2:user3>>{CE,FR}max=? (R{"r1"}[F e1=0] + R{"r2"}[F e2=0] + R{"r3"}[F e3=0])

// all users maximise the expected reward for the first k steps
<<user1:user2:user3>>max=? (R{"r1"}[C<=k] + R{"r2"}[C<=k] + R{"r3"}[C<=k])

// all players maximize the probability their battery becomes empty
// should be 1+1+1=3
<<user1:user2:user3>>max=? (P[F e1=0] + P[F e2=0] + P[F e3=0])