Thanks for your reply Stephan.
Your AlternatingBit.tla solution is not one I would have thought of and I will need more time to consider how you came to it. The two key ideas I lacked were (1) placing the dropping of packets in a separate process and (2) writing more sophisticated fairness conditions. I mistakenly thought only single steps could be used in fairness conditions - I am still not thinking of everything being a logical statement.
I know there are significant differences between process algebras and TLA+. But, I normally get students to sketch out a state graph of the individual process they want to model - it is then mechanical to translate finite state graphs into process algebra. For teaching purposes I have been trying to follow (find) a similar approach in TLA+. So my first step would be to isolate the required processes, Sender, Receiver and FaultyChannel. Your TLA+ solution although much neater than mine has introduced a separate process for dropping packets. I will try to adopt your more sophisticated fairness conditions while avoiding the use of the separate process for dropping packets. Or do you know is the additional process needed in TLA+ order to specify the fairness conditions?
I am still unsure how to define fairness in my modular version of ABP but will check if I can get a more sophisticated fairness condition to parse where I have failed to get what I thought of as simple conditions to parse.
Again many thanks - I am finally getting a sense of understanding TLA+