// 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 2 and 3 can guarantee to eventually send their packets
<<usr2,usr3>>R{"time"}min=?[F s2=3 & s3=3]

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

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


// Nonzero-sum properties

// probability user 1 eventually sends a packet
// and users 2 and 3 form a coalition to send two packets
<<usr1:usr2,usr3>>max=? (P[F s1=3] + P[F s2=3 & s3=3])
// should be 1.0+1.0=2.0 as can collaborate
// i.e. first one sends and then the other does afterwards as no deadline

// expected time user 1 eventually sends a packet
// and users 2 and 3 form a coalition to send two packets
<<usr1:usr2,usr3>>min=? (R{"time"}[F s1=3] + R{"time"}[F s2=3 & s3=3])

// probability user 1 eventually sends a packet by a deadline
// and users 2 and 3 form a coalition to send two packets by a deadline
<<usr1:usr2,usr3>>max=? (P[F (s1=3 & t<=D)] + P[F (s2=3 & s3=3 & t<=D)])

// probability user 1 eventually sends a packet by a deadline
// and users 2 and 3 form a coalition to send two packets
<<usr1:usr2,usr3>>max=? (P[F (s1=3 & t<=D)] + P[F (s2=3 & s3=3)])

// probability user 1 eventually sends a packet
// and users 2 and 3 form a coalition to send two packets by a deadline
<<usr1:usr2,usr3>>max=? (P[F (s1=3)] + P[F (s2=3 & s3=3 & t<=D)])

// nested props
// maximum probability the users can collaborate to reach a state where the users can then independently send their messages with probability 1 within 4 time units (with users 2 and 3 in coalition)
<<usr1,usr2,usr3>>Pmax=?[F <<usr1:usr2,usr3>>max>=2 (P[F (s1=3 & t<=D)] + P[F (s2=3 & s3=3 & t<=D)]) ]