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

As discussed in Chapter 17, 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.

  mod CONFIGURATION is  
    *** 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 17). 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 8.4.

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

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

  mod BANK-ACCOUNT is  
    protecting INT .  
    inc CONFIGURATION .  
    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 .  
  endm

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)

by

  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.

  mod BANK-ACCOUNT-TEST is  
    ex BANK-ACCOUNT .  
    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) .  
  endm

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

  mod BANK-MANAGER is  
    inc BANK-ACCOUNT .  
    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 > .  
  endm

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.

  mod BANK-MANAGER-TEST is  
    ex BANK-MANAGER .  
    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) .  
  endm

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.


PIC


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 [1103]. 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 _<|_.

  mod ACTOR-CONF is  
    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] .  
  endm

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

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.

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

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.

  mod TICKER-FACTORY is  
    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) .  
  endm

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.

  mod TICKER-CUSTOMER is  
    inc TICKER-FACTORY .  
    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) .  
  endm

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.


PIC


Figure 8.2: Importation graph of ticker modules


  mod TICKER-FACTORY-TEST is  
    ex TICKER-CUSTOMER .  
    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) .  
  endm

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

  mod ACTOR-O-CONF is  
    ...  
    op __ : AConf AConf -> AConf [ctor config assoc comm id: none] .  
    op _<|_ : Aid MsgBody -> Msg [ctor message] .  
    ...  
  endm

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

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

  mod O-TICKER-CUSTOMER is  
    ...  
    ops Cust Cust1 Cust2 : Aid Aid Nat -> Actor [ctor object] .  
    ...  
  endm

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:

1.
Its lefthand side has a configuration constructor on top with two arguments A and B,
2.
A and B are stable (that is, they cannot change their top symbol under a substitution),
3.
A has a message constructor on top,
4.
B has an object constructor on top, and
5.
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 11.5.3). When the fair traversal attempts to perform a single rewrite on a term headed by a configuration constructor, the following happens:

1.
Arguments headed by object constructors are collected. It is a runtime error for more than one object to have the same name.
2.
For each object, messages with its name as first argument are collected and placed in a queue.
3.
Any remaining arguments are placed on a remainder list.
4.
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.
5.
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.

  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.


PIC


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

8.4 External objects

This section explains Maude’s support for rewriting with external objects and an implementation of sockets as the first such external objects.

Configurations that want to communicate with external objects must contain at least one portal, where

  sort Portal .  
  subsort Portal < Configuration .  
  op <> : -> Portal [ctor] .

is part of the predefined module CONFIGURATION in the file prelude.maude. Rewriting with external objects is started by the external rewrite command erewrite (abbreviated erew) which is like frewrite (see Sections 5.4 and 8.2) except that it allows messages to be exchanged with external objects that do not reside in the configuration. Currently the command erewrite has some severe limitations, which might be fixed in future releases:

1.
Maude only checks for external rewrites when no “internal” rewrites are possible, so if, for example, there is a clock tick rewrite rule that is always enabled, external rewrites won’t take place.
2.
Rewrites that involve messages entering or leaving the configuration do not show up in tracing, profiling or rewrite counts.
3.
It is possible to have bad interactions with break points and the debugger.
4.
There is a potential race condition with ^C.

Note that, even if there are no more rewrites possible, erewrite may not terminate; if there are requests made to external objects that have not yet been fulfilled because of waiting for external events from the operating system, the Maude interpreter will suspend until at least one of those events occurs, at which time rewriting will resume. While the interpreter is suspended, the command erewrite may be aborted with ^C. External objects created by an erewrite command do not survive to the next erewrite. If a message to an external object is ill-formed or inappropriate, or the external object is not ready for it, it just stays in the configuration for future acceptance or for debugging purposes.

8.4.1 Sockets

