Difference between revisions of "Maude download and installation"

From The Maude System
Jump to: navigation, search
 
(11 intermediate revisions by the same user not shown)
Line 1: Line 1:
Maude 3.1 runs on many Unix variants, including Linux.  
+
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 [[installation guidelines|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 this section, we assume a Linux configuration. Please, substitute your platform name for 'linux' in what follows if you download for another platform.  
Line 6: Line 6:
 
The Maude system download consists of three parts: Core Maude, Full Maude, and documentation and examples.
 
The Maude system download consists of three parts: Core Maude, Full Maude, and documentation and examples.
  
==  Core Maude 3.2 ==
+
==  Core Maude 3.2.1 ==
  
The Linux64 and macOS versions of Maude 3.2 are available at [https://github.com/SRI-CSL/Maude/releases/tag/Maude3.2 its GitHub site].  
+
The Linux64 and macOS versions of Maude 3.2.1 are available at [https://github.com/SRI-CSL/Maude/releases/tag/3.2.1 its GitHub site].  
 
Its sources are available from the same place. You can find instructions together with the sources.  
 
Its sources are available from the same place. You can find instructions together with the sources.  
  
Line 20: Line 20:
 
   prelude.maude
 
   prelude.maude
 
   process.maude
 
   process.maude
  socket.maude
 
 
   smt.maude
 
   smt.maude
 +
  socket.maude
 
   term-order.maude
 
   term-order.maude
 +
  time.maude
 
Depending on your system you can now run Maude by starting the appropriate executable file: <tt>maude.linux64</tt> or <tt>maude.darwin64</tt>.
 
Depending on your system you can now run Maude by starting the appropriate executable file: <tt>maude.linux64</tt> or <tt>maude.darwin64</tt>.
  
== Full Maude 3.2 ==
+
== Full Maude 3.2.1 ==
  
Full Maude is written in Maude, and is thus platform-independent. Download [[Media:Full-Maude-3.2.zip|Full Maude 3.2]] and save it into the Core Maude directory.
+
Full Maude is written in Maude, and is thus platform-independent. Download [[Media:Full-Maude-3.2.1.zip|Full Maude 3.2.1]] and save it into the Core Maude directory.
  
 
== Maude manual and primer ==
 
== Maude manual and primer ==
  
The manual for Maude 3.2 is available in [[Media:Maude-3.2-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude32-manual-html/maude-manual.html HTML].  
+
The manual for Maude 3.2.1 is available in [[Media:Maude-3.2.1-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude321-manual-html/maude-manual.html HTML].  
 
The examples in the manual and in the book All About Maude is also available [[Media:Maude-3.1-manual-book-examples.zip|here]].
 
The examples in the manual and in the book All About Maude is also available [[Media:Maude-3.1-manual-book-examples.zip|here]].
  
== Main changes from Maude 3.1 to 3.2 ==
+
== Main changes from Maude 3.2.1 to 3.2 ==
  
Given the following general classes of theories E:
+
* Improvement on the vu-narrow command
  
- (1) Typed B-unification and B-matching for B any combination of associativity (A) and/or commutativity (C) and/or unit element (U) axioms.
+
== Main changes from Maude 3.1 to 3.2 ==
- (2) Typed E U B-unification and matching in the user-definable infinite class of theories E U B with B as in (1), and E U B having the finite variant property
+
(FVP).
+
  
- (3) Typed E U B-unification for the infinite class of user-definable theories E U B with B as in (1), and E confluent, terminating, and coherent modulo B.
+
* Support for filtered variant unification in vu-narrow command,
 
+
* Several improvements in unification modulo several axioms,
Maude 3.2 provides efficient support for:
+
* Several improvements of the external Maude I/O objects,
 
+
* A command flag for the depth of searching for A/AU unifiers, and
- computing minimal complete sets of most general B- (resp. E U B-) unifiers for classes (1) and (2) except for the A-without-C case;
+
* Some bugs fixed.
 
+
- a new E U B-matching algorithm for class (2); and  
+
 
+
- a new symbolic reachability analysis for concurrent systems based on narrowing with transition rules modulo equations E U B in class (2) enjoying powerful state-space reduction capabilities based on the minimality and completeness feature (i) and on "folding" less general symbolic states into more general ones through subsumption.
+
  
 
== Change list from Maude 3.0 to 3.1 ==
 
== Change list from Maude 3.0 to 3.1 ==
Line 63: Line 58:
 
* Some bugs fixed, and
 
* Some bugs fixed, and
 
* Some improvements in syntax error detection and recovering.
 
* Some improvements in syntax error detection and recovering.
 
<small>(If you use [http://www.xemacs.org/ XEmacs], then you might find the [[Media:Maude-mode.tar.gz|Maude mode]] for XEmacs
 
written by [http://www.iam.unibe.ch/~kai/ Kai Br&uuml;nnler] or
 
the [[Media:Maude-mode2.el.zip|Maude mode]] written by Ellef Gjelstad useful.
 
Extract the mode using the command "gunzip -c maude-mode.tar.gz | tar -xvf -" and follow instructions in maude-mode/README. Note that the Maude mode does not run under GNU Emacs. If you are using Emacs 24 please consider to use the [https://github.com/ssaavedra/maude-mode maude-mode] written by Santiago Saavedra. Please see the README for details.
 
There are also language packages for Atom, Visual Studio Code, and other editors.</small>
 

Latest revision as of 19:01, 11 July 2022

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

The manual for Maude 3.2.1 is available in PDF format and in HTML. The examples in the manual and in the book All About Maude is also available here.

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.