Warnings while using umaudemc 0.12.2 and Maude 3.3.1

[mfeliu]

Hi there.

I was trying the statistical model-checking examples of the manual and I got the following warnings:

python3 -m umaudemc scheck coin.maude head coin.quatex -a 0.00001
Warning: "prelude.maude", line 2864 (fmod META-LEVEL): failed to attach id-hook MetaLevelOpSymbol to metaPrettyPrint.
Warning: "prelude.maude", line 2864 (fmod META-LEVEL): bad special for operator metaPrettyPrint.
Warning: "prelude.maude", line 2132 (fmod META-LEVEL): this module contains one or more errors that could not be patched up and thus it cannot be used or imported.
Number of simulations = 3090
Query 1 (line 13:1)
  μ = 18.937216828478963        σ = 4.217378376501338         r = 0.3356828667120411
Query 2 (line 14:1)
  μ = 38.93559870550162         σ = 6.2452360384984935        r = 0.4970905025684883

Are they relevant? Can I safely ignore them? Is it appropriate to notify you of this type of issue?

Thank you.

Marco A.

OS: MacOS 13.6.4
Maude: 3.3.1
umaudemc: 0.12.2

[ningit]

Hi,

These warnings are caused by a mismatch between the version of the Maude implementation and the version of prelude.maude. umaudemc uses the maude Python package to interact with Maude, which is linked to a particular version of Maude and comes with the corresponding prelude. umaudemc will use always use this builtin version of the implementation, but any prelude.maude in MAUDE_LIB or in the current working directory will take precedence over the builtin prelude.maude, and if they are not compatible these warnings will appear.

I guess you have downloaded the official distribution of Maude 3.3.1 and run the example from the same directory. At that time, the latest version of the maude library was linked against the more recent Maude alpha154, and the signatures of metaPrettyPrint do not coincide.

The problem can be fixed by:

• Moving prelude.maude (or the Maude distribution, or the example) to another location where it does not interfere.
• Using the just-released Maude 3.4 and update the Maude library (pip install -U maude) so that both versions coincide and can live together.

Are they relevant? Can I safely ignore them?

In this case they are not relevant, because the META-LEVEL module is not actually used. If the module were used, the command would have not worked.

Is it appropriate to notify you of this type of issue?

Of course, it is appropriate to ask here, even if it is not a bug (the possibility of replacing the prelude is made on purpose, and this issue can also happen when using multiple versions of Maude as an executable).

Best regards.