README revision 888364a9d5168b06d67071ae0645997019af53c9
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringThis README belongs to a Hets release (and does not apply to
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringsources directly obtained via cvs).
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringThe subject of this release is a binary "hets" that is able to analyse
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringheterogeneous and in particular CASL specifications.
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringThe sources need to be compiled with ghc Glasgow Haskell Compiler
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringThe output of hets, if the input is successfully accepted, can be
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringdisplayed by "daVinci".
5430f7f2bc7330f3088b894166bf3524a067e3d8Lennart PoetteringdaVinci is maintained by b-novative and b-novative holds all rights.
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringThis release may be accompanied with free binary releases of daVinci
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringVersion 2.1, but daVinci 2.1 is no longer supported or maintained!
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringHowever, you are encouraged to obtain the latest version of daVinci
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringPresenter (currently 3.0.5) from http://www.b-novative.com that is
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringfree for academic purposes.
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringLinux: the linux binary release of daVinci 2.1 relies on the old
5430f7f2bc7330f3088b894166bf3524a067e3d8Lennart Poetteringshlibs5 that must be installed on your system (if ./daVinci cannot be
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringfound/executed, then shlibs5 are missing)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringSolaris: the solaris binary release of daVinci 2.1 should work without
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringMacintosh (Darwin): there is no release of daVinci for Macintosh, but
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringb-novative may have one in the mean time
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringFor best quality, get the latest version of daVinci from b-novative.
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringFor hets to find daVinci, the environment variables DAVINCIHOME and
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringUNIDAVINCI must be set to the installation directory of daVinci and to
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringthe actual executable, respectively.
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringexport DAVINCIHOME=<path>/daVinci_V2.1
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringexport UNIDAVINCI=<path>/daVinci_V2.1/daVinci
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringA typical call of hets is then: <path>/hets -g Basic/Numbers.casl
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringIf you need to rebuild the hets binary follow the instructions in INSTALL
160cd5c9aa2301892e13950015de7968c764340dLennart Poettering(This README belongs a to release created by "make release", in case
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringthat you obtained the HetCATS sources as CVS tree)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringThe heterogeneous tool set (Hets) is mainly maintained by
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringChristian Maeder (maeder@tzi.de) and Till Mossakowski
160cd5c9aa2301892e13950015de7968c764340dLennart Poettering(till@tzi.de). The mailing list is hets@tzi.de.
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringSources with maintainers:
160cd5c9aa2301892e13950015de7968c764340dLennart Poettering--------------------------------------------------------
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringLICENCE.txt Licence information (english) (Till Mossakowski)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringLIZENZ.txt Licence information (german) (Till Mossakowski)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringINSTALL Installation and compilation instructions (???)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringMakefile GNU-Makefile to compile sources (Klaus Luettich)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringREADME This file (Till Mossakowski)
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringhets.hs Top-level Haskell module for hets (Till Mossakowski)
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringversion_nr Current version (Till Mossakowski)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringATC/ Conversion from and to ATerms (Klaus Luettich)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringCASL/ Instance of Logic: CASL (Till Mossakowski/Christian Maeder/Martin Kuehl)
af3bccd6d87759f0b146bf5980bdd56144d70c7eLennart PoetteringCommon/ Modules common to all logics
af3bccd6d87759f0b146bf5980bdd56144d70c7eLennart PoetteringCommon/ATerm/ Conversion from and to ATerms (Christian Maeder)
af3bccd6d87759f0b146bf5980bdd56144d70c7eLennart PoetteringCommon/Lib/ Set, Map, Graph, Rel modules (Christian Maeder)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringCommon/Lib/Parsec/ Parsec combinator parser (Christian Maeder)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringCommon/PrettyPrint.hs pretty printing (Klaus Luettich)
160cd5c9aa2301892e13950015de7968c764340dLennart Poettering pretty printing should get an own directory
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringComorphisms/ Comorphisms of the logic graph (Till Mossakowski)
af62c704053b5d34672497eb5bdc4764ebbb5f4fKay SieversCspCASL/ Instance of Logic: CspCASL (Markus Roggenbach)
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringdoc/ Documentation (Till Mossakowski)
bb29785e0df6a7cf07db0259a60bc1f3b4814cb4Lennart Poetteringdocs/ Haddock generated documentation (Klaus Luettich)
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringghc/ ghc-specific "coerce" (Christian Maeder)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringGUI/ GUI for displaying development graphs (Till Mossakowski/Jorina Gerken)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringHasCASL/ Instance of Logic: HasCASL (Christian Maeder)
c36eecdfcb4afa09850002fbb81a95a24ffde599Lennart PoetteringHaskell/ Instance of Logic: Haskell (Christian Maeder)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringHaskell/Hatchet/ parsing, printing, analysis of Haskell
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringhetcats/ Command line interface (Klaus Luettich)
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringhugs/ hugs-specific "coerce" (Christian Maeder)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringIsabelle/ Instance of Logic: Isabelle
af62c704053b5d34672497eb5bdc4764ebbb5f4fKay SieversLogic/ Infrastructure for logic independence (Till Mossakowski)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringModal/ Instance of Logic: ModalCASL (Till Mossakowski)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringProofs/ Heterogeneous proof engine (Till Mossakowski/Jorina Gerken)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringStatic/ Heterogeneous development graphs and static analysis (Till Mossakowski/Maciek Makowski)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringSyntax/ Heterogeneous syntax and parsing (Till Mossakowski, Christian Maeder)
160cd5c9aa2301892e13950015de7968c764340dLennart PoetteringToHaskell/ translation to Haskell (Christian Maeder)
160cd5c9aa2301892e13950015de7968c764340dLennart Poettering should be moved to Comorphisms
c36eecdfcb4afa09850002fbb81a95a24ffde599Lennart Poetteringutils/ Utilities
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringutils/DrIFT-src/ DrIFT (for polytpyic conversion functions) (Klaus Luettich)
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringutils/GenerateRules/ generate files to be DRIFTed (Klaus Luettich)
160cd5c9aa2301892e13950015de7968c764340dLennart Poetteringutils/inlineAxioms parse inline axioms (Till Mossakowski)