Hi group,
I'm re-posing a question of mine that hasn't been answered (probably because it was too complex and long, so I'm trying again):
I have a modular spec describing a distributed repository built around the Plumtree* protocol (a flavor of a gossip protocol, see below). My problem is this: the Plumtree spec doesn't care about the message body, obviously, because the protocol is only concerned with having all the messages delivered to all peers. Yet the DistRepo spec needs to somehow "plug-in" message creation and processing into the protocol's behavior. So in order to achieve this, I defined a couple of constant operators in the Plumtree spec, that are assumed to create a message and to process it once received. Sort of "callbacks" to pass from the implementing spec. E.g:
------------------------------ MODULE Plumtree ------------------------------
...
\* An abstraction of gossip generation, which creates some gossip message with origin <peer> and
\* assignes it to message[peer].
\* For spec testing this is set to the TestCreateGossip(peer) operator
CONSTANT CreateGossipMsg(_)
...
\* Generate gossip and start spreading it
\* For simplicity, the gossip message is created and assigned to message[peer], and then sent over the network to localhost
GenerateGossip(peer) ==
/\ msgCounter <= MAX_MSG
/\ CreateGossipMsg(peer) \* sets message[peer] to the new gossip message
/\ Send( message'[peer], peer, peer ) \* gossip is sent to localhost
/\ msgCounter' = msgCounter + 1
/\ UNCHANGED <<pc, receivedUpdates, eagerPushPeers, lazyPushPeers, missingUpdateSrcs, timers, recipient>>
...
-------------------------- MODULE DistributedRepo --------------------------
...
\* The CreateGossipMsg implementation
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]]
...
So this works fine - TLC verifies the implementation and that the system indeed reaches consistency - but doesn't look very "elegant" to me. As a software developer it bothers me that this doesn't follow object-oriented principles where one module should not have to be aware of another one's inner state (here DistRepo has to know about the Plumtree's 'message' inner variable). On the other hand, I understand that specs are about discovering design flaws and verifying behaviors, not code modularity. So there's only so much abstraction one can expect (or want). I just wonder if there is a "cleaner" way to achieve this sort of spec interaction, that I'm not aware of. Would any of you have taken a different approach?
The full specs are attached, as well as a screenshot of the model configuration I used for testing.
* The Plumtree protocol is a self-healing broadcast tree embedded in a gossip-based overlay.
From the paper (http://homepages.gsd.inesc-id.pt/~jleitao/pdf/srds07-leitao.pdf): "The broadcast tree in created and maintained using a low cost algorithm, described in the paper. Broadcast is achieved mainly by using push gossip on the tree branches. However, the remaining links of the gossip-based overlay are also used to propagate the message using a lazy-push approach. The lazy-push steps ensure high reliability (by guaranteeing that, in face of failures, the protocol falls back to a pure gossip approach) and, additionally, also provide a way to quickly heal the broadcast tree".
