Changelog

• UPPAAL
• UPPAAL Stratego
• UPPAAL Tiga
• UPPAAL ECDAR
• UPPAAL CORA
• UPPAAL TRON

UPPAAL

This version history documents the development of Uppaal since the release of UPPAAL version 1.99 on December 2th, 1996. The first release of modern Uppaal (aka. Uppaal2k) was with beta version 3.0 on July 20th, 1999.

• December 11th, 2023: Uppaal 5.1.0-beta5
  Development snapshot of Uppaal-5.1.0.

  • Fixed uploading document to ULS (autocompletion language server) on a document change
  • Fixed bulk handling of struct and array types containing clocks in a simulate query
  • Fixed int to double conversion in inline-if expression
  • Fixed symbolic trace deadlock transition represented by multiple zones
  • Added a link and tooltips to license registration in the license dialog

• November 20th, 2023: Uppaal 5.1.0-beta4
  Development snapshot of Uppaal-5.1.0.

  • Added right-click on a query features: load trace into simulator and save strategy
  • Added splashscreen
  • Added all software licenses to LICENSES.txt
  • Unified parsing techniques and fixed issue where some engine errors wouldn’t be caught
  • Silenced Verifier result popups when verifying multiple queries
  • Updated libraries: openssl-3.0.11, lease-2.5.1, prlearn-1.1.1
  • Cosmetic fixes to some of the demo examples
  • Fixed toolchain names for ULS in release script
  • Fixed ULS (autocomplete) executable permissions and its library dependencies
  • Fixed engine and ULS executable lookup strategy

• October 23rd, 2023: Uppaal 5.1.0-beta3
  Development snapshot of Uppaal-5.1.0.

  • Minor autocomplete usability improvements
  • Test case generator improvements
  • Reduce unnecessary ULS communication by cancelling redundant operations
  • Fixed issue with auto sizing when clicking details button in message popups
  • Fixed issue where language server couldn’t be found on paths with spaces
  • Fixed out of memory exception with engine and language server communication
  • Fixed issue with options having invalid values with some locales
  • Fixed the enable autocomplete options
  • Fixed some issues on high dpi monitors

• September 25th, 2023: Uppaal 5.1.0-beta2
  Development snapshot of Uppaal-5.1.0.

  • Improved text editor and added autocomplete using Uppaal Language Server (ULS)
  • Added bounds query to record all values (generalizes inf and sup queries)
  • Update to newest UTAP version 2.1.0 (bounds query)
  • Fixed menu option when engine is disconnected
  • Fixed new version fetching and checking default to version.txt
  • Improved testability of simulator transition chooser
  • Added implicit clock to double conversion in ternary conditional operators
  • Fixed license checking for offline use
  • Fixed zoom to 100% hotkey exceptions

• July 14th, 2023: Uppaal 5.1.0-beta1
  Development snapshot of Uppaal-5.1.0.

  • Added concrete traces for random exploration option
  • Refactored model API
  • Added ModelDemo showing model and engine API
  • Increased floating-point precision in concrete trace output
  • Added space in error message popup.
  • Fixed error message in verifyta when license is not found

• June 21th, 2023: Uppaal 5.0.0
  The new major version of Uppaal.

• June 20th, 2023: Uppaal 5.0.0-rc6 - Pre release
  A release candidate of Uppaal 5.0.0 currently under development.

  • Fixed issue with clock expressions in conjunctions
  • Fixed issues with comparing clocks with equal rates

• June 19th, 2023: Uppaal 5.0.0-rc5 - Pre release
  A release candidate of Uppaal 5.0.0 currently under development.

  • Fixed AddLinks and launching scripts
  • Fixed SMC time-lock when floating-point variable is used as a clock bound

• May 31th, 2023: Uppaal 5.0.0-rc4 - Pre release
  A release candidate of Uppaal 5.0.0 currently under development.

  • Fixed Concrete Simulator the latest delay button when max delay is infinite
  • Removed results from bluetooth example model
  • Removed formula printing from verifyta results when using a query file (to be returned back when UTAP is fixed)
  • Fixed NullPointerException in licensing dialog without network connection
  • Fixed setting the lease duration if lease option is not used
  • Improved lease fetching performance when home folder is shared among multiple computers
  • Added lease-update scripts to bin folder to update lease on customized networks (firewall/proxy/VPN etc)

