Skip to content

spechub/Hets

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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:
svn co https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk Hets

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
(www.haskell.org/ghc) version 6.8.x or 6.10.x! Haskell as a logic is also
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"
(www.informatik.uni-bremen.de/uDrawGraph)

Additionally, in particular for the binding to uDrawGraph,
the sources of the uniform workbench are required:
https://svn-agbkb.informatik.uni-bremen.de/uni/trunk

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
http://developer.imendio.com/projects/gtk-macosx/

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

Example specifications can be found under:
https://svn-agbkb.informatik.uni-bremen.de/Hets-lib/trunk

For proving Mac users may need to set HETS_ISABELLE, so that Isabelle finds
Aquamacs.

export HETS_ISABELLE="isabelle-interface -p \
  '/Applications/Aquamacs\ Emacs.app/Contents/MacOS/Aquamacs\ Emacs'"

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:
www.dfki.de/sks/hets/installation_e.htm

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.