Since the execution environment for Full Maude has been implemented in Core Maude, to initialize the system so that we can start using it the first thing we have to do is to load the FULL-MAUDE module in the system. Assuming that the file full-maude.maude, which contains the executable specification of Full Maude, is located in the current directory (or in a place where Maude can locate it, see Section 2.2), we just need to type the corresponding in or load command in the Maude prompt:
Maude> load full-maude.maude
Full Maude 2.3 `(November 20th`, 2006`)
The Full Maude system is then loaded, and we can use it as any other module.
Since Maude can take file names as arguments when started, assuming one is working on a Linux platform, one may also run Maude as follows:
~/maude-linux/bin$ ./maude.linux full-maude.maude
\||||||||||||||||||/
--- Welcome to Maude ---
/||||||||||||||||||\
Maude 2.3 built: Nov 20 2006 18:55:03
Copyright 1997-2006 SRI International
Fri Dec 1 10:38:24 2006
Full Maude 2.3 `(November 20th`, 2006`)
At the end of this file full-maude.maude there is the command
loop init .
which initializes the system just after loading the specification. This command starts the read-eval-print loop (see Section 12.1) to allow the interaction with the user by entering modules, theories, views, and commands, and to maintain a database in which to store all the modules, theories and views being introduced. The term init is a constant of sort System, in the specification of Full Maude, standing for the initial state of the Full Maude database.
Typing control-C may result in the loop being broken, and with it the current execution of Full Maude. Maude may try to recover the loop by itself, but if it is not successful we must reinitialize it with the loop command. That is, we need to type
Maude> loop init .
This command will be successful only if the full-maude.maude file is loaded and the FULL-MAUDE module is the default one. If it is not the default one, we may select it with the select command (see Section 16.11):
Maude> select FULL-MAUDE . Maude> loop init .
The loop init command may be omitted here: Maude will try to restart the loop, using
the last loop command, if something is written in parentheses henceforth.
Let us recall from Section 12.1 that to get something into the LOOP-MODE system the text has to be enclosed in parentheses. This means that any module, theory, view, or command intended for Full Maude has to be enclosed in parentheses. Since Core Maude is running underneath Full Maude--indeed, it now provides what might be called the system programming level--it will handle any input not enclosed in parentheses. This allows the possibility of using both systems at the same time. Thanks to this, we may use many Core Maude commands when interacting with Full Maude. For example, we may use Core Maude trace or profile facilities on Full Maude specifications, may load files, etc. However, this may lead to some confusion, and we should take care of putting parentheses around those pieces of text intended for Full Maude.
A Core Maude module, such as those presented in previous sections, can be entered in Full Maude by enclosing it in parentheses. For example, a module PATH14.1can be entered to Full Maude as follows:
Maude> (fmod PATH is
sorts Node Edge .
ops source target : Edge -> Node .
sort Path .
subsort Edge < Path .
op _;_ : [Path] [Path] -> [Path] .
var E : Edge .
vars P Q R S : Path .
cmb E ; P : Path if target(E) = source(P) .
ceq (P ; Q) ; R
= P ; (Q ; R)
if target(P) = source(Q) /\ target(Q) = source(R) .
ops source target : Path -> Node .
ceq source(P) = source(E) if E ; S := P .
ceq target(P) = target(S) if E ; S := P .
protecting NAT .
ops n1 n2 n3 n4 n5 : -> Node .
ops a b c d e f : -> Edge .
op length : Path -> Nat .
eq length(E) = 1 .
ceq length(E ; P) = 1 + length(P) if E ; P : Path .
eq source(a) = n1 .
eq target(a) = n2 .
eq source(b) = n1 .
eq target(b) = n3 .
eq source(c) = n3 .
eq target(c) = n4 .
eq source(d) = n4 .
eq target(d) = n2 .
eq source(e) = n2 .
eq target(e) = n5 .
eq source(f) = n2 .
eq target(f) = n1 .
endfm)
rewrites: 5438 in 10ms cpu (157ms real) (543800 rews/sec)
Introduced module PATH
As in Core Maude, we can enter any module or command by writing it directly after the prompt, or by having it in a file and then using the in or load commands. Also as in Core Maude, we can write several Full Maude modules or commands in a file and then enter all of them with a single in or load command (without parentheses), but each of the modules or commands has to be enclosed in parentheses.
When entering a module, as above, Maude gives us information about the rewrites executed to handle such a module. This is the number of rewrites done by Full Maude to evaluate the module being entered. In the same way, every time we enter a command, although in most cases it finally makes a call to Core Maude, Full Maude needs to perform some additional rewrites. Thus, as we will see below, the number of rewrites given by the system for Full Maude commands includes the reductions due to the evaluation of the command and those due to the execution of the command itself.
We can perform reduction or rewriting using a syntax for commands such as that of Core Maude.
Maude> (red in PATH : b ; (c ; d) .)
rewrites: 893 in 30ms cpu (21ms real) (29766 rewrites/second)
reduce in PATH :
b ;(c ; d)
result Path :
b ;(c ; d)
Maude> (red length(b ; (c ; d)) .)
rewrites: 474 in 10ms cpu (2ms real) (47400 rewrites/second)
reduce in PATH :
length(b ;(c ; d))
result NzNat :
3
Maude> (red a ; (b ; c) .)
rewrites: 587 in 0ms cpu (2ms real) (~ rewrites/second)
reduce in PATH :
a ;(b ; c)
result [Path] :
a ;(b ; c)
Maude> (red source(a ; (b ; c)) .)
rewrites: 616 in 0ms cpu (2ms real) (~ rewrites/second)
reduce in PATH :
source(a ;(b ; c))
result [Node] :
source(a ;(b ; c))
rewrites: 622 in 0ms cpu (2ms real) (~ rewrites/second)
reduce in PATH :
target((a ; b); c)
result [Node] :
target((a ; b); c)
Maude> (red length(a ; (b ; c)) .)
rewrites: 579 in 0ms cpu (2ms real) (~ rewrites/second)
reduce in PATH :
length(a ;(b ; c))
result [Nat] :
length(a ;(b ; c))
Note the number of rewrites. These figures include, as said above, the rewrites accomplished by Full Maude in the processing of the inputs and outputs, plus the number of rewrites of the reduction itself. For example, the first two reductions above in Core Maude would produce the following output:
Maude> red in PATH : b ; (c ; d) . reduce in PATH : b ; (c ; d) . rewrites: 7 in 0ms cpu (23ms real) (~ rews/sec) result Path: b ; (c ; d) Maude> red length(b ; (c ; d)) . reduce in PATH : length(b ; (c ; d)) . rewrites: 12 in 0ms cpu (0ms real) (~ rews/sec) result NzNat: 3
Tracing, debugging, profiling, and the other facilities available in Core Maude (see Section 13.1) are also available in Full Maude. Since these facilities are provided by Core Maude, the corresponding commands for managing them must be written without parentheses. For example, we can do the following:
Maude> set trace on .
Maude> set trace mb off .
Maude> set trace condition off .
Maude> set trace substitution off .
Maude> (red length(b ; c) .)
*********** trial #1
ceq length(E:Edge ; P:Path) = length(P:Path) + 1
if E:Edge ; P:Path : Path .
*********** solving condition fragment
E:Edge ; P:Path : Path
*********** success for condition fragment
E:Edge ; P:Path : Path
*********** success #1
*********** equation
ceq length(E:Edge ; P:Path) = length(P:Path) + 1
if E:Edge ; P:Path : Path .
length(b ; c)
--->
length(c) + 1
*********** equation
eq length(E:Edge) = 1 .
length(c)
--->
1
*********** equation
(built-in equation for symbol _+_)
1 + 1
--->
2
rewrites: 444 in 0ms cpu (7ms real) (~ rewrites/second)
reduce in PATH :
length(b ; c)
result NzNat :
2
One should always bear in mind that Full Maude is part of the specification being run. The
specification of Full Maude is loaded in the system, and as said above, some of the rewrites taking
place are the result of applying equations or rules in these modules. In the case of tracing, the
rewrites done by Full Maude are not shown thanks to one of the trace commands available, namely
trace exclude (see Sections 13.1.1 and 16.5). With such a command
we may exclude particular modules from being traced. In particular, the full-maude.maude
file includes the command trace exclude FULL-MAUDE, where FULL-MAUDE is the top
module of the specification of Full Maude.