• May 17th, 2023: Uppaal 5.0.0-rc3 - Pre release
  A release candidate of Uppaal 5.0.0 currently under development.

  • Allow zero step bound in SMC queries
  • Improved floating point precision in SMC-related statistics
  • Fixed issue with counting successful runs with some probability queries
  • Fixed MITL run count reporting and changed the prob estimation to sequential procedure
  • Refactored the variance algorithm to a straight-forward formula to increase precision
  • Fixed value estimation with non-trivial clock expressions
  • Added F7 as hotkey for check syntax on macOS
  • Fixed move up locations when SnapToGrid is activated
  • Fixed template export option
  • Fixed heatmap coverage higlighting to use grayscale palette and arrow thickness
  • Fixed the problem when zooming-in in simulator tabs
  • Fixed unbounded bar drawing in Gantt chart in Concrete Simulator
  • Fixed Open Recent menu to use canonical paths and avoid duplicate path entries
  • Fixed Random button enabling when horizon is expanded and transitions appear
  • Fixed simulator hotkeys handling while editing plot names
  • Fixed display of samples at 0 in the plot widget
  • Improved plot widget performance by filtering overlaping sample points
  • Fixed Concrete Simulator exceptions when shortest Diagnostic trace is selected
  • Fixed saveStrategy to save the specified strategy when executed out-of-order
  • Added workaround for UTAP exception during pretty-printing in verifyta output
  • Added version and stdc-version commands to verifyta help section

• March 7th, 2023: Uppaal 5.0.0-rc2 - Pre release
  A release candidate of Uppaal 5.0.0 currently under development.

  • Updated example models to simplify and match query syntax changes
  • Added localization of value estimation error messages.
  • Fixed vertical line in graphs not going below 0.
  • Fixed issue where hybrid clocks cannot be assigned negative integers.

• March 2nd, 2023: Uppaal 5.0.0-rc1 - Pre release
  A release candidate of Uppaal 5.0.0 currently under development.

  • Changed colors of concrete simulator transition chooser
  • Moved global find and replace into local find menu
  • Fixed issue that broke symbolic queries for some models with derivatives

• February 27th, 2023: Uppaal 5.0.0-beta5 - Pre release
  A beta of Uppaal 5.0.0 currently under development.

  • Fixed issue that caused some transitions to be unavailable in concrete simulator due to floating point precision

• February 22nd, 2023: Uppaal 5.0.0-beta4 - Pre release
  A beta of Uppaal 5.0.0 currently under development.
  This beta includes a lot work which can be seen under the UPPAAL Stratego changelog.

• October 5th, 2022: Uppaal 4.1.26-2 - Development snapshot
  A snapshot of the 4.1-version currently under development. Changes:

  • Moved the old Linux libc libraries out of the way in favor of the host’s libc.
  • The old libraries are still included in old-libc directory for older distributions.

• February 7th, 2022: Uppaal 4.1.26-1 - Development snapshot
  A snapshot of the 4.1-version currently under development. Changes:

  • Fixed L&F NullPointerException experienced with OpenJDK 11.0.10 and later.

• December 2nd, 2021: Uppaal 4.1.26 - Development snapshot
  A snapshot of the 4.1-version currently under development. Changes:

  • Fixed interaction between tabs.
  • Fixed trace loading into simulators.
  • Fixed symbolic simulator showing deadlocks beyond invariant.
  • Fixed symbolic simulator executing disabled transitions beyond invariant.

• April 12th, 2021: Uppaal 4.1.25-5 - Development snapshot
  A snapshot 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 snapshot 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 snapshot 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 snapshot 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 snapshot 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 snapshot 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 snapshot 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 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. Uppaal2k

  • 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. Uppaal2k

  • 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. Uppaal2k

  • 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. Uppaal2k

  • 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. Uppaal2k

• Mar 1998, 2.17 (official)

• Feb 1998, 2.16 (internal)

  • Verifyta:
  • New/improved hash function.
  • Other improvements.

