Maude-help mailing list

["Hui Ding" <huiding AT uiuc.edu>]

I am using Maude version 2, which is the latest  version downloadable from 
the web.
Now I found that the problem may lie in the following statement, which is 
contained in
file "general.maude":
     var ATTRSET  : AttributeSet .
    op  shutdown : Configuration Oid -> Configuration .
     ceq shutdown(< O1 : Thread | parent : O3, ATTRSET > CF, O2)
            = < O1 : Thread | parent : O3, ATTRSET > shutdown(CF, O2)
           if O3 =/= O2 .
When "oidlist.maude" and "general.maude" is sequentially introduced, there 
are no warning
messages. Everything goes well by then.
But when "deadlock.maude" is introduced, the warning message appears to show 
that OidList
is not defined.

When I delete the above conditional equation, then all go through well to the 
end without
any warning messages.
So it seems that variables of sort AttributeSet  cannot be used in this 
style. In other
words, does this mean that if I want to deal with configurations in equations 
instead of
rewriting rules, I have to list ALL its attributes contained in this object, 
some of whose
information may be totally useless in the equation?

If this is true, how to deal with the following statement? Here, even the Cid 
cannot be
determined.
If ATTRSET is not allowed to be used this way, it seems that I have to list 
all the
different classes (since they have different attribute set) and define a 
conditional
equation for each class. Is this true?
  ceq shutdown(< O1 : C | parent : O3,  ATTRSET > CF, O2)
        = < O1 : C | parent : O3,  ATTRSET > shutdown(CF, O2)
        if C =/= Thread .

Another point is that: from the elimination of warning messages here, it 
shows that a
grammar error, which is not detected when introducing the file containing it, 
may only
shows its influence in later files, with a confusing warning message. Maybe 
this is a bug
in the Maude compiler?


> Hui Ding said:
> > I got really frustrated by the following phenomenon. First, I defined
> > four modules in four separate files.
>
> First, could you please specify the Maude version as well as the Full
> Maude version. In any case, please consider upgrading to the latest
> versions (available from the Maude web-page), if not already done.
>
> In addition, could you also send the whole code, or a link to them? It
> might be easier to answer your question then.
>
> > Now I do as follows
> > in full-maude -> in oidlist -> in general -> in control, all modules
> > have been correctly introduced until now. But ...
> > when I run command "in deadlock", I was told the following message tens
> > of times and this command just does not return :
> >        Advisory: could not find sort OidList in meta-module DEADLOCK.
> > Advisory: bad operator declaration op 'OIDLIST : nil -> 'OidList
> > [none] . in meta-module DEADLOCK.
>
> What seems to be happening is that Full Maude doesn't seem to detect an
> error in the OMod, but the translated module (as in Sec. 14.6 of the Maude
> 2 manual) triggers a warning from Core Maude.
>
> > When I delete those rewriting rules involving OIDLIST but keep the
> > variable OIDLIST declarations there,  the same phenomenon happens. When
> > I delete all the operation, equation and rewriting rules in module
> > DEADLOCK  and only keep those statements as shown above, the warning
> > messages disappear, but the command just does not return.
> >
> > What happens here? How to make it work? Thanks for the help.
>
> It could be possible that this is already fixed. Since I don't know know
> the version of Maude and Full Maude that you're using, and since I do not
> have access to the code, I am unable to reproduce the problem.
>
> Thanks,
> --
> Ambarish
>
>