Chapter 8
Object-Based Programming

Distributed systems can be naturally modeled in Maude as multisets of entities, loosely coupled by some suitable communication mechanism. An important example is object-based distributed systems in which the entities are objects, each with a unique identity, and the communication mechanism is message passing.

Core Maude supports the modeling of object-based systems by providing a predefined module CONFIGURATION that declares sorts representing the essential concepts of object, message, and configuration, along with a notation for object syntax that serves as a common language for specifying object-based systems. In addition, there is an object-message fair rewriting strategy that is well suited for executing object system configurations. To specify an object-based system, the user can import CONFIGURATION and then define the particular objects, messages, and rules for interaction that are of interest. In addition to simple asynchronous message passing, Maude also supports complex patterns of synchronous interaction that can be used to model higher-level communication abstractions. The user is also free to define his/her own notation for configurations and objects, and can still take advantage of the object-message rewriting strategy, simply by making the appropriate declarations. All this is explained in detail below.

Furthermore, Maude also supports external objects, so that objects inside a Maude configuration can interact with different kinds of objects outside it. At present, the external objects directly supported are internet sockets; but through them it is possible to interact with other external objects. In addition, sockets make possible distributed programming with rewrite rules. External objects are discussed in Section 9.

As discussed in Chapter 22, Full Maude provides additional support for object-oriented programming with classes, subclassing, and convenient abbreviations for rule syntax.

8.1 Configurations

The predefined module CONFIGURATION in the file prelude.maude provides basic sorts and constructors for modeling object-based systems.

*** basic object system sorts
sorts Object Msg Configuration .

*** construction of configurations
subsort Object Msg < Configuration .
op none : -> Configuration [ctor] .
op __ : Configuration Configuration -> Configuration
[ctor config assoc comm id: none] .

The basic sorts needed to describe an object system are: Object, Msg (messages), and Configuration. A configuration is a multiset of objects and messages that represents (a snapshot of) a possible system state. Configurations are formed by multiset union (represented by empty syntax, __) starting from singleton objects and messages. The empty configuration is represented by the constant none. The attribute config declares that configurations constructed with __ support the special object-message fair rewriting behavior (see Section 8.2).

A typical configuration will have the form

Ob-1 ... Ob-k Mes-1 ... Mes-n

where Ob-1, …, Ob-k are objects, Mes-1, …, Mes-n are messages, and the order is immaterial.

In general, a rewrite rule for an object system has the form

rl Ob-1 ... Ob-k Mes-1 ... Mes-n
=> Ob’-1 ... Ob’-j Ob-k+1 ... Ob-m Mes’-1 ... Mes’-p .

where Ob’-1, …, Ob’-j are updated versions of Ob-1, …, Ob-j for j k, Ob-k+1, …, Ob-m are newly created objects, and Mes’-1, …, Mes’-p are new messages. An important special case are rules with a single object and at most one message on the lefthand side. These are called asynchronous rules. They directly model asynchronous distributed interactions. Rules involving multiple objects are called synchronous; they are used to model higher-level communication abstractions.

The user is free to define any object or message syntax that is convenient. However, for uniformity in identifying objects and message receivers, the adopted convention is that the first argument of an object or message constructor should be an object’s name. This facilitates defining object system rewriting strategies independently of the particular choice of syntax and is essential for using Maude’s object-message fair rewriting strategy.

The remainder of the CONFIGURATION module provides an object syntax that serves as a common notation that can be used by developers of object-based system specifications. This syntax is also used by Full Maude (see Chapter 22). For this purpose four new sorts are introduced: Oid (object identifiers), Cid (class identifiers), Attribute (a named element of an object’s state), and AttributeSet (multisets of attributes). Further details about the CONFIGURATION module are discussed later in Section 9.

*** Maude object syntax
sorts Oid Cid .
sorts Attribute AttributeSet .
subsort Attribute < AttributeSet .
op none : -> AttributeSet [ctor] .
op _,_ : AttributeSet AttributeSet -> AttributeSet
[ctor assoc comm id: none] .
op <_:_|_> : Oid Cid AttributeSet -> Object [ctor object] .

In this syntax, objects have the general form

< O : C | att-1, ..., att-k >

where O is an object identifier, C is a class identifier, and att-1, …, att-k are the object’s attributes. Attribute sets are formed from singleton attributes by a multiset union operator _,_ with identity none (the empty multiset). The object attribute in the <_:_|_> operator declares that objects made with this constructor have object-message fair rewriting behavior (see Section 8.2).