• Nov 1997, 2.14 (internal)

  • uppaal:
    • Support for simta.text added.
    • Support for simta.text removed.
    • Filter setting removed (obsolete).
  • xuppaal:
    • [<–] problem fixed. Help menu is now activated with Ctrl-E.
    • Zombie processes problem solved.
  • verifyta:
    • GTA support added.
    • General expressions on integer expressions added.
    • Max and Min time derivation inactivated.

• Oct 1997, 2.12 (internal)

  • simta.text:
    • Borned. Simulator with textual interface.
  • verifyta:
    • Now handles integer guards on transitions with urgent actions in a well defined way.
    • Termination using max time constant.
    • Max and Min time derivation added.
    • Parametric leadsto algorithm added.

• Jul 1997, 2.12 (internal)

  • verifyta:
    • DBM optimisations (reduced number of close operations performed).
    • Trace display problem fixed.
    • Problems with parsing constants fixed.
    • Live-lock warning added, displayed if a reachable state is found with no outgoing transitions but the state allows for unbounded delay.

• Jun 1997, 2.11 (internal)

  • verifyta:
    • Integer implementation (v.2.09) refined.
    • Constant declarations can now be mixed with other variable declarations.

• Jun 1997, 2.10 (internal)

  • xuppaal:
    • Options->Deadlock Warnings added: turns on/off deadlock warning.
    • Problem with interface to Local Reduction fixed.
  • Man pages: verifyta.1, uppaal.1, ta.5 updated.

• Jun 1997, 2.09 (internal)

  • verifyta & checkta:
    • Added integer variables with explicit ranges. Declaration syntax
    • changed. Also, new more general expressions added to integer
    • variables.

• May 1997, 2.08 (internal)

  • verifyta:
    • The waitlist now uses STL-lists again.
    • The algorithm of adding states to the wait list has been changed in a way that might alter the order in which the state space is searched.
    • Memory leaks removed.

• May 1997, 2.07 (internal)

  • verifyta:
    • Memory leaks removed.

• May 1997, 2.06 (internal)

  • verifyta:
    • A lot of internal things changed, nothing visible to the user, including: reimplementation of passedlist, and adding of some destructors.

• May 1997, 2.05 (internal)

  • verifyta:
    • Interval removed from implementation of integer variables.

• May 1997, 2.04 (internal)

  • verifyta:
    • -h added. If given, verifyta print a short help message describing all the command line options.

• Apr 1997, 2.03 (internal)

  • verifyta:
    • -D added. If not given, a deadlock waring is displayed if a reached state have no possible outgoing transitions.

• Mar 7 1997, 2.02 (official)

  • xuppaal:
    • Help->Problems added,
    • Run->Show Model and Run->Show Req. Spec improved, erroneous line breaks removed,
    • Help text improved,
    • Double click on verification output changes view point in property editor (if displayed).
  • Man pages: xuppaal.1 new, uppaal.1 updated.

• Mar 3 1997, 2.02 (beta)

  • verifyta:
    • bug fix,
    • number referring to lines in the property file now shown in verification output.

• Feb 26 1997, 2.01 (beta)

  • uppaal is now a bash-script again, all verification options supported.
  • Comments and line breaks in formula format. “//” - rest of line is ignored, “\” - line break in formula.
  • atg2ta, hs2ta, checkta, verifyta and uppaal compiled for MS-DOS (DPMI server required).
  • Man pages: uppaal.1 updated.

• Jan 16 1997, 2.00 (beta)

  • New optimisations in verifyta: -S for control structure reduction (semantics changed from previous version), -C for disabeling use of compact data structes for constraints (default enabled).
  • Man pages: verifyta.1 updated.
  • Support for new optimisations in xuppaal.

• Dec 2 1996, 1.99, (official)

  • New optimisations in verifyta: -S for Control Structure Reduction, -T for reusing generated state space when checking several properties in sequence.
  • Support for new optimisations in xuppaal.
  • Simple Requirement Specification Editor added to xuppaal.
  • atg2ta, hs2ta, checkta, verifyta, uppaal and xuppaal compiled for Linux.

  UPPAAL Stratego

