// property A of [D'AJJL01]
// the probability the sender reports a certain unsuccessful transmission but the receiver got the complete file
P=?[ F srep=1 & rrep=3 & recv ]

// property B of [D'AJJL01]
// the probability the sender reports a certain successful transmission but the receiver did not get the complete file
P=?[ F srep=3 & !(rrep=3) & recv ]

// property 1 of [D'AJJL01]
// the probability the sender does not report a successful transmission
P=?[ F s=5 ]

// property 2 of [D'AJJL01]
// the probability the sender reports an uncertainty on the success of the transmission
P=?[ F s=5 & srep=2 ]

// property 3 of [D'AJJL01]
// the probability the sender reports an unsuccessful transmission after more than 8 chunks have been sent successfully
P=?[ F s=5 & srep=1 & i>8 ]

// property 4 of [D'AJJL01]
// the probability the receiver does not receive any chunk and the sender tried to send a chunk
P=?[ F !(srep=0) & !recv ]