No me queda claro el problema a resolver.
Trato de llevar el problema a las definiciones del libro,
Donde un problema es una terna P = <P_init, P_final, R>, y es correcto si existe t > 0 : Correct(t), es decir si existe t : para todo t' > t, se cumple P_final(t').
¿Cual sería una condición P_final para decir que "la comunicación half-duplex terminó correctamente"?
Había pensado en definir el problema como el de lograr que dos entidades A y B logren enviar un mensaje sin que estos choquen y que luego de enviar un mensaje exitosamente pasen a un estado de finalización.
Y que P_final sea que estado(A) = estado(B) = finalizado.
Capaz no estoy entendiendo el objetivo del ejercicio, agradezco ayuda.
Otra duda, ¿alguna chance de que la hora de entrega sea hasta mañana a la noche?