• December 23rd, 2022 Uppaal 4.1.20 Stratego 11

  • Fix issue with strategies being set when no system is set
  • Tighter grid is disabled, when grid is tightest
  • Fixed the problem with fontColor in JFreeChartPlot
  • Remove race condition in SimulationThread
  • Correctly evaluate arrays of channels
  • Symbolic Simulator “Mark visited”-related fixes
  • Added “controllable” popup option to the edge context menu
  • Improved UX in Find
  • Fixed issue where the meta type was ignored for boolean variables
  • Fixes dynamic library support across Linux, macOS and Windows
  • Avoid disappearing error highlights
  • Allow constant variables in translated parameters
  • Unify GUI colors
  • Updated UTAP to 1.1.6 (enable quantifiers {sum,forall,exists} at compile time)
  • Fix issue where location predicates were always true or false
  • Cancel edge creation with undo action
  • Improve expression printing
  • Make error dialog more user friendly
  • Improve safety and readability of opcodes in program and some exception handling
  • Fix quantifier expressions as constant expressions
  • Refactor query results and add run limit to Probability queries
  • Refactor JSON serialization in GUI to use GSON
  • Get back the old color for location
  • Remove EmptyCommand and fixed edge creation issues
  • Translate constant parameters through evaluation
  • Updated OpenSSL to 3.0.7
  • Fixes NPE when the document child node has no “name” property
  • Fixes non-deterministic inputs in concrete simulator
  • Check whether the file exists for better error reporting
  • Concrete simulator under strategy minor fixes
  • Fixed issue where clocks are overwritten during guard evaluation
  • Minor fixes for error dialog
  • Reintroduced engine output localization
  • Terminate trace if step bounded and no steps can be reached
  • Refactored FMU generation with better I/O error handling
  • Fix handling of non-deterministic inputs in Concrete Simulator
  • Concrete sim handle 0 delay case with diagonal constraints with differing rates
  • Fix error positions for synchronization expressions
  • Learning strategy fix and concrete simulator support
  • Opening non-existing file and better error messages
  • Let strategy to choose the longest delay when all outgoing edges are input-guarded
  • Don’t remove strategies when receiving feedback from query
  • Re-enable concrete trace recovery from verification errors
  • Fixed time-lock error message to include state info
  • Fixed clock rate precomputation before a stochastic trace is generated
  • Add target invariant checking in concrete simulator
  • Make simulation trajectory count respect successful number of runs
  • Improve error handling and reporting
  • Allow urgent edges to override exponential rate requirement
  • Added two new stratego examples: train-gate-strat.xml and cat-and-mouse.xml
  • Skip input edges with no matching output
  • Upload system before firing system changed event
  • Removed SwiXML checks on standard Swing components

• October 3rd, 2022 Uppaal 4.1.20 Stratego 10

  • Added strategy selection in the Concrete Simulator.
  • Added local and global search and replace (ctrl+f, ctrl+r, ctrl+shift+f, ctrl+shift+r).
  • Added “Open Example” and “Open Recent” menu items.
  • Added built-in declarations of C constants (INT32_MAX, M_PI etc) and types (int8_t, int32_t etc).
  • Added arrow key handling in timed automaton editor (ctrl+arrow, ctrl+shift+arrow).
  • Added contextual popup menu for multiple selected timed automaton elements.
  • Added opening of dragged over XML files.
  • Added error message when free template parameter is unbounded, which caused unintended instantiation of 64K processses.
  • Added an option to use JFreeChart for plots in Preferences (enables pan and zoom).
  • Added advanced text editor mode to Preferences (automatic tabulation and nesting of parenthesis).
  • Fixed SMC query syntax to specify the number of runs inside square braces.
  • Fixed many issues in Concrete Simulator.
  • Fixes several issues in plots.
  • Fixed loading of diagnostic traces on macOS.
  • Fixed color and box handling of comments over timed automaton.
  • Fixed handling of variables in the Test Generator.
  • Fixed keyboard shortcut consistency.
  • Fixed engine-related menu layout.
  • Fixed layout of engine connection dialog.
  • Fixed license dialog and lease handling.
  • Fixed DBL_MAX value display in Concrete Simulator.
  • Fixed undo support for change of initial location.
  • Fixed exception when clicking on empty query list.
  • Fixed drag-and-drop of templates between instances.
  • Fixed icons and positions of popup windows.
  • Fixed status bar scaling.

