README revision f2702f0db4fab72edae97be5132f54c2a32a0283
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
f2702f0db4fab72edae97be5132f54c2a32a0283Christian Maeder(www.haskell.org/ghc) version 6.8.x or 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
f63a335a037098b08817e7137087d42240be74c1Christian MaederUNIDAVINCI must 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
947d21ed43ec33fac7c3772470d984479ee5f64aChristian Maederlibraries. Mac users may consult
947d21ed43ec33fac7c3772470d984479ee5f64aChristian Maederhttp://developer.imendio.com/projects/gtk-macosx/
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
947d21ed43ec33fac7c3772470d984479ee5f64aChristian MaederFor proving Mac users may need to set HETS_ISABELLE, so that Isabelle finds
947d21ed43ec33fac7c3772470d984479ee5f64aChristian Maederexport HETS_ISABELLE="isabelle-interface -p \
f2702f0db4fab72edae97be5132f54c2a32a0283Christian Maeder '/Applications/Aquamacs\ Emacs.app/Contents/MacOS/Aquamacs\ Emacs'"
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.