README revision e472118997ef12138109ffa93a265292c5d20a6c
5f184698e58f31e670c54c12d858a7c7322277b4Christian MaederThis README belongs to a "The heterogeneous tool set" (Hets) source
5f184698e58f31e670c54c12d858a7c7322277b4Christian Maederrelease created by "make release" from the original svn repository.
5f184698e58f31e670c54c12d858a7c7322277b4Christian MaederThe original svn sources can be obtained by:
5f184698e58f31e670c54c12d858a7c7322277b4Christian Maedersvn co https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk Hets
87e1c83f10355e0fe80761367b75f83bc682770aTill MossakowskiInformation not contained here can be found in the Hets user guide
5f184698e58f31e670c54c12d858a7c7322277b4Christian Maeder(doc/UserGuide.pdf) or on the Hets web page www.dfki.de/sks/hets.
5f184698e58f31e670c54c12d858a7c7322277b4Christian MaederThe subject of this source release is to create a binary "hets" that
5f184698e58f31e670c54c12d858a7c7322277b4Christian Maederis able to analyse heterogeneous and in particular CASL
5f184698e58f31e670c54c12d858a7c7322277b4Christian Maederspecifications.
5f184698e58f31e670c54c12d858a7c7322277b4Christian MaederThe sources need to be compiled using ghc Glasgow Haskell Compiler
e472118997ef12138109ffa93a265292c5d20a6cChristian Maeder(www.haskell.org/ghc) version 6.10.x! Haskell as a logic is also
947d21ed43ec33fac7c3772470d984479ee5f64aChristian Maedera part of Hets via "Programatica" (http://programatica.cs.pdx.edu/).
5f184698e58f31e670c54c12d858a7c7322277b4Christian MaederBeside output written to the console (stdout) or to files, hets can
c68c8248d86d5bea90acaff0433ff5ab8dee0b11Christian Maederdisplay graphs using "uDraw(Graph)", formerly "daVinci"
5f184698e58f31e670c54c12d858a7c7322277b4Christian MaederAdditionally, in particular for the binding to uDrawGraph,
5f184698e58f31e670c54c12d858a7c7322277b4Christian Maederthe sources of the uniform workbench are required:
5f184698e58f31e670c54c12d858a7c7322277b4Christian Maederhttps://svn-agbkb.informatik.uni-bremen.de/uni/trunk
5f184698e58f31e670c54c12d858a7c7322277b4Christian MaederFor hets (and uni) to find "uDrawGraph", the environment variables UDG_HOME and
e472118997ef12138109ffa93a265292c5d20a6cChristian MaederUNIDAVINCI may be set to the installation directory of uDraw(Graph) and to
c68c8248d86d5bea90acaff0433ff5ab8dee0b11Christian Maederthe actual executable, respectively.
947d21ed43ec33fac7c3772470d984479ee5f64aChristian MaederSome dialogs depend on Gtk and Glade that require a couple of further
e472118997ef12138109ffa93a265292c5d20a6cChristian Maederlibraries. Mac users are expected to install gtk2-framework.dmg from
e472118997ef12138109ffa93a265292c5d20a6cChristian Maederhttp://www.dfki.de/sks/hets/intel-mac/gtk2-framework.dmg
f63a335a037098b08817e7137087d42240be74c1Christian MaederA typical call of hets is then: hets -g Basic/Numbers.casl
5f184698e58f31e670c54c12d858a7c7322277b4Christian MaederExample specifications can be found under:
5f184698e58f31e670c54c12d858a7c7322277b4Christian Maederhttps://svn-agbkb.informatik.uni-bremen.de/Hets-lib/trunk
e472118997ef12138109ffa93a265292c5d20a6cChristian MaederFor proving users may set HETS_ISABELLE, if "isabelle emacs" is not the right
e472118997ef12138109ffa93a265292c5d20a6cChristian Maedercall for their system. Only Isabelle version 2009-1 is supported.
f2702f0db4fab72edae97be5132f54c2a32a0283Christian MaederFurther environment variables for provers are:
f2702f0db4fab72edae97be5132f54c2a32a0283Christian Maeder HETS_OWL_TOOLS
5f184698e58f31e670c54c12d858a7c7322277b4Christian MaederIf you need to build the hets binary follow the instructions in
5f184698e58f31e670c54c12d858a7c7322277b4Christian MaederINSTALL, alternatively try to get a binary or a complete installer from:
2295e38944bfcd91b9507e2fa9abe5a561817648Till MossakowskiThe heterogeneous tool set (Hets) is mainly maintained by
5f184698e58f31e670c54c12d858a7c7322277b4Christian MaederChristian Maeder (Christian.Maeder@dfki.de) and
5f184698e58f31e670c54c12d858a7c7322277b4Christian MaederTill Mossakowski (Till.Mossakowski@dfki.de).
c68c8248d86d5bea90acaff0433ff5ab8dee0b11Christian MaederThe mailing list is hets-devel@informatik.uni-bremen.de.