Commercial Licenses

For information about commercial licenses and support, please contact sales@uppaal.com. When doing so, please provide the following information: how Uppaal will be used; duration and size of project in which Uppaal will be used; amount of training and support required; and information about the corporation (employees etc).

Academic Licenses

The following releases and utilities are available for free for non-commercial applications in academia, and for private persons:

• Uppaal 4.0
  The current official release of the academic version (also available for Mac OS X).
• Uppaal 4.1 (development snapshot)
  A development version of Uppaal version 4.1 (also available for Mac OS X)
• Parser Library
  Uppaal Timed Automata Parser Library (libutap). Distributed separately under the LGPL license.
• DBM Library
  Implementation of DBM, an efficient data structure for representing clock constraints in timed automata.
• convert.jar
  Utility that converts files from version 3.2 to 3.4, see version history
• Memtime
  Small utility to measure time and memory consumption.

Installation Instructions

To download and install (or upgrade to) the current version of Uppaal:

1. Choose the version from the download area.
2. Fill in the license agreement and press the "Accept and Download" button.
3. Download the zip-file containing the installation files.
4. Unzip the downloaded zip-file. This should created a number of files, including: uppaal.jar, uppaal, and the directories bin-Linux, bin-Win32, and demo. The bin-directories should all contain the two files server(.exe) and verifyta(.exe) plus some additional files, depending on the platform. The directory demo should contain some demo files with suffixes .xml, and .q.
   
5. Make sure you have the Java version 6 (e.g. J2SE Java Runtime Environment) or newer installed and properly configured on your system. The Uppaal GUI will not run without Java installed. Java for Windows and Linux can be downloaded from java.sun.com.
6. To run Uppaal on Linux systems run the startup script named uppaal. To run on Windows systems, just double-click the file uppaal.jar.
7. (Optional) Join the Uppaal mailinglist. The mailinglist is intended for users of the tool. To join the list, email uppaal-subscribe@yahoogroups.com. To post to the mailing list, email uppaal@yahoogroups.com. For more information, see this page.

Please e-mail bug-uppaal@list.it.uu.se if you have problems to install, if you find bugs or have suggestions how Uppaal can be improved. Before e-mailing us, please check the Known Issues, the Frequently Asked Questions sections below, and the messages at the Uppaal mailinglist.

Version History

This version history documents the devlopements in Uppaal since the first beta release of Uppaal 3.0 in July 20, 1999. The version history of the previous Uppaal versions (i.e. version 2.17 and earlier) can be found in this README file.

• Sep 21, 2009: Uppaal 4.0.10 - Current Official Release
  The new major version of Uppaal.
  • Fixed bug 481.
• Sep 11, 2009: Uppaal 4.0.9 - Current Official Release
  The new major version of Uppaal.
  • Fixed rare bug in storing integers.
  • Fixed bugs: 474, 472, 476, 477, 440, 469, 468, and 466.
  • Fixed zoom labels on Mac.
  • The semantics of priorities has been changed. Before, priority was resolved by comparing the priorities of the processes involved in two transitions by descending order. Now, it is resolved by considering the highest priority process, which is in line with priority ceiling protocols.
• Sep 11, 2009: Uppaal 4.1.2 - Development snapshot
  A snapshot of the 4.1-version currently under development. New features include:
  • Fixed rare bug in storing integers.
  • Fixed bugs: 467, 474, 476, 477, 440, 469, 468, 478, and 479.
  • Fixed zoom labels on Mac.
  • Added some support for statistics under Mac OS.
  • The semantics of priorities has been changed. Before, priority was resolved by comparing the priorities of the processes involved in two transitions by descending order. Now, it is resolved by considering the highest priority process, which is in line with priority ceiling protocols.
  • Updated the robust reachability implementation to be applicable to more general models.
• Mars 24, 2009: Uppaal 4.0.8
  The new major version of Uppaal.
  • Support for proxies (commercial version).
  • Fixed bugs: 455, 458, 459, 463, and 465.
  • Fixed Japanese locale.
• Mars 24, 2009: Uppaal 4.1.1 - Development snapshot
  A snapshot of the 4.1-version currently under development. New features include:
  • Added new Japanese and Chinese locales.
  • Improved locale support: Now syntax errors are also localized.
  • Improved "about" window.
  • Saving the system saves the queries too.
  • The model is uploaded automatically in the simulator when a new model is opened.
  • Improved uppaal script.
  • Added experimental drag-and-drop.
  • Improved MSC.
  • Removed mis-feature that // type of comments had precedence over /* .. */ type of comments.
  • Updated robust reachability algorithm w.r.t. Piotr's new algorithm.
  • Removed Mani's reachability algorithm (E<>+ expr).
  • Extended use of forall to clock rates in invariant expressions (for stop-watches).
  • Added "sum(id:type) expr" language extension.
  • Improved support of stop-watches for liveness properties.
  • Fixed generation of traces in the simulator when using stop-watches.
  • Added "sup: list of expr" language extension.
  • Fixed bug with leadsto traces.
  • Fixed bugs: 341, 356, 366, 417, 421, 422, 423, 427, 428, 437, 438, 441, 443, 448, 454, 456, 458, 459, 463, and 465.
