Maude-help mailing list

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

Hi,

Thanks very much for the bug report. There is a serious and subtle bug in the 
sort computation code. Specifically, when an A or AU argument list becomes 
long enough, Maude switches to a persistent deque representation which allows 
certain kinds of patterns to be matched in constant time, certain kinds of 
rhs replacements to be reflattened in constant time and sort computations to 
be performed incrementally in constant time. There is a bug in the pointer 
reversal code for the latter algorithm such that sorts previously calculated 
for parts of an argument list are not used in the final calculation, with the 
possibility that the wrong final sort will be calculated. Since the 
persistent deque representation is highly redundant you have to do just the 
right sequence of rewrites to hit the bad case.

The will be an alpha release with a fix in the next day or so, with a public 
release in a week or two. If you would like to be an alpha tester let me know 
and I will send you the alpha release site details.

Best regards,

Steven Eker

On Tuesday 08 June 2004 04:15 am, Jon Haugsand wrote:
> Hi,
>
> Thanks for previous help.  Here is a question I do not understand.
> Included is short Maude specification where an Int (from the INT
> module) is matched to a sequence of integers as defined in included
> module.  Part of trace is follows here:
>
> *********** equation
> eq seqtotree(N) = tree(ntree, N, ntree) .
> N --> 29 28 27 26 25 24 23 22 21 20 19 18 17 16 15 14 13 12 11 10 9 8 7 6 5
> 4 3 2 1
> seqtotree(29 28 27 26 25 24 23 22 21 20 19 18 17 16 15 14 13 12 11 10 9 8 7
> 6 5 4 3 2 1)
> --->
> tree(ntree, 29 28 27 26 25 24 23 22 21 20 19 18 17 16 15 14 13 12 11 10 9 8
> 7 6 5 4 3 2 1, ntree)