Commercial Licenses

Uppaal is free for academic use only. Any other use requires a license of Uppaal. As academic use, we consider only work performed by researchers or students at institutions delivering academic degrees. In addition, the work or the worker may not be contracted by any non-academic institution. Note that, any use at companies, private use, use at national research agencies, or any other non-academic use requires a license of Uppaal.

For information about commercial licenses and support, please visit www.uppaal.com.

Academic Licenses

The following releases and utilities are available for free only for academic institutions that deliver academic degrees:

• Uppaal 4.0
  This is the current official stable release of the academic version. There is no 64-bit version.
  • 32-bit Windows and Linux, version 4.0.15 download.
  • 32-bit Mac OS X, version 4.0.13 Mac OS X.
• Uppaal 4.1 (development snapshot)
  This is the current development release of the academic version. This version includes the SMC extension. There is no 64-bit version for Windows.
  • 64-bit Windows and Linux, version 4.1.25-5 download (update to Java-11!).
  • 32-bit Windows and Linux, version 4.1.24 download.
  • 64-bit Linux only, version 4.1.24 download.
  • 64-bit Mac OS X only, version 4.1.24 download (Catalina users may need a workaround).
  • 32-bit Windows and Linux, version 4.1.19 download.
  • 32-bit Mac OS X, version 4.1.14 download.
  • 64-bit Linux only, version 4.1.19 download.
  • 64-bit Mac OS X, version 4.1.19 download.
  You should use the 64-bit version if it is available for your platform and if you have 8GB of memory or more.
• 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 (old repository)
  Small utility to measure time and memory consumption on POSIX OSes.
  Alternatively one can use time utility with an environment vairable setting TIME="Max RSS: %Mkb\nUser: %Us\nKernel: %Ss\nElapsed: %es" or similar.

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 at least Java 7 configured on your system. The Uppaal GUI will not run without Java installed. Java for Windows and Linux can be downloaded from java.oracle.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.
   New: Launch AddLinks.vbs to create links in programs menu and desktop. This should take care of proxy settings automatically as well.
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.

• April 12th, 2021: Uppaal 4.1.25-5 - Development snapshot
  A shapshot of the 4.1-version currently under development. Changes:
  • Updated to Java-11 which fixed HiDPI issues.
  • Updated Test Case generation tab and updown.xml example.
  • Fixed Windows 64-bit issues.
  • Fixed graphical export issues.
• November 26th, 2019: Uppaal 4.1.24 - Development snapshot
  A shapshot of the 4.1-version currently under development. Changes:
  • Fixed opening of older model files (created by Uppaal 4.0).
  • Fixed query selection in Verifier.
• November 18, 2019: Uppaal 4.0.15 - Stable release
  Changes:
  • This is a maintenance release that fixes minor bugs.
• September 11th, 2019: Uppaal 4.1.23 - Development snapshot
  A shapshot of the 4.1-version currently under development. Changes:
  • Fixed symbolic simulator freeze in a complicated tab-switching scenario.
  • Fixed test case saving.
  • Fixed clipboard (Cmd+C, Cmd+V) actions for Mac OS X.
• March 28th, 2019: Uppaal 4.1.22 - Development snapshot
  A shapshot of the 4.1-version currently under development. Changes:
  • Fixed diagnostic trace loading into simulators.
• March 28th, 2019: Uppaal 4.1.21 - Development snapshot
  A shapshot of the 4.1-version currently under development. Changes:
  • Fixed symbolic simulator to display the current state locations.
• March 20th, 2019: Uppaal 4.1.20 - Development snapshot
  A shapshot of the 4.1-version currently under development. Changes:
  • Changed simulate query syntax so that the number of runs can be omitted or can be specified inside simulation bounds, e.g. simulate[<=5]{x} computes one run, and simulate[<=5;100]{x} computes 100.
  • SMC: added more common math functions from standard C library.
  • SMC: added floating point conversion to integer via int fint(double) function.
  • SMC: added more random number generation functions, including random_normal, random_poisson, random_beta, random_gamma, random_weibull, random_tri (triangular distribution).
  • SMC: improved floating point simulation boundary checks.
  • Yggdrasil/Test case generator refactored and moved into Tools menu.
  • HiDPI/Retina display support by font scaling in Edit/Preferences (set the scale to 2 or 2.5 and restart).
  • Russian locale translated by Dmitry Ivanov.
  • Fixed verification results when multiple properties are submitted in a batch.
  • Fixed histograms when there is only one or no data points.
  • Fixed 621, 637, query export and many other bugs.
• July 1st, 2014: Uppaal 4.1.19 - Development snapshot
  A shapshot of the 4.1-version currently under development. Changes:
  • Fixed some problems with the concrete simulator and broadcast sync.
  • Improved error feedback.
  • Added support for "hybrid" clocks - clocks ignored for model-checking, used for SMC only. They may not be active. The type double is now ignored for model-checking purposes as well.
  • Added Yggdrasil to the distribution.
  • Improvements to the GUI.
  • Merged query files with the model file. There is no need for .q files any more. Existing query files can be imported.
  • Better undo-redo.
  • Updated MITL syntax and improved the stability of the checker. Still some issues with the checker.
  • Added some support for OSCL. More info to come.
  • Improved the Gantt chart.
  • Fixed bug 551. Fixed arrays of double as arguments of templates.
  • Updated the demos.
  • Better support of Java 8 by the install script.