• Nov 24, 2008: Uppaal 4.0.7
  The new major version of Uppaal. Plese note that the GUI now requires Java 6.
  • New features:
    • Added localization support for Japanese, Chinese, Lithuanian, and Danish.
    • New application icon.
    • Improved "about" window.
    • Saving the system saves the queries too.
    • The model is uploaded automatically in the simulator when a new model is opened.
    • Improved uppaal script.
    • Licence handling: academic and commercial versions available.
  • System requirements: Java 6. A recent Linux based distribution, Windows XP, Windows Vista, or Mac OS X 10.5. Under Mac OS 10.5, please do /Applications/Utilities/Java/Java Preferences.app and activate Java 6 because the default activated one is Java 5.
  • Fixed bugs: 437, 427, 448, 423, 422, 430, 431, 417, 421, 443, 341, 356, 428, 366, 438, 432, 409, 414, 412, and 403.
• Feb 26, 2008: Uppaal 4.1 - Development snapshot
  A snapshot of the 4.1-version currently under development. New features include:
  • On-the-fly merging of DBMs
  • Support for stop-watches
  • Heuristic search (experimental)
  • Two robust reachability algorithms
• Mar 5, 2007: Uppaal 4.0.6 - Current Official Release
  Notice that the GUI requires Java version 5. Be aware that this version contains changes to the syntax and you will need to convert your old models. Binaries for Mac OS X are available for download (requires MacOS 10.4 - known as Tiger - as Java 5 is not available for earlier versions).
  • Fixed bugs: 392, 394, 395, 397, and 398.
• Feb 12, 2007: Uppaal 4.0.5
  The new major version of Uppaal.
  • Fixed bugs: 386, and 389.
• Jan 2, 2007: Uppaal 4.0.4
  The new major version of Uppaal.
  • Fixed bugs: 352, 370, 371, 372, 375, 376, 381, 382, 383, and 384.
• Oct 16, 2006: Uppaal 4.0.3
  The new major version of Uppaal.
  • Fixed bugs: 105, 340, 345, 349, 350, 354, 355, and 358.
  • The train gate model has been updated to demonstrate some of the new 4.0 features.
• Aug 7, 2006: Uppaal 4.0.2
  The new major version of Uppaal.
  • Fixed bugs: 331, 332, 333, 334, 335, 336, 337, 339, and 340.
• June 21, 2006: Uppaal 4.0.1
  The new major version of Uppaal.
  • The Mac version now has universal binaries, which run natively on both PowerPC based Macs and Intel based Macs.
  • Sparc Solaris binaries included.
  • Improved performance for models with priorities.
  • Fixed bugs: 48, 328, 329, and 330.
• May 29, 2006: Uppaal 4.0.0
  The new major version of Uppaal.
  Changes listed below are from version 3.6 beta 3 (previous release version was 3.4.11):
  • Performance improvement of symmetry reduction.
  • Tooltips with useful information in the automaton editor (thanks Kim Algreen).
  • The help system is now fully searchable (thanks John).
  • New splash screen (thanks Leonid).
  • Support for meta scalar variables (thanks Martijn).
  • Server binary now respect the UPPAAL_OLD_SYNTAX environment variable. You can switch UPPAAL (including the GUI) into a 3.4 compatibility mode by definining this environment variable.
  • Changed the ordering of -n settings for verifyta (run verifyta -h for details).
  • Fixed null pointer exception in GUI when cancelling verification.
  • Fixed bitstate hashing for large hash tables (512MB).
  • Changed interpretation of -H option for verifyta: hash table size is now always a power of two (run verifyta -h for details).
  • Documentation updates.
  • Renamed the documentation field to comments in the GUI.
    Note: Previous models with documentation will lose the documentation.
  • Bug in deadlock checker has been fixed.
  • More verification options are available within the GUI (extrapolation and hash table size for bit state hashing).
  • Dedlock checker and liveness checker have been disabled for models with priorities.
  • Performance improvements for huge models (with thousands of processes).
  • Repaint problems during movement of elements have been fixed.
  • The DTD and the URL to the DTD has been updated.
  • Fixed bugs: 259, 285, 286, 308, 317, 322, 323, 324, 325, and 327.
• Apr 28, 2006: Uppaal 3.6 beta 3 - Beta release.
  A beta release of the next major version of Uppaal.
  • Symmetry reduction is now applied also in the presence of multi-dimensional arrays.
  • Fixed bugs: 112, 261, 280, 297, 305, 306, 307, 309, 312, 315, 316, 320, and 321.
• Mar 24, 2006: Uppaal 3.6 beta 2 - Beta release.
  A beta release of the next major version of Uppaal.
  • Fixed bugs: 300, 301, 302, and 303.
• Mar 20, 2006: Uppaal 3.6 beta 1 - Beta release.
  A beta release of the next major version of Uppaal.
  • New feature: Documentation label on locations and edges (bug 142).
  • New feature: Partial and automatic instantiation of templates (bug 278).
  • New feature: Possibility to hide labels in the editor (from the View menu).
  • Changed semantics of array parameters: Unless you explicitly provide an ampersand, the parameter will have call-by-value semantics.
  • Template sets have been removed
  • Fixed memory leak caused by deadlocks in the model
  • Documentation has been updated
  • verifyta can now be instructed to terminate after the internal compilation step by defining the UPPAAL_COMPILE_ONLY environment variable. verifyta will output a textual description of the compiled UPPAAL model.
  • Renamed uppaal2k.jar to uppaal.jar
  • Fixed bugs: 56, 142, 154, 206, 258, 272, 278, 279, 288, 289, 290, 291, 292, 293, 294, 295, and 296.