The first example of external objects is sockets, which are accessed using the messages declared in the following SOCKET module, included in the file socket.maude which is part of the Maude distribution.

  mod SOCKET is  
    protecting STRING .  
    including CONFIGURATION .  
 
    op socket : Nat -> Oid [ctor] .  
 
    op createClientTcpSocket : Oid Oid String Nat -> Msg  
         [ctor msg format (b o)] .  
    op createServerTcpSocket : Oid Oid Nat Nat -> Msg  
         [ctor msg format (b o)] .  
    op createdSocket : Oid Oid Oid -> Msg [ctor msg format (m o)] .  
 
    op acceptClient : Oid Oid -> Msg [ctor msg format (b o)] .  
    op acceptedClient : Oid Oid String Oid -> Msg  
         [ctor msg format (m o)] .  
 
    op send : Oid Oid String -> Msg [ctor msg format (b o)] .  
    op sent : Oid Oid -> Msg [ctor msg format (m o)] .  
 
    op receive : Oid Oid -> Msg [ctor msg format (b o)] .  
    op received : Oid Oid String -> Msg [ctor msg format (m o)] .  
 
    op closeSocket : Oid Oid -> Msg [ctor msg format (b o)] .  
    op closedSocket : Oid Oid String -> Msg [ctor msg format (m o)] .  
 
    op socketError : Oid Oid String -> Msg [ctor msg format (r o)] .  
 
    op socketManager : -> Oid [special (...)] .  
  endm

Currently only IPv4 TCP sockets are supported; other protocol families and socket types may be added in the future. The external object named by the constant socketManager is a factory for socket objects.

To create a client socket, you send socketManager a message

  createClientTcpSocket(socketManager, ME, ADDRESS, PORT)

where ME is the name of the object the reply should be sent to, ADDRESS is the name of the server you want to connect to (say “www.google.com”), and PORT is the port you want to connect to (say 80 for HTTP connections). You may also specify the name of the server as an IPv4 dotted address or as “localhost” for the same machine where the Maude system is running on.

The reply will be either

  createdSocket(ME, socketManager, NEW-SOCKET-NAME)

or

  socketError(ME, socketManager, REASON)

where NEW-SOCKET-NAME is the name of the newly created socket and REASON is the operating system’s terse explanation of what went wrong.

You can then send data to the server with a message

  send(SOCKET-NAME, ME, DATA)

which elicits either

  sent(ME, SOCKET-NAME)

or

  closedSocket(ME, SOCKET-NAME, REASON)

Notice that all errors on a client socket are handled by closing the socket.

Similarly, you can receive data from the server with a message

  receive(SOCKET-NAME, ME)

which elicits either

  received(ME, SOCKET-NAME, DATA)

or

  closedSocket(ME, SOCKET-NAME, REASON)

When you are done with the socket, you can close it with a message

  closeSocket(SOCKET-NAME, ME)

with reply

  closedSocket(ME, SOCKET-NAME, "")

Once a socket has been closed, its name may be reused, so sending messages to a closed socket can cause confusion and should be avoided.

Notice that TCP does not preserve message boundaries, so sending "one" and "two" might be received as "on" and "etwo". Delimiting message boundaries is the responsibility of the next higher-level protocol, such as HTTP. We will present an implementation of buffered sockets in Section 8.4.2 which solves this problem.

The following modules implement an updated version of the five rule HTTP/1.0 client from the paper “Towards Maude 2.0” [19] that is now executable. The first module defines some auxiliary operations on strings.

  fmod STRING-OPS is  
    pr STRING .  
    var S : String .  
    op extractHostName : String -> String .  
    op extractPath : String -> String .  
    op extractHeader : String -> String .  
    op extractBody : String -> String .  
 
    eq extractHostName(S)  
      = if find(S, "/", 0) == notFound  
        then S  
        else substr(S, 0, find(S, "/", 0))  
        fi .  
 
    eq extractPath(S)  
      = if find(S, "/", 0) == notFound  
        then "/"  
        else substr(S, find(S, "/", 0), length(S))  
        fi .  
 
    eq extractHeader(S)  
      = substr(S, 0, find(S, "\r\n\r\n", 0) + 4) .  
    eq extractBody(S)  
      = substr(S, find(S, "\r\n\r\n", 0) + 4, length(S)) .  
  endfm

