[an error occurred while processing this directive]

<!-- ##### Side Menu #####
<p class="doNotDisplay doNotPrint">This page&rsquo;s menu:</p>
<ul id="side-bar">
  <li><a href="../about.shtml#introdution">Introduction</a></li>
  <li><a href="../about.shtml#team">Team</a></li>
  <li><a href="#here">Version 3.4</a></li>
</ul>
 -->
<div id="main-copy">
<h1>UPPAAL 3.4 Release Info</h1>

<p>UPPAAL 3.4.0 is a new stable release of UPPAAL and can be
downloaded from the <a href="http://www.uppaal.com/">UPPAAL web
site</a>.</p>

<p>Compared to the 3.2 release, this release features performance
improvements, language improvements, and user interface
improvements. Each will be considered in detail in the following.</p>

<h2>Runtime Requirements</h2>

<p>UPPAAL 3.4 requires the Java Runtime Environment version 1.4.0 or
newer. One of the following operating systems is required: </p>

<ul>
<li>Microsoft Windows 95 or newer</li>
<li>Microsoft Windows NT 4 or newer</li>
<li>Linux on INTEL compatible processors</li>
<li>SUN Solaris on UltraSparc processors</li>
</ul>

<p>Some users have reported success running Uppaal on FreeBSD, but
this platform is not officially supported. Also, it should be possible
to run the GUI on any platform supported by the Java Runtime
Envionrment 1.4.0 or newer, but the verification engine is not
supported on other platforms than those listed above.</p>

<h2>Performance Improvements</h2>

<p>The core verification engine has once again been reworked and
features improved memory management and modularity. Combined with
major changes in the internal data structures and minor tweaks in
various algorithms, this has lead to much improved performance.</p>

<p>Detailed list of major changes:</p>

<ul>
<li>Shared passed and waiting list scheme results in reduced memory
consumption and improved performance.</li>
<li>New memory management scheme results in less memory fragmentation
and consequently improved performance.</li>
<li>New modular pipelined architecture.</li>
<li>New extrapolation algorithms.</li>
</ul>

<h2>Language Improvements</h2>

<p>We are currently moving to a new language for UPPAAL 4.0, which
will feature a nice subset of the C programming language. We will keep
the automata based interface, but add the ability to use C data types
and C expressions including calls to user defined functions, which are
evaluated as atomic statements (thus eliminating one of the uses of
committed locations). Most of the new parser library has been
implemented (see <a
href="http://www.cs.auc.dk/%7Ebehrmann/utap">libutap</a> for more
information on the library) and is used in a restricted mode in the
3.4 release.</p>

<p>The language in UPPAAL 3.4 is a superset the language in UPPAAL
3.2, <em>i.e.</em> every valid 3.2 file should also be a valid 3.4
file (there are a few exceptions, which we consier bugs in the 3.2
parser). A number of features from the 4.0 language have been enabled
in 3.4. This includes multi dimensional arrays, arrays of constants,
channels and clocks (in addition to arrays of integers), array
initialisers, booleans, and C expressions (with the exception of
binary negation).</p>

<p>Finally, a new <em>broadcast channel</em> type has been added
(non-blocking one-to-many communication).</p>

<p>One important change is the interpretation of out-of-range
assignments. UPPAAL 3.2 uses a "wrap-arround" semantics, e.g. when
assigning the value 10 to a variable with range [0,3] the result would
be 2. One can argue, that this is not always the intended behaviour,
and if it is it should be explicitly incorporated into the model
rather than handled by the verification engine. Therefore we now
consider such assignments invalid. In case of invalid assignments (or
other invalid operations like out-of-range array lookups and division
by zero), the successor is pruned from the state-space (since it is
not well-defined). The command line tool can produce warnings whenever
this happens. At the moment there is no way to get access to these
warnings from the graphical users interface (this will be fixed in a
future version).</p>

<p>Detailed list of major changes:</p>

<ul>
<li>New operators:
<ul>
<li>Logical: &amp;&amp; (logical and), || (logical or), ! (logical negation),
<span style="color: blue;"><tt>and</tt>, <tt>or</tt>, <tt>not</tt>,
<tt>imply</tt> (in 3.2 these were restricted to the requirement
specification language; in 3.4 they are also available in the
modelling language - added in beta 3)</span>.</li>
<li>Bitwise: ^ (xor), &amp; (bitwise and), | (bitwise or),
</li><li>Bit shift: &lt;&lt; (left), &gt;&gt; (right)</li>
<li>Numerical: % (modulo), &lt;? (min), &gt;? (max)</li>
<li>Assignments: +=, -=, *=, /=, ^=, &lt;&lt;=, &gt;&gt;=, := </li>
<li>Prefix and postfix: ++ (increment), -- (decrement)</li>
</ul></li>
<li>Boolean data-type.</li>
<li>Multi dimensional arrays.</li>
<li>Arrays of integers, channels, clocks, constants.</li>
<li>Disjunctions over non-clock expressions are allowed in
guards.</li>
<li>Array initialiser.</li>
<li>Use of non-constant integer expressions in comparisons with and
assignments to clocks are allowed.</li>
<li>Booleans and integers are type compatible.</li>
<li>Broadcast channels.</li>
<li>Interpretation of out-of-range assignments has changed.</li>
</ul>

<h2>User Interface Improvements</h2>

<p>In UPPAAL 3.4, the graphical user interface has gotten a face
lift. Besides a new tool bar and new icons, the editor component has
been rewritten, featuring anti-aliasing, curved edges, and a new
interaction pattern. Also, a list of all syntax errors is shown
directly in the editor, thus making it much easier to get an overview
of errors.</p>

<p>The simulator reuses the new rendering component. It also features
a new message sequence chart view of the trace loaded, making it easy
to analyse the communication structure of the model. Selecting one of
the enabled transitions in the simulator now restricts the zone of the
state to those points were the transition is enabled.</p>

<p> The verifier can generate shortest (in number of edges) and
fastest (in terms of model time) diagnostic traces. This is a back
port of some of the features of the unofficial cost optimising version
of UPPAAL.</p>

<p>Finally, the command line tool (verifyta) is now able to read TA,
XTA and XML files directly. Thus there is no need for the TA format
anymore and the "Save As TA file" feature has been deprecated. Notice
that the XTA format is a superset of the TA format, and users
preferring to create models directly in the TA format can simply use
the XTA format and get all the benefits of the template mechanism.</p>

<p>Detailed list of major changes:</p>

<ul>
<li>Message Sequence Charts.</li>
<li>New tool bar.</li>
<li>Persistent settings.</li>
<li>New editor component.</li>
<li>New help system.</li>
<li>List of all errors.</li>
<li>Printing in simulator.</li>
<li>Command line tool (verifyta) handles TA, XTA, and XML files
directly.</li>
<li>Support for generating shortest and fastest traces.</li>
<li>Simulator applies guards of selected transition to current
state.</li>
<li>Command line tool (verifyta) can generate XTR tace files (which
can be read by the GUI).</li>
<li>Unix man-page added (thanks to John A. Murdie).</li>
<li>Visualisation of deadlocks.</li>
</ul>
</div>
    <!-- ##### Footer ##### -->
    <div id="footer">
      
      <strong>Updated &raquo;</strong> 01/11/2005
    </div>
  </body>
</html>