README revision f2702f0db4fab72edae97be5132f54c2a32a0283
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederThis README belongs to a "The heterogeneous tool set" (Hets) source
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian Maederrelease created by "make release" from the original svn repository.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederThe original svn sources can be obtained by:
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maedersvn co https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk Hets
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederInformation not contained here can be found in the Hets user guide
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder(doc/UserGuide.pdf) or on the Hets web page www.dfki.de/sks/hets.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederThe subject of this source release is to create a binary "hets" that
d8c71aacc9f1c8cd40a8ad8dcdad9be8854b849fChristian Maederis able to analyse heterogeneous and in particular CASL
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maederspecifications.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederThe sources need to be compiled using ghc Glasgow Haskell Compiler
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder(www.haskell.org/ghc) version 6.8.x or 6.10.x! Haskell as a logic is also
d27ad22f77ca7399742b54e9dce2cdceed12d5e0Christian Maedera part of Hets via "Programatica" (http://programatica.cs.pdx.edu/).
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederBeside output written to the console (stdout) or to files, hets can
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederdisplay graphs using "uDraw(Graph)", formerly "daVinci"
83394c6b6e6de128e71b67c9251ed7a84485d082Christian MaederAdditionally, in particular for the binding to uDrawGraph,
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maederthe sources of the uniform workbench are required:
c9acb8681bcc512245b4f0d1a9f2b189c60e10d4Christian Maederhttps://svn-agbkb.informatik.uni-bremen.de/uni/trunk
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederFor hets (and uni) to find "uDrawGraph", the environment variables UDG_HOME and
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederUNIDAVINCI must be set to the installation directory of uDraw(Graph) and to
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederthe actual executable, respectively.
2e2094a642e3775b0d76b890556407941d3a53b6Christian MaederSome dialogs depend on Gtk and Glade that require a couple of further
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maederlibraries. Mac users may consult
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederhttp://developer.imendio.com/projects/gtk-macosx/
c0c2380bced8159ff0297ece14eba948bd236471Christian MaederA typical call of hets is then: hets -g Basic/Numbers.casl
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederExample specifications can be found under:
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederhttps://svn-agbkb.informatik.uni-bremen.de/Hets-lib/trunk
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus LuettichFor proving Mac users may need to set HETS_ISABELLE, so that Isabelle finds
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maederexport HETS_ISABELLE="isabelle-interface -p \
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder '/Applications/Aquamacs\ Emacs.app/Contents/MacOS/Aquamacs\ Emacs'"
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian MaederFurther environment variables for provers are:
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder HETS_OWL_TOOLS
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian MaederIf you need to build the hets binary follow the instructions in
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian MaederINSTALL, alternatively try to get a binary or a complete installer from:
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederThe heterogeneous tool set (Hets) is mainly maintained by
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederChristian Maeder (Christian.Maeder@dfki.de) and
55adfe57a4de1f36adc3e3bfc16f342e44a7d444Christian MaederTill Mossakowski (Till.Mossakowski@dfki.de).
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederThe mailing list is hets-devel@informatik.uni-bremen.de.