The second module requests one web page to a HTTP server.

  mod HTTP/1.0-CLIENT is  
    pr STRING-OPS .  
    inc SOCKET .  
    sort State .  
    ops idle connecting sending receiving closing : -> State [ctor] .  
    op state:_ : State -> Attribute [ctor] .  
    op requester:_ : Oid -> Attribute [ctor] .  
    op url:_ : String -> Attribute [ctor] .  
    op stored:_ : String -> Attribute [ctor] .  
 
    op HttpClient : -> Cid .  
    op httpClient : -> Oid .  
    op dummy : -> Oid .  
 
    op getPage : Oid Oid String -> Msg [msg ctor] .  
    op gotPage : Oid Oid String String -> Msg [msg ctor] .  
 
    vars H R R’ TS : Oid .  
    vars U S ST : String .

First, we try to connect to the server using port 80, updating the state and the requester attribute with the new server.

    rl [getPage] :  
      getPage(H, R, U)  
      < H : HttpClient |  
          state: idle, requester: R’, url: S, stored: "" >  
      => < H : HttpClient |  
             state: connecting, requester: R, url: U, stored: "" >  
         createClientTcpSocket(socketManager, H,  
           extractHostName(U), 80) .

Once we are connected to the server (we have received a createdSocket message), we send a GET message (from the HTTP protocol) requesting the page. When the message is sent, we wait for a response.

    rl [createdSocket] :  
      createdSocket(H, socketManager, TS)  
      < H : HttpClient |  
          state: connecting, requester: R, url: U, stored: "" >  
      => < H : HttpClient |  
             state: sending, requester: R, url: U, stored: "" >  
         send(TS, H, "GET " + extractPath(U) + " HTTP/1.0\r\nHost: " +  
         extractHostName(U) + "\r\n\r\n") .  
 
    rl [sent] :  
      sent(H, TS)  
      < H : HttpClient |  
          state: sending, requester: R, url: U, stored: "" >  
      => < H : HttpClient |  
             state: receiving, requester: R, url: U, stored: "" >  
         receive(TS, H) .

While the page is not complete, we receive data and append it to the string on the stored attribute. When the page is completed, the server closes the socket, and then we show the page information by means of the gotPage message.

    rl [received] :  
      received(H, TS, S)  
      < H : HttpClient |  
          state: receiving, requester: R, url: U, stored: ST >  
      => receive(TS, H)  
         < H : HttpClient | state: receiving,  
             requester: R, url: U, stored: (ST + S) > .  
 
    rl [closedSocket] :  
      closedSocket(H, TS, S)  
      < H : HttpClient |  
          state: receiving, requester: R, url: U, stored: ST >  
      => gotPage(R, H, extractHeader(ST), extractBody(ST)) .

We use a special operator start to represent the initial configuration. It receives the server URL we want to connect to. Notice the occurrence of the portal <> in such initial configuration.

    op start : String -> Configuration .  
    eq start(S)  
      = <>  
        getPage(httpClient, dummy, S)  
        < httpClient : HttpClient | state: idle, requester: dummy,  
            url: "", stored: "" > .  
  endm

Now we can get pages from servers, say “www.google.com”, by using the following Maude command:

  Maude> erew start("www.google.com") .

It is also possible to have optional bounds on the erewrite command, and then use the continuation commands to get more results, like, for example,

  Maude> erew [1, 2] start("www.google.com") .  
  Maude> cont 1 .

To have communication between two Maude interpreter instances, one of them must take the server role and offer a service on a given port; generally ports below 1024 are protected. You cannot in general assume that a given port is available for use. To create a server socket, you send socketManager a message

  createServerTcpSocket(socketManager, ME, PORT, BACKLOG)

where PORT is the port number and BACKLOG is the number of queue requests for connection that you will allow (5 seems to be a good choice). The response is either

  createdSocket(ME, socketManager, SERVER-SOCKET-NAME)

or

  socketError(ME, socketManager, REASON)

