Maude-help mailing list

["Ambarish Sridharanarayanan" <srdhrnry AT uiuc.edu>]

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