Re: A refinement mapping using "callbacks"

[Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>]

In Plumtree:

    /\ message' \in { [message EXCEPT ![peer] = msg] : msg \in GenerateGossip }

In the other module:

     CreateUpdate(peer) == { [mtype |-> Gossip, 

                                                    mid   |-> msgCounter, 

                                                 mbody |-> CreateEntity(peer, eid, v),

                                                   msrc  |-> peer]

                                           : eid \in ENTITY_ID, v \in ENTITY_VAL }

Now there's no access to message (sorry I confused you before). The same "randomness" (really nondeterminism) you had before is preserved now.