Maude-help mailing list

[Alexandre Rademaker <rademake AT fgv.br>]

Hello Team,

Please, someone could help me? My question below about Model Checking in 
Full Maude is still open!

Thanks for all,
Alexandre Rademaker

-------- Original Message --------
Subject: Full Maude 2.1.1 and Model Checker
Date: Tue, 26 Oct 2004 13:18:29 -0200
From: Alexandre Rademaker 
<rademake AT eml.cc>
Reply-To: 
rademake AT eml.cc
To: 
maude-help AT maude.cs.uiuc.edu

How can I use the Model Checker in Full-Maude?

After removing the comment in line 124 of Full-Maude file I am
not able to import the Model Checker modules in others Modules in Full
Maude database. Example:

(omod S-VER-PCB is
 inc MODEL-CHECKER .
 subsort Configuration < State .
 ...
endom)

In the Full-Maude 2.1 one could extend the equation:

  op builtIns : -> ModNameSet .
  eq builtIns
    = 'TRUTH-VALUE . ...

and add references for MODEL-CHECKER modules at Core Maude database,
but in the current version of Full-Maude it seems to me that the
operator builtIns was removed! So, since the Model Checker modules are
load in Core Maude, how can I use the Core Maude Modules in
Full-Maude?

Best regards,
Alexandre Rademaker