Maude-help mailing list

[Ionut Tutu <ittutu AT gmail.com>]

Dear Răzvan,

I don't think `search' is faster than `rewrite'; this issue might
actually be related to the internal computation of resource usage.

On my computer, Maude (2.7.1) reported the following information:

Maude> rewrite in SEQUENCE123-TRAVERSE : < nil | sequence-of-digits(from 1 till 2016) | 0 > .
rewrites: 33273750 in 15316ms cpu (15403ms real) (2172402 rewrites/second)

Maude> search in SEQUENCE123-TRAVERSE : < nil | sequence-of-digits(from 1 till 2016) | 0 > =>* < L | nil | c > .
states: 6958  rewrites: 33273915 in 1279ms cpu (1282ms real) (26011747 rewrites/second)

But the second command was in fact executed in almost 17 seconds,
which is not unexpected. This becomes clear if one times externally
how long it takes to execute each of the two commands:

$ time maude rewrite-vs-search.maude
==========================================
rewrite in SEQUENCE123-TRAVERSE : < nil | sequence-of-digits(from 1 till 2016) | 0 > .
rewrites: 33273750 in 12753ms cpu (12804ms real) (2608889 rewrites/second)
Bye.
------------------------------------------
real 0m12.895s
user 0m12.818s
sys 0m0.025s

$ time maude rewrite-vs-search.maude
==========================================
search in SEQUENCE123-TRAVERSE : < nil | sequence-of-digits(from 1 till 2016) | 0 > =>* < L | nil | c > .
states: 6958  rewrites: 33273915 in 1362ms cpu (1366ms real) (24417619 rewrites/second)
Bye.
------------------------------------------
real 0m14.394s
user 0m14.186s
sys 0m0.143s

I hope this helps.

All the best,
Ionut

On Tue, 18 Jun 2019 at 18:03, Razvan Diaconescu <Razvan.Diaconescu AT ymail.com> wrote:

Dear Friends,

Consider the following Maude program (the comments explain what it does).
I do not understand why when running both search and rewrite on the same
example, although the number of rewrites is about ther same, the former runs
about 20 times faster than the latter. Somehow I thought the opposite, that
in principle rewrite is always faster than search.

I apologise if the question may be a bit stupid, but my knowledge of the
Maude engine is very low.

Thanks,
Razvan

==========================================

--- ------------------------------------------
--- counts the number of the sub-sequences 123
--- in the sequence of all digits obtained by
--- concatenating all numbers from 1 to 2016
--- ------------------------------------------


--- generates the list of the numbers from m to n

mod LIST-OF-NUMBERS-FROM-TILL is
  protecting LIST{Nat} .
  op from_till_ : Nat Nat -> List{Nat} .
  vars n m : Nat .
  ceq from m till n = m (from (m + 1) till n) if m <= n .
  ceq from m till n = nil                   if n < m .
endm

--- concatenates the numbers of a list of numbers
--- then builds the list of digits of the obtained number

mod SEQUENCE-OF-DIGITS is
  protecting LIST-OF-NUMBERS-FROM-TILL .
  var n : Nat .
  var L : List{Nat} .
  op sequence-of-digits : List{Nat} -> List{Nat} .
  eq sequence-of-digits(nil) = nil .
  ceq sequence-of-digits(n L) = (n sequence-of-digits(L))
    if  n < 10 .
  ceq sequence-of-digits(n L) =
      sequence-of-digits((n quo 10) (n rem 10) sequence-of-digits(L))
    if 10 <= n .
endm

***(
reduce in SEQUENCE-OF-DIGITS : sequence-of-digits(from 1 till 2016) .
)

--- the main program, by traversing a list of digits

mod SEQUENCE123-TRAVERSE is
  protecting SEQUENCE-OF-DIGITS .
  sort Config .
  op <_|_|_> : List{Nat} List{Nat} Nat -> Config .
  vars L L' : List{Nat} .
  vars m n k c : Nat .
  rl < nil | (n L) | c > => <     n | L | c > .
  rl < m   | (n L) | c > => < (m n) | L | c > .
  rl  < (1 2) | (3 L) | c > => < (2 3) | L | c + 1 > .
  crl < (m n) | (k L) | c > => < (n k) | L | c     >
    if k =/= 3 or m =/= 1 or n =/= 2 .
endm

***(
search in SEQUENCE123-TRAVERSE :
  < nil | sequence-of-digits(from 1 till 2016) | 0 > =>*
  <   L | nil                                  | c > .
rewrite in SEQUENCE123-TRAVERSE :
  < nil | sequence-of-digits(from 1 till 2016) | 0 > .
)