The rewrite command

We can use the rewrite command (abbreviated rew) to explore the behavior of different initial markings. The bracketed number between the command and the term to be rewritten provides an upper bound for the number of rule applications that are allowed.

  Maude> rew [1] in VENDING-MACHINE : $ $ q q .
  rewrite [1] in VENDING-MACHINE : $ $ q q .
  rewrites: 1 in 0ms cpu (9ms real) (~ rews/sec)
  result Marking: $ $ q q q

  Maude> rew [2] $ $ q q .
  rewrite [2] in VENDING-MACHINE : $ $ q q .
  rewrites: 2 in 0ms cpu (0ms real) (~ rews/sec)
  result Marking: $ $ $ q q q

  Maude> rew [3] $ $ q q .
  rewrite [3] in VENDING-MACHINE : $ $ q q .
  rewrites: 3 in 0ms cpu (0ms real) (~ rews/sec)
  result Marking: $ $ $ q q q q

  Maude> rew [4] $ $ q q .
  rewrite [4] in VENDING-MACHINE : $ $ q q .
  rewrites: 4 in 0ms cpu (0ms real) (~ rews/sec)
  result Marking: $ $ $ $ q q q q

  Maude> rew [5] $ $ q q .
  rewrite [5] in VENDING-MACHINE : $ $ q q .
  rewrites: 5 in 0ms cpu (0ms real) (~ rews/sec)
  result Marking: $ $ $ $ $

  Maude> rew [6] $ $ q q .
  rewrite [6] in VENDING-MACHINE : $ $ q q .
  rewrites: 6 in 0ms cpu (0ms real) (~ rews/sec)
  result Marking: $ $ $ $ $ q

  Maude> rew [200] $ $ q q .
  rewrite [200] in VENDING-MACHINE : $ $ q q .
  rewrites: 200 in 10ms cpu (10ms real) (20000 rews/sec)
  result Marking: $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $
      $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $
      $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $
      $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ q q q

Executing one rewrite starting with two dollars and two quarters, Maude chooses to apply the add-q rule. If we allow two rewrites Maude applies add-q and then add-$. The third rule to be applied is add-q again; then, add-$. It goes on applying add-q and add-$ until the rule change can be applied. The top-down rule-fair rewrite strategy keeps trying to apply rules on the top operator (__ in this case) in a fair way. The rules applicable at the top are add-q, add-$, and change, which are tried in this order. Since the top operator is always the same one, no other rules are used. We can modify the rules buy-c and buy-a so that the lefthand side has an explicit top level __ as follows:

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

Now starting with two dollars and two quarters, and executing increasing numbers of rewrites we see that Maude applies the rules add-$, add-q, buy-c, buy-a, and change.

  Maude> rew [2] in VENDING-MACHINE-TOP : $ $ q q .
  Advisory: "v.maude", line 18 (mod VENDING-MACHINE-TOP): collapse at 
     top of $ M may cause it to match more than you expect.
  Advisory: "v.maude", line 19 (mod VENDING-MACHINE-TOP): collapse at 
     top of $ M may cause it to match more than you expect.
  rewrite [2] in VENDING-MACHINE-TOP : $ $ q q .
  rewrites: 2 in 0ms cpu (0ms real) (~ rews/sec)
  result Marking: $ $ $ q q q

  Maude> rew [3] $ $ q q .
  rewrite [3] in VENDING-MACHINE-TOP : $ $ q q .
  rewrites: 3 in 0ms cpu (0ms real) (~ rews/sec)
  result Marking: $ $ q q q c

  Maude> rew [4] $ $ q q .
  rewrite [4] in VENDING-MACHINE-TOP : $ $ q q .
  rewrites: 4 in 0ms cpu (0ms real) (~ rews/sec)
  result Marking: $ q q q q a c

  Maude> rew [5] $ $ q q .
  rewrite [5] in VENDING-MACHINE-TOP : $ $ q q .
  rewrites: 5 in 0ms cpu (0ms real) (~ rews/sec)
  result Marking: $ $ a c

The advisory is about the modified rules for buying. Maude is letting us know that the pattern $ M will match a term not containing the top-level operator __, when M is instantiated to null. This is exactly what we want in this case, but it may not always be what the user intended, so Maude gives you a heads up; see Section 13.2.6 for more details.

Notice that rewriting in VENDING-MACHINE is not terminating. If we remove the rules for adding coins we obtain a terminating system and can explore vending behavior using unbounded rewriting. Let us consider the following module SIMPLE-VENDING-MACHINE.

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

For example, starting with two dollars and rewriting as much as possible we can get an apple, a cake and a quarter in change.

  Maude> rew in SIMPLE-VENDING-MACHINE : $ $ .
  rewrite in SIMPLE-VENDING-MACHINE : $ $ .
  rewrites: 2 in 0ms cpu (0ms real) (~ rews/sec)
  result Marking: q a c

Starting with two dollars and three quarters and using only three rewrite rule applications we get an apple and a cake with a dollar left over.

  Maude> rew [3] $ $ q q q .
  rewrite [3] in SIMPLE-VENDING-MACHINE : $ $ q q q .
  rewrites: 3 in 0ms cpu (0ms real) (~ rews/sec)
  result Marking: $ a c

The command continue $\langle$Bound$\rangle$ (abbreviated cont) tells Maude to continue rewriting using at most $\langle$Bound$\rangle$ additional rule applications. For example, we can continue the last rewrite command (that performed three rewrites) for one more step to get an apple and two cakes:

  Maude> cont 1 .
  rewrites: 1 in 0ms cpu (0ms real) (~ rews/sec)
  result Marking: a c c