• January 24th, 2022: Uppaal 4.1.20 Stratego 9

  • Fixed an issue when symbolic simulator would not correctly show deadlocks.
  • Improved stability of concrete simulator.
  • Added support for (re)generated trajectory plots when loading a trace (concrete simulator)
  • Fixed memory issue in UTAP

• January 7th, 2022: Uppaal 4.1.20 Stratego 8
  General:

  • Support for 64-bit Windows
  • Support for MacOS
  • Package Bundle (.app) for MacOS
  • Numerous bugfixes and stability improvement fixes in the engine and GUI.

  Graphical user interface:

  • Editor: template popup menu by right-clicking in the Project tree.
  • Editor: fixed caret position issue on multiple screen desktops
  • Help: improved and moved to online documentation: https://docs.uppaal.org/
  • Preferences: Look-and-feel themes (Native, Java, Flat), dark mode
  • Preferences: JetBrains monospace font with ligatures
  • Preferences: backported HiDPI/scaling
  • Select a custom engine (bundled, remote or configure a custom command)
  • Improved Platform Integration (MacOS)

  Verifier:

  • Learning: deprecated loop over RESET location in favor of { integral } -> { floating } expression in the query, where integral is a comma-separated-list of observed integer variables and floating is a comma-separated-list of observed floating point variables (double or clock type) See demo/stratego/cruise.xml example.
  • Learning: support for external learning (experimental)
  • Randomized reachability exploration to quickly find concrete counter-examples using symbolic queries like A[] and E<> See menus Options -> Exploration -> Randomized, and Options -> Randomized parameters.
  • Engine option settings are saved and loaded with the model file
  • Queries can have custom engine settings (click gear button next to the query editor)
  • Query results are saved and loaded with the model file
  • Verification dialog option to kill the engine
  • Zoom action support to change the query font size

  Symbolic Simulator:

  • Fixed invariant applicationa and removed superfluous deadlock transitions beyond invariant

  Concrete Simulator:

  • Complete rewrite of control panel (transition chooser, trace navigation)
  • Hybrid automata support (ODE invariant and algebraic guard)
  • Trajectory plot widget (right-click on the variable to create one)
  • Random and stochastic simulation support (right-click on the “Random” button)
  • Saving and loading traces from files
  • Simulator tabs are disabled if the model contains unsupported features

  Internals:

  • New GUI-engine communication protocol based on JSON
  • Ported GUI plugin API, support for simulation trace access

• December 6, 2019. Version 4.1.20-7 released.

  • Fixed engine protocol memory bug (server binary was crashing on Windows).
  • Fixed unicode encoding in engine protocol (GUI was showing mangled characters).

• October 10, 2019. Version 4.1.20-6 released.

  • Integrated Q-learning and M-learning methods.
  • Changed the engine protocol from “dot” format to JSON (the schema is not final).

• February 19, 2019. Version 4.1.20-5 released.

  • Added C-library functions, including fint() for float to integer conversion.
  • Loading external functions from dynamic library (DLL) into model code
    (papers demonstrating examples and use cases).
  • New simulation-engine for SMC and Stratego queries.
  • Fixed a number of floating point precision bugs.
  • Integration uses more stable Runge-Kutta method (see –truncation-error and –truncation-time-error)
    bounded by a minimum delta (–discretization)
  • Improved static analysis and derived speedups for non-hybrid models.
  • Major refactor and stabilization of Stratego/Learning.
  • Fine-tuning of search-strategy (see –random-search-limit and –determnistic-search-limit).
  • Strategy output of learned strategies (available for –learning-method 1,3,4 and 5)
    in JSON format with header describing mapping to system (see –print-strategies).
  • Manual feature-selection using the “{a,b,c}->{d,e,f}"-style notation (examples)
  • New learning algorithms (4+5) utilizing Q and M-learning (paper under review).
    (options –qlearning-alpha, –split-upper-t, –split-lower-t, –split-ks,
    –split-filter-rate, –split-filter-val, –discount, –indefference-smoothing
    and –indefference-scale are unique to these methods)
  • Added layout checking for overlapping elements.
  • Added Dockerfile for MacOS and 64bit Windows (instructions in res/Docker.md).
  • Disabled rare event support via “Reach” and “Rare” queries.

  Known issues:

  • Missing strategy import
  • Missing strategy export for symbolic (TIGA) strategies
  • Missing translations/text strings of options and engine output
  • Missing documentation of new features in help-file

