This CD contains the DisCo Toolset for animating DisCo specifications.
Latest version and further documentation can be downloaded
from 'http://disco.cs.tut.fi/'. Bug reports can be filed through
'http://disco.cs.tut.fi/bugreport/'.

Three platforms are supported: Solaris, Linux and Windows.
The tools require Java 2 SDK version 1.3 which can be downloaded from
'http://java.sun.com/'.

Installing the tools in Windows
  Create a directory (e.g. C:\disco) for the tools.
  Copy windows/disco-0.9-win.zip into the created directory.
  Unpack disco-0.9-win.zip.
  Copy file 'DisCoAnimator' to your home directory as '.DisCoAnimator'
  (notice dot at the beginning).
  Note: You should either have a path to DisCo compiler (discoc) in your
  environment variable PATH or you should edit '.DisCoAnimator' to
  reflect the absolute path to discoc.
  Append the created directory (e.g. C:\disco) into 
  your environment variable CLASSPATH.
  Then DisCo animator is started by applying the command 'bin/disco' in the
  created directory.

Sometimes there are problems with opening specifications with windows.
In such a case add path to the directory where the DisCo specification
being opened is located to CLASSPATH and try again.


List of the features that are not properly implemented in DisCo compiler are
given below. Numbers refer to the language definition.

3.1.5: Subobjects are not implemented.
3.2.3: Nondeterministic operators are deterministic.
3.2.6: Local assertions for records.
3.2.8: See 3.2.3.
3.2.17 See 3.2.8.
3.2.21: See 3.2.8.
3.2.26: See 3.2.8.
3.4.2: The value of a base type cannot be assigned to a derived type.
3.6.4: Subobjects are not implemented.
3.6.5: Shadow mechanism is not implemented.
3.7.1: No local assertrions for type definitions.
3.7.2: See 3.7.1.
3.7.3: See 3.7.1.

4.0.1: The structure of a class cannot be given corresponding record.
4.1.2: See 3.1.5.
4.1.2: See 3.1.5.
4.1.3: See 3.1.5.
4.2.6: See 3.6.5.
4.2.7: See 3.6.5.

5.1.3: Quantified roles are not implemented.
5.1.4: Quantifiers can refer alse other objects than participants.
5.1.5: More than one optional parts for set or sequence membership tests
       are allowed.
5.2.5: See 5.1.3.
5.5.4

6.2.4: See 5.1.3.
6.5.2: See 5.1.3.
6.5.3: Compiler utilizes traditional static typing.
6.5.8: See 5.1.3.
6.6.2: See 5.1.3.
6.7.3: See 5.1.3.
6.8.3: Negative values are not treated as zeros.
6.9.4: See 5.1.3.
6.10.2: Parameters cannot be omitted.
6.10.9: See 6.10.2.
6.10.14: See 3.1.5.
6.10.15: See 3.6.5.
6.10.16
6.10.17
6.10.20: Replacements are not implemented.
6.10.26: See 3.6.5.
6.11.4: See 3.6.5.
6.11.6
6.11.9: See 6.10.20.

7.1.3: Base/derived difference is allowed to be the only difference.

8.1.7
8.4.3: Concatenation is not implemented.
8.4.4