We use the object-message system to allow interactions with external objects that represent external entities with state. This section explains Maude’s support for rewriting with external objects and an implementation of sockets, standard streams, files, processes, and meta-interpreters 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. From an implementation point of view, the main purpose of having a portal term in a configuration is to avoid the degenerate case of a configuration that consists just of an object waiting for a message from outside of the configuration. This would be problematic because the special behavior for object-message rewriting and exchanging messages with external objects is attached to the configuration constructor.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.
Certain predefined external objects are available and some of them are object managers that can create more ephemeral external objects that represent entities such as files and sockets, and as we will see in Chapter 19, virtual copies of the Maude interpreter itself.
Access to external objects represents a potential threat. It is difficult for a user to tell just by looking at it, if an arbitrary Maude program contains malware. Furthermore, a Maude program can assemble meta-malware using innocent looking code and then execute it in a meta-interpreter. File handling and process execution are now disabled by default. These features need to be enabled with the command line flags -allow-files and -allow-processes. To run completely trusted code, the command line flag -trust enables all dangerous features. See Section 23.1.
Each Unix process has three I/O channels, called standard streams: standard input (stdin), standard output (stdout), and standard error (stderr). In Maude, these are represented as three unique external objects, that are defined in a predefined module STD-STREAM in the file.maude file included in the Maude distribution. Because some of the messages that are useful for streams are also useful for file I/O, these messages are pulled out into a module COMMON-MESSAGES.
mod COMMON-MESSAGES is
protecting STRING .
including CONFIGURATION .
op gotLine : Oid Oid String -> Msg [ctor msg format (m o)] .
op write : Oid Oid String -> Msg [ctor msg format (b o)] .
op wrote : Oid Oid -> Msg [ctor msg format (m o)] .
endm
mod STD-STREAM is
including COMMON-MESSAGES .
op getLine : Oid Oid String -> Msg [ctor msg ...] .
op cancelGetLine : Oid Oid -> Msg [ctor msg ...] .
op canceledGetLine : Oid Oid -> Msg [ctor msg ...] .
op streamError : Oid Oid String -> Msg [ctor msg ...] .
op stdin : -> Oid [special (...)] .
op stdout : -> Oid [special (...)] .
op stderr : -> Oid [special (...)] .
endm
I/O on standard streams is always line-oriented and in text mode. stdout and stderr accept the write() message just like file handlers. They are automatically flushed so this is the only message they can accept. They always return a wrote() message.
The stdin object accepts a three-argument getLine() message:
ME is the identifier of the sender object, to which the answer will be sent. PROMPT is a string that will be shown to inform the user that some input is expected. Once the message is processed, when the user hits the return key, stdin replies with a message
where TEXT contains just a "\n" character in the case of an empty line, and is empty in the case of an error or end-of-file (^D). The getLine operation is non-blocking on stdin and it can be canceled with
If this message is processed before the line is actually read, it will be replied withErrors while reading and writing on streams are reported with the
where CAUSE is a string describing the error cause. For example, an attempt to write an empty string to the standard output with write(stdout, ME, "") is replied with a streamError(ME, stdout, "Empty string.") message.The module HELLO below shows a very simple program implementing an interaction with the user, which is asked to introduce his/her name to be properly greeted. The equation for run produces a starting configuration, containing the portal, a user object to receive messages, and a message to stdin to read a line of text from the keyboard. When stdin has a line of text, it sends the text to the requesting object in a gotLine message.
mod HELLO is
including STD-STREAM .
op myClass : -> Cid .
op myObj : -> Oid .
op run : -> Configuration .
var O : Oid .
var A : AttributeSet .
var S : String .
var C : Char .
eq run
= <>
< myObj : myClass | none >
getLine(stdin, myObj, "What is your name? ") .
rl < myObj : myClass | A >
gotLine(myObj, O, S)
=> < myObj : myClass | A >
if S =/= ""
then write(stdout, myObj, "Hello " + S)
else none
fi .
endm
Maude> erew run .
What is your name? Joe
Hello Joe
result Configuration: <> wrote(myObj, stdout) < myObj : myClass | none >
As a second example of the use of standard streams, let us consider the specification in the module ROT13 below. The example prints out a banner and then reads lines from the keyboard, encrypts each line using the ROT13 cypher, and finally prints out the result.
mod ROT13 is
including STD-STREAM .
protecting INT .
op myClass : -> Cid .
op myObj : -> Oid .
op run : -> Configuration .
op rot13 : String -> String .
vars O O2 : Oid .
var A : AttributeSet .
vars S T : String .
var C : Char .
eq rot13(C)
= if C >= "A" and C <= "Z"
then char(ascii("A") + ((13 + (ascii(C) - ascii("A"))) rem 26))
else if C >= "a" and C <= "z"
then char(ascii("a") + ((13 + (ascii(C) - ascii("a"))) rem 26))
else C
fi
fi .
eq rot13(S)
= rot13(substr(S, 0, 1)) + rot13(substr(S, 1, length(S)))
[owise] .
eq run
= <>
< myObj : myClass | none >
write(stdout, myObj, "\nROT13 Encryption\n----------------\n") .
rl < O : myClass | A >
wrote(O, O2)
=> < O : myClass | A >
getLine(stdin, O, "Enter plain text> ") .
rl < O : myClass | A >
gotLine(O, O2, T)
=> < O : myClass | A >
if T =/= ""
then write(stdout, O, "Cypher text: " + rot13(T) + "\n")
else none
fi .
endm
The equation for run produces a starting configuration, containing the portal, a user object to receive messages, and an initial message to stdout to print out the banner. Each time stdout prints out some text, it sends a wrote reply to the requesting object; this is matched in the first rule which then sends a getLine message to stdin to read a line of text from the keyboard. When stdin has a line of text, it sends the text to the requesting object in a gotLine message; the second rule matches this message, calls the equationally defined rot13 function to encrypt the text, and sends a message to stdout to print the encrypted text. When the wrote reply comes back, the sequence repeats.
We can have the following interaction:
Maude> erewrite run .
erewrite in ROT13 : run .
ROT13 Encryption
----------------
Enter plain text> Maude
Cypher text: Znhqr
Enter plain text>
rewrites: 107 in 0ms cpu (3364ms real) (149025 rewrites/second)
result Configuration: <> < myObj : myClass | none >
The following program illustrates the use of functions metaReduce and metaParse (from module META-LEVEL, described later in Chapter 17) and functions tokenize and printTokens (from module LEXICAL in Section 7.11) to read Maude arithmetic expressions from the terminal and evaluate them.
mod CALCULATOR is
including STD-STREAM .
protecting LEXICAL .
protecting META-LEVEL .
op myClass : -> Cid .
op myObj : -> Oid .
op run : -> Configuration .
vars O O2 : Oid .
var A : AttributeSet .
vars S T : String .
op compute : String -> String .
eq compute(S) = compute2(metaParse([’CONVERSION], tokenize(S), anyType)) .
op compute2 : ResultPair? -> String .
eq compute2({T:Term, Q:Qid}) = compute3(metaReduce([’CONVERSION], T:Term)) .
eq compute2(noParse(N:Nat)) = printTokens(’\r) + "syntax error" + printTokens(’\o) .
op compute3 : ResultPair? -> String .
eq compute3({T:Term, Q:Qid}) = printTokens(metaPrettyPrint([’CONVERSION], T:Term)) .
eq run
= <>
< myObj : myClass | none >
write(stdout, myObj, "\nCalculator\n------------\n") .
rl < O : myClass | A >
wrote(O, O2)
=> < O : myClass | A >
getLine(stdin, O, "Expression> ") .
rl < O : myClass | A >
gotLine(O, O2, T)
=> < O : myClass | A >
if T == ""
then none
else write(stdout, O, "Answer: " + compute(T) + "\n")
fi .
endm
Maude> erew run .
erewrite in CALCULATOR : run .
Calculator
------------
Expression> 3/6 + 12/32
Answer: 7/8
Expression>
As pointed out in the introduction of the chapter, access to external objects represents a potential threat. File handling is disabled by default. The feature may be enabled with the command line flags -allow-files or -trust. See Section 23.1.
Unlike standard streams, of which there are exactly three, a Unix process may have many different files open at any one time. Thus, in order to create new file handle objects as needed, we have a unique external object called fileManager. To open a file, the fileManager is sent a message openFile. On success, an openedFile message is returned, with the name of an external object that is a handle on the open file as one of its arguments. Messages to read and write the file can be directed to the handle object. On failure, a fileError message is returned, with a text explanation of why the file could not be opened as one of its arguments. These messages are defined in the module FILE, which is distributed as part of the Maude system in the file.maude file.
mod FILE is
including COMMON-MESSAGES .
protecting INT .
sorts Base LinkType .
ops start current end : -> Base [ctor] .
ops hard symbolic : -> LinkType [ctor] .
op file : Nat -> Oid [ctor] .
op openFile : Oid Oid String String -> Msg [ctor msg format (b o)] .
op openedFile : Oid Oid Oid -> Msg [ctor msg format (m o)] .
op removeFile : Oid Oid String -> Msg [ctor msg format (b o)] .
op removedFile : Oid Oid -> Msg [ctor msg format (m o)] .
op getLine : Oid Oid -> Msg [ctor msg format (b o)] .
op getChars : Oid Oid Nat -> Msg [ctor msg format (b o)] .
op gotChars : Oid Oid String -> Msg [ctor msg format (m o)] .
op flush : Oid Oid -> Msg [ctor msg format (b o)] .
op flushed : Oid Oid -> Msg [ctor msg format (m o)] .
op setPosition : Oid Oid Int Base -> Msg [ctor msg format (b o)] .
op positionSet : Oid Oid -> Msg [ctor msg format (m o)] .
op getPosition : Oid Oid -> Msg [ctor msg format (b o)] .
op positionGot : Oid Oid Nat -> Msg [ctor msg format (m o)] .
op closeFile : Oid Oid -> Msg [ctor msg format (b o)] .
op closedFile : Oid Oid -> Msg [ctor msg format (m o)] .
op makeLink : Oid Oid String String LinkType -> Msg [ctor msg format (b o)] .
op madeLink : Oid Oid -> Msg [ctor msg format (m o)] .
op fileError : Oid Oid String -> Msg [ctor msg format (m o)] .
op fileManager : -> Oid [special (...)] .
endm
This API basically wraps the C stdio library. To open a file you send fileManager a message
where ME is the name of the object the reply should be sent to, PATH is the path of the file you want to open, and MODE is one of: r, r+, w, w+, a, a+.1
The reply is either
orwhere FILE-HANDLE is the name of the object used to access the file, and REASON is a textual explanation from the operating system of what went wrong.
If the file was opened for writing you can send
to write data to the file, and receive a reply
orA file that is opened for writing can also be sent
to flush any buffered data and receive a reply
orA file that is opened for reading can be read on a line-by-line basis using the message:
where the reply is either
orHere TEXT includes the newline character (if present, since end-of-file also ends the current line). TEXT is empty to indicate end-of-file with no more characters to read.
A file that is opened for reading can also be read on a character basis (which is more appropriate for binary files) using the message
where the reply is either
orHere if DATA is shorter than requested, it indicates the end-of-file was reached.
Reading and writing share a common position into the file where the next read or write takes place. This position in bytes from the start of the file can be obtained by sending the message
where the reply is either
orThe position may be changed with the message
Here the OFFSET is relative to BASE, where BASE can take one of three values: start, the start of the file, current, the current position, or end, the end of the file. In the current and end cases, negative values of OFFSET are allowed. The reply is either
orFinally, an open file can be closed with the message
Since it is always OK to close an open file, the response is always
Note that messages that are not recognized or that are sent to nonexistent objects will be silently ignored and left in the configuration. Messages that are recognized but are not appropriate for the object they are sent to or which have bad arguments will similarly be ignored but will generate a “message declined” advisory.
In addition to the previous messages for operating with the contents of files, some filesystem operations are also available in the API. Files can be removed with the removeFile message
whose reply is or a fileError message if an error occurs. Links between files can be created with that creates a new file in LINK-PATH pointing to TARGET-PATH, where TYPE can be either symbolic for a symbolic link or hard for a hard link. The message is answered with or with a fileError in case of error.The COPY-FILE module below illustrates the basic use of files. It specifies a simple algorithm to copy files. In this case, the run operator takes two arguments, namely the name of the file to be copied and the name of the new file. The equation for run produces a starting configuration, containing the portal, a user object to receive messages, and an initial message to open the original file. Once it is opened, the new file is created. Notice the "w" argument of the openFile message. Once both files are opened, a loop in which a line is read from the original file and written in the copy file is initiated. This loop ends when the end of the file is reached. Both files are then closed.
fmod MAYBE{X :: TRIV} is
sort Maybe{X} .
subsort X$Elt < Maybe{X} .
op maybe : -> Maybe{X} [ctor] .
endfm
mod COPY-FILE is
including FILE .
protecting (MAYBE * (op maybe to null)){Oid} .
op myClass : -> Cid .
op myObj : -> Oid .
ops in:_ out:_ : Maybe{Oid} -> Attribute .
ops inFile:_ outFile:_ : String -> Attribute .
op run : String String -> Configuration .
vars Text Original Copy : String .
vars FHIn FHOut : Oid .
var Attrs : AttributeSet .
eq run(Original, Copy)
= <>
< myObj : myClass | in: null, inFile: Original,
out: null, outFile: Copy >
openFile(fileManager, myObj, Original, "r") .
rl < myObj : myClass | in: null, outFile: Copy, Attrs >
openedFile(myObj, fileManager, FHIn)
=> < myObj : myClass | in: FHIn, outFile: Copy, Attrs >
openFile(fileManager, myObj, Copy, "w") .
rl < myObj : myClass | in: FHIn, out: null, Attrs >
openedFile(myObj, fileManager, FHOut)
=> < myObj : myClass | in: FHIn, out: FHOut, Attrs >
getLine(FHIn, myObj) .
rl < myObj : myClass | in: FHIn, out: FHOut, Attrs >
gotLine(myObj, FHIn, Text)
=> < myObj : myClass | in: FHIn, out: FHOut, Attrs >
if Text == ""
then closeFile(FHIn, myObj)
closeFile(FHOut, myObj)
else write(FHOut, myObj, Text)
fi .
rl < myObj : myClass | in: FHIn, out: FHOut, Attrs >
wrote(myObj, FHOut)
=> < myObj : myClass | in: FHIn, out: FHOut, Attrs >
getLine(FHIn, myObj) .
rl < myObj : myClass | in: FHIn, out: FHOut, Attrs >
closedFile(myObj, FHIn)
closedFile(myObj, FHOut)
=> none .
endm
You can then execute the program to copy a file "in.txt" with the following command:
The sockets external objects 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
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 eitheror
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 eitheror
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 9.3.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” [27] that is now executable. The first module defines some auxiliary operations on strings.
fmod STRING-OPS is
protecting 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 from an HTTP server.
mod HTTP/1.0-CLIENT is
protecting STRING-OPS .
including 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 (note the ellipsis in the output):
Maude> erew start("www.google.com") .
result Configuration: <> gotPage(dummy, httpClient, "HTTP/1.0 ... </html>")
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") .
result Configuration:
<>
< httpClient : HttpClient |
state: connecting,
requester: dummy,
url: "www.google.com",
stored: "" >
createClientTcpSocket(socketManager, httpClient, "www.google.com", 80)
Maude> cont 1 .
result Configuration:
<>
< httpClient : HttpClient |
state: connecting,
requester: dummy,
url: "www.google.com",
stored: "" >
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 eitheror
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.
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 <>.
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,2 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.
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:
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.
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 mark3 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 [29, Chapter 16].
Unix processes can be handled as Maude external objects through the API contained in the process.maude file. As pointed out in the introduction of the chapter, access to external objects represents a potential threat. Process execution is disabled by default. The feature may be enabled with the command line flags -allow-processes or -trust. See Section 23.1.
The external object processManager allows us to create new processes (with the createProcess message), with which we may directly interact.
fmod STRING-LIST is
protecting LIST{String} *
(sort NeList{String} to NeStringList, sort List{String} to StringList) .
endfm
mod PROCESS is
including SOCKET .
protecting STRING-LIST .
sorts ProcessOption ProcessOptionSet .
subsort ProcessOption < ProcessOptionSet .
op none : -> ProcessOptionSet [ctor] .
sort ExitStatus .
op normalExit : Nat -> ExitStatus [ctor] .
op terminatedBySignal : String -> ExitStatus [ctor] .
op process : Nat -> Oid [ctor] .
op createProcess : Oid Oid String StringList ProcessOptionSet -> Msg [ctor msg format (b o)] .
op createdProcess : Oid Oid Oid Oid Oid -> Msg [ctor msg format (m o)] .
op signalProcess : Oid Oid String -> Msg [ctor msg format (b o)] .
op signaledProcess : Oid Oid -> Msg [ctor msg format (m o)] .
op waitForExit : Oid Oid -> Msg [ctor msg format (b o)] .
op exited : Oid Oid ExitStatus -> Msg [ctor msg format (m o)] .
op processError : Oid Oid String -> Msg [ctor msg format (r o)] .
op processManager : -> Oid [special (...)] .
endm
New processes are created with the createProcess message, which has five arguments:
As usual, the first argument is the addressee of the message, in this case the special builtin object processManager, a constant of sort Oid;
the second argument is the Oid of the requesting object, to which the response will be sent;
the third argument is a String with the system command that executes the new process;
the fourth argument is a StringList with the arguments to the command; and
the fifth argument is a ProcessOptionSet, which is reserved for future use (currently we will use none).
On success, the reply to a createProcess message is a message createdProcess, which also carries five arguments, all of type Oid:
the requesting object,
the sender object (the processManager object),
the identifier of the new process object, which uses the process constructor,
the identifier of the new socket object for stdin/stdout, and
the identifier of the new socket object for stderr.
One can communicate with the new process using its stdin/stdout socket and the normal socket interface defined in socket.maude (see Section 9.3). Error messages can be read on the stderr socket. It is probably good practice to always have receives pending on both sockets so the process is not stalled due to socket buffers filling. The stderr socket ignores send messages.
Maude will stop rewriting and return to the command line as soon as there are no rewrites possible and no external events pending that could change the rewrite state, even if the newly created process is still running. It is therefore good practice to wait for a process to exit, if only to avoid filling the process table with zombies. This may be done by sending the process a waitForExit message. If such a message is sent, Maude will not return to the command line until the process actually exits, which is what happens when there are no further pending external events. When the process finally exits, the reply message is exited, with the last argument being either normalExit with an 8-bit exit code for a normal exit or a terminatedBySignal with the name of the signal in the case of termination by signal. The waitForExit message is nonblocking, so it can be sent any time after the createdProcess message is received. A second waitForExit message to the same process will not be accepted.
When a process has been waited for, its stdin/stdout and stderr are closed. If processes are not waited to be closed, it is the user’s responsibility to close the sockets to avoid leaking file descriptors. One way to do this is to keep receiving any final characters from the process until an end-of-file or error condition arises and Maude returns a closedSocket message. Alternatively, sockets can be closed by explicitly sending them closeSocket messages.
Different executables have different conventions for telling them to quit. You can send a process the empty string to cause an EOF condition on its stdin (see below). You can also send a signal to a process using the signalProcess message, whose third argument is a string with the name of the Unix signal.4 The process responds with a signaledProcess message.
The message processError is used as the reply for errors coming from the operating system. In particular a processError reply is generated if the child process cannot execute the specified executable.
We provide simple examples illustrating these features in the following sections.
Our first example invokes the dc (desk calculator) program to do some calculations and then kills it with a SIGTERM signal. To interact with the external objects we use an object of class User with attributes state (to keep track of the state the object is in), process (to keep the Oid of the external object), io and err (to keep the socket objects’ identifiers), and result (to store the response). Please, see inlined comments explaining the rules.
mod PROCESS-DC is
inc PROCESS .
inc MAYBE{Oid} * ( op maybe to null ).
op me : -> Oid .
op User : -> Cid .
op state:_ : Nat -> Attribute .
ops process:_ io:_ err:_ : Maybe{Oid} -> Attribute .
op result:_ : String -> Attribute .
vars X P ERR IO : Oid .
vars Result Str : String .
var Atts : AttributeSet .
---- once the process is created, a request to the dc and a waitForExit are sent
rl < X : User | state: 1, process: null, io: null, err: null, Atts >
createdProcess(X, processManager, P, IO, ERR)
=> < X : User | state: 2, process: P, io: IO, err: ERR, Atts >
send(IO, X, "10 16 + p\n") ---- dc keeps the result in p
waitForExit(P, X) .
---- once the message has been sent, a response is requested
rl < X : User | state: 2, io: IO, Atts >
sent(X, IO)
=> < X : User | state: 3, io: IO, Atts >
receive(IO, X) .
---- upon reception of the response, a new request is sent
---- the useful part of the response is stored in the result attribute
rl < X : User | state: 3, io: IO, result: "", Atts >
received(X, IO, Result) ---- Result --> "26\n"
=> < X : User | state: 4, io: IO,
result: substr(Result, 0, sd(length(Result), 1)), Atts >
send(IO, X, "4 * p\n") .
---- once the message has been sent, a new response is requested
rl < X : User | state: 4, io: IO, Atts >
sent(X, IO)
=> < X : User | state: 5, io: IO, Atts >
receive(IO, X) .
---- once this response is received, the process is terminated with a SIGTERM signal
rl < X : User | state: 5, process: P, io: IO, result: Str, Atts >
received(X, IO, Result) ---- Result --> "104\n"
=> < X : User | state: 6, process: P, io: IO,
result: substr(Result, 0, sd(length(Result), 1)), Atts >
signalProcess(P, X, "SIGTERM") .
---- signaledProcess and exited messages are received to confirm the operation
rl < X : User | state: 6, process: P, Atts >
signaledProcess(X, P)
exited(X, P, terminatedBySignal("SIGTERM"))
=> < X : User | state: 7, process: P, Atts > .
endm
We can run the above program with the following erewrite command:
Maude> erew <>
< me : User | state: 1, process: null, io: null, err: null, result: "" >
createProcess(processManager, me, "dc", nil, none) .
result Configuration:
<>
< me : User | state: 7,
process: process(66941), io: socket(3), err: socket(5),
result: "104" >
The execution terminates with the User object in its final state, with "104" as final result of the operations carried out by the dc process. Notice that when the current erewrite context is destroyed (say, by running a new rewrite command), Maude will kill any processes and close any sockets that correspond to Maude external objects in that context.
Each application has its own form of interaction. In this section we present a Maude program that interacts with a second Maude process, and, to analyze its output, it uses a Python program that is run on the Python 3 interpreter. Specifically, the program runs an external Maude process in which it loads the process-dc.maude file presented in the previous section. As shown there, the program uses the dc to do a calculation. Since the output is rather complex, we use a Python program to process the given output and extract the part we are interested in. The output is processed in a Python interpreter process using the function select_text. The string "104" is returned as result.
Although just for illustration purposes in this case, the use of other languages applications may be convenient in some of our programs. In this case, the use of regular expressions for the manipulation of strings comes quite handy. Our Python function select_text is very simple; it uses the functionality provided in the re module for searching a string s, passed as first argument, for a regular expression with the exact pattern we are interested in, which is given as second argument p:
As for the example in Section 9.4.1, we use an object to keep track of the process and information of the different sockets. Since we are going to have two of these processes, we can introduce the appropriate definitions as a generic class.
mod PROCESS-PROXY is
inc PROCESS .
inc MAYBE{Oid} * ( op maybe to null ) .
---- class Proxy | state: Nat, process: Maybe{Oid}, io: Maybe{Oid}, err: Maybe{Oid} .
sort Proxy .
subsort Proxy < Cid .
op Proxy : -> Proxy .
op state:_ : Nat -> Attribute .
ops process:_ io:_ err:_ : Maybe{Oid} -> Attribute . ---- process and channels
endm
In this program, we assume that both the Maude system (maude.darwin64) and the Python interpreter (python3) are in your path, and that the process-dc.maude file from the previous section is in your working directory. If this is not the case, please change the code below appropriately. A PATH constant is given for the location of Maude’s executable, which should be changed depending on your setting.
The functionality provided by the select_text Python function may be useful in different contexts. To make it available as an auxiliary function, we show below the PROCESS-PYTHON module, which provides a function string-extract that extracts a substring from a given string that matches a given pattern. Specifically, given a string-extract(X, Y, Str, Pat) message, it returns either string-extracted(Y, X, Result), with the matched substring, or string-extract-error(Y, X, Result), if any error happens.
mod PROCESS-PYTHON is
inc PROCESS-PROXY .
---- class Python | string: String, pattern: String, requester: Maybe{Oid} .
---- subclass Python < Proxy .
ops string:_ pattern:_ : String -> Attribute [ctor] .
op requester:_ : Maybe{Oid} -> Attribute [ctor] .
sort Python .
subsort Python < Proxy .
op Python : -> Python .
op string-extract : Oid Oid String String -> Msg .
ops string-extracted string-extract-error : Oid Oid String -> Msg .
vars X Y P ERR IO : Oid .
vars Result Str Pat : String .
var Atts : AttributeSet .
rl string-extract(X, Y, Str, Pat)
=> < X : Python | state: 1, process: null, io: null, err: null,
requester: Y, string: Str, pattern: Pat >
createProcess(processManager, X, "python3", "-iu" "string_extract.py", none) .
rl < X : Python | state: 1, process: null, io: null, err: null,
string: Str, pattern: Pat, Atts >
createdProcess(X, processManager, P, IO, ERR)
=> < X : Python | state: 2, process: P, io: IO, err: ERR, Atts >
send(IO, X, "select_text(’’’" + Str + "’’’, ’" + Pat + "’)\n")
waitForExit(P, X) .
rl < X : Python | state: 2, io: IO, err: ERR, Atts >
sent(X, IO)
=> < X : Python | state: 3, io: IO, err: ERR, Atts >
receive(IO, X)
receive(ERR, X) .
rl < X : Python | state: 3, io: IO, requester: Y, Atts > ---- output received
received(X, IO, Result) ---- Result --> "’104’\n"
=> < X : Python | state: 4, io: IO, requester: Y, Atts >
string-extracted(Y, X, substr(Result, 1, sd(length(Result), 3)))
send(IO, X, "quit()\n") .
rl < X : Python | state: 4, io: IO, Atts > ---- quit sent
sent(X, IO)
=> < X : Python | state: 5, io: IO, Atts > .
rl < X : Python | err: ERR, requester: Y, Atts > ---- error
received(X, ERR, Result)
=> < X : Python | err: ERR, requester: Y, Atts > ---- error msg might be empty
if Result == ">>> ... ... ... >>> " then none
else string-extract-error(Y, X, Result) fi .
rl < X : Python | state: 5, process: P, Atts > ---- process terminated
exited(X, P, normalExit(0))
=> none .
endm
The rules are explained in inline comments, but several issues are worth pointing out:
Although string-extract is declared as a message, notice that its first argument is the identifier used to create the proxy.
The string and the pattern need to be kept by the wrapper until the reception of the createdProcess message.
The Python process is started in interactive mode (using the -i flag), and the file string_extract.py with the above select_text function is also passed as a command argument.
In Python, strings may use either single quotes (’), quotes ("), or triple quotes (""" or ’’’). Since the output from the Maude process may contain quotes and new line characters, the string to search in is passed using triple single quotes. The pattern is passed using single quotes, assuming that it does not contain new line characters. Quotes could also be used in both cases, but then the string on which the search is performed should have to be manipulated before it is sent as an argument of the Python command. Remember that quotes inside strings must be double quoted, i.e., a string like "\"hi\"" must be sent as argument of the function as "select_text(\"\\\"hi\\\"\")". Notice that, since to put a quote inside a string you use \", and to put a backslash inside a string you use \\, then, to put \" inside a string you must use \\\".
The process is terminated using its quit command. Once the process is terminated, the wrapper is removed.
The following module uses the above string-extract function to extract the result from the execution of the process-dc.maude program.
Although the rules are explained in inlined comments below, there are a couple of issues worth pointing out:
The process-dc.maude file is passed as an argument of the maude.darwin64 command when the createProcess is sent. Notice also that Maude has to be invoked with the -trust flag to run external processes.
Maude gives a welcome header when started, and when a command is sent to it, it first acknowledges the command being executed, and then gives the actual output when it finishes.
In this case, we use a constant init to initiate the execution. The output and potential error messages are given with respective operators result and error.
mod PROCESS-MAUDE is
---- Maude’s path, empty string if in the system path or in the same directory
op PATH : -> String .
eq PATH = "" . ---- E.g., "/Users/duran/maude/maude-3.2"
inc PROCESS-PYTHON .
ops result error : String -> Msg .
op init : -> Configuration .
ops me python : -> Oid .
vars X Y P ERR IO : Oid .
vars Result Str Pat : String .
var Atts : AttributeSet .
---- the program begins by creating the Maude process
rl init
=> < me : Proxy | state: 1, process: null, io: null, err: null >
createProcess(processManager, me,
PATH + "maude.darwin64", "-trust" "process-dc.maude", none) .
---- Upon creation of the Maude process, it requests its banner
rl < X : Proxy | state: 1, process: null, io: null, err: null, Atts >
createdProcess(X, processManager, P, IO, ERR)
=> < X : Proxy | state: 2, process: P, io: IO, err: ERR, Atts >
receive(IO, X)
waitForExit(P, X) .
---- When the banner is received, the command is sent
---- This is the same command used in the previous section
rl < X : Proxy | state: 2, io: IO, Atts >
received(X, IO, Result) ---- Maude’s header
=> < X : Proxy | state: 3, io: IO, Atts >
send(IO, X,
"erew <> " +
"< me : User | state: 1, process: null, io: null, err: null, result: \"\" >"
+ " createProcess(processManager, me, \"dc\", nil, none) .\n") .
---- When the sending is confirmed, a request for input is sent
rl < X : Proxy | state: 3, io: IO, Atts >
sent(X, IO)
=> < X : Proxy | state: 4, io: IO, Atts >
receive(IO, X) .
---- Maude first sends the command being executed
---- In this case we send a receive message on both channels
rl < X : Proxy | state: 4, io: IO, err: ERR, Atts >
received(X, IO, Result) ---- command being executed
=> < X : Proxy | state: 5, io: IO, err: ERR, Atts >
receive(IO, X) ---- request output
receive(ERR, X) . ---- and potential error message
---- Once an answer is received, a quit command is sent to the Maude
---- process to terminate it, and a string-extract message is delivered
rl < X : Proxy | state: 5, io: IO, Atts > ---- result from ok execution
received(X, IO, Result)
=> < X : Proxy | state: 6, io: IO, Atts >
send(IO, X, "q\n")
string-extract(python, X, Result, "result: \"([^\"]*)\"") .
---- the response from the string-extract message is handled
rl < X : Proxy | state: 6, io: IO, Atts > ---- result from ok execution
string-extracted(X, Y, Result)
=> < X : Proxy | state: 7, io: IO, Atts > ---- result from ok execution
result(Result) .
rl < X : Proxy | Atts > ---- error execution
string-extract-error(X, Y, Result)
=> < X : Proxy | Atts >
error(Result) .
---- non-empty error messages are forwarded
rl < X : Proxy | err: ERR, Atts > ---- error
received(X, ERR, Result)
=> < X : Proxy | Atts >
if Result == "" then none else error(Result) fi . ---- no error message
---- sent and exited messages are consumed
rl < X : Proxy | state: 7, io: IO, process: P, Atts >
sent(X, IO)
exited(X, P, normalExit(0))
=> none .
endm
The execution of the program is then as follows.
When a control-C is typed during regular rewriting, execution is suspended and Maude gets into its debugger. However, when Maude is suspended on an external event, because no internal rewrites are possible, and it receives a control-C, it prints a message rather than immediately aborting. A second control-C without intervening rewrites will cause an abort to the command line without any attempt to print the current state.
The reason for this is to leave open the possibility of recovering from potential problems happening on external objects. Following the conventions of the underlying operative systems, “Interrupt signals generated in the terminal are delivered to the active process group, which here includes both parent and child.” In other words, when a control-C is typed, the signal is not only received by the Maude process, but also by all other active external processes depending on it. Each of these processes may respond to a control-C in different ways, but there might be cases in which we can make it recover once interrupted. If we do not want to try to recover the execution, and it remains suspended on the same event, we may type a second control-C to abort.
Let us illustrate some of these ideas in concrete examples. Specifically, let us revisit the examples presented in Section 9.4. To get the execution to suspend on an external event, let us introduce a little change in the specification of the desk calculator process example (module PROCESS-DC in Section 9.4.1). The file process-dc-faulty.maude includes exactly the same code as the one used in Section 9.4.1, but when submitting the second expression to be evaluated, instead of the message
it is being sent Notice that without \n, the dc does not process the input, and therefore it does not respond to our subsequent receive message. The process gets suspended waiting for an answer that will never arrive. By typing a control-C while the process is suspended, we observe the following behavior:
Maude> erew <>
> < me : User | state: 1, process: null, io: null, err: null, result: "" >
> createProcess(processManager, me, "dc", nil, none) .
erewrite in PROCESS-DC :
<>
< me : User | state: 1, process: null, io: null, err: null, result: "" >
createProcess(processManager, me, "dc", nil, none) .
^C
Control-C while suspended on external event(s).
A second control-C on the same suspension will abort execution and return to command
line.
rewrites: 11 in 1ms cpu (4721ms real) (8560 rewrites/second)
result Configuration:
<>
< me : User |
state: 6, process: process(58212), io: socket(3), err: socket(5), result: "" >
signalProcess(process(58212), me, "SIGTERM")
exited(me, process(58212), terminatedBySignal("SIGINT"))
Maude>
The control-C does not kill the Maude run. It shows the message
Control-C while suspended on external event(s).
A second control-C on the same suspension will abort execution and return to command
line.
Let us now consider our second example, the PROCESS-MAUDE specification in Section 9.4.2. We do not change anything on this example, just make it use the PROCESS-DC specification modified as above (available in file process-maude-faulty.maude). The question is that if we load the specification and run it with the corresponding erew command, we observe that the execution gets suspended. Notice that the program is creating a Maude process which loads the process-dc-faulty.maude file. The execution of the erew command gets suspended, as we saw above. The interesting thing is that we have just learnt how Maude handles an interrupt signal, and then, we know that if we type control-C, the external process also receives a control-C (an interrupt signal). Upon reception of this interrupt signal, the external Maude process produces some output, which is received by the main Maude process. It however does not receive a valid output, which leads to another suspension, although in this case it is the Python process that suspends, because it is unable to handle the text that receives. If a new control-C is typed, since it is a different suspension, the execution does not abort. Instead, we get a new message informing us about the situation, and telling us that, if the execution remains suspended in the same place, a second control-C will abort the execution. Since the interrupt signal received by the Python process does not get the execution to advance, a third control-C (second on this suspension event), forces the execution to abort. The following shows the interaction just explained:
erewrite in PROCESS-MAUDE : <> init .
^C
Control-C while suspended on external event(s).
A second control-C on the same suspension will abort execution and return to command line.
^C
Control-C while suspended on external event(s).
Note that this is a different suspension than the one that received a control-C 63 rewrites ago.
A second control-C on the same suspension will abort execution and return to command line.
^C
Second control-C while suspended on external event(s).
Aborting execution and returning to command line.
Advisory: closing open files.
Maude>
Note that no final output is presented. As we have seen above, if a control-C triggers some behavior in the external process that exits the suspension, Maude can complete its execution to a final state or end up suspended on some other external event which again requires two control-C events to abort. However, aborting execution is inherently a messy procedure that never has a printable final state.