External objects

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

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

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

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

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

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