Maude-help mailing list

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

Hi Emmanuel,

There is no function in the CRChC that you can call to get a metamodule 
checked as with the check commands, since there is a lot of previous checks 
and massaging of the modules before the actual check. The check itself is 
carried out by CRCheck, but it assumes some preprocessing of the module and 
returns a set of membership assertions and and a set of critical pairs. And 
similarly for the ChC.

Simpler than that may be adding a metamodule to FM's database. There is an 
undocumented load command available in the latests versions of Full Maude 
that can do that for you. (If you type (help .) you get a list of the 
experimental undocumented new features.) The syntax is just (load 
<meta-module> .), and you can use it with either a metamodule or with a term 
resulting in a metamodule after reducing it. See the attached load-command.fm 
and load-command-2.fm files for examples. 

Francisco

Attachment: load-command-2.fm
Description: Binary data

Attachment: load-command.fm
Description: Binary data

El 09/09/2010, a las 22:44, Emmanuel Castro escribió:

> Hello,
> 
> I would like to run the Church Rosser checker of CRCHC on a module
> computed at meta level (something like :
> sometransformation(upModule('SOME-MODULE))...)
> 
> The CRCHC command only takes the name of a module as argument, not a
> metalevel expression.
> 
> Is there a not too complex way to run CRCHC as a 'reduce/rewrite'
> expression? I checked the sources but it does not seem obvious?
> 
> Or else, is there a way to put a module computed at the meta-level
> into the Full Maude model database.
> 
> At present, I can export the transformed module into a text file and
> then load it, but it is not convenient.
> 
> Thank you for your answers
> 
> Emmanuel
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help