• November 10, 2016. Version 4.1.20-4 released.

  • Rare event support via “Reach” and “Rare” queries.

• April 14, 2015. Version 4.1.20 released.

  • Fixed symbolic simulator.
  • Canceling verification job preserves strategies.
  • Allow output synchronization on outgoing branches.

• November 19, 2014. Version 4.1.20 4th pre-release.

  • Enabled the editor to modify “controllable” property of edges.
  • Better default learning parameters.
  • Fixed crashing when loading new model.

• November 19, 2014. Version 4.1.20 3rd pre-release.

  • Fixed minimization expressions for learned strategies.

• November 19, 2014. Version 4.1.20 2nd pre-release.

  • Fixed engine options handling.
  • Updated newspaper.xml example with more comments.

• October 23, 2014. Version 4.1.20 1st prerelease.

  UPPAAL Tiga

• Version 0.18 is released. (July 1st, 2014)
  This version adds partial support for SMC and UPPAAL checks under the constraints of a given strategy. Reinforcement learning is now supported too and works for DPA systems.

• Version 0.17 is released. (Mar 27th, 2014)
  This version is a maintenance release fixing the GUI to work with Java 7. It also includes Ecdar.

• Version 0.16 is released. (Feb 18th, 2011)
  This version is a maintenance release fixing bug 502 and a crash when exceptions were thrown in the liveness checker of UPPAAL.

• Version 0.15 for Mac released. (Oct 21st, 2010) The Mac version of TIGA is now available, courtesy of Didier Lime.

• Version 0.15 released. (Oct 14th, 2010)
  This version improves the simulator. Occurences of states “getting out of the strategy” are rarer now. However, verification will take longer when asking for strategies.

• Version 0.14 released. (Nov 6th, 2009)
  This version improves the simulator: stop-watches are better treated and the Gantt chart respects urgent/committed states.

• ** Version 0.13 released. (Sep 11th, 2009)**
  This version fixes issues with the simulator and fixes bugs in the verifier. Fixes of the development versions 4.1.1 and 4.1.2 haved been ported. The simulator includes a new experimental Gantt chart. The examples in the demo directory have been fixed. This version supports simulation check of timed game automata.

  UPPAAL ECDAR

• Version 0.10 released. (13 Apr 2013)
  Bug fix release. IO specifications are now explicit and must be defined after the system declaration. See the updated examples for the intuitive syntax. A 64-bit version for the command line verifier has been added - do not use any option that uses CDDs, do not use interactive play.

• Version 0.9 for Mac released. (21 Oct 2010)
  The Mac version of ECDAR is now available, courtesy of Didier Lime.

• Version 0.9 released. (14 Oct 2010)
  This version fixes numerous problems related to the simulator and the checker.

• Version 0.8 released. (7 May 2010)
  This version fixes a crash in the server when no strategy is available and the simulator is used anyway.

• Version 0.7 released. (5 May 2010)
  This version improves the simulator and has a better support for the quotient.

