This page’s menu:



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.

 * Added TRON executable as dynamically linked library (
 * 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.
 * 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.
 * 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.
 * 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.
 * 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).
 * 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.
* 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.
* 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.
    * Changed name to Uppaal TRON.
    * Minor fixes in help output.
    * Added input/output interface printout before testing.
* 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.

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.