Downloading and Running Real-Time Maude |
\||||||||||||||||||/ --- 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.