// zero-sum properties

// minimum expected time user 1 can guarantee to eventually send a packet
<<usr1>>R{"time"}min=?[F s1=3]

// minimum expected time users 1 and 2 can guarantee to eventually send their packets
<<usr1,usr2>>R{"time"}min=?[F s1=3 & s2=3]

// minimum expected time users 1, 2 and 3 can guarantee to eventually send their packets
<<usr1,usr2,usr3>>R{"time"}min=?[F s1=3 & s2=3 & s3=3]

// minimum expected time users 1, 2, 3 and 4 can guarantee to eventually send their packets
<<usr1,usr2,usr32,usr4>>R{"time"}min=?[F s1=3 & s2=3 & s3=3 & s4=3]

// maximum probability user 1 can guarantee to send a packet
<<usr1>>Pmax=?[F s1=3]

// maximum probability users 1 and 2 can guarantee to send their packets
<<usr1,usr2>>Pmax=?[F (s1=3 & s2=3)]

// maximum probability users 1, 2 and 3 can guarantee to send their packets
<<usr1,usr2,usr3>>Pmax=?[F (s1=3 & s2=3 & s3=3)]

// maximum probability users 1, 2, 3 and 4 can guarantee to send their packets
<<usr1,usr2,usr3,user4>>Pmax=?[F (s1=3 & s2=3 & s3=3 & s4=3)]

// maximum probability user 1 can guarantee to send a packet within a deadline
<<usr1>>Pmax=?[F (s1=3 & t<=D)]

// maximum probability users 1 and 2 can guarantee to send their packets within a deadline
<<usr1,usr2>>Pmax=?[F (s1=3 & s2=3 & t<=D)]

// maximum probability users 1, 2 and 3 can guarantee to send their packets within a deadline
<<usr1,usr2,usr3>>Pmax=?[F (s1=3 & s2=3 & s3=3 & t<=D)]

// maximum probability users 1, 2, 3 and 4 can guarantee to send their packets within a deadline
<<usr1,usr2,usr3,user4>>Pmax=?[F (s1=3 & s2=3 & s3=3 & s4=3 & t<=D)]


// nonzero-sum properties

// expected time each user eventually sends a packet
// players act individually
<<usr1:usr2:usr3:usr4:usr5>>min=? (R{"time"}[F s1=3] + R{"time"}[F s2=3] + R{"time"}[F s3=3] + R{"time"}[F s4=3] + R{"time"}[F s5=3])

// expected time each user eventually sends a packet
// players 4 and 5 form a coaltion
<<usr1:usr2:usr3:usr4,usr5>>min=? (R{"time"}[F s1=3] + R{"time"}[F s2=3] + R{"time"}[F s3=3] + R{"time"}[F s4=3 &  s5=3])

// expected time each user eventually sends a packet
// players 1 and 2 and 4 and 5 form a coaltions
<<usr1,usr2:usr3:usr4,usr5>>min=? (R{"time"}[F s1=3 & s2=3] + R{"time"}[F s3=3] + R{"time"}[F s4=3 &  s5=3])

// expected time each user eventually sends a packet
// players 1, 2 and 3 and 4 and 5 form a coaltions
<<usr1,usr2,usr3:usr4,usr5>>min=? (R{"time"}[F s1=3 & s2=3 & s3=3] + R{"time"}[F s4=3 &  s5=3])

// probability each user eventually sents a packet
<<usr1:usr2:usr3:usr4:usr5>>max=? (P[F s1=3] + P[F s2=3] + P[F s3=3] + P[F s4=3] + P[F s5=3])

// probability each user eventually sents a packet within a deadline
<<usr1:usr2:usr3:usr4:usr5>>max=? (P[F (s1=3 & t<=D)] + P[F (s2=3 & t<=D)] + P[F (s3=3 & t<=D)] + P[F (s4=3 & t<=D)] + P[F (s5=3 & t<=D)])