# Re: A refinement mapping using "callbacks"

On Tuesday, February 2, 2016 at 3:57:03 PM UTC+2, Nira Amit wrote:
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.

I don't think you need to return the set of *all* possible gossip messages. If your original spec was:

CreateUpdate(peer) == \E eid \in ENTITY_ID, v \in ENTITY_VAL:
message' = [message EXCEPT ![peer] =
[mtype |-> Gossip,
mid   |-> msgCounter,
mbody |-> CreateEntity(peer, eid, v),
msrc  |-> peer]]