README for UPPAAL2k 3.2.9, April 2002
Uppsala University and Aalborg University.
Copyright (c) 1995 - 2002. All right reserved.

April 16th, 2002

1. Introduction
2. Installation
3. New features in this release
4. Known issues is this release
5. License Agreement

1. Introduction
===============

This is version 3.2.9 of UPPAAL2k -- a model checker for timed automata.

Note that UPPAAL2k is free for non-profit applications but we want all
users to fill in a license agreement. This can be done online on the
web site http://www.uppaal.com/ or by sending in the form attched
below.

UPPAAL2k contains software copyrighted by The Apache Software 
Foundation, The World Wide Web Consortium, and Sun Microsystems.
Please read the files starting with the prefix License found in
the UPPAAL2k distribution.

2. Installation
===============

To install, unzip the zip-file uppaal-3.2.9.zip. This should create
the directory uppaal-3.2.9 containing at least the files uppaal2k,
uppaal2k.jar, and the directories lib, bin-Linux, bin-SunOS,
bin-Win32, and demo. The bin-directories should all contain the two
files verifyta(.exe) and server(.exe) plus some additional files, 
depending on the platform. The demo-directory should contain some 
demo files with suffixes .xml and .q.

Note that UPPAAL2k will not run without Java installed on the host
system. Java for SunOS, Windows95/98/Me/NT/2000, and Linux can be
downloaded from http://java.sun.com.

We strongly recommend using the most recent version of the Java
Runtime Environment (JRE) available for your platform, currently
version 1.4. Notice that exporting your X display on a Unix host
(Linux, Solaris) is very slow with JRE 1.2 and 1.3. This is not a
problem with JRE 1.1 or 1.4. In case of JRE 1.1, you also need to
download and install Swing. On Windows JRE versions prior to 1.2 are
not supported.

To run UPPAAL2k on Linux or SunOS systems run the uppaal2k script. To
run on Windows95/98/NT systems double click the file uppaal2k.jar.

3. New features and changes in this release
===========================================

- XML based file format.
- The GUI can save and load syntactically invalid systems.
- The GUI supports anonymous locations (locations without a name).
- The syntax checker in the GUI is much better.
- E[] p (there exists a path where p allways holds), A<> p (for all
  paths p will eventually hold), and p --> q (whenever p holds q will
  eventually hold).
- A major redesign of the engine resulted in fewer dependencie
  between verification options (e.g. "Global reduction" and "reuse
  state-space" can be used at the same time).
- Drag and drop support for changing the source and target of 
  a transition.
- Deadlock state predicate (the CDD based deadlock checker now detects
  all deadlocks).
- Command line support for loading projects.
- On Windows the socketserver has been removed.
- verifyta now supports both symbolic and concrete traces
- Bug fixes and many minor improvements.

4. Known issues is this release
===============================

1. XTA/TA import cannot read invariants placed directly on
   transitions.
2. Save as postscript is missing in the simulator (feature is
   available in UPPAAL2k 3.0).
3. UPPAAL2k 3.2.2 added a proper DOCTYPE to generated XML
   files. UPPAAL2k 3.2.1 (the previous release) does not know this
   DOCTYPE and will try to access a definition of it on our web
   server. If this is impossible or unacceptable you might need to
   manually delete the DOCTYPE line from the XML file before loading
   it into UPPAAL2k 3.2.1.

5. License Agreement
====================

Please read the license agreement carefully, fill in the form, and
send it to 

  Wang Yi
  Department of Computer Systems
  Uppsala University
  Box 325
  751 05 Uppsala, Sweden

The text of the agreement follows:
                                              
We (the licensee) understand that UPPAAL2k includes the programs:
uppaal2k.jar, uppaal2k, server, socketserver, atg2ugi,
atg2ta, atg2hs2ta, hs2ta, checkta, simta, verifyta, 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 UPPAAL2k. 

2. You neither have any responsibility for the correctness of systems
   verified using UPPAAL2k, nor for the correctness of UPPAAL2k itself.

3. We will never distribute or modify any part of the UPPAAL2k 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 UPPAAL2k for non-profit research purposes. This
   implies that neither UPPAAL2k 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 UPPAAL2k to us, we
agree that they will also fall under all of these terms.
