The search command

The rewrite and frewrite commands each explore just one possible behavior (sequence of rewrites) of a system described by a set of rewrite rules and an initial state. The search command allows one to explore (following a breadth-first strategy) the reachable state space in different ways. Its syntax conforms to the following general scheme

  search  [ ] in $\langle$ModId$\rangle$ : $\langle$Term-1$\rangle$ $\langle$SearchArrow$\rangle$ $\langle$Term-2$\rangle$
    such that $\langle$Condition$\rangle$ .

where

• $n$ is an optional argument providing a bound on the number of desired solutions;
• $m$ is another optional argument stating the maximum depth of the search;
• the module $\langle$ModId$\rangle$ where the search takes place can be omitted;
• $\langle$Term-1$\rangle$ is the starting term;
• $\langle$Term-2$\rangle$ is the pattern that has to be reached;
• $\langle$SearchArrow$\rangle$ is an arrow indicating the form of the rewriting proof from $\langle$Term-1$\rangle$ until $\langle$Term-2$\rangle$:
  • =>1 means a rewriting proof consisting of exactly one step,
  • =>+ means a rewriting proof consisting of one or more steps,
  • =>* means a proof consisting of none, one, or more steps, and
  • =>! indicates that only canonical final states are allowed, that is, states that cannot be further rewritten; and
  The one step arrow =>1 is an abbreviation of the one-or-more steps arrow =>+ with the depth bound $m$ set to 1.
• $\langle$Condition$\rangle$ states an optional property that has to be satisfied by the reached state; the syntactic form of the condition is the same as the one of conditions for conditional equations and memberships (see Section 4.3).

For example, for our finite vending machine, SIMPLE-VENDING-MACHINE, we can use the search command to answer the question: if I have a dollar and three quarters, can I get a cake and an apple? This is done by searching for states that match a corresponding pattern. In this example, we use the =>! symbol, meaning that we are searching for terminal states, that is, for states that cannot be further rewritten. Moreover, no bound in the number of solutions or in the depth of the search is needed.

  Maude> search in SIMPLE-VENDING-MACHINE : 
           $ q q q =>! a c M:Marking .
  search in SIMPLE-VENDING-MACHINE : $ q q q =>! a c M:Marking .

  Solution 1 (state 4)
  states: 6  rewrites: 5 in 0ms cpu (0ms real) (~ rews/sec)
  M:Marking --> null

  No more solutions.
  states: 6  rewrites: 5 in 0ms cpu (1ms real) (~ rews/sec)

The answer is yes, and the desired state is numbered 4. To see the sequence of rewrites that allowed us to reach this state we can type

  Maude> show path 4 .
  state 0, Marking: $ q q q
  ===[ rl $ => q a [label buy-a] . ]===>
  state 2, Marking: q q q q a
  ===[ rl q q q q => $ [label change] . ]===>
  state 3, Marking: $ a
  ===[ rl $ => c [label buy-c] . ]===>
  state 4, Marking: a c

One can get just the sequence of labels of applied rules with a similar command:

  Maude> show path labels 4 .
  buy-a
  change
  buy-c

It is also possible to print out the current search graph generated by a search command using the command show search graph. After the above search we get

  Maude> show search graph .
  state 0, Marking: $ q q q
  arc 0 ===> state 1 (rl $ => c [label buy-c] .)
  arc 1 ===> state 2 (rl $ => q a [label buy-a] .)

  state 1, Marking: q q q c

  state 2, Marking: q q q q a
  arc 0 ===> state 3 (rl q q q q => $ [label change] .)

  state 3, Marking: $ a
  arc 0 ===> state 4 (rl $ => c [label buy-c] .)
  arc 1 ===> state 5 (rl $ => q a [label buy-a] .)

  state 4, Marking: a c

  state 5, Marking: q a a

This search graph is represented graphically in Figure 5.2.

Figure 5.2: Graphical representation of search graph in example

From the same initial state, $ q q q, we can see if it is possible to reach a final state with an apple and more things, learning that there are exactly two possibilities:

  Maude> search $ q q q =>! a M:Marking such that M:Marking =/= null .
  search in SIMPLE-VENDING-MACHINE : $ q q q =>! a M:Marking 
    such that M:Marking =/= null = true .

  Solution 1 (state 4)
  states: 6  rewrites: 6 in 0ms cpu (0ms real) (~ rews/sec)
  M:Marking --> c

  Solution 2 (state 5)
  states: 6  rewrites: 7 in 0ms cpu (0ms real) (~ rews/sec)
  M:Marking --> q a
 
  No more solutions.
  states: 6  rewrites: 7 in 0ms cpu (0ms real) (~ rews/sec)