Although the user is free to define the syntax of elements of sort Attribute according to taste, we will follow the standard Maude notation in most of our examples. The module BANK-ACCOUNT illustrates the use of the Maude object syntax to define simple bank account objects. Note that by defining the attribute bal with syntax bal :_ we are able to write account objects as < A : Account | bal : N >.

protecting INT .
op Account : -> Cid [ctor] .
op bal :_ : Int -> Attribute [ctor gather (&)] .
ops credit debit : Oid Nat -> Msg [ctor] .
vars A B : Oid .
vars M N N : Nat .

rl [credit] :
< A : Account | bal : N >
credit(A, M)
=> < A : Account | bal : N + M > .

crl [debit] :
< A : Account | bal : N >
debit(A, M)
=> < A : Account | bal : N - M >
if N >= M .

The class identifier for bank account objects is Account. Each account object has a single attribute named bal of sort Nat (the account balance). There are two message constructors credit and debit, each taking an object identifier (the receiver) and a number (the amount to credit or debit). The rule labeled credit describes the processing of a credit message and the rule labeled debit describes the processing of a debit message. Suppose that constants A-001, A-002, and A-003 of sort Oid have been declared. Then, the following is an example of a bank account configuration.

< A-001 : Account | bal : 300 >
< A-002 : Account | bal : 250 >
< A-003 : Account | bal : 1250 >
debit(A-001, 200)
debit(A-002, 400)
debit(A-003, 300)
credit(A-002, 300)

Note that the messages debit(A-001, 200) and debit(A-003, 300) can be delivered concurrently, either before or after the other messages. However, the message debit(A-002, 400) cannot be delivered until after credit(A-002, 300) has been delivered, due to the balance condition for the debit rule.

The credit and debit rules are examples of asynchronous message passing rules involving one object and one message on the lefthand side. In these examples no new objects are created and no new messages are sent.

In order to combine the debit(A-003, 300) and credit(A-002, 300) messages so that the delivery of these two messages becomes a single atomic transaction, we could define a new message constructor from_to_transfer_. The rule for handling a transfer message involves the joint participation of two bank accounts in the transfer, as well as the transfer message. This is an example of a synchronous rule.

op from_to_transfer_ : Oid Oid Nat -> Msg [ctor] .
crl [transfer] :
(from A to B transfer M)
< A : Account | bal : N >
< B : Account | bal : N >
=> < A : Account | bal : N - M >
< B : Account | bal : N + M >
if N >= M .

Now we could replace

debit(A-003, 300) credit(A-002,300)


from A-003 to A-002 transfer 300

in the example configuration. The module BANK-ACCOUNT-TEST declares the object identifiers introduced above and defines a configuration constant bankConf.

ops A-001 A-002 A-003 : -> Oid .
op bankConf : -> Configuration .
eq bankConf
= < A-001 : Account | bal : 300 >
debit(A-001, 200)
debit(A-001, 150)
< A-002 : Account | bal : 250 >
debit(A-002, 400)
< A-003 : Account | bal : 1250 >
(from A-003 to A-002 transfer 300) .

From the specification we see that only one of the debit messages for A-001 can be processed. Using the default rewriting strategy we find that the message debit(A-001, 150) is processed first in this strategy.

Maude> rew in BANK-ACCOUNT-TEST : bankConf .
result Configuration:
debit(A-001, 200)
< A-001 : Account | bal : 150 >
< A-002 : Account | bal : 150 >
< A-003 : Account | bal : 950 >

We use the search command to confirm that it is possible to process the message debit(A-001, 200) as well, where the =>! symbol indicates that we are searching for states reachable from bankConf that cannot be further rewritten (see Sections 5.4.3 and 23.4).

Maude> search bankConf =>! C:Configuration debit(A-001, 150) .
search in BANK-ACCOUNT-TEST : bankConf
=>! C:Configuration debit(A-001, 150) .

Solution 1 (state 8)
states: 9 rewrites: 49 in 0ms cpu (0ms real) (~ rews/sec)
C:Configuration --> < A-001 : Account | bal : 100 >
< A-002 : Account | bal : 150 >
< A-003 : Account | bal : 950 >