• May 20, 2014: Uppaal 4.0.14 - Stable release
  Changes:
  • This is a maintenance release that fixes minor bugs.
• November 7, 2013: Uppaal 4.1.18 - Development snapshot
  A snapshot of the 4.1-version currently under development. Changes:
  • Fixed an error introduced at the release of 4.1.17 that broke parsing the extension for dynamic creation of processes.
  • Added a client-server example that uses dynamic creation of processes.
• November 6, 2013: Uppaal 4.1.17 - Development snapshot
  A snapshot of the 4.1-version currently under development. Changes:
  • Added support for floating point inside clock constraints (guards and invariants).
  • Added support for dynamic creation of processes.
  • Added tree view of the variables.
  • Exceptions work again under Linux.
  • Fixed assignments to clocks for SMC (broken in 4.1.16).
• August 30, 2013: Uppaal 4.1.16 - Development snapshot
  A snapshot of the 4.1-version currently under development. Changes:
  • Removed license check.
  • Added support for double precision floating point numbers (type double).
  • Changed semantics of meta variables. They are now part of the model-checker, not the states.
  • Added clock initializers.
  • Added persistent view options for labels and grid.
  • Added visualization of comments in the editor and simulator.
  • Updated freehep and added support for encapsulated pdf export.
  • Implemented a fix to work-around Java on Mac.
  • The operators <? and >? now support clocks and double (for SMC).
  • Added French locale (Mathieu Giorgino).
  • Fixed down operation on DBMs.
  • Minor fixes and improments to the symbolic simulator.
• April 19, 2013: Uppaal 4.1.15 - Development snapshot
  A snapshot of the 4.1-version currently under development. Changes:
  • Using now the Clopper-Pearson bound instead of Chernoff-Hoeffding for probability evaluations (non-MPI implementation only).
  • Fixed the virtual machine for some instructions doing clock arithmetics (comparisons and evaluation of functions with constant arguments).
  • Fixed synchronization with broadcast channels that could be broken in certain situations.
  • Added warnings on models using urgent transitions with strict guards. This can break SMC.
  • Added new concrete simulator. This is a technological preview. The simulator is not operational on SMC models and the verifier does not interact with it.
  • Updated the GUI look and feel.
  • This version is not available for Mac because it simply does not work on that platform yet.
• March 12, 2013: Uppaal 4.1.14 - Development snapshot
  A snapshot of the 4.1-version currently under development. Changes:
  • Improved copy-paste.
  • Updated MITL syntax.
  • Fixed down operator for models using stop watches (can affect traces).
  • Added modeldoc.zip to the distribution.
  • Added xgmml2ctmc to the distribution (Linux 64).
  • Added sbml2uppaal to the distribution (Linux 64).
  • Added checks on declaration of ranges.
  • Improved static analysis for models containing clock differences.
  • Added progress (verifier) for the liveness checker.
  • Changed the location of the license to $HOME/.uppaal under Unix and $HOMEPATH/UPPAAL under Windows.
  • Enabled drag & drop under Linux.
  • Fixed a bug in SMC for models using urgency.
  • Fixed a bug in models using broadcast with guard on the receiver side.
  • Fixed a crash in the typechecker for models using the wrong type array[dot]name.
  • Changed the semantics of log in SMC to compute log10 (and not natural logarithm).
  • Added ln, pow, abs, ceil, and floor to SMC.
  • Added handling of null exponential rates (disable all guards).
  • The distribution now includes a visual basic script to automate the installation under Windows.
  We recommend that users upgrade to Java 7. On Mac, Apple has disabled Java 6 so users do not have the choice there.
• November 14, 2012: Uppaal 4.1.13 - Development snapshot
  A snapshot of the 4.1-version currently under development. Changes:
  • Vectorized some DBM operations. Models with many clocks will be faster to check.
  • Changed hash function (Murmur2). Minor improvement in general performance.
  • Further improved static analysis of models.
  • Fixed critical bug in saving new models (GUI, introduced in 4.1.12).
  • Added copy-paste support in the GUI. This works between applications as well.
• November 3, 2012: Uppaal 4.1.12 - Development snapshot
  A snapshot of the 4.1-version currently under development. Changes:
  • More efficient static analysis of active clocks.
  • Enabled LU extrapolation for liveness (proved correct by Guangyuan Li).
  • Fixed "zeno behavior with confidence" bug.
  • Added new icon and Visual Basic installation script for Windows.
  • Fixed issues with Java 7.
  • Improved handling of paths in the GUI.
  • Improved SMC functionalities.
  • Added log output for SMC simulations.
  • Floating point constants are supported for exponential rates (SMC).
  • Improved SMC/MITL checker.
