fancy-vending.maude

mod FANCY-VENDING is
  --- a single sort Q of states
  sort Q .
  
  --- a state may have no tokens...
  op ø : -> Q [ctor] .
  --- ...or it may have one token of some kind...
  ops $ $c q qc m&m orr cok : -> Q [ctor] .
  --- ...or it may be the union of two such states
  op _ _ : Q Q -> Q [ctor assoc comm id: ø] .

  --- exchanging between dollars and dollar credits
  rl [∂] : $ => $c .
  rl [#] : $c => $ .

  --- exchanging between quarters and quarter credits
  rl [∂'] : q => qc .
  rl [#'] : qc => q .

  --- changing four quarter credits up to a dollar credit
  rl [chng] : qc qc qc qc => $c .

  --- inflation is really getting out of hand these days
  rl [1] : $c $c => m&m qc qc qc .
  rl [2] : $c $c $c => orr qc qc qc .
  rl [3] : $c $c $c => cok qc qc .
endm