No more solutions.
states: 9 rewrites: 49 in 0ms cpu (0ms real) (~ rews/sec)

The BANK-MANAGER module below illustrates asynchronous message passing with object creation.

op Manager : -> Cid [ctor] .
op new-account : Oid Oid Nat -> Msg [ctor] .
vars O C : Oid .
var N : Nat .
rl [new] :
< O : Manager | none >
new-account(O, C, N)
=> < O : Manager | none >
< C : Account | bal : N > .

To open a new account, one sends a message to the bank manager with the account name and initial balance, for example, new-account(A-000, A-004, 100). Of course, in a real system more care would be needed to assure unique account identities. To see the bank manager in action, we define the following module.

ops A-001 A-002 A-003 A-004 : -> Oid .
op mgrConf : -> Configuration .
eq mgrConf
= < A-001 : Account | bal : 300 >
< A-004 : Manager | none >
new-account(A-004, A-002, 250)
new-account(A-004, A-003, 1250) .

Then, we rewrite the configuration mgrConf:

Maude> rew in BANK-MANAGER-TEST : mgrConf .
result Configuration:
< A-001 : Account | bal : 300 >
< A-002 : Account | bal : 250 >
< A-003 : Account | bal : 1250 >
< A-004 : Manager | none >

The relationships between all the modules involved in this example are illustrated in Figure 8.1, where the different types of arrows correspond to the different modes of importation: single arrow for including, double arrow for extending, and triple arrow for protecting.


Figure 8.1:Importation graph of bank modules

The examples above illustrate object-based programming in Maude using the common object syntax. Notice that message constructors obey the “first argument is an object identifier” convention. Alternative object syntax is also possible, by defining an associative and commutative configuration constructor and suitable object and message syntax. It is of course also possible not to use the config attribute when defining the multiset union operator, but this will prevent taking advantage of object-message fair rewriting (see Section 8.2). As an example (not using for the moment the config attribute, to illustrate different forms of rewriting with objects), we model a ticker, the classic example of an actor [1132]. First we specify the configurations, objects, and messages of the actor world in the module ACTOR-CONF. Actor configurations (of sort AConf) are multisets of actors (of sort Actor) and messages (of sort Msg). Messages are constructed uniformly from an actor identifier and a message body. Thus we introduce sorts Aid (actor identifier) and MsgBody, and a message constructor _<|_.

sorts Actor Msg AConf .
subsorts Actor Msg < AConf .
op none : -> AConf [ctor] .
op __ : AConf AConf -> AConf [ctor assoc comm id: none] .
*** actor messages
sorts Aid MsgBody .
op _<|_ : Aid MsgBody -> Msg [ctor] .

A ticker maintains a counter that it updates in response to a tick message. Ticker(T:Aid, N:Nat) is an actor with identifier T:Aid and counter value N:Nat. The ticker sends the current value of its counter in response to a timeReq message.

mod TICKER is
including ACTOR-CONF .
protecting NAT .
op Ticker : Aid Nat -> Actor [ctor] .
op tick : -> MsgBody [ctor] .
op timeReq : Aid -> MsgBody [ctor] .
op timeReply : Nat -> MsgBody [ctor] .

vars T C : Aid .
var N : Nat .
rl Ticker(T, N) (T <| tick)
=> Ticker(T, s N) (T <| tick) .
rl Ticker(T, N) (T <| timeReq(C))
=> Ticker(T, N) (C <| timeReply(N)) .

To test the ticker we define actor identifiers for the ticker, myticker, a customer, me, and an initial configuration with one ticker, one tick message, and a timeReq message from me.

extending TICKER .
ops myticker me : -> Aid [ctor] .
op tConf : -> AConf .
eq tConf
= Ticker(myticker, 0)
(myticker <| tick)
(myticker <| timeReq(me)) .

If we ask Maude to rewrite the configuration tConf without placing an upper bound on the number of rewrites, Maude will go on forever. This is because there will always be a tick message in the configuration, and the ticker can always process this message. Thus we rewrite with an upper bound of, say, 10 rewrites.

Maude> rew [10] tConf .
rewrite [10] in TICKER-TEST : tConf myticker <| timeReq(me) .
result AConf:
(myticker <| tick) (me <| timeReply(1)) Ticker(myticker, 9)

We see that the timeReq message was processed after just one tick was processed.

