Hi Ron,
1. I didn't know that about Strings, thanks for pointing it out.
2. Regarding your suggestion: I was thinking about returning a message as you described, but couldn't find a way to make it work. If CreateGossipMsg(peer) is the set of all possible gossip messages then it quickly becomes too big for TLC to calculate. This is, of course, a technical problem and not a theoretical limitation of the language. I just saw another thread by FL suggesting a change to the CHOOSE mechanism that avoids calculating the entire set just to select a suitable member in it, this sounds like pretty much the same issue:
https://tlaplus.codeplex.com/workitem/24
I intend to dive into the TLC code and see if I can contribute, this might be a good place for me to start.
Nira.