Sometimes it is necessary to impose a limit on the number of solutions searched for, since in general the number of such solutions could be infinite. In the previous examples there were only one or two solutions, so imposing a bound would not make any difference. But, returning to the coin generating (and thus nonterminating) vending machine module VENDING-MACHINE, the search space becomes now infinite, so it is important to be able to limit either the number of solutions sought or the depth of the search, or both.

We can look for different ways to use a dollar and three quarters to buy an apple and two cakes. First we ask for one solution, and then use the bounded continue command to see another solution. Note that here we use the search mode =>+, which means searching for states reachable by at least one rewrite. Searching for terminal states in the VENDING-MACHINE module is futile!

  Maude> search [1] in VENDING-MACHINE : $ q q q =>+ a c c M:Marking .
  search in VENDING-MACHINE : $ q q q =>+ a c c M .

  Solution 1 (state 108)
  states: 109 rewrites: 1857 in 0ms cpu (41ms real)(~rews/sec)
  M --> q q q q

  Maude> cont 1 .
  Solution 2 (state 113)
  states: 114 rewrites: 185 in 0ms cpu (4ms real) (~ rews/sec)
  M --> null

We can also use the maximum depth optional argument, but if we put a too small depth, we do not get any solution:

  Maude> search [, 4] $ q q q =>+ a c c M:Marking .
  search [, 4] in VENDING-MACHINE : $ q q q =>+ a c c M .

  No solution.
  states: 66  rewrites: 875 in 10ms cpu (3ms real) (87500 rews/sec)

By increasing the depth to 10 we will get 98 solutions. If we are interested in only a few of those, we can set both bounds, like in the following example:

  Maude> search [4, 10] $ q q q =>+ a c c M:Marking .
  search [4, 10] in VENDING-MACHINE : $ q q q =>+ a c c M .

  Solution 1 (state 108)
  states: 109  rewrites: 1857 in 0ms cpu (7ms real) (~ rews/sec)
  M --> q q q q

  Solution 2 (state 113)
  states: 114  rewrites: 2042 in 0ms cpu (7ms real) (~ rews/sec)
  M --> null

  Solution 3 (state 160)
  states: 161  rewrites: 3328 in 0ms cpu (11ms real) (~ rews/sec)
  M --> q q q q q

  Solution 4 (state 164)
  states: 165  rewrites: 3524 in 0ms cpu (12ms real) (~ rews/sec)
  M --> q

If we insist now in the marking M being different from null, then one of the previous solutions is discarded, but we still get four solutions:

  Maude> search [4, 10] $ q q q =>+ a c c M:Marking 
           such that M:Marking =/= null .
  search [4, 10] in VENDING-MACHINE : $ q q q =>+ a c c M 
    such that M =/= null = true .

  Solution 1 (state 108)
  states: 109  rewrites: 1858 in 0ms cpu (5ms real) (~ rews/sec)
  M --> q q q q

  Solution 2 (state 160)
  states: 161  rewrites: 3331 in 10ms cpu (13ms real) (333100 rews/sec)
  M --> q q q q q

  Solution 3 (state 164)
  states: 165  rewrites: 3528 in 10ms cpu (14ms real) (352800 rews/sec)
  M --> q

  Solution 4 (state 175)
  states: 176  rewrites: 3904 in 10ms cpu (15ms real) (390400 rews/sec)
  M --> $ q q q q

In Chapter 9 we will see how the search command can be used to model check invariant properties of a concurrent system specified in Maude as a system module.

In case you forget to set a bound on the search command or on its continuation, you can also interrupt a search in progress by typing control-C. In this case one of two things will happen, depending on what Maude is doing at the instant you hit control-C. If Maude is not doing a rewrite, the command will exit. If Maude is doing a rewrite, you will end up in the debugger. In this latter case it is probably best to type abort, since the debugger has no special support for search at the moment. See Sections 13.1.3 and 16.10 for more information on the debugger.

The full syntax and different options for the search command and for all the other commands illustrated in this section are explained in detail in Chapter 16.