An interesting property of this configuration is that the reply to the timeReq message can contain an arbitrarily large natural number, since any number of ticks could be processed before the timeReq. For particular numbers this can be checked using the search command.

Maude> search [1] tConf =>+ tc:AConf me <| timeReply(100) .
search [1] in TICKER-TEST :
tConf =>+ tc:AConf me <| timeReply(100) .

Solution 1 (state 5152)
states: 5153 rews: 5153 in 0ms cpu (285ms real)(~ rews/sec)

tc:AConf --> (myticker <| tick) Ticker(myticker, 100)

Notice that we used the search relation =>+ (one or more steps) rather than =>! (terminating rewrites) since there are no terminal configurations starting from tConf. Moreover, we have searched only for the first ([1]) solution.

There are two important considerations regarding object systems that are not illustrated by the preceding examples: uniqueness of object names and fairness of message delivery. To illustrate some of the issues we elaborate the ticker example by defining a ticker factory that creates tickers, and a ticker-customer. The ticker factory accepts requests for new tickers newReq(c) where c is the customer’s name. When such a request is received, a ticker is created and its name is sent to the requesting customer (newReply(o(a, i))). To make sure that each ticker has a fresh (unused) name, the ticker factory keeps a counter. It generates ticker names of the form o(a, i), where a is the factory name and i is the counter value. The counter is incremented each time a ticker is created. This is just one possible method for assuring unique names for dynamically created objects. If objects are only created by factories that use the above method for generating names, then starting from a configuration of objects with unique names (not of the form o(a, i)) the unique name property will be preserved.

inc TICKER .
op TickerFactory : Aid Nat -> Actor [ctor] .
ops newReq newReply : Aid -> MsgBody [ctor] .
op o : Aid Nat -> Aid [ctor] .

vars A C : Aid .
vars I J : Nat .
rl [newReq] :
TickerFactory(A, I) (A <| newReq(C))
=> TickerFactory(A, s I) (C <| newReply(o(A, I)))
Ticker(o(A, I), 0) (o(A, I) <| tick) .

A ticker customer knows the name of a ticker factory. It asks for a ticker, waits for a reply, asks the ticker for the time, waits for a reply, increments its reply counter (used just for the user to monitor customer service) and repeats this process.

ops Cust Cust1 Cust2 : Aid Aid Nat -> Actor [ctor] .

vars C TF T : Aid .
vars N M : Nat .

rl [req] :
Cust(C, TF, N)
=> Cust1(C, TF, N) (TF <| newReq(C)) .

rl [newReply] :
Cust1(C, TF, N) (C <| newReply(T))
=> Cust2(C, TF, N) (T <| timeReq(C)) .

rl [timeReply] :
Cust2(C, TF, N) (C <| timeReply(M))
=> Cust(C, TF, s N) .

Now we define a test configuration with a ticker factory and two customers. The importation graph of all the modules involved at this point is shown in Figure 8.2.


Figure 8.2:Importation graph of ticker modules

ops tf c1 c2 : -> Aid [ctor] .
ops ic1 ic2 : -> AConf .
eq ic1 = TickerFactory(tf, 0) Cust(c1, tf, 0) .
eq ic2 = ic1 Cust(c2, tf, 0) .

Rewriting this configuration using the rewrite command with a bound of 40 results in one ticker being created, and ticking away, while customer c2 is not given an opportunity to execute at all.

Maude> rew [40] ic2 .
rewrite [40] in TICKER-FACTORY-TEST : ic2 .
rewrites: 42 in 0ms cpu (0ms real) (~ rewrites/second)
result AConf:
(o(tf, 0) <| tick)
Ticker(o(tf, 0), 35) TickerFactory(tf, 1)
Cust(c1, tf, 1) Cust(c2, tf, 0)

In contrast, rewriting using the frewrite strategy with the same bound of 40, several tickers are created, however only the first one gets tick messages delivered.

Maude> frew [40] ic2 .
frewrite [40] in TICKER-FACTORY-TEST : ic2 .
rewrites: 42 in 0ms cpu (1ms real) (~ rewrites/second)
result (sort not calculated):
(o(tf, 0) <| tick) (o(tf, 1) <| tick)
(o(tf, 2) <| tick) (o(tf, 3) <| tick)
(o(tf, 4) <| tick) (o(tf, 5) <| tick)
(o(tf, 6) <| tick)
(o(tf, 6) <| timeReq(c1))
Ticker(o(tf, 0), 6) Ticker(o(tf, 1), 0)
Ticker(o(tf, 2), 0) Ticker(o(tf, 3), 0)
Ticker(o(tf, 4), 0) Ticker(o(tf, 5), 0)
Ticker(o(tf, 6), 0)
TickerFactory(tf, 7)
((tf <| newReq(c2))
Cust1(c2, tf, 3)) Cust2(c1, tf, 3)

