as Leslie once observed, processes are in the eye of the beholder . I am not sure I get your remark about using a separate process for dropping packets: aren't you doing the same with your two processes dataChannel and dropChannel? But certainly you could combine the two into a single process that non-deterministically chooses between transmitting and dropping a message. You would then add a (strong) fairness condition on the subaction that corresponds to data transmission.
 http://lamport.azurewebsites.net/pubs/pubs.html#lamport-eye-of-beholder, with an explicit reference to process algebra--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.