This works and I like it better than the way I had written this, but it still involves DistRepo setting an internal variable of spec Plumtree (message). Maybe I'm just confused about the syntax but here's what I'd like to do and don't see how:
GenerateGossip(peer) ==
/\ msgCounter <= MAX_MSG
/\ message' = [message EXCEPT ![peer] =
[mtype |-> Gossip,
mid |-> msgCounter,
mbody |-> <GET ME A RANDOM MESSAGE BODY>,
msrc |-> peer]]
/\ Send( message'[peer], peer, peer ) \* gossip is sent to localhost
/\ msgCounter' = msgCounter + 1
/\ UNCHANGED <<pc, receivedUpdates, eagerPushPeers, lazyPushPeers, missingUpdateSrcs, timers, recipient>>
Do you see a way to do this? Actually even CHOOSE won't help me here because it is deterministic, and I want a (possibly) different message in different behaviors.
Nira.