Here SERVER-SOCKET-NAME refers to a server socket. The only thing you can do with a server socket (other than close it) is to accept clients, by means of the following message:

  acceptClient(SERVER-SOCKET-NAME, ME)

which elicits either

  acceptedClient(ME, SERVER-SOCKET-NAME, ADDRESS, NEW-SOCKET-NAME)

or

  socketError(ME, socketManager, REASON)

Here ADDRESS is the originating address of the client and NEW-SOCKET-NAME is the name of the socket you use to communicate with that client. This new socket behaves just like a client socket for sending and receiving. Note that an error in accepting a client does not close the server socket. You can always reuse the server socket to accept new clients until you explicitly close it.

The following modules illustrate a very naive two-way communication between two Maude interpreter instances. The issues of port availability and message boundaries are deliberately ignored for the sake of illustration (and thus if you are unlucky this example could fail).

The first module describes the behavior of the server.

  mod FACTORIAL-SERVER is  
    inc SOCKET .  
    pr CONVERSION .  
    op _! : Nat -> NzNat .  
    eq 0 ! = 1 .  
    eq (s N) ! = (s N) * (N !) .  
 
    op Server : -> Cid .  
    op aServer : -> Oid .  
 
    vars O LISTENER CLIENT : Oid .  
    var  A : AttributeSet .  
    var  N : Nat .  
    vars IP DATA S : String .

Using the following rules, the server waits for clients. If one client is accepted, the server waits for messages from it. When the message arrives, the server converts the received data to a natural number, computes its factorial, converts it into a string, and finally sends this string to the client. Once the message is sent, the server closes the socket with the client.

    rl [createdSocket] :  
      < O : Server | A > createdSocket(O, socketManager, LISTENER)  
      => < O : Server | A > acceptClient(LISTENER, O) .  
 
    rl [acceptedClient] :  
      < O : Server | A > acceptedClient(O, LISTENER, IP, CLIENT)  
      => < O : Server | A > receive(CLIENT, O)  
         acceptClient(LISTENER, O) .  
 
    rl [received] :  
      < O : Server | A > received(O, CLIENT, DATA)  
      => < O : Server | A >  
         send(CLIENT, O, string(rat(DATA, 10)!, 10)) .  
 
    rl [sent] :  
      < O : Server | A > sent(O, CLIENT)  
      => < O : Server | A > closeSocket(CLIENT, O) .  
 
    rl [closedSocket] :  
      < O : Server | A > closedSocket(O, CLIENT, S)  
      => < O : Server | A > .  
  endm

The Maude command that initializes the server is as follows, where the configuration includes the portal <>.

  Maude> erew <>  
              < aServer : Server | none >  
              createServerTcpSocket(socketManager, aServer, 8811, 5) .

The second module describes the behavior of the clients.

  mod FACTORIAL-CLIENT is  
    inc SOCKET .  
    op Client : -> Cid .  
    op aClient : -> Oid .  
 
    vars O CLIENT : Oid .  
    var  A : AttributeSet .

Using the following rules, the client connects to the server (clients must be created after the server), sends a message representing a number,3 and then waits for the response. When the response arrives, there are no blocking messages and rewriting ends.

    rl [createdSocket] :  
      < O : Client | A > createdSocket(O, socketManager, CLIENT)  
      => < O : Client | A > send(CLIENT, O, "6") .  
 
    rl [sent] :  
      < O : Client | A > sent(O, CLIENT)  
      => < O : Client | A > receive(CLIENT, O) .  
  endm

The initial configuration for the client will be as follows, again with portal <>.

  Maude> erew <>  
              < aClient : Client | none >  
              createClientTcpSocket(socketManager,  
                aClient, "localhost", 8811) .

Almost everything in the socket implementation is done in a nonblocking way; so, for example, if you try to open a connection to some webserver and that webserver takes 5 minutes to respond, other rewriting and transactions happen in the meanwhile as part of the same command erewrite. The one exception is DNS resolution, which is done as part of the createClientTcpSocket message handling and which cannot be nonblocking without special tricks.

