T-UPPAAL 1.3.0 Release
====================
News in this release:
* 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.
* New Adapter API.


T-UPPAAL Licence and Responsibilities
=====================================
Copyright (c) 1995-2005 by Uppsala University and Aalborg University.

We (the licensee) understand that Uppaal includes the programs:
uppaal2k.jar, uppaal, uppaal.bat, server, socketserver, atg2ugi,
atg2ta, atg2hs2ta, hs2ta, checkta, simta, verifyta, uppaal, xuppaal,
tuppaal, and tuppaal-s 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.


T-UPPAAL Requirements
=====================
GNU Compiler Collection versions 2.95 or 3.2 or newer.
Java 1.4 for lightcontroller demo.

Currently supported platforms:
SunOS 5.9   sparc gcc-3.3.1
Linux 2.6.9 intel gcc-3.3.5 (Debian unstable)


Ultra-short T-UPPAAL Guide
==========================
1) Download tuppaal-X.tar.gz, where X is a version number:
go to http://www.cs.auc.dk/~marius/tuppaal/download/

2) Extract the archive (where X is version number):
tar -xzvf tuppaal-X.tar.gz

3) step into T-UPPAAL directory:
cd tuppaal-X

4) and ask for hints:
make help

5) Currently there are three examples available:
  1) the train-gate controller (specification in timed-gate-free.tta):
    a) in simulated time:
      make test-timedgate-s
    b) in real-time:
      make test-timedgate
  2) the lightcontroller demo (specification is in LightContrFull_lowprec.tta):
     make test-lightcontroller
  3) the mouse-button (specification is in button.tta):
    a) in simulated time (no faults found):
      make test-button-s
    b) in real-time (the drift in IUT and TUPPAAL clocks is very appearent):
      make test-button


Common problems
===============
* Compilation OK, but libstdc++.so.X.Y not found when run.
  Reason: the specific version of C++ dynamic library not found. This is part 
  of so called dll-hell problem: tuppaal was compiled with different compiler 
  than the one available on the system. 
  Quick fix: create a symbolic link called libstdc++.so.X.Y pointing to the 
  available library (remember to set LD_LIBRARY_PATH to "./" if link is created
  in current directory). 
  A reliable fix is to find and use the corresponding GCC version.

* Compilation OK, but symbol Executable::joinThread not found when run.
  Reason: different C++ symbol mangling on GCC 2.x and 3.x. tuppaal was 
  compiled using different version of GCC (3.x) than the adapter 
  (probably 2.x) which led to different C++ symbol mangling. 
  Fix: ask for corresponding tuppaal binary or find a corresponding GCC 
  version for adapter.

* Compilation OK, but lots of messages about symbol relocation errors when 
  run on Sun OS.
  Reason: symbols in the library are not properly aligned the way OS expects. 
  Fix: compile your adapter library with "-fPIC -DPIC" options.

Feedback
========
Please write your comments and experiences to T-UPPAAL maintainer:
Marius Mikucionis <marius@cs.aau.dk>.