README revision f2702f0db4fab72edae97be5132f54c2a32a0283
This README belongs to a "The heterogeneous tool set" (Hets) source
release created by "make release" from the original svn repository.
(for svn see http://subversion.tigris.org/)
The original svn sources can be obtained by:
Information not contained here can be found in the Hets user guide
(doc/UserGuide.pdf) or on the Hets web page www.dfki.de/sks/hets.
The subject of this source release is to create a binary "hets" that
is able to analyse heterogeneous and in particular CASL
specifications.
The sources need to be compiled using ghc Glasgow Haskell Compiler
a part of Hets via "Programatica" (http://programatica.cs.pdx.edu/).
Beside output written to the console (stdout) or to files, hets can
display graphs using "uDraw(Graph)", formerly "daVinci"
Additionally, in particular for the binding to uDrawGraph,
the sources of the uniform workbench are required:
For hets (and uni) to find "uDrawGraph", the environment variables UDG_HOME and
UNIDAVINCI must be set to the installation directory of uDraw(Graph) and to
the actual executable, respectively.
export UNIDAVINCI=$UDG_HOME/bin/uDrawGraph
Some dialogs depend on Gtk and Glade that require a couple of further
libraries. Mac users may consult
A typical call of hets is then: hets -g Basic/Numbers.casl
Example specifications can be found under:
For proving Mac users may need to set HETS_ISABELLE, so that Isabelle finds
Aquamacs.
export HETS_ISABELLE="isabelle-interface -p \
Further environment variables for provers are:
PELLET_PATH
HETS_OWL_TOOLS
HETS_APROVE
If you need to build the hets binary follow the instructions in
INSTALL, alternatively try to get a binary or a complete installer from:
The heterogeneous tool set (Hets) is mainly maintained by
Christian Maeder (Christian.Maeder@dfki.de) and
Till Mossakowski (Till.Mossakowski@dfki.de).
The mailing list is hets-devel@informatik.uni-bremen.de.