This README belongs to a Hets release (and does not apply to

sources directly obtained via cvs).

The subject of this release is a binary "hets" that is able to analyse

heterogeneous and in particular CASL specifications.

The output of hets, if the input is successfully accepted, can be

displayed by "daVinci".

SYSTEM requirements:

- A Linux, Solaris or Macintosh OS-X machine with 64 MB RAM

- Tcl/Tk

- daVinci (comes with this distribution)

daVinci is maintained by b-novative and b-novative holds all rights.

This release may be accompanied with free binary releases of daVinci

Version 2.1, but daVinci 2.1 is no longer supported or maintained!

However, you are encouraged to obtain the latest version of daVinci

Presenter (currently 3.0.5) from http://www.b-novative.com that is

free for academic purposes.

Linux: the linux binary release of daVinci 2.1 relies on the old

shlibs5 that must be installed on your system (if ./daVinci cannot be

found/executed, then shlibs5 are missing)

Solaris: the solaris binary release of daVinci 2.1 should work without

problems

Macintosh (Darwin): there is no release of daVinci for Macintosh, but

b-novative may have one in the mean time

For best quality, get the latest version of daVinci from b-novative.

INSTALLATION:

You can either copy the folder Hets to your local file system,

or directly start from the CD-ROM.

For hets to find daVinci, the environment variables DAVINCIHOME and

UNIDAVINCI must be set to the installation directory of daVinci and to

the actual executable, respectively.

export DAVINCIHOME=<path>/daVinci_V2.1

export UNIDAVINCI=<path>/daVinci_V2.1/daVinci

A typical call of hets is then: <path>/hets -g Basic/Numbers.casl

HETS SOURCES:

If you need to rebuild the hets binary follow the instructions in INSTALL.

The sources need to be compiled with ghc Glasgow Haskell Compiler

(www.haskell.org/ghc).

The heterogeneous tool set (Hets) is mainly maintained by

Christian Maeder (maeder@tzi.de) and Till Mossakowski

(till@tzi.de). The mailing list is hets@tzi.de.

Files in the Tools/Hets/src directory:

--------------------------------------

README This file

hets Hets binary

UserGuide.ps Hets documentaion

docs/ Overview and index for Hets sources

src/ Hets sources

src/ATC/ Conversion from and to ATerms (specific)

src/ATC/doc/ documentation

src/aterm_conv/ ATerm Conversion

src/CASL/ Instance of Logic: CASL

src/CASL/doc/ documentation

src/CASL/test/ test examples

src/Common/ Modules common to all logics

src/Common/ATerm/ Conversion from and to ATerms (general)

src/Common/doc/ Documentation

src/Common/Lib/ Third-party modules

src/Common/Lib/Graph/ Functional Graph Library

src/Common/Lib/Parsec/ Parsec combinator parser

src/Common/test/ Text examples

src/Comorphisms/ Comorphisms of the logic graph

src/CspCASL/ Instance of Logic: CspCASL

src/CspCASL/Doku/ documentation

src/docs/ Haddock documentation

src/ghc/ Some ghc-specific stuff

src/GUI/ GUI for displaying development graphs

src/HasCASL/ Instance of Logic: HasCASL

src/HasCASL/doc/ documentation

src/HasCASL/test/ text examples

src/Haskell/ Instance of Logic: Haskell

src/Haskell/Hatchet/ Static anaylsis of Haskell

src/Haskell/Language/ Haskell syntax in Haskell

src/Haskell/Language/Haskell/

src/haterm-1.0/ ATerm Conversion

src/haterm-1.0/ac-macros/

src/haterm-1.0/src/

src/hetcats/ Command line interface

src/hugs/ Some hugs-specific stuff

src/Logic/ Infrastructure for logic independence

src/mini/ Some toy version of Hets, used in a paper

src/Modal/ Instance of logic: modal logic

src/parsec/ ??

src/pretty/ ??

src/Proofs/ Heterogeneous proof engine

src/Static/ Heterogeneous development graphs and static analysis

src/Syntax/ Heterogeneous syntax and parsing

src/test/ Text examples

src/ToHaskell/ Translation from HasCASL to Haskell

src/utils/ Utilities

src/utils/AG-src/ Static analyser generator (not used by Hets)

src/utils/DrIFT-src/ DrIFT (for polytpyic conversion functions)

src/utils/GenerateRules/

src/utils/hd-lib/