Why does your CreateGossipMessage directly touch the message variable? Indeed, this may be problematic, as it makes the CreateGossipMsg constant a level-1 _expression_, and I don't think you'd even be able to pass it to an INSTANCE of Plumtree with a WITH clause, only externally through the TLC configuration (as, indeed you seem to be doing). A better approach -- so it would seem to me -- would be to change the line:
/\ CreateGossipMsg(peer)
in the Plumtree module to:
/\ message' = CreateGossipMsg(peer)
and have CreateUpdate "return" the message. However, then you'd lose the nondeterminstic creation of the message. This can be easily resolved with:
/\ message' \in CreateGossipMsg(peer)
and having CreateGossipMsg return a set of possible messages.
Unrelated, I've noticed that in your configuration you use strings as some constant values (Prune, Graft, Peer). A model value may be a better fit for what you want. The problem with strings is that they cannot be tested for equality (or membership) with other, non-string sets (numbers, all forms of functions, explicit sets), while model values can be compared with anything.
Ron