Hi Ron,
It works! Thanks!!
So to sum it up: my problem was that I couldn't find a way to blindly select a gossip message-body from within the Plumtree module when it is implemented by another spec. Declaring the body to be \in the constant set of all possible message bodies would result in calculating this set, which can be very big. But it was actually possible to narrow down the set of relevant message bodies substantially.
This is probably not a silver-bullet solution for all such cases, but for now I have my spec nicely broken down into fairly independent modules, so I'm happy :-)
For reference, I'm adding here a summery of the changes and attaching the modified specs:
In module Plumtree:
...
\* The set of possible message bodies for gossip-messages with origin <peer>
\* For spec testing this is set to the MBody constant for all peers
CONSTANT GossipMsgBody(_)
ASSUME \A p \in Peer: GossipMsgBody(p) \in SUBSET(MBody)
...
\* The set of possible gossip messages with origin <peer>
GossipMsg(peer) == { [mtype |-> Gossip,
mid |-> msgCounter,
mbody |-> body,
msrc |-> peer]
: body \in GossipMsgBody(peer) }
...
\* Generate gossip and start spreading it
\* For simplicity, the gossip message is created and assigned to message[peer], and then sent over the network to localhost
GenerateGossip(peer) ==
/\ msgCounter <= MAX_MSG
/\ message' \in { [message EXCEPT ![peer] = msg] : msg \in GossipMsg(peer) }
/\ Send( message'[peer], peer, peer ) \* gossip is sent to localhost
/\ msgCounter' = msgCounter + 1
/\ UNCHANGED <<pc, receivedUpdates, eagerPushPeers, lazyPushPeers, missingUpdateSrcs, timers, recipient>>
...
And in module DistributedRepo:
...
\* The GossipMsgBody implementation
CreateUpdate(peer) == { CreateEntity(peer, eid, v)
: eid \in ENTITY_ID, v \in ENTITY_VAL }
