In this section we give an example of a simple distributed dataset in which each agent in a collection of data agents manages a local version of a global data dictionary that maps keys to values. An agent may only have part of the data locally, and must contact other agents to get the value of a key that is not in its local version. To simplify the presentation, we assume that data agents work in pairs.
This example illustrates one way of representing request-reply style of object-based programming in Maude, and also a way of representing information about the state of the task an object is working on when it needs to make one or more requests to other objects in order to answer a request itself. As in the ticker example, we define a uniform syntax for messages. Here, messages have both a receiver and a sender in addition to a message body, and are constructed with the msg constructor. The technique for maintaining task information is to define a sort Request and a requests attribute that holds the set of pending requests. The constant empty indicates that an object has no pending request. The request w4(O:Oid, C:Oid, MB:MsgBody) indicates that the object is processing a message from C:Oid with body MB:MsgBody and is waiting for a message from O:Oid.
The module DATA-AGENTS-CONF extends CONFIGURATION with the uniform message syntax and the specification of the sort Request.
mod DATA-AGENTS-CONF is
ex CONFIGURATION .
*** my msg syntax
sort MsgBody .
op msg : Oid Oid MsgBody -> Msg [ctor message] .
*** agents may be pending on requests
sort Request .
op w4 : Oid Oid MsgBody -> Request [ctor] .
endm
A data agent stores a dictionary, mapping keys to data elements. To specify such dictionaries, we use the predefined parameterized module MAP (see Section 7.13), renaming the main sort as well as the lookup and update operators as follows:
MAP{K, V} * (sort Map{K, V} to Dict{K, V},
op _[_] to lookup,
op insert to update) .
Remember that the constant undefined is the result returned by the lookup operators when the map is not defined on the given key.
We split the specification of data agents into two modules: the parameterized functional module DATA-AGENTS-INTERFACE, which defines the interface, and the parameterized system module DATA-AGENTS , which gives the rules for agent behavior. This illustrates a technique for modularizing object-based system specifications in order to allow the same interface to be shared by more than one ``implementation'' (rule set). We already applied this technique in the specification of a vending machine as a system module in Section 5.1. Notice also that DATA-AGENTS-CONF is imported in extending mode, because we add data to the old sorts, but without making further identifications (the interface module has no equation).
mod DATA-AGENTS-INTERFACE{K :: TRIV, V :: TRIV} is
ex DATA-AGENTS-CONF .
*** messages
op getReq : K$Elt -> MsgBody [ctor] .
op getReply : K$Elt [V$Elt] -> MsgBody [ctor] .
op setReq : K$Elt V$Elt -> MsgBody [ctor] .
op setReply : K$Elt [V$Elt] -> MsgBody [ctor] .
op tellReq : K$Elt V$Elt -> MsgBody [ctor] .
op tellReply : K$Elt V$Elt -> MsgBody [ctor] .
op lookupReq : K$Elt -> MsgBody [ctor] .
op lookupReply : K$Elt [V$Elt] -> MsgBody [ctor] .
endm
In a request-reply style of interaction, message body constructors come in pairs. For example, (lookupReq, lookupReply) and (tellReq, tellReply) are the message body pairs used when a customer interacts with a data agent in order to access and set data values. Similarly, (getReq, getReply) and (setReq, setReply) constitute the message body pairs for an agent to access and set data values from a pal.
A data agent has class identifier DataAgent. In addition to the requests attribute, each data agent has a data attribute holding the agent's local version of the data dictionary, and a pal attribute holding the identifier of the other agent. If sam and joe are collaborating data agents, then their initial state might look like
< sam : DataAgent | data : empty, pal : joe, requests : empty > < joe : DataAgent | data : empty, pal : sam, requests : empty >
The module DATA-AGENTS specifies a data agent's behavior by giving a rule for handling each type of message it expects to receive (other messages will simply be ignored).
Since we are adding rules acting on the sort Configuration, coming from the CONFIGURATION module via DATA-AGENTS-CONF, we need to make explicit that such modules are imported in including mode. We also import in protecting mode the predefined parameterized module SET, instantiated with the following Request view, to define the sets of requests stored in the requests attribute.
view Request from TRIV to DATA-AGENTS-CONF is
sort Elt to Request .
endv
mod DATA-AGENTS{K :: TRIV, V :: TRIV} is
inc DATA-AGENTS-INTERFACE{K, V} .
inc DATA-AGENTS-CONF .
inc CONFIGURATION .
pr MAP{K, V} * (sort Map{K, V} to Dict{K, V},
op _[_] to lookup,
op insert to update) .
pr SET{Request} .
vars A O C : Oid .
var D : Dict{K, V} .
var Key : K$Elt .
vars Val Val' : [V$Elt] .
var Atts : AttributeSet .
var RS : Set{Request} .
*** class structure
op DataAgent : -> Cid [ctor] .
op data :_ : Dict{K, V} -> Attribute [ctor] .
op pal :_ : Oid -> Attribute [ctor] .
op requests :_ : Set{Request} -> Attribute [ctor] .
*** lookup request
rl [lookup] :
< A : DataAgent | data : D, pal : O, requests : RS >
msg(A, C, lookupReq(Key))
=> if lookup(D, Key) == undefined
then < A : DataAgent | data : D, pal : O,
requests : (RS, w4(O, C, lookupReq(Key))) >
msg(O, A, getReq(Key))
else < A : DataAgent | data : D, pal : O, requests : RS >
msg(C, A, lookupReply(Key, lookup(D, Key)))
fi .
*** lookup request missing data from pal
rl [getReq] :
< A : DataAgent | data : D, pal : O, Atts >
msg(A, O, getReq(Key))
=> < A : DataAgent | data : D, pal : O, Atts >
msg(O, A, getReply(Key, lookup(D, Key))) .
*** receive lookup requested missing data from pal
rl [getReply] :
< A : DataAgent | data : D, pal : O,
requests : (RS, w4(O, C, lookupReq(Key))) >
msg(A, O, getReply(Key, Val))
=> < A : DataAgent | pal : O, requests : RS,
data : if Val == undefined
then D
else update(Key, Val, D)
fi >
msg(C, A, lookupReply(Key, Val)) .
*** tell request
rl [tell] :
< A : DataAgent | data : D, requests : RS, pal : O >
msg(A, C, tellReq(Key, Val))
=> if lookup(D, Key) == undefined
then < A : DataAgent |
data : D,
requests : (RS, w4(O, C, tellReq(Key, Val))),
pal : O >
msg(O, A, setReq(Key, Val))
else < A : DataAgent | data : update(Key, Val, D),
requests : RS, pal : O >
msg(C, A, tellReply(Key, Val))
fi .
*** request update for missing data from pal
rl [setReq] :
< A : DataAgent | data : D, pal : O, Atts >
msg(A, O, setReq(Key, Val))
=> if lookup(D, Key) == undefined
then < A : DataAgent | data : D, pal : O, Atts >
msg(O, A, setReply(Key, undefined))
else < A : DataAgent | data : update(Key, Val, D),
pal : O, Atts >
msg(O, A, setReply(Key, Val))
fi .
*** receive requested update for missing data from pal
rl [setReply] :
< A : DataAgent | data : D, pal : O,
requests : (RS, w4(O, C, tellReq(Key, Val))) >
msg(A, O, setReply(Key, Val'))
=> < A : DataAgent | pal : O, requests : RS,
data : if Val' == undefined
then update(Key, Val, D)
else D
fi >
msg(C, A, tellReply(Key, Val)) .
endm
The rule labeled lookup specifies how an agent handles a
lookupReq message. The agent first looks to see if its local
dictionary contains the requested entry. If lookup(D, Key) ==
undefined, then a getReq is sent to the pal and the agent
waits for a reply, remembering the pending lookup request
(w4(O, C, lookupReq(Key))).
If the agent has the requested entry, then it is returned in a
lookupReply message.
The rules labeled getReq and getReply specify how agents
exchange dictionary entries. An agent can always answer a getReq
message, since the Atts variable will match any status attribute. The
agent simply replies with the result, possibly undefined, of looking up
the requested key in its local dictionary. An agent only expects a
getReply message if it has made a request, and this only happens if
the agent is trying to handle a lookupReq message. Thus the rule only
matches if the agent has the appropriate request w4(O, C, lookupReq(Key))
in its requests attribute.
The agent records the received reply with update(Key, Val, D) when
this reply is not undefined, and in any case
sends it on to the customer with the message msg(C, A, lookupReply(Key, Val)).
The rules labeled tell, setReq, and setReply specify how an agent handles a tellReq message, following a protocol similar to the one described for the lookup request.
Note that in the case of agents with just these three attributes, using the
Atts variable of sort AttributeSet or the
requests : RS
expression, with RS a variable of sort Set{Request},
are equivalent ways of saying that the rule matches any set of requests. The
first way is more extensible, in that the rule would still work for agents
belonging to a subclass of DataAgent that uses additional attributes.
To test the data agent specification, we define a module AGENT-TEST. This module defines object identifiers sam and joe for data agents, and me to name an external customer. It also defines an initial configuration containing two agents named sam and joe with empty data dictionaries, and two initial tellReq messages for each agent. We take both keys and data elements to be quoted identifiers, by instantiating the parameterized DATA-AGENTS module with the predefined Qid view.
mod AGENT-TEST is
ex DATA-AGENTS{Qid, Qid} .
ops sam joe me : -> Oid [ctor] .
op iconf : -> Configuration .
eq iconf
= < sam : DataAgent | data : empty,
pal : joe, requests : empty >
msg(sam, me, tellReq('a, 'bc))
msg(sam, me, tellReq('d, 'ef))
< joe : DataAgent | data : empty,
pal : sam, requests : empty >
msg(joe, me, tellReq('g, 'hi))
msg(joe, me, tellReq('j, 'kl)) .
endm
The importation graph of all the modules involved in this example is shown in Figure 8.3, where the three different types of arrows correspond to the three different modes of importation.
The following are results from test runs. First we rewrite the initial configuration iconf, resulting in a configuration in which the agents have updated appropriately their data, and there is one reply for each tellReq message.
Maude> rew iconf .
result Configuration:
< sam : DataAgent | data : ('a |-> 'bc, 'd |-> 'ef),
pal : joe, requests : empty >
< joe : DataAgent | data : ('g |-> 'hi, 'j |-> 'kl),
pal : sam, requests : empty >
msg(me, sam, tellReply('a, 'bc))
msg(me, sam, tellReply('d, 'ef))
msg(me, joe, tellReply('g, 'hi))
msg(me, joe, tellReply('j, 'kl))
Next we try adding a lookup request and discover that, using Maude's default rewriting strategy, the lookup request is delivered before the tell requests, so the reply is undefined.
Maude> rew iconf msg(sam, me, lookupReq('a)) .
result Configuration:
< sam : DataAgent | data : ('a |-> 'bc, 'd |-> 'ef),
pal : joe, requests : empty >
< joe : DataAgent | data : ('g |-> 'hi, 'j |-> 'kl),
pal : sam, requests : empty >
msg(me, sam, tellReply('a, 'bc))
msg(me, sam, tellReply('d, 'ef))
msg(me, sam, lookupReply('a, undefined))
msg(me, joe, tellReply('g, 'hi))
msg(me, joe, tellReply('j, 'kl))
To see if a good answer can be obtained, we use the search command to look for a state in which there is a lookupReply with data entry different from undefined.
Maude> search iconf msg(sam, me, lookupReq('a))
=>! msg(me, sam, lookupReply('a, Q:Qid)) C:Configuration .
Solution 1 (state 1081)
C:Configuration -->
< sam : DataAgent | data : ('a |-> 'bc, 'd |-> 'ef),
pal : joe, requests : empty >
< joe : DataAgent | data : ('g |-> 'hi, 'j |-> 'kl),
pal : sam, requests : empty >
msg(me, sam, tellReply('a, 'bc))
msg(me, sam, tellReply('d, 'ef))
msg(me, joe, tellReply('g, 'hi))
msg(me, joe, tellReply('j, 'kl))
Q:Qid --> 'bc
No more solutions.
Indeed, there is just one such reply.
Notice that two collaborating agents may get inconsistent data, that is, different values for the same key, if they receive simultaneously tell requests for the same key. We may use the search command to illustrate how this may happen.
Maude> search iconf
msg(sam, me, tellReq('m, 'no))
msg(joe, me, tellReq('m, 'pq))
=>! C:Configuration
< sam : DataAgent |
data : ('m |-> Q:Qid, R:Dict{Qid, Qid}),
Atts:AttributeSet >
< joe : DataAgent |
data : ('m |-> Q':Qid, R':Dict{Qid, Qid}),
Atts':AttributeSet >
such that Q:Qid =/= Q':Qid .
Solution 1 (state 5117)
C:Configuration -->
msg(me, sam, tellReply('a, 'bc))
msg(me, sam, tellReply('d, 'ef))
msg(me, sam, tellReply('m, 'no))
msg(me, joe, tellReply('g, 'hi))
msg(me, joe, tellReply('j, 'kl))
msg(me, joe, tellReply('m, 'pq))
Atts:AttributeSet --> pal : joe, requests : empty
R:Dict{Qid,Qid} --> 'a |-> 'bc, 'd |-> 'ef
Q:Qid --> 'no
Atts':AttributeSet --> pal : sam, requests : empty
R':Dict{Qid,Qid} --> 'g |-> 'hi, 'j |-> 'kl
Q':Qid --> 'pq
No more solutions.
Note the use of the such that condition to filter search solutions (see Section 5.4.3 and 16.4).