• ECDAR pre-release 0.6. (9 Apr 2010)
  This version improves the simulator and fixes some bugs related accepted models for the refinement checker. The simulator works better for simulating refinement strategies.

  UPPAAL CORA

  • 20060910: Fixes bug 346 and a bug in concrete trace generation. Models of the air craft landing problem and the vehicle routing problem with timed windows have been added to the demo directory. The engine in this release is based on the latest development version of UPPAAL. The GUI is identical to that of UPPAAL 4.0.2.

  • 20060808 (PTA): This release fixes a serious memory leak. The engine is based on the latest development version of UPPAAL. The GUI is identical to that of UPPAAL 4.0.2.

  • 20060626 (PTA): This release is based on UPPAAL 4.0.1 (the GUI is identical to UPPAAL 4.0.1). No new CORA specific end user functionality was added compared to the previous UPPAAL CORA release. Universal binaries for Mac OS X are now available.

  • 20060206 (PTA): This release is based on UPPAAL 3.6 Alpha 4. Besides all the bug fixes in UPPAAL, at least one CORA related bug (bug 243) that caused the verifier to go into an infinite loop was fixed. Notice that the 3.6 syntax is now enabled by default in verifyta. The -N option is no longer needed.

  • 20051027 (PTA): This release is based on the soon to be released UPPAAL 3.6 Alpha 1. Since the last release in June 2005 approximately 50 bugs and enhancement requests have been closed and numerous minor problems have been fixed. There are no new CORA specific features in this release, however a number of critical bugs specific to CORA have been fixed. A number of those relate to trace generation.

  • 20050621 (PTA): This release is based on UPPAAL 3.5.7. The previous release was rather buggy and I hope most issues are fixed by this release. In particular the use of a heuristic variable for defining the search order was broken.

  • 20050531 (PTA): This release is based on UPPAAL 3.5.6. There are lots of changes since the last release: Bug fixes, performance improvements, and new features. The most notable fix is probably that the simulator now works (in the previous release it worked for most simple models, but failed for more complicated models). Also traces can now be loaded reliably from the model checker into the GUI. The most notable new feature is probably the concrete trace generator for priced time automata. This trace generator produces optimal concrete traces. It is only available from the command line (verifyta), though.

  • 20041109 (PTA): First release under the new CORA name and first publicly announced release. UPPAAL CORA is now packaged with a GUI (an unmodified version of the latest development version from main line UPPAAL) and ships with the Linux and Windows version in one package. If a Solaris version is needed, please email us and we will add it. Other changes in this release: bug fixes in the parser, active clock reduction added, several optimisations in successor computation. Addition of best depth first search order.

  • 20040819 (PTA): New release of PTA version. This release contains all the changes from the 20040625 UPTA version (record-types and UCode support). It also contains support for incrementing the cost on edges using the += operator. Finally, it contains bug fixes and performance improvements.

  • 20040625: New release of UPTA version. This release fixes bugs in how meta variables are handled. It also contains basic support for record-types and UCode (support for functions).

  • 20040519 (PTA): Merged bug fixes from 3.4 branch.

  • 20040518 (PTA): First release of PTA version. This is the first release of UPPAAL PTA.

  • 20040106: Bug fixes. Fixed some memory leaks and a problem with how meta variables are handled. Also changed the default syntax back to 3.4. Use the -N to enable the extended 4.x syntax with support for the UPTA extensions. Notice however that this option is not listed in the synopsis of verifyta.

  • 20031217: Ported UTAP support to the 3.4 series of UPPAAL. Notice that the syntax has changed. Please read the documentation before upgrading. Your old models will not work with this version!

  • 20021218: Wrong estimate detection. Added warning message when a goal state is reached and the estimate of the remaining cost is non-zero.

  • 20021212: Added support for remaining cost estimation. An extra implicit variable called remaining was added. This variable can be assigned to on the transitions or using a global assignment right before the global heur assignment. The value of this variable should be set to a lower bound on the remaining cost to reach the goal from the current state. Pruning is done with respect to cost + remaining. If you want to find the best solution, use heur := cost + remaining as your global heur assignment and use the -o and -E option.

  • 20021210: Added -R option. This option randomises the ordering between states with equal heur value (only relevant with -o and -O).

  • 20021201: Initial release

  UPPAAL TRON

• June 17, 2009. Version 1.5

  • Added TRON executable as dynamically linked library (libtron.so)
  • Compiled pthread-win32 library from repository (not yet released v.2.9.0).
  • Revised virtual clock framework.
  • Fixed virtual clock deadlock exhibited on SMP setup (especially Windows).
  • Cleaned up and restructured java examples.
  • Added Jester script for automatic mutations in java examples.
  • Added response times measurements in latency example.

