Download the Maude LTLR and LMC Model Checkers

The Maude LTLR model checker and LMC model checker are implemented as an extra module of Core Maude 2.7. You can download the binary or the source code below. The binary file contains executable files (maude.linux64 and maude.intelDarwin) for both of the tools, and examples in the directories ltlr-examples (for LTLR) and symbolic-examples (for LMC). To compile the source, please follow the Maude installation instruction (Note that GNU gcc 4.8 or later is needed to compile the source, with the CXXFLAGS option -std=c++11).

• Linux on Intel x86 and MacOSX on Intel
• Sources

The user interfaces of the LTLR and LMC model checkers are implemented by extending Full-Maude. The following Maude files define the interfaces of the model checkers (already contained in the above links, in addition to the file full-maude27.maude).

• LTLR Core Maude interface : ltlr-checker.maude
• LTLR Full Maude interface: ltlr-interface.maude
• LMC Full Maude interface: symbolic-checker.maude
• Full Maude 2.7: full-maude27.maude