User interfaces

In order to generate in Maude an interface for an application $\mathcal{P}$, the first thing we need to do is to define the language for interaction. This can be done by defining a data type $\mathit{Sign}_\mathcal{P}$ for commands and other constructs.

As a running example for this chapter, we will specify a basic interface for the vending machine introduced in Section 5.1. First, we define in the module VENDING-MACHINE-GRAMMAR a language for interacting with the vending machine. The signature of this module extends the signature of VENDING-MACHINE-SIGNATURE with operators to represent the valid actions, namely: $ and q for inserting a dollar or a quarter in the machine; showBasket and showCredit for showing the items already bought or the remaining credit; buy1Apple and buy1Cake for buying an apple or a cake; and buy_:_ for buying a number of pieces of the same item.

  fmod VENDING-MACHINE-GRAMMAR is
    protecting VENDING-MACHINE-SIGNATURE .
    protecting NAT .
    sort Action .
    op $ : -> Action .
    op q : -> Action .
    op showBasket : -> Action .
    op showCredit : -> Action .
    op buy1Cake : -> Action .
    op buy1Apple : -> Action .
    op buy_:_ : Item Nat -> Action .
  endfm

Next, we define in an extension of the LOOP-MODE module the terms of sort State representing the state of the loop for this application. In the module VENDING-MACHINE-INTERFACE below, we define this state as a triple: its first component is the next action requested by the client (inserting a coin, showing information about the remaining credit or the items already bought, or buying one or more items); its second component is the current state of the machine (the marking of the vending machine, that is, the remaining credit plus the items already bought); and its third component represents the response of the machine to the last action requested by the client. The response of the vending machine will have the form of a message, which can be represented as a list of quoted identifiers. The constant init denotes the initial state of the whole system, including the empty input and output streams and the ``empty'' initial state of the vending machine.

  mod VENDING-MACHINE-INTERFACE is
    including LOOP-MODE .
    including VENDING-MACHINE-GRAMMAR .
    protecting BUYING-STRATS .
    protecting CONVERSION .

    op <_;_;_> : Action Marking QidList -> State .
    op init : -> System .
    op idle : -> Action .
    eq init = [nil, < idle ; null ; nil >, nil] .

    var  A : Action .
    var  I : Item .
    var  C : Coin .
    var  M : Marking .
    vars QIL QIL' QIL'' : QidList .
    var  N : Nat .

Now we define in this module, using rewrite rules, the interaction of the state of the vending machine with the loop--and, consequently, with the client--and the changes produced in the state of the vending machine by the actions requested by the client. As explained before, the client will request an action by enclosing the text in parentheses, which will then be converted into a list of quoted identifiers and placed in the first slot of the loop object. The rule in detects when a valid request has been introduced by the user and, if the vending machine is idle, passes it as the next action to be attempted. To define the interaction of the state of the vending machine with the client, we can use the strategies introduced in the BUYING-STRATS module described in Section 11.5. Recall that BUYING-STRATS includes the META-LEVEL module.

In the rule in below, the operation metaParse checks whether the input stream corresponds to a term of sort Action. If this is the case, metaParse returns the metarepresentation of that term, which is then ``moved down'' using the META-LEVEL function downTerm (see Section 11.4.1), and is placed in the action slot of the State triple; otherwise, an error message is placed in its output.

    crl [in] :
      [QIL, < idle ; M ; nil >, QIL']
       => if T:ResultPair? :: ResultPair
          then [nil, 
                < downTerm(getTerm(T:ResultPair?), idle) ; M ; nil >, 
                QIL']
          else [nil, < idle ; M ; nil >, 'ERROR QIL]
          fi
       if QIL =/= nil
          /\ T:ResultPair?  
               := metaParse(upModule('VENDING-MACHINE-GRAMMAR, false), 
                    QIL, 'Action) .

For the other direction of the interaction, the rule out detects when the vending machine has a response to be output and, in that case, it places it in the output slot of the loop object.

    crl [out] :
       [QIL, < A ; M ; QIL' >, QIL'']
       => [QIL, < A ; M ; nil >, QIL''  QIL']
       if QIL' =/= nil .

Next, we define the effects of the different actions on the state of the vending machine. The rules showBasket and showCredit extract the information about the remaining credit or the items already bought, and place it in the output slot of the state; the rule out will then take care of moving it to the output slot of the loop object. In the definitions of the auxiliary functions showBasket and showCredit, the operation metaPrettyPrint takes the metarepresentation of a coin or an item, and returns the list of quoted identifiers that encode the list of tokens produced by pretty-printing the coin or the item in the module VENDING-MACHINE-SIGNATURE. Coins and items, and, more generally, markings of a vending machine are metarepresented using the META-LEVEL function upTerm (see Section 11.4.1).

    op showBasket : Marking -> QidList .   
    eq showBasket(I M)
       = metaPrettyPrint(upModule('VENDING-MACHINE-SIGNATURE, false), 
           upTerm(I))
         showBasket(M) .
    eq showBasket(C M) = showBasket(M) .
    eq showBasket(null) = nil .

    op showCredit : Marking -> QidList .
    eq showCredit(C M)
       = metaPrettyPrint(upModule('VENDING-MACHINE-SIGNATURE, false), 
           upTerm(C))
         showCredit(M) .
    eq showCredit(I M) = showCredit(M) .
    eq showCredit(null) = nil .

    rl [showBasket] :
        < showBasket ; M ; nil >
        => < idle ; M ; ('\u 'basket: '\o showBasket(M) '\n) > .

    rl [showCredit] :
       < showCredit ; M ; nil >
       => < idle ; M ; ('\u 'credit: '\o showCredit(M) '\n) > .

The rules labeled insertCoin implement the actions of inserting a dollar or a quarter in the vending machine. The strategy insertCoin defined in the module BUYING-STRATS (see Section 11.5) is used to produce the corresponding change in the current marking of the vending machine. Since strategies are applied at the metalevel, both the marking of the vending machine and the coin to be inserted must be first metarepresented using again the META-LEVEL function upTerm.

    rl [insertCoin] :
      < q ; M ; nil >
      => < idle ; 
           downTerm(insertCoin('add-q, upTerm(M)), null) ; 
           nil > .

    rl [insertCoin] :
      < $ ; M ; nil >
      => < idle ; 
           downTerm(insertCoin('add-$, upTerm(M)), null) ; 
           nil > .

The rules buy1Cake, buy1Apple, and buyNitems implement the actions of buying one or more items. The strategy onlyNitems defined in the module BUYING-STRATS (see Section 11.5) is used to produce the corresponding change in the current marking of the vending machine. Again, since strategies are applied at the metalevel, the marking of the vending machine must be first metarepresented.

    rl [buy1Cake]:
      < buy1Cake ; M ; nil >
      => < buy c : 1 ; M ; nil > .

    rl [buy1Apple]:
      < buy1Apple ;  M ; nil >
      => < buy a : 1 ; M ; nil > .

    rl [buyNitems]:
      < buy c : N ;  M ; nil >
      => < idle ; 
           downTerm(onlyNitems(upTerm(M), 'buy-c, N), null) ; 
           nil > .

    rl [buyNitems]:
      < buy a : N ;  M ; nil >
      => < idle ; 
           downTerm(onlyNitems(upTerm(M), 'buy-a, N), null) ; 
           nil > .
  endm