Unconditional rules

Mathematically, an unconditional rewrite rule has the form $l: t \rightarrow t'$, where $t,t'$ are terms of the same kind, which may contain variables, and $l$ is the label of the rule. Intuitively, a rule describes a local concurrent transition in a system: anywhere in the distributed state where a substitution instance $\sigma(t)$ of the lefthand side $t$ is found, a local transition of that state fragment to the new local state $\sigma(t')$ can take place. And if many instances of the same or of several rules can be matched in different nonoverlapping parts of the distributed state, then all of them can fire concurrently.

An unconditional rule is introduced in Maude with the following syntax:

  rl [$\langle$Label$\rangle$] : $\langle$Term-1$\rangle$ => $\langle$Term-2$\rangle$ [$\langle$StatementAttributes$\rangle$] .

As explained in Section 4.5.1, a label can alternatively be declared as a statement attribute; also, Maude allows declaration of unlabeled rules. In these two cases, the part ``[$\langle$Label$\rangle$] :'' is omitted.

As a first example of a system module we consider the following specification of a vending machine which dispenses apples and cakes. The module VENDING-MACHINE-SIGNATURE is the underlying functional module. This module is imported by the system module VENDING-MACHINE, which then adds the rules for operating the machine. Although not necessary, in addition to making the underlying functional module explicit, such splitting of modules can be useful in organizing a large specification, where a functional part may be shared by several system modules; see Chapter 6 for a discussion on module importation.

The constants $ and q represent coins of one dollar and one quarter, respectively, while the constants a and c represent apples and cakes, respectively.

  fmod VENDING-MACHINE-SIGNATURE is
    sorts Coin Item Marking .
    subsorts Coin Item < Marking .
    op __ : Marking Marking -> Marking [assoc comm id: null] .
    op null : -> Marking .
    op $ : -> Coin [format (r! o)] .
    op q : -> Coin [format (r! o)] .
    op a : -> Item [format (b! o)] .
    op c : -> Item [format (b! o)] .
  endfm

The format declaration for each constant (see Section 4.4.5) is used to print the constants using different colors, so that coins can easily be separated from items in a given marking.

  mod VENDING-MACHINE is
    including VENDING-MACHINE-SIGNATURE .
    var M : Marking .
    rl [add-q] : M => M q .
    rl [add-$] : M => M $ .
    rl [buy-c] : $ => c .
    rl [buy-a] : $ => a q .
    rl [change] : q q q q => $ .
  endm

This module specifies a concurrent machine to buy cakes and apples with dollars and quarters. A cake costs a dollar, and an apple three quarters. We can insert dollars and quarters in the machine, although due to an unfortunate design, the machine only accepts buying cakes and apples with dollars. When the user buys an apple the machine takes a dollar and returns a quarter. To alleviate in part this problem, the machine can change four quarters into a dollar.

The machine is concurrent, because we can push several buttons at once (that is, we can apply several rules at once), provided enough resources exist in the corresponding slots, called places. For example, if we have one dollar in the $ place and four quarters in the q place, we can simultaneously push the buy-a and change buttons, and the machine returns, also simultaneously, one dollar in $, one apple in a, and one quarter in q.

Note that, since the Maude interpreter is sequential, the above concurrent transitions in the VENDING-MACHINE module are simulated by corresponding interleavings of sequential rewriting steps. In a socket-based concurrent implementation, it is possible to execute concurrently many rewriting steps for a wide range of system modules.^5.1

We might have tried a simpler alternative, namely, using the rule null => q instead of the add-q rule. However, this would not work. Instead, we have to write M => M q with M a variable of sort Marking. The reason is that the constant null is not a __-subterm of any marking except itself, and therefore it would be impossible to apply the rule null => q with extension (see Section 4.8).