License

Please read the license agreement carefully. The text of the agreement follows:

We (the licensee) understand that UPPAAL includes but is not limited to the programs: uppaal2k.jar, uppaal2k, server, socketserver, atg2ugi, atg2ta, atg2hs2ta, hs2ta, checkta, simta, verifyta, tron, tron-s, uppaal, and xuppaal and that they are supplied "as is", without expressed or implied warranty. We agree on the following:

1. You (the licensers) do not have any obligation to provide any maintenance or consulting help with respect to UPPAAL.
2. You neither have any responsibility for the correctness of systems verified using UPPAAL, nor for the correctness of UPPAAL itself.
3. We will never distribute or modify any part of the UPPAAL code (i.e. the source code and the object code) without a written permission of Wang Yi (Uppsala University) or Kim G Larsen (Aalborg University).
4. We will only use UPPAAL for non-profit research purposes. This implies that neither UPPAAL nor any part of its code should be used or modified for any commercial software product.

In the event that you should release new versions of UPPAAL to us, we agree that they will also fall under all of these terms.

Requirements

TRON requires Unix environment and GNU C++ compiler (g++) or Microsoft Visual Studio or Sun Java 1.5 for creating custom adapters. It has been built on Debian GNU/Linux SID (unstable) and also for Windows in Cygwin environment using g++ from MingGW so it's very likely to work with C-library adapters built there. There's a small example C-library adapter built by Microsoft compiler, however currently it is only useful to connect to real IUTs in real-time, the virtual-time framework won't work in Windows, unless through TCP/IP socket adapter. Here is the dependency list with Debian package names in parenthesis:

• Java 2 Standard Development Kit 1.5 (AKA J2SDK 5.0) from http://java.sun.com/. Used by: TRON Tracer GUI, smart-lamp. Earlier Java versions won't work.
• Dot/Graphviz (graphviz) from http://www.graphviz.org/. Used by: TRON Tracer GUI.
• R (r-base) from http://www.r-project.org/. Used by: latency.
• GhostView (gv) from http://wwwthep.physik.uni-mainz.de/~plass/gv/. Used by: latency.

Install them all on Debian:

Download

By downloading any version of Uppaal, you agree to the above licensing terms.

• TRON-1.5 for [Linux on Intel PC] and [Windows].
• TRON-1.4 Beta 5 for [Linux on Intel PC] and [Windows].
• TRON-1.4 Beta 4 for [Linux on Intel PC] and [Windows].
• TRON-1.4 Beta 3 for [Linux on Intel PC] and [Windows].
• TRON-1.4 Beta 2 for [Linux on Intel PC].
• TRON-1.4 Beta 1 for [Windows].
• TRON-1.3.3 for [Linux and Solaris].
• TRON-1.3.2 for [Linux and Solaris].
• TRON-1.3.1 for [Linux and Solaris].

Please also check the Requirements section.

You may want to read an early draft of user-manual (still under development, comments are welcome).

Status of the Project

Now Uppaal TRON version 1.4 Beta 1 is available. The tool is still in early development and experimental phase, but now anyone can checkout and taste the early fruits on his/her own. The current version is based on the latest Uppaal 4.1. Current availability and limitations:

1. System specification accepted in Uppaal xta and xml format. The interface is specified separately in adapter library code.
2. Supported main Uppaal features: clocks, data variables, paired channel synchronizations, urgent locations. The use of arrays, broadcast channel, and committed locations are experimental and not tested.
3. Input and output actions through channel handshake synchronization (no buffering or value passing).
4. User supplied adapter loading via dynamic library interface.
5. Adapter development framework (C++), interfaces are not completely stabilized yet.
6. Examples of tool applications against C++ programs as IUT.
7. Use Uppaal to create and edit models.
8. TRON Tracer GUI demonstrates the main concepts: system model partitioning, interactive traces in testing, system emulation and monitoring.
9. Graphical user interface is mounted on generic trace-interpreter-adapter (special IUT adapter library) and serves as generic example of how to connect/link to TRON.
10. Stripped binary executable form of Uppaal TRON. No source code provided due to licensing restrictions. Binary is dynamically linked in order to provide efficient connectivity with user-supplied adapter.
11. The tool is prepared on the following platforms:
    • Windows 2000 Professional, GNU Compiler Collection 3.4.5
    • Linux 2.6.18 on Intel PC, GNU Compiler Collection 4.1.2
    Latest builds for Sun Solaris could also be provided upon request. It is important that the machine architecture should match and GCC-2 should not be mixed with GCC-3. The same holds for GCC-4. Please report your experiences.

Version History

• 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 05, 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.
  

• Older versions are available as T-Uppaal.