T-UPPAAL 1.1 Release ==================== News in this release: * new input-output locking mechanism in SampleAdapter: T-UPPAAL and IUT must agree on the same input and output ordering, thus SampleAdapter implements a simple protocol for deciding who is first to deliver action. All examples implement this protocol. On the other hand the user is not forced to use it, but must be aware that specification must include communication buffers alowing different input and output interleaving. - the TestAdapter interface changed, callback required upon delivery, - no more I/O synchronisation conflicts, - testing is more reliable since I/O interleaving is explicit now. * new simulated clock implementation: - the interface did not change, only the internals, - no more deadlocks, - condition notifications are not lost anymore, - no more segmentation faults on exit (and I don't experience them at all) * added shell and R scripts to reproduce the timed-gate experiment results and benchmarks, the only documentation about scripts and logs are just comments within scripts :-( * new example: mouse-button program responds with single-click or double-click to a series of clicks depending on click occurance in time. * no new bugs discovered, fewer of the old ones left (hopefully). T-UPPAAL Licence and Responsibilities ===================================== Copyright (c) 1995-2004 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.8 sparc gcc-2.95.3 and gcc-3.2.2 SunOS 5.9 sparc gcc-3.3.1 Linux 2.6.5 intel gcc-3.3.3 (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 Bugs ==== * 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 (2.x or 3.x) than the adapter (3.x or 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. * tuppaal gives false FAILED verdict even when IUT is obviously correct. Reason: lost time synchrony between tuppaal and IUT clocks. Quick fix: analyze the testing log to spot the lost synchrony; try testing your IUT in simulated-time if possible to make sure that IUT is really correct. Reliable fix: testing algorithm will be improved to handle time u ncertainties. * Environment invariants are not respected by TUPPAAL. Reason: bug in testing algorithm. Quick fix: avoid using invariants in environment model. Reliable fix: testing algorithm will be improved to include smart delay/action planning. * tuppaal stops testing with INCONCLUSIVE verdict and gives the reason "no input allowed by environment or IUT". Reason: bug in testing algorithm. Quick fix: add two automata, one capable of producing zzz at any time, and another capable of consuming zzz, declare zzz() as input. Reliable fix: testing algorithm will be improved to include smart delay/action planning. Feedback ======== Please write your comments and experiences to T-UPPAAL maintainer: Marius Mikucionis . I am waiting impatiently for your comments! :-) marius