The number of rewrites reported by Maude includes both equational and rule rewrites. In the examples above there were 2 equational rewrites (the two equations defining the initial configuration ic2 and its subconfiguration ic1) and 40 rule rewrites. If you execute the command

Maude> set profile on .

(see Section 20.1.5) before rewriting and then execute

Maude> show profile .

you will discover that executing the rewrite command the rule delivering the tick message is used 35 times and the other rules are each used once, while executing the frewrite command the tick rule is executed only 6 times and each of the other rules are executed between 6 and 8 times.

Turning profiling on substantially reduces performance, so you will want to turn it off

Maude> set profile off .

when you have found out what you want to know.

Note that frewrite uses a fair rewriting strategy, but since it does not know about objects, messages, and configurations, it can only follow a position-fair strategy. As we will explain in the next section, in order to enable the object-message fair rewriting we need only do three things:

To maintain the separate rewriting semantics we also modify the name of each module by putting an O at the front (except for ACTOR-CONF which we rename ACTOR-O-CONF). Thus we modify the configuration, actor, and message constructor declarations as follows.

op __ : AConf AConf -> AConf [ctor config assoc comm id: none] .
op _<|_ : Aid MsgBody -> Msg [ctor message] .

mod O-TICKER is
op Ticker : Aid Nat -> Actor [ctor object] .

op TickerFactory : Aid Nat -> Actor [ctor object] .

ops Cust Cust1 Cust2 : Aid Aid Nat -> Actor [ctor object] .

Now the frewrite command will use object-message fair rewriting, as explained in detail in the next section. The counting of object-message rewrites has two aspects: for the purposes of the rewrite argument given to frewrite, a visit to a configuration that results in one or more rewrites counts as a single rewrite; though for other accounting purposes all rewrites are counted. For example, with an upper bound of 40 as above, thirteen tickers are created. To simplify the output we show the results for rewriting with a bound of 20.

Maude> frew [20] ic2 .
frewrite [20] in O-TICKER-FACTORY-TEST : ic2 .
rewrites: 76 in 0ms cpu (1ms real) (~ rewrites/second)
result (sort not calculated):
(o(tf, 0) <| tick) (o(tf, 1) <| tick)
(o(tf, 2) <| tick) (o(tf, 3) <| tick)
(o(tf, 4) <| tick) (o(tf, 5) <| tick)
Ticker(o(tf, 0), 11) Ticker(o(tf, 1), 11)
Ticker(o(tf, 2), 7) Ticker(o(tf, 3), 7)
Ticker(o(tf, 4), 3) Ticker(o(tf, 5), 3)
TickerFactory(tf, 6)
((tf <| newReq(c1)) Cust1(c1, tf, 3))
(tf <| newReq(c2)) Cust1(c2, tf, 3)

Notice that each ticker gets a chance to tick (tickers created later will show less time passed), and each customer is treated fairly. In fact using profiling we find that the tick rule is used 42 times (which is the total of the counts for the six tickers created), while the other rules are used 6-8 times and there are 2 equational rewrites as before.

Suppose that we try to violate the unique name condition, for example by adding a copy of customer c1 to the test configuration. When Maude discovers this (it may take a few rewrites), a warning is issued.

Maude> frew [4] ic2 Cust(c1, tf, 0) .
Warning: saw duplicate object: Cust1(c1, tf, 0)
frewrite [4] in O-TICKER-FACTORY-TEST : ic2 Cust(c1, tf, 0) .
rewrites: 8 in 0ms cpu (0ms real) (~ rewrites/second)
result AConf:
(c1 <| newReply(o(tf, 0))) (c1 <| newReply(o(tf, 1)))
(c2 <| newReply(o(tf, 2)))
(o(tf, 0) <| tick) (o(tf, 1) <| tick) (o(tf, 2) <| tick)
Ticker(o(tf, 0), 0) Ticker(o(tf, 1), 0) Ticker(o(tf, 2), 0)
TickerFactory(tf, 3)
Cust1(c1, tf, 0) Cust1(c1, tf, 0) Cust1(c2, tf, 0)