• April 5, 2008. Version 1.4 Beta 5

  • Enabled zone merging (2x speedup on models with a lot of concurrency).
  • Added explicit virtual clock clean up (fixes deadlock on exit in Windows)
  • Updated smartlamp description, added batch scripts for quick start-up.

• April 27, 2007. Version 1.4 Beta 4

  • Fixed segfault in -i dot option (bug from 1.4 Beta 3).
  • Removed dependency on mingwm10.dll from pthreadGCE2.dll (2.8.0).
  • Replaced -P random option to -P 10,200 in smartlamp.

• April 20, 2007. Version 1.4 Beta 3

  • Fixed diagnostics for output event timing (bug 369).
  • Fixed partitioning algorithm to analyze function calls too.
  • Fixed resizing of window in smart-lamp example (bug 413).
  • Fixed potential adapter API abuses (bug 311).
  • More user-friendly logging of time (log shows time units and microseconds).
  • Improved diagnostics for output events with variable values.
  • Compressed events in diagnostics to avoid repetition.
  • Removed exceptions from sockets, now terminates gracefully with pthread-win32.

• October 18, 2006. Version 1.4 Beta 2 for Linux

  • Removed dependencies on libgcc_s, libm and libc dynamic libraries
    which was a problem on Ubuntu 6.06 (thanks Kyller Costa Gorgônio for reporting).

• October 13, 2006. Version 1.4 Beta 1 (Linux readme, Windows readme):

  • This build is the first for Windows (earlier were Linux/Solaris only).
  • Microsoft Visual C library adapter example.
  • Textual communication via standard I/O adapter (see tracer example).
  • TCP/IP socket adapter for remote IUTs.
  • Java adapter framework with virtual and real-time support.
  • Check for correct system model partitioning by input/output channels.
  • Emulate only environment invariants when deciding input stimuli timing.

• September 26, 2005. Version 1.3.3 (readme.txt):

  • Major clean-up in examples.
  • Fixed problem with too late delay choice.
  • Added generic trace-interpreter-adapter to interact with model.
  • Added Java GUI based on trace-adapter.

• April 25, 2005. Version 1.3.2:

  • Compiled in libxml2-2.6.16 statically (fixes older xml2 issues).
  • Fixed environment guard “strict greater” fault, experienced only in
    simulated time (detected in timedgate example in 1-2 runs out of 1000).
  • Fixed “id” cleanup when moving across different architectures.
  • Fixed benchmark and verdict logging to files (they were absent).
  • Changed delay/action choice to choose from inputs and internal actions
    at ones rather than from inputs and then internal if no inputs available.
    This improves coverage by allowing sometimes to postpone inputs if they
    are optional. Notice that the choice is very sensitive to -F option.
  • Added redirection of driver log (-D), benchmark log (-B), statistics (-S).
  • Output verbosity restructured. Now -v bit-flags control the information
    dumped on terminal or to file (-o).
  • Real-time Round-Robin scheduler is selected in RT-clock if allowed.
    Usually it requires root permissions and has an advantage over other
    lower-priority programs. All Executable objects have this priority.
  • Added experiments for examining scheduler latency: ping-pong and ticking.

• March 1, 2005. Version 1.3.1:

  • Changed name to Uppaal TRON.
  • Minor fixes in help output.
  • Added input/output interface printout before testing.

• February 7, 2005. In 1.3.0 (As T-UPPAAL):

  • Environment invariants are supported (to the extent of CPU time available).
  • Simple observation uncertainty added to time-stampping.
  • Data value binding supported in input/output actions.
  • New adapter API.

• November 30, 2004. (As T-UPPAAL)
  In 1.2:

  • the first implementation of smart delay choice.
  • no need for zzz hack, invariants on environment are respected.
  • the coverage of the model is poor since the algorithm is not completely
    randomized because of smart delay choice (you may want to use 1.1.3 version).

  In 1.1.3:

  • first experiments with observation uncertainty added.
  • improved clock synchrony.
  • fixed bug in the driver: last delay reporting.
  • no smart delay implementation, zzz hack is still needed.