Thanks the reference explains much of my confusion.
In process algebras, PA, process are in the eye of the beholder in as much as you can compute the observational equivalence of a set of communication processes with a single process. For finite state processes this can be done mechanically. None the less individual problems have explicitly or implicitly distinct processes for example the ABP has two processes the Sender and the Receiver which if all four were thought of as a single process there would be little need to use any communication channels.
So my intention was only to have four processes that I actually thought to be implicit in the question, the Sender, Receiver and the two communication Channels. I split each of these four into two processes not because I wanted to to but because I could not find a way of doing what you say can be done:
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.
In fact this is the crux of my confusion. I can find no way to do this.
At the moment this seems impossible give the how the either.. or .. command and the if .. then command work with component steps.
I need to be very careful here as non-determinism and fairness are defined very subtly differently in TLA+ and PA. I am not trying to say one is wrong and one right. The State Graph for fairSimple has a branch between two steps with the same name "myStart" in PA this would be called internal (or non-deterministic) choice whereas the State Graph for fairHacked has a branch between steps with different names "myLoop" and "myEnd" in PA this would be called external (or deterministic) choice. I believe that in TLA+ both are non-deterministic but have different fairness properties. So simply to distinguish them I will call them unfair choice and fair choice.
In PA we are forced to define fairness on processes we cannot define fairness on single actions (events) because we wish to analyse processes by hiding internal events and this can change which action exits a loop. In this sence TLA+ is certainly more expressive that PA.
I have attached a process simpleFair.tla with fair behaviour that loops forever and ignores the either branch that exits the loop. This is correct behaviour as the loop only appears to offer the myEnd step infinitely often whereas actually even in a fair execution myEnd need never be offered in the loop as can be seen from the State Graph.
I do not claim to have a detailed understanding of TLA+ or its internal working but have come up with a very tentative
alternative translation of either .. or.. that prevents fair behaviour from allowing the myEnd step being forever ignored.
This can be found in fairHacked.tla
I freely accept that I may have completely got the wrong end of the stick and there is a way to encode fair non-determinism in a single process.
kind regards david