Figure 8.1: Importation graph of bank modules
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.
The predefined module CONFIGURATION in the file prelude.maude provides basic sorts and constructors for modeling object-based systems.
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
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
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.
In this syntax, objects have the general form
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 >.
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.
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.
Now we could replace
by
in the example configuration. The module BANK-ACCOUNT-TEST declares the object identifiers introduced above and defines a configuration constant bankConf.
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.
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).
The BANK-MANAGER module below illustrates asynchronous message passing with object creation.
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.
Then, we rewrite the configuration mgrConf:
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.
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 [1, 116]. 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 _<|_.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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
(see Section 14.1.4) before rewriting and then execute
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
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.
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.
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.
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:
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:
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.
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.
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:
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).
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
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.
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.
The importation graph of all the modules involved in this example is shown in Figure 8.3, where the three different types of arrows correspond to the three different modes of importation.
The following are results from test runs. First we rewrite the initial configuration iconf, resulting in a configuration in which the agents have updated appropriately their data, and there is one reply for each tellReq message.
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.
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.
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.
Note the use of the such that condition to filter search solutions (see Section 5.4.3 and 18.4).
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
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:
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.
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.
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
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
or
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
which elicits either
or
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
which elicits either
or
When you are done with the socket, you can close it with a message
with reply
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” [24] that is now executable. The first module defines some auxiliary operations on strings.
The second module requests one web page to a HTTP server.
First, we try to connect to the server using port 80, updating the state and the requester attribute with the new server.
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.
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.
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.
Now we can get pages from servers, say “www.google.com”, by using the following Maude command:
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,
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
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
or
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:
which elicits either
or
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.
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.
The Maude command that initializes the server is as follows, where the configuration includes the portal <>.
The second module describes the behavior of the clients.
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.
The initial configuration for the client will be as follows, again with portal <>.
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.
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
instead of a message
All the messages have exactly the same declarations, the only difference being their initial capitalization:
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.
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.
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.
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:
BufferedSocket objects are created and destroyed when the corresponding sockets are. Thus, we have rules
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.
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.
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 [26, Chapter 16].
