Maude-help mailing list

[Francisco Durán <duran AT lcc.uma.es>]

Hi Vlad,

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

> 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