• Mar 3, 2006: Uppaal 3.6 alpha 5 - Alpha release.
  An alpha release of the next major version of Uppaal.
  • Symmetry reduction has been added (thanks to Martijn Hendriks, University of Nijmegen)
  • Priorities have been added.
  • The generalized sweep-line method is implemented.
  • Documentation is updated (on-line help).
  • Note: This version of UPPAAL does not work with Java 6 Beta 1 (vote for bug 6375901 at the Sun Developer Network to make it work).
  • Note: Symmetry reduction is automatically disabled when trace generation is enabled.
  • Fixed bugs: 23, 50, 96, 114, 172, 196, 252, 253, 255, 256, 262, 263, 264, 265, 266, 267, 268, 269, 270, 271, 273, 281, and 284.
• Jan 24, 2006: Uppaal 3.6 alpha 4 - Alpha release.
  An alpha release of the next major version of Uppaal.
  • The menu structure has been reworked.
  • The train gate example was updated to use template sets and the universal quantifier.
  • verifyta can now produce prestable symbolic traces.
  • verifyta options summary has been divided into categories.
  • verifyta now tolerates inexact extrapolation choices. The verification is correctly marked as an over approximation.
  • Redrawing problems have been fixed in the GUI editor.
  • The process instantiation node has been removed in the editor (use system declaration node).
  • Mac OS integration has been improved.
  • Fixed bugs: 48, 67, 90, 117, 178, 222, 233, 241, 244, 245, 248, 249, and 250.
• Dec 20, 2005: Uppaal 3.6 alpha 3 - Alpha release.
  An alpha release of the next major version of Uppaal.
  • New feature: Syntax highlighting has been added (editor).
  • The communication protocol between GUI and server has been changed so that old servers/GUIs cannot be mixed with new servers/GUIs.
  • The behavior in the presence of out of range assignments, out of bound array indices, division by zero etc. has been changed. Previously, states triggering such behavior have been discarded and were ignored in the verification. Now, the verification is aborted with an error message.
  • Fixed bugs: 134, 168, 211, 212, 214, 215, 217, 228, 229, 230, 231, 232, 234, 235, 237, and 238.
• Nov 25, 2005: Uppaal 3.6 alpha 2 - Alpha release.
  An alpha release of the next major version of Uppaal.
  • Fixed bugs: 16, 171, 180, 183, 188, 195, 213, 218, 219, 220, 223, 225, 226, and 227.
• Nov 7, 2005: Uppaal 3.6 alpha 1 - Alpha release.
  An alpha release of the next major version of Uppaal.
  • New features: Iterator statements and Quantifier expressions (forall).
  • Fixed bugs: 29, 116, 118, 139, 146, 167, 176, 181, 184, 185, 187, 189, 190, 191, 197, 200, 203, 204, 205, 207, 209, and 210.
• Aug 8, 2005: Uppaal 3.5.9 - Development Snapshot.
  A snapshot of the 3.5 version currently under development.
  • Fixed bugs: 177, and 178.
• Jul 14, 2005: Uppaal 3.5.8 - Development Snapshot.
  A snapshot of the 3.5 version currently under development.
  • Fixed bugs: 42, 102, 163, 165, 166, 169, 170, 173, 174, and 175.
• Jun 23, 2005: Uppaal 3.5.7 - Development Snapshot.
  A snapshot of the 3.5 version currently under development.
  • Fixed concrete trace generation for models with urgent and committed locations (May 12th)
  • Relaxed restrictions on invariants: (b-expr imply x <= c) is a valid invariant now (May 28th)
  • Optimized handling of minimal constraint form (May 31th and June 1st)
  • Fixed race conditions in GUI (May 31th& June 8th)
  • Fixed progress information in verifyta for bitstate hashing (June 3rd)
  • Fixed memory leak in liveness checker (June 16th)
  • Changed default in GUI such that the grid is now shown (June 16th)
  • Fixed null pointer exception in GUI when loading a model (June 16th)
  • Fixed snap to grid in GUI (June 16th)
  • Properties are no longer stored in a .uppaalrc file - on Windows they are now stored in the registry; on Unix under .java (June 16th)
  • Changed default colors in GUI such that guard, sync and assignments have different colors (June 16th)
  • Fixed repaint problem when deleting the last template (June 17th)
  • Fixed bugs: 147, 151, 152, 153, 155, 157, 158, 159, 160, and 162.
• May 3, 2005: Uppaal 3.5.6 - Development Snapshot.
  A snapshot of the 3.5 version currently under development.
  • The communication protocol between GUI and server has been updated. This GUI cannot be used with previous servers and vice versa.
  • Trace generation and trace handling has been fixed for models that cause symbolic states to split. This also fixes a problem with generating concrete traces to deadlock states.
  • Type checking for template parameters has been fixed.
  • The GUI has been extended with a simple converter from 3.4 to 3.5 syntax.
  • The command line version can now output statistics after each verification (the -u option).
  • Bug fixes: 119 and 148.
