[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: A refinement mapping using "callbacks"

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.