Maude-help mailing list

[Alexandre Rademaker <rademake AT eml.cc>]

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