• April 7, 2005: Uppaal 3.5.5 - Development Snapshot.
  A snapshot of the 3.5 version currently under development.
  • Uses sharing to reduce the memory usage (a significant improvement).
  • Performance of liveness checker has been improved (significantly for some models) both w.r.t. speed and memory usage.
  • Reimplemented trace representation, solving the problem of not being able to use all memory on machines with large memory. This also reduces the amount of memory needed for representing traces.
  • Trace handling in the GUI has been reimplemented to reduce the memory requirements for loading large traces.
  • Bug fixes: 7, 108, 111, 121, 131, 135, and 140. In addition, parser bugs for record handling, a minor memory leak and an XTA export bug have been fixed.
• Feb 4, 2005: Uppaal 3.5.4 - Development Snapshot.
  A snapshot of the 3.5 version currently under development.
  • Binaries for Linux and Windows (no SunOS binaries).
  • Parser crashes have been fixed.
  • Active clock reduction has been improved in the presence of arrays of clocks.
  • A problem with arrays in records has been fixed.
  • Disabled unimplemented language constructs like switch.
  • GUI: The zone description in the variable view has been made more compact.
  • GUI: The scroll position of the variable view is maintained when traversing a trace.
  • GUI: A NullPointerException has been eliminated.
• Dec 22, 2004: Uppaal 3.5.3 - Development Snapshot.
  A snapshot of the 3.5 version currently under development.
• Dec 21, 2004: Uppaal 3.5.2 - Development Snapshot.
  A snapshot of the 3.5 version currently under development.
  • Binaries for Linux and Windows (no SunOS binaries).
  • Note: reqires Java version 1.5.
• Jun 23, 2005: Uppaal 3.4.11
  Binaries for Mac OS X are available for download.
  Bug fixes: 155 and 162.
• May 11, 2005: Uppaal 3.4.10
  Bug fixes: 131 and 151.
• Mar 31, 2005: Uppaal 3.4.9
  Bug fixes: 135, 140, and 141.
• Feb 17, 2005: Uppaal 3.4.8
  Bug fixes: 107, 125, 126, and 127.
• Oct 5, 2004: Uppaal 3.4.7
  Bug fixes: 100, and 106.
• Jun 16, 2004: Uppaal 3.4.6
  Bug fixes: 39, 52, 64, 80, 91, 94, 97, 98, 99, 100, and 103.
• Mar 29, 2004: Uppaal 3.4.5
  Bug fixes: 52, 55, 83, 84, 85, 86, 87, 88, 89, 91, 92, and 93.
• Jan 26, 2004: Uppaal 3.4.4
  Bug fixes: 77, 78, 79, 80, and 82.
• Dec 25, 2003: Uppaal 3.4.3
  Bug fixes: 67, 69, 71, 72, 73, 74, 75, and 76.
• Oct 14, 2003: Uppaal 3.4.2
  Bug fixes: 62, 63, and 65.
  Known problems: here
• Sep 22, 2003: Uppaal 3.4.1
  Bug fixes: 58, 59, and 60.
  Known problems: here
• Sep 12, 2003: Uppaal 3.4 (3.4.0) - Uppaal 3.4.0 is a new stable release of Uppaal. Compared to the 3.2 release, this release features performance improvements, language improvements, and user interface improvements. For more information see the release info. Compared to the last beta version (version 3.4 beta 3) the following have been changed:
  • Fixed bug 56, 54, 53, 47, 46, 43, 41, 40, 38, and 37.
  • Removed the --psSplines option from GUI.
  • Help file for command line options.
  • Fixed bug in broadcast synchronisation.
  • Fixed interpretation of boolean values (and non-zero integer is interpreted as true).
  • Changed interpretation of out-of-range assignments to integers: Now the successor is simply not well-defined and thus does not exist (there is still no way to get info about such states in the GUI).
  • Fixed libutap error related to integer parameters without a range.
  • Fixed some errors in the README files.
  • Upgraded JavaCC to 3.2.
