Maude download and installation
Maude 3.2.1 runs on many Unix variants, including Linux. The installations is straightforward, there is one single executable file with no dependencies whatsoever. Nevertheless, some hints on how to use it and how to install it in Windows platforms can be found here.
In this section, we assume a Linux configuration. Please, substitute your platform name for 'linux' in what follows if you download for another platform. In any case, please consider subscribing to the Maude users mailing list, as this is also the mechanism by which we will make announcements about the system.
The Maude system download consists of three parts: Core Maude, Full Maude, and documentation and examples.
Core Maude 3.2.1
The Linux64 and macOS versions of Maude 3.2.1 are available at its GitHub site. Its sources are available from the same place. You can find instructions together with the sources.
To install from one of the above binaries, simply extract the downloaded zip file. This generates the folder with the following files in it:
file.maude linear.maude machine-int.maude maude.[linux64|darwin64] metaInterpreter.maude model-checker.maude prelude.maude process.maude smt.maude socket.maude term-order.maude time.maude
Depending on your system you can now run Maude by starting the appropriate executable file: maude.linux64 or maude.darwin64.
Full Maude 3.2.1
Full Maude is written in Maude, and is thus platform-independent. Download Full Maude 3.2.1 and save it into the Core Maude directory.
Maude manual and primer
Main changes from Maude 3.2.1 to 3.2
- Improvement on the vu-narrow command
Main changes from Maude 3.1 to 3.2
- Support for filtered variant unification in vu-narrow command,
- Several improvements in unification modulo several axioms,
- Several improvements of the external Maude I/O objects,
- A command flag for the depth of searching for A/AU unifiers, and
- Some bugs fixed.
Change list from Maude 3.0 to 3.1
- Support for unification modulo associativity-identity,
- Support for the generation of irredundant unifiers,
- Support for the filtering of variant unifiers using variant subsumption,
- Support for the generation of variant matchers,
- An implementation of Unix processes as Maude external objects,
- Several improvements in the presentation of results,
- Several improvements in the handling of control-c,
- Some bugs fixed, and
- Some improvements in syntax error detection and recovering.