Changes from Real-Time Maude 2.2 to version 2.3:
------------------------------------------------------------
There are actually no changes, apart from the fact that
version 2.3 is implemented by extending (the publicly
available) version 2.3 of Duran's Full Maude. This in turn
runs on version 2.3 of Maude.
Notice that some new features of Maude version 2.3
are not reflected in the current version of Full Maude.
This includes useful features such as rewrite bounds
in search commands, as well as exhibiting the rewrite path
to the (un)desired states found in searches. These features
are therefore not included in version 2.3 of Real-Time Maude.
(Of course, the bound on the number of rewrites is not crucial
in Real-Time Maude, since it allows for a time bound instead.)
Changes from Real-Time Maude 2.1 to version 2.2:
------------------------------------------------------------
Fortunately, as described in the manual, there are very
few changes from version 2.1 to version 2.2 of Real-Time Maude.
Essentially all modules and analysis commands for 2.1 should also
work for 2.2, so there should be little need to redo
specifications or analyses.
1. Adapted to Maude version 2.2 and to Full Maude version 2.2.
2. In timed and untimed searches (and in contrast to Full Maude),
the system now gives a "match" if an object belonging
to a proper subclass of the class C given in the object
pattern (otherwise) matches the pattern. In addition,
the object pattern no longer has to capture all attributes
(i.e., it is no longer needed to explicitly add a variable
of sort 'AttributeSet' to an object pattern).
3. The addition operator _+_ is extended to the infinity value
INF in the predefined modules NAT-TIME-DOMAIN-WITH-INF
and POSRAT-TIME-DOMAIN-WITH-INF.
4. The operators 'min' and 'max' in the skeleton module TIME-INF
are now called 'minimum' and 'maximum'. Any module
containing NAT-TIME-DOMAIN or POSRAT-TIME-DOMAIN can still
use 'min' and 'max'.
5. The new sort for the nonnegative rational numbers is
'NNegRat' (since in Maude 2.2, and hence in Real-Time Maude 2.2,
PosRat denotes the non-zero positive rationals). If your
specifications use 'NzTime' and 'Time' you should not need
to make (m)any changes.
-------------------------------------------------------------------
Previous changes:
-------------------------------------------------------------------
Main changes from Real-Time Maude 2.0 to Real-Time Maude 2.1:
1. Adapted to Maude version 2.1 and to Full Maude version 2.1.
2. Therefore, we allow "such that" (abbreviated "s.t.")
conditions on the patterns in timed and search, find
latest/earliest, and check commands. Notice that the
variables occurring the such conditions should be given
explicitly of the form "VAR:SORT".
3. The comparison operators >, >=, <, <= are extended
to the sort TimeInf in the predefined modules
NAT-TIME-DOMAIN-WITH-INF and POSRAT-TIME-DOMAIN-WITH-INF,
so that numbers can be compared also with the infinity
value INF using these comparison operators.
4. The Full Maude search error is corrected on line
12469 below. This line corresponds to line 12118 in
the public distribution of full-maude.maude from April 19.
--- -----
Change from April 30 version to May 5 version:
- the arrow '=>' in the tsearch and utsearch commands
is changed to the current Maude arrow for one-step
searches, namely, the arrow '=>1'. Furthermore, the semantics
is slightly changed in that states reachable in 0 steps are
no longer shown as a result of '=>1'-searches.