In reply to hisingh:
!($rose(read) && (readID == prev_ID )) s_until_with
($rose(readAck) && readAckID == prev_ID );
// IS eauivalent to
strong( !($rose(read) && (readID == prev_ID)) throughout
($rose(readAck) && readAckID == prev_ID) [->1]);