Maude-help mailing list

[Ethan Aubin <ethan.aubin AT gmail.com>]

Hi, I'm having some difficulty running some of the full-maude
examples. For example, the account example below from the manual gives
the output "Error: Module". What does this mean? Thanks - Ethan

  (omod ACCOUNT is
    protecting QID .
    protecting INT .

    subsort Qid < Oid .
    class Account | bal : Int .
    msgs credit debit : Oid Int -> Msg .
    msg from_to_transfer_ : Oid Oid Int -> Msg .

    vars A B : Oid .
    var  M : Nat .
    vars N N’ : Int .

    rl [credit] :
      credit(A, M)
      < A : Account | bal : N >
      => < A : Account | bal : N + M > .

    crl [debit] :
      debit(A, M)
      < A : Account | bal : N >
      => < A : Account | bal : N - M >
      if N >= M .

    crl [transfer] :
      (from A to B transfer M)
      < A : Account | bal : N >
      < B : Account | bal : N’ >
      => < A : Account | bal : N - M >
         < B : Account | bal : N’ + M >
      if N >= M .
  endom)

(rew < ’A-06238 : Account | bal : 2000 > debit(’A-06238, 1000) .)



--- Ouputs
                     \||||||||||||||||||/
                   --- Welcome to Maude ---
                     /||||||||||||||||||\
            Maude 2.6 built: Dec 10 2010 11:12:39
            Copyright 1997-2010 SRI International
                   Thu Jul 26 15:00:26 2012

            Full Maude 2.5b January 14th 2011

Introduced module ACCOUNT

Error: Module
Maude>