Dear Maude Abusers,

A new alpha release can be accessed at SRI-CSL in:

~eker/public_html/Maude/Alpha112/

or downloaded from:

http://www.csl.sri.com/~eker/Maude/Alpha112/

Alpha release site authentication:

User Name: maudeabuser
Password: bughunter

This is an urgent bug fix release to fix a bug in Maude's NatSet class.
Ever since 64-bit support, there has been a bug in NatSet comparison where
64-bit vectors are copied to local 32-bit variables before comparison,
leading to errors any time a value greater than 95 is stored in a NatSet
(the first 64 bits are stored separately since usually NatSets only
hold dense sets of small naturals). This bug has the potential to
break many things, but in practice, things such as the number of
variables in an equation tend to be less than 96, so this is probably
why such a serious bug has few visible effects.

It is visible in the following example reported by Peter (and found
by his student Tore Norderud <torenord@student.matnat.uio.no>):


mod TEST is
    protecting NAT .
    sort Clock .
    op clock : Nat -> Clock [ctor] .
    var N : Nat .
    rl [tick] : clock(N) => clock((N + 1) rem 60) .
endm

load model-checker

mod TEST-CHECK is
    including TEST .
    including MODEL-CHECKER .

    subsort Clock < State .

    op clock-is : Nat -> Prop [ctor] .
    eq clock(N) |= clock-is(N') = false .

    vars N N' : Nat .
    var PHI : Formula .
    op F : Nat Formula -> Formula .
    eq F(0, PHI) = clock-is(100) U PHI .
    eq F(s(N), PHI) = clock-is(100) U (PHI \/ (O (F(N, PHI)))) .
endm

red modelCheck(clock(1), F(31, clock-is(200))) .

Here the single predicate is always false but Maude fails to
find a counter-example. The problem is the LTL formula to
Very Weak Alternating Automata conversion generates > 96 states
(because of the size of the formula) and these are held in
NatSets and trigger the comparison bug, resulting in an
incorrect Very Weak Alternating Automaton.

Steven