// assumption on environment property: performs rec1 and rec2 only finitely many times
// uses two assumption on the host
// assumption 1: error automata (safety properties of host)
// assumption 2: send1 and send2 performed only finitely many time
multi ( Pmax=?[ G F (t=2)] , P<=0[ G F (t=1) ] )