8.4.2 Buffered sockets

As we said before, TCP does not preserve message boundaries; to guarantee it we may use a filter class BufferedSocket, defined in the module BUFFERED-SOCKET, which is described here. We interact with buffered sockets in the same way we interact with sockets, with the only difference that all messages in the module SOCKET have been capitalized to avoid confusion. Thus, to create a client with a buffered socket, you send socketManager a message

  CreateClientTcpSocket(socketManager, ME, ADDRESS, PORT)

instead of a message

  createClientTcpSocket(socketManager, ME, ADDRESS, PORT).

All the messages have exactly the same declarations, the only difference being their initial capitalization:

  op CreateClientTcpSocket : Oid Oid String Nat -> Msg  
       [ctor msg format (b o)] .  
  op CreateServerTcpSocket : Oid Oid Nat Nat -> Msg  
       [ctor msg format (b o)] .  
  op CreatedSocket : Oid Oid Oid -> Msg [ctor msg format (m o)] .  
 
  op AcceptClient : Oid Oid -> Msg [ctor msg format (b o)] .  
  op AcceptedClient : Oid Oid String Oid -> Msg  
       [ctor msg format (m o)] .  
 
  op Send : Oid Oid String -> Msg [ctor msg format (b o)] .  
  op Sent : Oid Oid -> Msg [ctor msg format (m o)] .  
 
  op Receive : Oid Oid -> Msg [ctor msg format (b o)] .  
  op Received : Oid Oid String -> Msg [ctor msg format (m o)] .  
 
  op CloseSocket : Oid Oid -> Msg [ctor msg format (b o)] .  
  op ClosedSocket : Oid Oid String -> Msg [ctor msg format (m o)] .  
 
  op SocketError : Oid Oid String -> Msg [ctor msg format (r o)] .

Thus, apart from this small difference, we interact with buffered sockets in exactly the same way we do with sockets, the boundary control being completely transparent to the user.

When a buffered socket is created, in addition to the socket object through which the information will be sent, a BufferedSocket object is also created on each side of the socket (one in each one of the configurations between which the communication is established). All messages sent through a buffered socket are manipulated before they are sent through the socket underneath. When a message is sent through a buffered socket, a mark is placed at the end of it; the BufferedSocket object at the other side of the socket stores all messages received on a buffer, in such a way that when a message is requested the marks placed indicate which part of the information received must be given as the next message.

An object of class BufferedSocket has two attributes: read, of sort String, which stores the messages read, and bState, which indicates whether the filter is idle or active.

    op BufferedSocket : -> Cid [ctor] .  
    op read :_ : String -> Attribute [ctor gather(&)] .  
    op bState :_ : BState -> Attribute [ctor gather(&)] .  
    sort BState .  
    ops idle active : -> BState [ctor] .

The identifiers of the BufferedSocket objects are marked with a b operator, i.e., the buffers associated with a socket SOCKET have identifier b(SOCKET). Note that there is a BufferedSocket object on each side of the socket, that is, there are two objects with the same identifier, but in different configurations.

    op b : Oid -> Oid [ctor] .

A buffered socket object understands capitalized versions of the messages a socket object understands. For most of them, it just converts them into the corresponding uncapitalized message. There are messages AcceptClient, CloseSocket, CreateServerTcpSocket, and CreateClientTcpSocket with the same arities as the corresponding socket messages, with the following rules.

    vars SOCKET NEW-SOCKET SOCKET-MANAGER O : Oid .  
    vars ADDRESS IP IP’ DATA S S’ REASON : String .  
    var  Atts : AttributeSet .  
    vars PORT BACKLOG N : Nat .  
 
    rl [createServerTcpSocket] :  
      CreateServerTcpSocket(SOCKET-MANAGER, O, PORT, BACKLOG)  
      => createServerTcpSocket(SOCKET-MANAGER, O, PORT, BACKLOG) .  
 
    rl [acceptClient] :  
      AcceptClient(SOCKET, O)  
      => acceptClient(SOCKET, O) .  
 
    rl [closeSocket] :  
      CloseSocket(b(SOCKET), SOCKET-MANAGER)  
      => closeSocket(SOCKET, SOCKET-MANAGER) .  
 
    rl [createClientTcpSocket] :  
      CreateClientTcpSocket(SOCKET-MANAGER, O, ADDRESS, PORT)  
      => createClientTcpSocket(SOCKET-MANAGER, O, ADDRESS, PORT) .

