Maude-help mailing list

[rusu AT irisa.fr]

Hi,

I'm a bit puzzled by how matching and [owise] equations behave in
the following simple example. I'm running Core Maude 2.4 on a Mac.

Many thanks in advance for help!

 Vlad

*****
The intention is to encode the following automaton

s1 =a=> s1
s1 =a=> s2
s2 =b=> s2

using equations, and to also accumulate the trace (aaabb, for instance)
together with the control node (s1 or s2). The specification is simple:

fmod AUTOMATA-WITH-EQUATIONS is
sorts Label LabelList Node State StateSet .

subsort Label < LabelList .
subsort State < StateSet .

ops a b eps : -> Label .
ops s1 s2 : ->  Node .
op __ : LabelList LabelList -> LabelList [assoc id: eps] .

op <_,_> : Node LabelList -> State .
op empty : -> StateSet .
op __ : StateSet StateSet -> StateSet [assoc comm id: empty] .
var st : State  .
eq st st = st .


var tr : LabelList .


ops _=a=> _=b=> : StateSet -> StateSet .

var sts : StateSet .
eq < s1, tr >  sts =a=> = < s1, tr a  > < s2, tr a > sts .
eq sts =a=> = sts [owise] .
eq < s2, tr > sts =b=> = < s2, tr b > sts .
eq sts =b=> = sts [owise] .

endfm

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?

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?

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?
*****