• June 8, 2012: Uppaal 4.1.11 - Development snapshot
  A snapshot of the 4.1-version currently under development. Changes:
  • Repaired broken Windows version.
  • Added log scale for SMC plots.
  • Added fixed file output with fixed sampling rate for SMC.
  • Fixed rounding bug in corner case in SMC that could generate zeno behaviours.
• May 31, 2012: Uppaal 4.1.10 - Development snapshot
  A snapshot of the 4.1-version currently under development. Changes:
  • Improved support for ODEs in invariants (SMC).
  • Added support clock guards with urgent channels (SMC).
  • Fixed bugs with diagonal constraints (SMC).
  • Added built-in functions (sin, cos, log, exp, sqrt) for SMC.
• Mar 23, 2012: Uppaal 4.1.9 - Development snapshot
  A snapshot of the 4.1-version currently under development. Changes:
  • Fixed bug 535 .
  • Fixed bugs in SMC, fixed some crashes.
  • Fixed until in SMC.
  • Improved MITL checker.
  • Improved floating point computations in SMC.
  • Fixed copies when using arrays of clocks.
• Feb 29, 2012: Uppaal 4.1.8 - Development snapshot
  A snapshot of the 4.1-version currently under development. Changes:
  • Improved clock arithmetics for SMC.
  • Added clock copies.
  • Fixed the delay choice history optimization in SMC.
  • Fixed bugs in SMC linked to negative clock rates.
  • Removed implicit invariant x≥0 for SMC.
  • Added support for hybrid systems (1st order ODE) for SMC.
  • Added the simulate query.
• Nov 24, 2011: Uppaal 4.1.7 - Development snapshot
  A snapshot of the 4.1-version currently under development. Changes:
  • Fixed clock arithmetics for SMC.
  • Fixes for parsing large xml files.
  • Fixed non termination for step-bounded runs in SMC.
  • Fixed random generator bug (introduced in 4.1.6).
• Oct 25, 2011: Uppaal 4.1.6 - Development snapshot
  A snapshot of the 4.1-version currently under development. Changes:
  • Fixes on rounding errors that cause problems in SMC (invariants and such).
  • Repaired error feedback in the GUI (the protocol was changed in 4.1.5).
  • Improved arithmetics on clocks with auto cast from int to double.
  • Used the Mersenne twister mt19937 pseudo-random generator for SMC.
• Oct 19, 2011: Uppaal 4.1.5 - Development snapshot
  A snapshot of the 4.1-version currently under development. Changes:
  • Fixed the liveness checker when the Modest tool semantics is used.
  • Added drag and drop (inside and between different instances of UPPAAL).
  • Fixed crash upon exit when exceptions are thrown (common on Mac).
  • Improvements on SMC.
  • Changed zeno detection for SMC.
  • Extended clock arithmetics for SMC.
  • Copy-paste improvements on Unix platforms.
  • Extrapolation optimization for models containing guards of the form x >= 0.
• Jul 11, 2011: Uppaal 4.1.4 - Development snapshot
  A snapshot of the 4.1-version currently under development. New features include:
  • Fixed bug 502.
  • New 64-bit versions for Linux and Mac.
    This version will use roughly 90% more memory compared to the 32-bit version on the same models, which is due to pointers being represented on 64 bits. You can go beyond 4GB now but for this to be worth it you should have at least 8GB available. Please do not misuse this version for comparisons on memory consumption.
  • New statistical model-checker engine (SMC) (CAV 2011 tool paper [dllmw11]).
  • New distributed SMC (with OpenMPI), presented in an invited talk at PDMC 2011. This requires ubuntu 11.04 or equivalent Linux distribution, or MacOS 10.6.
  • New optional semantics for transition updates for compatibility with Modest.
  • New CSP-style synchronisations.
• Oct 7, 2010: Uppaal 4.1.3 - Development snapshot
  A snapshot of the 4.1-version currently under development. New features include:
  • Fixed bugs: 471, 482, 484, 485, 486, 488, and 489.
  • Added support for broadcasts with clock constraints on the receiver side.
  • The liveness checker now supports models with priorities and broadcasts with clock constraints on the receiver side.
  • Fixed traces for models that had these features.
  • Added new "inf" query and improved "sup" query.
  • Added activation check for unauthorized non-academic users.
  • Added live sequence charts in the Linux version. This is an experimental feature that allows users to specify properties as LSCs and check if a given system satisfies such LSCs. It is operational only under Linux.
• Sep 27, 2010: Uppaal 4.0.13
  The new version of Uppaal.
  • Solved problem with offline mode.
• Aug 20, 2010: Uppaal 4.0.12
  
  • Fixed bugs 471, 485, 488, and 489.
  • Added activation check for unauthorized non-academic users.
• Feb 11, 2010: Uppaal 4.0.11
  
  • Fixed bug 482,
  • Fixed menu entries for Mac (undo/redo). - "About" windows now displays the expiration date of the license and in parenthesis (if applicable) the expiration time and date of the current lease.
• Sep 21, 2009: Uppaal 4.0.10
  
  • Fixed bug 481.
• Sep 11, 2009: Uppaal 4.0.9
  
  • 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), <? (min), >? (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.