Note that in these cases the buffered-socket versions of the messages are just translated into the corresponding socket messages.

A BufferedSocket object can also convert an uncapitalized message into the capitalized one. The rule socketError shows this:

    rl [socketError] :  
      socketError(O, SOCKET-MANAGER, REASON)  
      => SocketError(O, SOCKET-MANAGER, REASON) .

BufferedSocket objects are created and destroyed when the corresponding sockets are. Thus, we have rules

    rl [acceptedclient] :  
      acceptedClient(O, SOCKET, IP’, NEW-SOCKET)  
      => AcceptedClient(O, b(SOCKET), IP’, b(NEW-SOCKET))  
         < b(NEW-SOCKET) : BufferedSocket |  
             bState : idle, read : "" > .  
 
    rl [createdSocket] :  
      createdSocket(O, SOCKET-MANAGER, SOCKET)  
      => < b(SOCKET) : BufferedSocket | bState : idle, read : "" >  
         CreatedSocket(O, SOCKET-MANAGER, b(SOCKET)) .  
 
    rl [closedSocket] :  
      < b(SOCKET) : BufferedSocket | Atts >  
      closedSocket(SOCKET, SOCKET-MANAGER, DATA)  
      => ClosedSocket(b(SOCKET), SOCKET-MANAGER, DATA) .

Once a connection has been established, and a BufferedSocket object has been created on each side, messages can be sent and received. When a Send message is received, the buffered socket sends a send message with the same data plus a mark4 to indicate the end of the message.

    rl [send] :  
      < b(SOCKET) : BufferedSocket | bState : active, Atts >  
      Send(b(SOCKET), O, DATA)  
      => < b(SOCKET) : BufferedSocket | bState : active, Atts >  
         send(SOCKET, O, DATA + "#") .  
 
    rl [sent] :  
      < b(SOCKET) : BufferedSocket | bState : active, Atts >  
      sent(O, SOCKET)  
      => < b(SOCKET) : BufferedSocket | bState : active, Atts >  
         Sent(O, b(SOCKET)) .

The key is then in the reception of messages. A BufferedSocket object is always listening to the socket. It sends a receive message at start up and puts all the received messages in its buffer. Notice that a buffered socket goes from idle to active in the buffer-start-up rule. A Receive message is then handled if there is a complete message in the buffer, that is, if there is a mark on it, and results in the reception of the first message in the buffer, which is removed from it.

    rl [buffer-start-up] :  
      < b(SOCKET) : BufferedSocket | bState : idle, Atts >  
      => < b(SOCKET) : BufferedSocket | bState : active, Atts >  
         receive(SOCKET, b(SOCKET)) .  
 
    rl [received] :  
      < b(SOCKET) : BufferedSocket |  
          bState : active, read : S, Atts >  
      received(b(SOCKET), O, DATA)  
      => < b(SOCKET) : BufferedSocket |  
             bState : active, read : (S + DATA), Atts >  
         receive(SOCKET, b(SOCKET)) .  
 
    crl [Received] :  
      < b(SOCKET) : BufferedSocket |  
          bState : active, read : S, Atts >  
      Receive(b(SOCKET), O)  
      => < b(SOCKET) : BufferedSocket |  
             bState : active, read : S’, Atts >  
         Received(O, b(SOCKET), DATA)  
      if N := find(S, "#", 0)  
         /\ DATA := substr(S, 0, N)  
         /\ S’ := substr(S, N + 1, length(S)) .

The BUFFERED-SOCKET module is used in the specification of Mobile Maude, a mobile agent language based on Maude, which is discussed in detail in [21, Chapter 16].