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

Re: A refinement mapping using "callbacks"

Why does your CreateGossipMessage directly touch the message variable? Indeed, this may be problematic, as it makes the CreateGossipMsg constant a level-1 _expression_, and I don't think you'd even be able to pass it to an INSTANCE of Plumtree with a WITH clause, only externally through the TLC configuration (as, indeed you seem to be doing). A better approach -- so it would seem to me -- would be to change the line:

    /\ CreateGossipMsg(peer)

in the Plumtree module to:

    /\ message' = CreateGossipMsg(peer)

and have CreateUpdate "return" the message. However, then you'd lose the nondeterminstic creation of the message. This can be easily resolved with:

    /\ message' \in CreateGossipMsg(peer)

and having CreateGossipMsg return a set of possible messages.

Unrelated, I've noticed that in your configuration you use strings as some constant values (Prune, Graft, Peer). A model value may be a better fit for what you want. The problem with strings is that they cannot be tested for equality (or membership) with other, non-string sets (numbers, all forms of functions, explicit sets), while model values can be compared with anything.