metaSearchPath

The operation metaSearchPath is complementary to metaSearch and carries out the same search, but instead of returning the final state and matching substitution it returns the sequence of states and rules on a path starting with the reduced initial state and leading to (but not including) the final state.

  op metaSearchPath : 
       Module Term Term Condition Qid Bound Nat ~> Trace?
       [special (...)] .

The sort Trace is used to represent the path as a list of triples by means of the following syntax:

  sorts TraceStep Trace Trace? .
  subsorts TraceStep < Trace < Trace? .
  op {_,_,_} : Term Type Rule -> TraceStep [ctor] .
  op nil : -> Trace [ctor] .
  op __ : Trace Trace -> Trace [ctor assoc id: nil format (d n d)] .
  op failure : -> Trace? [ctor] .

We run again the same two examples as above, with the following results.

  Maude> reduce in META-LEVEL :
           metaSearchPath(upModule('VENDING-MACHINE, false),
             '__['$.Coin, 'q.Coin, 'q.Coin,'q.Coin],
             '__['c.Item, 'a.Item, 'c.Item, 'M:Marking],
             nil, '+, unbounded, 0) .
  result Trace:
    {'__['$.Coin,'q.Coin,'q.Coin,'q.Coin],
     'Marking,
     rl 'M:Marking => '__['$.Coin,'M:Marking] [label('add-$)] .}
    {'__['$.Coin,'$.Coin,'q.Coin,'q.Coin,'q.Coin],
     'Marking,
     rl 'M:Marking => '__['$.Coin,'M:Marking] [label('add-$)] .}
    {'__['$.Coin,'$.Coin,'$.Coin,'q.Coin,'q.Coin,'q.Coin],
     'Marking,
     rl '$.Coin => 'c.Item [label('buy-c)] .}
    {'__['$.Coin,'$.Coin,'q.Coin,'q.Coin,'q.Coin,'c.Item],
     'Marking,
     rl '$.Coin => 'c.Item [label('buy-c)] .}
    {'__['$.Coin,'q.Coin,'q.Coin,'q.Coin,'c.Item,'c.Item],
     'Marking,
     rl '$.Coin => '__['q.Coin,'a.Item] [label('buy-a)] .}

  Maude> reduce in META-LEVEL :
           metaSearchPath(upModule('VENDING-MACHINE, false),
             '__['$.Coin, 'q.Coin, 'q.Coin, 'q.Coin],
             '__['c.Item, 'a.Item, 'c.Item, 'M:Marking],
             nil, '+, unbounded, 1) .
  result Trace:
    {'__['$.Coin,'q.Coin,'q.Coin,'q.Coin],
     'Marking,
     rl 'M:Marking => '__['$.Coin,'M:Marking] [label('add-$)] .}
    {'__['$.Coin,'$.Coin,'q.Coin,'q.Coin,'q.Coin],
     'Marking,
     rl '$.Coin => 'c.Item [label('buy-c)] .}
    {'__['$.Coin,'q.Coin,'q.Coin,'q.Coin,'c.Item],
     'Marking,
     rl '$.Coin => '__['q.Coin,'a.Item] [label('buy-a)] .}
    {'__['q.Coin,'q.Coin,'q.Coin,'q.Coin,'a.Item,'c.Item],
     'Marking,
     rl '__['q.Coin,'q.Coin,'q.Coin,'q.Coin] => '$.Coin 
       [label('change)] .}
    {'__['$.Coin,'a.Item,'c.Item],
     'Marking,
     rl '$.Coin => 'c.Item [label('buy-c)] .}

The operations metaSearchPath and metaSearch share caching, so calling one after the other on the same arguments only performs a single search.