// liveness (requires unconditional fairness assumption)
min=? [ F l=4 ]
fairness(SF({true}, {[env],[reset],[time],[send1],[send2],[rec0],[rec1]}),SF({true}, {[host],[reset],[time],[send1],[send2],[rec0],[rec1]}))

// min expected time to configure
Rmin=? [ F l=4 ]

// max expected time to configure
Rmax=? [ F l=4 ]