8.2 Object-message fair rewriting

Object-message fair rewriting is a special rewriting strategy associated with configuration constructors which are declared with the config attribute. Configuration constructors must be associative and commutative, and may optionally have an identity element. The empty syntax constructors in the CONFIGURATION and ACTOR-O-CONF modules above (which have been given the config attribute) are examples of valid configuration constructors, but such default syntax can easily be changed by renaming the __ operator (see Section 6.2.2). Configurations only have their special behavior with respect to arguments that are constructed using operators that are object or message constructors, that is, they are declared with the object or message attribute. Such object and message constructors must have at least one argument. Examples include the Maude object constructor in CONFIGURATION, the various actor constructors imported into O-TICKER-FACTORY-TEST, all of which have been given the object attribute, and the actor message constructor which has been given the message attribute (which can be abbreviated as msg).

An operator can have at most one of the three attributes: config, object, and message. For object constructors, the first argument is considered to be the object’s name. For message constructors, the first argument is considered to be the message’s target or addressee. There may be multiple configuration, object and message constructors. A rule is considered to be an object-message rule if the following requirements hold:

Its lefthand side has a configuration constructor on top with two arguments A and B,
A and B are stable (that is, they cannot change their top symbol under a substitution),
A has a message constructor on top,
B has an object constructor on top, and
The first arguments of A and B are identical.

For example, the rules newReply and timeReply in the O-TICKER-CUSTOMER module are object-message rules (because configurations are associative and commutative A and B can appear in the rule in either order) while the rule labeled req is not, because there is no message term, only an object, in its lefthand side. This rule will be applied in the rewriting that happens after all the enabled object-message rules have been applied, as discussed below.

The object-message fair behavior appears with the command frewrite (and at the metalevel with the descent function metaFrewrite—see Section 17.6.3). When the fair traversal attempts to perform a single rewrite on a term headed by a configuration constructor, the following happens:

Arguments headed by object constructors are collected. It is a runtime error for more than one object to have the same name.
For each object, messages with its name as first argument are collected and placed in a queue.
Any remaining arguments are placed on a remainder list.
For each object, and for each message in its queue, an attempt is made to deliver the message by performing a rewrite with an object-message rule. If all applicable rules fail, the message is placed on the remainder list. If a rule succeeds, the righthand side is constructed, reduced, and the result is searched for the object. Any other arguments in the result configuration go onto the remainder list. If the object cannot be found, any messages left in its queue go onto the remainder list. Once its message queue is exhausted, the object itself is placed on the remainder list.
A new term is constructed using the configuration constructor on top of the arguments in the remainder list. This is reduced, and a single rewrite using the non-object-message rules is attempted.

There is no restriction on object names, other than uniqueness. An object may change its object constructor during the course of a rewrite and delivery of any remaining message will still be attempted.1 If the configuration constructor changes during the course of a rewrite, the resulting term is considered alien, and does not participate any further in the object-message rewriting for the original term. The order in which objects are considered and messages are delivered is system-dependent, but note that newly created messages are not delivered until some future visit to the configuration (though all arguments including new messages and alien configurations could potentially participate in the single non-object-message rewrite attempt). Message delivery is “just” rather than “fair”: in order for message delivery to be guaranteed, an object must always be willing to accept the message.2 If multiple object-message rules contain the same message constructor, they are tried in a round-robin fashion. Non-object-message rules are also tried in a round-robin fashion for the single non-object-message rewrite attempt.

The counting of object-message rewrites is nonstandard: for the purposes of the rewrite argument given to frewrite, a visit to a configuration that results in one or more rewrites counts as a single rewrite, though for other accounting purposes all rewrites are counted. Finally, for tracing, profiling, and breakpoints only, there is a fake rewrite at the top of the configuration in the case that object-message rewriting takes place but the single non-object-message rewrite attempt fails. It is not included in the reported rewrite total, but it is inserted to keep tracing consistent.

8.3 Example: data agents

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.

*** 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] .

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.14), 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).


*** 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] .

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 .

mod DATA-AGENTS{K :: TRIV, V :: TRIV} is
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)) .

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.

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)) .

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.


Figure 8.3:Importation graph of data-agents modules

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 23.4).