• June 30, 2003: Uppaal 3.4 beta 3 (3.3.36) - Third beta release of version 3.4.
  This version is the third public beta release of the upcoming Uppaal 3.4. Compared to the second beta release (3.3.35), this release features:
  • Enhancements/additions/compatibility:
    • Changed handling of integer template parameters: A parameter without an explicit range is not compatible with integer arguments with any range (ensure compatibility with 3.2).
    • Channel parameters now accept arguments according to the type of guards allowed by the channel, i.e. 'no clock guards', 'no clock guards on send', 'clock guards on both send and receive'. The argument must at least provide the same capabilities as required by the parameter, e.g. you can use channel argument to urgent channel parameter, but not vice versa.
    • Documentation updates.
    • The range of integer types can now depend on template parameters.
    • The dimension of arrays can now depend on template parameters.
    • Added documentation for expressions and synchronisations.
    • Made 'and', 'or', 'not', 'imply', 'true' and 'false' keywords available in the modelling language (previously they were restricted to the property language). Consistent with languages like Perl, this operators have a lower precedence than the corresponding C-like operators. We now officially consider 'bool' to be valid type (by accident this was already the case in beta 2 - now it is an official feature).
    • Changed error reporting in verifyta for XML files (now includes XPath).
    • verifyta now only prints the waiting list size when using bitstate hashing.
    • Deadlocks are now shown in the GUI as entries in the "enabled transitions" list.
    • Added support for DOS style newlines.
    • Added handling of 'divide-by-zero'. In case the computation of a successor involves a division by zero, the successor is considered to be undefined (i.e. it does not exist).
    • Added pseudo-formal semantics to online help.
    • Demos have been updated to use some of the new features (e.g. mutual exclusion is much easier expressed in the new syntax).
  • Bug fixes:
    • Forced width of global declaration editor to 4000 pixels (fixes bug 5).
    • Fixed a problem with starting the engine if the path contains white space (as is common on windows).
    • Fixed problem were the template name field or template parameter field in the GUI would not be saved.
    • Fixed problem were the text editor sometimes used a proportional font.
    • Fixed problem with local constants (bug 11).
    • Fixed memory leak when multible properties are checked (bug 10).
    • Fixed memory leak when using the reuse option (bug 12).
    • Fixed line counting bug in libutap affecting error message generation.
    • Fixed a minor problem in the DBM library, which caused the liveness checker to produce wrong results.
    • Fixed active clock reduction (did not work in the pressence of arrays of clocks or conditional assignments).
    • In models were guards over clock differences are reset of clocks to other values than zero are used, we now mark the verification as an overapproximation.
• April 3, 2003: Uppaal 3.4 beta 2 (3.3.35) - Second beta release of version 3.4.
  This version is the second public beta release of the upcoming Uppaal 3.4. Compared to the first beta release (3.3.32), this release features:
  • Various improvments:
    • 'uppaal2k' script renamed to 'uppaal'
    • man page added
    • default window size changed to 800x600
    • documentation updated
    • fixed engine crashes (empty template name, duplicate template declarations, error recovery, etc.)
    • syntax check speed has been improved
    • All binaries have been build with GCC 3.2.2.
    • The GUI now uses Xerces Java 2 2.4.0 and Xalan Java 2 2.5.D1.
  • Depecrated features:
    • Export to TA-format from the editor is not supported in the version.
    • Interactive mode is not suppored in the verifyta.
  • Known issues:
    • Syntax errors in parameters are not underlined (will be fixed in beta 3)
    • Uppaal 3.2 does not correctly save in UTF-8 encoding and this can prevent the system from being loaded in Uppaal 3.4.
    • Use of the character sequence ]]> in an expression produces invalid XML files (put a space between ]] and > to avoid the problem).
    • The editor is not supposed to wrap long lines, but until a character has been entered, lines are wrapped anyway (will be fixed in beta 3).
    • XTR trace files for TA and XTA files saved with previous version of Uppaal cannot be opened. The workaround is to open the system in an older version and then save it as an XML file.
    • Hitting backspace in parameter or template name fields will delete selected objects on drawing canvas (will be fixed in beta 3)
• February 17, 2003: Uppaal 3.4 beta 1 (3.3.32)- First beta release of version 3.4.
  As of March 20:th 2003 we have stopped distributing this beta release. Several critical bugs has been found and we are now working hard on a second beta release that should be available within a couple of weeks.
  This version is the first public beta release of the upcoming Uppaal 3.4 and is considered to be feature complete. Compared to 3.2, this release features:
  • Performance Improvements:
    • Shared passed and waiting list scheme results in reduced memory consumption and improved performance.
    • New memory management scheme results in less memory fragmentation and consequently improved performance.
    • New modular pipelined architecture.
    • New extrapolation algorithms.
  • Language Improvements:
    • New operators:
      • Logical: && (logical and), || (logical or), ! (logical negation),
      • Bitwise: ^ (xor), & (bitwise and), | (bitwise or),
      • Bit shift: << (left), >> (right)
      • Numerical: % (modulo), ? (max)
      • Assignments: +=, -=, *=, /=, ^=, <<=, >>=, :=
      • Prefix and postfix: ++ (increment), -- (decrement)
    • Multi dimensional arrays.
    • Arrays of integers, channels, clocks, constants.
    • Disjunctions over non-clock expressions are allowed in guards.
    • Array initialiser.
    • Use of non-constant integer expressions in comparisons with and assignments to clocks are allowed.
    • Booleans and integers are type compatible.
    • Broadcast channels.
  • User Interface Improvements:
    • Message Sequence Charts.
    • New tool bar.
    • Persistent settings.
    • New editor component.
    • New help system.
    • List of all errors.
    • Printing in simulator.
    • Command line tool (verifyta) handles TA, XTA, and XML files directly.
    • Support for generating shortest and fastest traces.
    • Warnings for potential out of range assignments and array indices.
    • Simulator applies guards of selected transition to current state.
  • Known Problems:
    • Export to TA-format from the editor is not supported in the version.
    • Interactive mode is not suppored in the verifyta.
    • Syntax errors in parameters are not underlined.
    • Constants cannot be outside the range -32768 to 32767.
    • Uppaal 3.2 does not correctly save in UTF-8 encoding and this can prevent the system from being loaded in Uppaal 3.4 beta 1 (see message 302 of the Uppaal discussion group at Yahoo! Groups for more information).
      Solution: To solve the problem (i.e. to convert ISO-8859-1 files to UTF-8 encoding) use the utility convert.jar.
    • Use of comma as an and operator does not work in invariants (use && instead).
    • Missing operands to binary operators cause a server crash.
    • Use of the character sequence ]]> in an expression produces invalid XML files (put a space between ]] and > to avoid the problem).
