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

Re: A refinement mapping using "callbacks"

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:

In spec Plumtree:

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.
Thanks again,