README revision 87e1c83f10355e0fe80761367b75f83bc682770a
2295e38944bfcd91b9507e2fa9abe5a561817648Till MossakowskiThis README belongs to a Hets release (and does not apply to
2295e38944bfcd91b9507e2fa9abe5a561817648Till Mossakowskisources directly obtained via cvs).
87e1c83f10355e0fe80761367b75f83bc682770aTill MossakowskiInformation not contained here can be found in the Hets user guide
87e1c83f10355e0fe80761367b75f83bc682770aTill Mossakowski(doc/UserGuide.pdf) or on the Hets web page (www.tzi.de/cofi/hets).
39debaf3f18854486e9c5d21fecf3eb2630e5aa7Till MossakowskiThe subject of this release is a binary "hets" that is able to analyse
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederheterogeneous and in particular CASL specifications.
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederThe sources need to be compiled with ghc Glasgow Haskell Compiler
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederThe output of hets, if the input is successfully accepted, can be
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederdisplayed by "daVinci".
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederdaVinci is maintained by b-novative and b-novative holds all rights.
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederThis release may be accompanied with free binary releases of daVinci
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederVersion 2.1, but daVinci 2.1 is no longer supported or maintained!
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederHowever, you are encouraged to obtain the latest version of daVinci
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederPresenter (currently 3.0.5) from http://www.b-novative.com that is
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederfree for academic purposes.
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederLinux: the linux binary release of daVinci 2.1 relies on the old
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maedershlibs5 that must be installed on your system (if ./daVinci cannot be
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederfound/executed, then shlibs5 are missing)
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederSolaris: the solaris binary release of daVinci 2.1 should work without
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederMacintosh (Darwin): there is no release of daVinci for Macintosh, but
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederb-novative may have one in the mean time
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederFor best quality, get the latest version of daVinci from b-novative.
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederFor hets to find daVinci, the environment variables DAVINCIHOME and
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederUNIDAVINCI must be set to the installation directory of daVinci and to
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederthe actual executable, respectively.
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederexport DAVINCIHOME=<path>/daVinci_V2.1
ceee56b395227c495432d0f3baa407730d7a09d2Christian Maederexport UNIDAVINCI=<path>/daVinci_V2.1/daVinci
ceee56b395227c495432d0f3baa407730d7a09d2Christian MaederA typical call of hets is then: <path>/hets -g Basic/Numbers.casl
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederIf you need to rebuild the hets binary follow the instructions in INSTALL
f946026468db3a4a74f5f7651a86b22c58a708d1Christian Maeder(This README belongs a to release created by "make release", in case
f946026468db3a4a74f5f7651a86b22c58a708d1Christian Maederthat you obtained the HetCATS sources as CVS tree)
2295e38944bfcd91b9507e2fa9abe5a561817648Till MossakowskiThe heterogeneous tool set (Hets) is mainly maintained by
7b66a58641c3e6f6369c95d5bc16beaad20749a0Christian MaederChristian Maeder (maeder@tzi.de) and Till Mossakowski
7b66a58641c3e6f6369c95d5bc16beaad20749a0Christian Maeder(till@tzi.de). The mailing list is hets@tzi.de.
87e1c83f10355e0fe80761367b75f83bc682770aTill MossakowskiOverview of source modules, with maintainers:
87e1c83f10355e0fe80761367b75f83bc682770aTill MossakowskiFor more details, see the Haddock documentation in docs/
87e1c83f10355e0fe80761367b75f83bc682770aTill Mossakowski(after generation with "make doc")
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski--------------------------------------------------------
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiLICENCE.txt Licence information (english) (Till Mossakowski)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiLIZENZ.txt Licence information (german) (Till Mossakowski)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiINSTALL Installation and compilation instructions (???)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiMakefile GNU-Makefile to compile sources (Klaus Luettich)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiREADME This file (Till Mossakowski)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskihets.hs Top-level Haskell module for hets (Till Mossakowski)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskiversion_nr Current version (Till Mossakowski)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiATC/ Conversion from and to ATerms (Klaus Luettich)
00fb6704203f4de9f98434f9bca3543033fa07e1Till MossakowskiCASL/ Instance of Logic: CASL (Till Mossakowski/Christian Maeder/Martin Kuehl)
f946026468db3a4a74f5f7651a86b22c58a708d1Christian MaederCommon/ Modules common to all logics
888364a9d5168b06d67071ae0645997019af53c9Christian MaederCommon/ATerm/ Conversion from and to ATerms (Christian Maeder)
d59034af17352fe521c9cc2420f360ff9eda7033Christian MaederCommon/Lib/ Set, Map, Graph, Rel modules (Christian Maeder)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiCommon/Lib/Parsec/ Parsec combinator parser (Christian Maeder)
f5f33d4959160b579024d387d0235ed338341dc5Till MossakowskiCommon/PrettyPrint.hs pretty printing (Klaus Luettich)
f5f33d4959160b579024d387d0235ed338341dc5Till Mossakowski pretty printing should get an own directory
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiComorphisms/ Comorphisms of the logic graph (Till Mossakowski)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiCspCASL/ Instance of Logic: CspCASL (Markus Roggenbach)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskidoc/ Documentation (Till Mossakowski)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskidocs/ Haddock generated documentation (Klaus Luettich)
d59034af17352fe521c9cc2420f360ff9eda7033Christian Maederghc/ ghc-specific "coerce" (Christian Maeder)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiGUI/ GUI for displaying development graphs (Till Mossakowski/Jorina Gerken)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiHasCASL/ Instance of Logic: HasCASL (Christian Maeder)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiHaskell/ Instance of Logic: Haskell (Christian Maeder)
d59034af17352fe521c9cc2420f360ff9eda7033Christian MaederHaskell/Hatchet/ parsing, printing, analysis of Haskell
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskihetcats/ Command line interface (Klaus Luettich)
d59034af17352fe521c9cc2420f360ff9eda7033Christian Maederhugs/ hugs-specific "coerce" (Christian Maeder)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiIsabelle/ Instance of Logic: Isabelle
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiLogic/ Infrastructure for logic independence (Till Mossakowski)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiModal/ Instance of Logic: ModalCASL (Till Mossakowski)
00fb6704203f4de9f98434f9bca3543033fa07e1Till MossakowskiProofs/ Heterogeneous proof engine (Till Mossakowski/Jorina Gerken)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiStatic/ Heterogeneous development graphs and static analysis (Till Mossakowski/Maciek Makowski)
d59034af17352fe521c9cc2420f360ff9eda7033Christian MaederSyntax/ Heterogeneous syntax and parsing (Till Mossakowski, Christian Maeder)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiToHaskell/ translation to Haskell (Christian Maeder)
f946026468db3a4a74f5f7651a86b22c58a708d1Christian Maederutils/ Utilities
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskiutils/DrIFT-src/ DrIFT (for polytpyic conversion functions) (Klaus Luettich)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskiutils/GenerateRules/ generate files to be DRIFTed (Klaus Luettich)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskiutils/inlineAxioms parse inline axioms (Till Mossakowski)