• December 11, 2002: Uppaal2k 3.2.13
  • Upgraded to Condensity 2.0.14 (this fixes some JRE 1.4.x problems)
  • Uppaal can now detect where it is installed. This means that it is possible to start Uppaal from a different directory than the installation directory (very nice on windows when creating a file association).
  • Fixed problems in simulator when using JRE 1.4.1 on Windows
  • Fixed bug in active clock reduction
  • Removed list of templates from template menu (the old behavior had some problems with models with many templates).
  • Print the error message produced by the XML parser when the validation of an XML file fails.
  • Fixed bug in GUI code for committed and urgent locations (this bug resulted in invalid XML files)
  • Fixed problem with invalid references in <init> tag in the XML file.
  • Changed placement of help menu
  • Note: This version no longer supports Java 1.1 - JRE 1.2.2 or newer is required (this seems to fix the problems that people have had starting Uppaal on various platforms)
• November 4, 2002: Uppaal2k 3.2.12.
  • Uppaal now checks and fixes invalid references when opening an XML file,
  • fixed bug in server which prevented redeclaration of identifiers previously used for channels,
  • XML validation in GUI,
  • fixed memory allocation bug in property parser,
  • fixed detection of invalid properties (invalid in the sense that Uppaal cannot handle them),
  • fixed critical bug in handling of expressions involving disjunction of conditions over clocks,
  • Windows version compiled with GCC 3.2 and new mingw32 release.
• September 6, 2002: Uppaal2k 3.2.11.
  • Max constant problems related to non-zero clock updates have been fixed.
  • Max constant problems related to guards on clock differences have been fixed for models with 3 or fewer clocks. For more than 3 clocks the analysis is marked as being an over approximation.
  • Backported a number of simple performance optimisations:
    • new hash function,
    • computation of active/inactive clocks,
    • computation of Minimum Constraint Systems (a.k.a the Compact Data Structure), and
    • increased default hash table size.
  • Fixed bug with encoding of bounds (only caused real harm with models having guards on clock differences, but might have reduced performance for other models).
  • Fixed problem in GUI with anonymous locations.
  • Backported PostScript export from 3.3 (uses arcs instead of bezier curves).
  • Fixed a number of memory management bugs
  • Enforced a sane window size in the GUI
• May 6, 2002: Uppaal2k 3.3.23 - Development Snapshot.
  A snapshot of the 3.3 version currently under development. To download, use the ordinary license agreement.
  • New editor interface (read the build-in help if in doubt; tips: double click to make the buttons stick or try the middle mouse button to create objects).
  • New canvas implementation (supporting curved transitions).
  • New help system (based on JavaHelp).
  • Engine updated to version 3.2.9.
  • Various bug fixes.
  • See also version 3.3.14 (below).
• April 18, 2002: Uppaal2k 3.2.9.
  • Fixed performance bug.
  • Fixed -U option for verifyta (exact inclusion checking for "compact data structure") - this should reduce the memory usage.
  • Made the "Compact Data Structure" option in the GUI use the equivalent of -U in verifyta.
  • Fixed a crash on Linux.
  • Made liveness checker respect the -S option in verifyta and the "State Space Reduction" option in the GUI
  • Fixed bug in leads-to checker (the bug was triggered by disjunctions on the left side of the leads to arrow).
  • Added "maybe satisfied" verification output to GUI (was supported in verifyta, but not in the GUI).
  • Fixed performance bug in trace view.
  • Allowed the use of x[c] (where x is an int array and c a constant expression) as argument to int parameters.
  • Fixed highlight bug when deleting related items.
  • Fixed bounding box computation for PostScript export.
  • Fixed scope bug in property parser.
• Mar 8, 2002: Uppaal2k 3.2.6.
  • Fixed error in the deadlock detection of the liveness algorithm.
    See message 213 of the Uppaal discussion group at Yahoo! Groups for more information.
  • Fixed problem with saving and loading traces.
  • Fixed problem with systems without a well defined initial state.
  • Fixed repaint problem in simulator when new project is loaded.
• Feb 18, 2002: Uppaal2k 3.2.5.
  • Fixed liveness checker bug reported by danka on the mailinglist.
  • Fixed liveness checker bug related to deadlocks.
  • Fixed XTA export bug.
  • Fixed bug related to empty labels.
  • Improved scrolling performance in editor.
  • Changed shortcut for exit to Ctrl+Q.
  • Fixed dialog problem triggered by JRE 1.4 on Windows.
  • Fixed mouse problem triggered by exporing the X display.
