The rewrite, frewrite, and search commands

Now we illustrate the use of the Maude commands available for system modules. Recall the vending machine example:

  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

In addition to the show commands discussed in Section 4.9, there is an additional show rls command for system modules to show the rules of a module. For example, showing the sorts and the rules of the VENDING-MACHINE module we get:

  Maude> show sorts VENDING-MACHINE .
  sort Bool .
  sort Coin .     subsort Coin < Marking .
  sort Item .     subsort Item < Marking .
  sort Marking .  subsorts Item Coin < Marking .

  Maude> show rls VENDING-MACHINE .
  rl M => q M [label add-q] .
  rl M => $ M [label add-$] .
  rl $ => c [label buy-c] .
  rl $ => q a [label buy-a] .
  rl q q q q => $ [label change] .