Downloading and Running Real-Time Maude
  1. The current version 2.3 of Real-Time Maude runs on Maude versions 2.3 and 2.4, so you first need to download the Maude system and install it properly.
  2. The Real-Time Maude tool is the Maude program real-time-maude.maude which you should download to your desired directory. (The file rtm-tctl.maude contains Real-Time Maude with the TCTL model checker developed by Daniela Lepri.)
  3. Real-Time Maude can now be started by executing it as a usual Maude specification, that is, by giving the UNIX command
          maude real-time-maude
    (assuming that your command for starting Maude is maude). The system should respond with something a la
                         \||||||||||||||||||/
                       --- Welcome to Maude ---
                         /||||||||||||||||||\
                Maude 2.3 built: Feb 14 2007 17:53:50
                Copyright 1997-2007 SRI International
                       Wed Aug  8 11:47:50 2007
    
                 Full Maude 2.3 `(February 12th`, 2007`)
    
              Real-Time Maude 2.3 extension May 2, 2007
    
    Maude> 
    
    and you can now enter Real-Time Maude input, such as in
    Maude> (tmod ... is ... endtm)
    
    Once an input module is given, other commands or input, such as the definition of a new module, definition of a time sampling strategy, a timed rewrite/search/model checking command can be given, such as in the following interaction:
    Maude> (set tick def 1 .)
    rewrites: 282 in 0ms cpu (0ms real) (~ rewrites/second)
    
    Tick mode set to default mode
    
    Maude> (trew {clock(0)} in time <= 100 .)
    rewrites: 3837 in 0ms cpu (25ms real) (~ rewrites/second)
    
    Timed rewrite  {clock(0)} in MODEL-CHECK-DENSE-CLOCK with mode default time
        increase 1 in time <= 100
    
    Result ClockedSystem :
      {stopped-clock(24)} in time 100
    
    Maude> (utsearch {clock(0)} =>* {clock(25)} .)
    rewrites: 2646 in 0ms cpu (44ms real) (~ rewrites/second)
    
    Untimed search in MODEL-CHECK-DENSE-CLOCK
            {clock(0)} =>* {clock(25)}
    with mode default time increase 1 :
    
    No solution
    
    Maude>
    
    The help command is also useful, as it directs to other help commands which explain most Real-Time Maude commands in detail:
    Maude> (help .)
    

    Finally, you may want to write your specification(s) and/or commands in a file, say clock.rtmaude. If this file starts with the line

    load real-time-maude
    
    (and continues with e.g.
    (tmod ... is ... endtm)
    
    you can start Real-Time Maude and read your file by giving the UNIX command maude clock.rtmaude.
  4. The system is carefully explained in the user manual.
 
Peter Ölveczky