• Dec 18, 2001: Uppaal2k 3.3.14 - Development Snapshot.
  A snapshot of the 3.3 version currently under development. To download, use the ordinary license agreement.
  • Verification engine: same as in version 3.2.2.
  • Graphical User Interface:
    • A new Message Sequence Chart (MSC) view in the simulator.
    • 3-button mouse support. The middle mouse button can be used to move objects.
    • Support for customized settings. Several settings are now stored in a file named '.uppaalrc'. Attributes of graphical objects etc. can be changed by manually editing the file (no GUI for this yet).
    • Java2D updates.
    • Note: if Uppaal reports problems with contacting the verification server. Try delete the '.uppaalrc' file.
    • Note: Java version 1.1 is not supported by Uppaal2k version 3.3.
• Dec 17, 2001: Uppaal2k 3.2.4.
  • Fixed GUI problem with import of templates.
  • The other binaries (server, verifyta, etc) are the same as in the 3.2.2 release.
• Dec 4, 2001: Uppaal2k 3.2.2.
  • Fix for problem with name-clashes between locations and global variables,
  • Removed 'cost', 'heur', 'costrate', 'transcost', and 'localtime' keywords from the parser (i.e. they are no longer reserved keywords),
  • Fixed bug where only the first local clock could override a globally declared variable
  • Added 'global' prefix for clocks, integers, constants and channels (only in the verification engine),
  • Fixed unfolding algorithm when arguments clash with local variables (the fix uses the 'global' prefix).
  • Constant expressions on invariants are now allowed in the verification engine,
  • DOCTYPE for XML format added,
  • JAXP 1.1.3 integrated,
  • Note: if you have installed an older version of JAXP yourself (in the ext directory of the JRE), you have to upgrade it as well.
  • Note: due to the upgrade to JAXP 1.1.3, files generated with version 3.2.2 can be loaded into version 3.2.1 only on machines with internet connections (as Uppaal needs to retreive the Document Type Definition from the Uppaal web server).
• Oct 29, 2001: Uppaal2k 3.2.1.
  • Semantics of deadlock changed to also consider the invariant of the successors states.
  • Examples updated to use new features.
• Oct 3, 2001: Uppaal2k 3.2 Beta 6 (3.1.73).
  • New menu for verification options.
  • Bug fix in normalization.
  • Removed race condition at start up.
  • Fixed problem with constant parameters in templates and arrays.
  • Fixed problem with importing templates and syntax checking.
  • Added check that disallows use of "deadlock" keyword in liveness properties.
  • The two programs atg2ta and atg2ugi have been removed from the distribution (they can be found in the 3.0 distribution).
• July 4, 2001: Uppaal2k 3.2 Beta 4 (3.1.64).
  • Navigation tree of editor reimpemented. This solves the problem with duplicated template names.
  • Deadlock checker has been reimplemented and now uses CDDs. A deadlocked state is a (concrete) state where there are no enabled outgoing syntactic transitions. Note that this semantics of deadlocks uses syntactic transitions, thus invariants on the target state have no influence on whether the source state is deadlocked or not.
• June 17, 2001: Uppaal2k 3.2 Beta 3 (3.1.63).
  • Added command line support for loading projects.
  • Fixed bug when deleting templates.
  • Fixed syntax checker bug for clock guards.
  • Fixed scroll bar problem in navigation tree.
  • Fixed problems with MS-DOS style newline in server engine.
  • Fixed problem when trying to load non-existing projects.
  • Fixed urgent/clock guard conflict detection in syntax checker.
  • Fixed problem in verfiyta with system line.
• June 10, 2001: Uppaal2k 3.2 Beta 2 (3.1.60).
  • New support for modifying the end-points of edges. (Point near the end-point of an edge, then drag-and-drop the end-point to a new location. Alternatively, the source end-point is can be dropped outside a location to create a new nail.)
  • New direct server engine connection when the engine is executed by the GUI (as opposed to using a TCP/IP connection) on all Java 2 platforms.
  • Bug fix in concrete trace generator of verifyta.
  • Very annoying bug when editing labels has been fixed.
  • Labels of different type now (once again) have different colors.
  • Syntax checker bug fix (clock guards on edges with urgent channels etc.).
  • The socketserver on Windows is gone - no more socketserver crashes and no more zombie server processes. This also means that is no longer possible to remote connect to an Uppaal server running on a Windows machine.
  • The server engine should finally adhere to its own protocol. This means that you should see the irritating "Server violated protocol" error message much less frequently.
  • Documentation updates.
  • Note for Windows users: The uppaal2k.bat file is gone. If Java is properly installed on your machine, you should be able to double click the uppaal2k.jar file in order to start Uppaal. JDK 1.1 is no longer supported on Windows.
• May 12, 2001: Uppaal2k 3.2 Beta 1 (3.1.57).
  • New platform and syntax independent robust XML file format.
  • Anonymous locations in the GUI.
  • Simple liveness properties can be verified: E[], A<> and p --> q are supported.
  • Deadlock properties can be verified from the GUI using the new "deadlock" state property.
  • A major redesign of the verification engine results in fewer dependencies between verification options.
  • The stand-alone verifier supports both concrete and symbolic traces.
  • A major redesign of the GUI core features new syntax checker.
  • Many bug-fixes.
