Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

Hi,

Rules are not required to be confluent or terminating and thus to do a useful 
computation with them, some strategy is required. Currently Maude has several 
ways of executing rules:

rewrite (rew) finds a single path, trying to do rewrites near the top of the 
term first, and chosing rules in a round robin.

frewrite (frew) finds a single path, making passes over the term, and in each 
bottom up pass it tries to do a certain number of rewrites at each position.

erewrite (erew) is like frewrite but with special handling of external 
objects.

search looks at the whole rewriting graph, considering every possible rewrite 
from each term, in a breadthfirst manner.

srewrite (srew) is only partly implemented in recent alpha releases; it does 
search under a user provided strategy.

The model checker considers the whole term graph, but does a double 
depthfirst 
search for a single counter-example.

It's hard to predict which execution mechanism will be fastest on a given 
example - they are intended for different purposes and if the system is non-
confluent or non-terminating, will produce different results.

I suspect your system has additional rewriting paths that are non-intuitive 
because they involve rewriting at the top, perhaps duplicating subterms that 
are rewritable and thus increasing the amount of work done.

You could try frewrite.

Steven


On Saturday 17 April 2010, Sung-Shik Jongmans wrote:
> Hi,
> 
> I have a Maude system whose rewrite rules define only one possible behavior
>  (i.e. computation-path) given some initial state q_0. Let <> foo be an LTL
>  property, and let foo be false in the "last" state, say q_n, on the
>  computation-path. Entering:
> 
>     Maude> red modelCheck(q_0, <> foo) .
> 
> results in a counterexample as expected, and Maude reports that it has
>  performed 18848 rewrites; the counterexample Maude displays is the whole
>  computation path from q_0 up to and including q_n. So far so good :).
> 
> However, when I enter:
> 
>     Maude> rew q_0 .
> 
> Maude reports that is has performed 59203 rewrites, and it displays state
>  q_n. That is, it seems as if Maude required three times more rewrites to
>  get to q_n in this latter case, than that it required to generate the
>  counterexample when model-checking. This appears a bit counterintuitive to
>  me: it would suggest that model-checking in this case is less
>  resource-demanding than "normal" execution, even though the same states
>  are explored.
> 
> Could anyone shed some light on what's happening here?
> 
> Kind regards,
> -Sung.
>