Maude-help mailing list

[rusu AT irisa.fr]

> Hi Vlad,
>
> I guess you have just a parsing problem. I however get some results
> different. Please, confirm.
>

Yes, that's right - got tricked by the parser. Should have learned about
those precedence and gathering issues but somehow never got to them...

 Thanks for the info, and best wishes for the new year.

 Vlad

>> 1st issue:
>> I would expect
>> red < s1, eps > = a=> .
>> to return < s1, a > < s2, a >
>> but all I get is < s1, eps >,
>> and setting trace on confirms that the first [owise] equation applied.
>> So, it must be that matching did not work? But then, the match command
>> for the lhs of the first equation
>> match < s1, tr > sts <=? < s1, eps > .
>> returns
>>
>> Solution 1
>> sts --> empty
>> tr --> eps
>> so the first equation should have applied ? Why didn't it?
>
> Notice however that
>
> match < s1, tr > sts =a=> <=? < s1, eps > =a=> .
> match in AUTOMATA-WITH-EQUATIONS : sts =a=> < s1,tr > <=? < s1,eps >
> =a=> .
> Decision time: 0ms cpu (0ms real)
> No match.
>
> By default, operators __ and _=a=> get precedences 41 and 15,
> respectively, and gathering patterns e E and E. Notice that the
> parsing used is (sts =a=>) < s1,tr >.
>
> You can easily fix it with parentheses.
>
> match (< s1, tr > sts) =a=> <=? < s1, eps > =a=> .
> match in AUTOMATA-WITH-EQUATIONS : (sts < s1,tr >) =a=> <=? < s1,eps >
> =a=> .
> Decision time: 0ms cpu (0ms real)
>
> Solution 1
> sts --> empty
> tr --> eps
>
>> 2nd issue:
>> Next,  I tried removing the first [owise] equation and reducing
>>
>> red < s1, eps > empty =a=> .
>> (note the additonal "empty")
>>
>> and got the "expected" result StateSet: < s1,a > < s2,a > .
>> Why did the first equation apply now? I only "added" empty in my term.
>> Since empty is the identity element, why did it make a difference?
>
> This term parses as  < s1, eps > (empty =a=>), which matches the
> equation's LHS.
>
>> 3rd issue:
>> I now put back in the [owise] equation I had commented out, and for
>> red < s1, eps > empty = a=> .
>> I get again < s1, eps > .
>> So, the [owise] equation "took precedence over" the first equation? I
>> thought the [owise] attibute was designed to avoid just that?
>
> I don't understand this. It works for me.
>
> You can fix your spec in two ways. You can either write parentheses in
> your equations
>
> eq (< s1, tr > sts) =a=> = < s1, tr a  > < s2, tr a > sts .
> eq (< s2, tr > sts) =b=> = < s2, tr b > sts .
>
> Or you can assign explicit precedences to the operators involved. E.g.:
>
> op __ : StateSet StateSet -> StateSet [prec 10 assoc comm id: empty] .
> ops _=a=> _=b=> : StateSet -> StateSet [prec 15] .
>
> Cheers,
>
> Paco
>