Configurations

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

  mod CONFIGURATION is
    *** basic object system sorts
    sorts Object Msg Configuration .

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

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

A typical configuration will have the form

  $\langle$Ob-1$\rangle$ ... $\langle$Ob-k$\rangle$  $\langle$Mes-1$\rangle$ ... $\langle$Mes-n$\rangle$

where $\langle$Ob-1$\rangle$, ..., $\langle$Ob-k$\rangle$ are objects, $\langle$Mes-1$\rangle$, ..., $\langle$Mes-n$\rangle$ are messages, and the order is immaterial.

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

  rl $\langle$Ob-1$\rangle$ ... $\langle$Ob-k$\rangle$ $\langle$Mes-1$\rangle$ ... $\langle$Mes-n$\rangle$
    => $\langle$Ob'-1$\rangle$ ... $\langle$Ob'-j$\rangle$ $\langle$Ob-k+1$\rangle$ ... $\langle$Ob-m$\rangle$ $\langle$Mes'-1$\rangle$ ... $\langle$Mes'-p$\rangle$ .

where $\langle$Ob'-1$\rangle$, ..., $\langle$Ob'-j$\rangle$ are updated versions of $\langle$Ob-1$\rangle$, ..., $\langle$Ob-j$\rangle$ for $j \leq k$, $\langle$Ob-k+1$\rangle$, ..., $\langle$Ob-m$\rangle$ are newly created objects, and $\langle$Mes'-1$\rangle$, ..., $\langle$Mes'-p$\rangle$ 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 15). For this purpose four new sorts are introduced: Oid (object identifiers), Cid (class identifiers), Attribute (a named element of an object's state), and AttributeSet (multisets of attributes). Further details about the CONFIGURATION module are discussed later in Section 8.4.

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

In this syntax, objects have the general form

  < O : C | $\langle$att-1$\rangle$, ..., $\langle$att-k$\rangle$ >

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

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

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

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

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

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

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

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

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

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

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

Now we could replace

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

by

  from A-003 to A-002 transfer 300

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

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

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

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

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

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

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

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

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

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

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

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

Then, we rewrite the configuration mgrConf:

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

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

Figure 8.1: Importation graph of bank modules

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  mod TICKER-CUSTOMER is
    inc TICKER-FACTORY .
    ops Cust Cust1 Cust2 :  Aid Aid Nat ->  Actor [ctor] .

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

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

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

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

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

Figure 8.2: Importation graph of ticker modules

  mod TICKER-FACTORY-TEST is
    ex TICKER-CUSTOMER .
    ops tf c1 c2 : -> Aid [ctor] .
    ops ic1 ic2 : -> AConf .
    eq ic1 = TickerFactory(tf, 0) Cust(c1, tf, 0)  .
    eq ic2 = ic1 Cust(c2, tf, 0) .
  endm

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

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

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

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

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

  Maude> set profile on .

(see Section 13.1.4) before rewriting and then execute

  Maude> show profile .

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

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

  Maude> set profile off .

when you have found out what you want to know.

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

• give to the constructor of object and message configurations the config attribute,
• give to the message constructor the message attribute, and
• give to each object constructor the object attribute.

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

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

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

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

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

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

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

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

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

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