• May 12, 2000: Uppaal2k version 3.0.41.
  • The use of unknown tokens (such as "&" and "|" in guards) are now detected and reported as syntax errors.
  • Windows binaries recompiled for new version of cygwin1.dll. Apparently, this results in a more stable behaviour on (e.g.) Windows 98 machines.
  • The (in-)active clock reduction functionality is now included in the windows binaries. By mistake it was not included in the versions 3.0.39 and 3.0.40.
  • The Sun and Linux binaries in this distribution are identical to those in version 3.0.39.
• May 5, 2000: Uppaal2k version 3.0.40.
  • Bug fix in Verifier GUI.
  • Note: the binaries in this distribution are from the previous version 3.0.39, only the file uppaal.jar has been changed.
• March 7, 2000: Uppaal2k version 3.0.39.
  • Problems with combining Active clocks and Reuse options in server(.exe) solved.
  • Default verification options changed.
  • Dependencies between verification options modified (in Option menu of GUI).
  • Some modifications to online help pages.
  • Some modifications to distributed demo files.
• February 17, 2000: Uppaal2k version 3.0.36.
  • Bug fix in implementation of (in-)active clock reduction.
  • "Full DBM" option is now enabled by default .
  • Some online help pages modifed.
• February 11, 2000: Uppaal2k version 3.0.35.
  • Improved algorithm for detecting loop-entry points (used by "Global Reduction" algorithm).
  • Change in system editor allowing the source and destination node of a transitions to be modified.
  • Use of "Under-Approximation" option no longer causes protocol exception (problem reported with version 3.0.27).
  • Bug fix in stand-alone verifier verifyta (which is not used by GUI).
• January 10, 2000: Uppaal2k version 3.0.27.
  • Changes in GUI (trace loading dialog window shown more often, default verification options changed, etc.).
  • Problem with diagnostic traces of length zero solved (caused protocol exception in previous version).
  • Bug fix in server and verifyta.
• December 20, 1999: Uppaal2k version 3.0.23.
  • Bug in DBM library (used both by server and verifyta) found and removed.
  • Traces generated with the "Diagnostic Trace" and "Active-Clock Reduction" options now also show values of inactive clocks.
  • Tool tips added to buttons in GUI.
  • Improved syntax/type error messages in GUI.
• December 6, 1999: Uppaal2k version 3.0.20.
  • Support for (in-)active clock reduction.
  • Solved problems with MS-DOS style newlines in system descriptions.
  • Three new help pages.
  • Minor bug fixes.
  • Note: When the (in-)active clock reduction is used in combination with the diagnostic trace option, currently only the active clocks are displayed in the generated traces.
• October 15, 1999: Patch level 2.
  • Problem with combining the verification options "Under-Approximate" and "Diagnostic Trace" solved.
  • Problems when deleting last nail in self-looping transition solved.
  • Added support for automata without transitions.
  • Added support for initialization of integer variables.
  • Binary of stand-alone verifier verifyta added to the distribution.
  • Minor bug fixes: in postscript header, JDK 1.2, 1.2.2 and 1.3 compability problems, dependencies between verification options, etc.
• September 20, 1999: Patch level 1.
  • Bug fixes.
• September 17, 1999: Uppaal2k (first official version).
  • New help pages added, describing the system editor, the simulator, and the verifier.
  • Problems with use of paramters and constants in local declarations (e.g. array size/range) solved.
  • Problems with use of global constants in array declarations solved.
  • Solved two problems with file saving, causing the saved file to be empty.
  • Problems with erronous display of local variables in simulator solved.
• September 6, 1999: Fifth beta version.
  • New requirement specification editor and verification interface.
  • Integreated help pages describing the system description language, the requirement specification language, and the tool menus.
  • Postscript output in color.
  • New command line options:
    • -fastScroll on|off enables/disables "Window Blit" (default value is "on"),
    • -psColors on|off enables/disables postscript output in color (default value is "on", when "off" output will be generated in black and white),
    • -psSplines on|off to enables/disables use of splines in postscript output (default value is "on").
  • Improved detection of system modifications in the system editor.
  • Note: the new requirement specification editor will not parse comment-lines starting with "//" when loading existing .q-files, instead comments should be enclosed within "/*" and "*/".

  • Note: the startup script uppaal2k.(bat) has been changed in this version to accept command line options.

• August 18, 1999: Fourth beta version.
  
  • New system overview in system editor.
  • Support for local clocks, integer variables and constant declarations in process templates.
  • Support for reusing (importing) process templates from existing .xta-files.
  • Substantially faster saving and loading of files.
  • Bug fixes in postscript generation, requirement specification editor, etc..
• August 6, 1999: Third beta version.
  • Lots of GUI bugs solved.
  • Problem with zombie server-processes solved.
  • Improved drawing grid with optional "snap" function.
  • New zoom sub menu with zoom to fit and to fixed values.
  • Note: .ugi-file names should no longer be prefixed with "." (a dot). Remember to manually rename existing .ugi-files.
  • Note: the command line option "-schoolEdition on|off" is no longer recognized (the option has been removed from the startup script).
• July 20, 1999: Second beta version.
  • Faster updating of graphics in editor and simulator.
  • Improved communication with verification server.
  • Faster loading of traces.
  • Cancel button during verification.
  • Bug fixes, etc.
• 2 July 1999: First official beta version.