Throughout V/S s_until_with

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]);