README revision 87e1c83f10355e0fe80761367b75f83bc682770a
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederThis README belongs to a Hets release (and does not apply to
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian Maedersources directly obtained via cvs).
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederInformation not contained here can be found in the Hets user guide
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder(doc/UserGuide.pdf) or on the Hets web page (www.tzi.de/cofi/hets).
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederThe subject of this release is a binary "hets" that is able to analyse
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederheterogeneous and in particular CASL specifications.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederThe sources need to be compiled with ghc Glasgow Haskell Compiler
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederThe output of hets, if the input is successfully accepted, can be
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederdisplayed by "daVinci".
d03ce8efc673309b40746bf5f66299cc3cefa3b0Klaus LuettichdaVinci is maintained by b-novative and b-novative holds all rights.
8e494181dee5cfc59ae494e4082c71edfde24f58Christian MaederThis release may be accompanied with free binary releases of daVinci
b7839add0728fef3cbb28244373661db382f6588Christian MaederVersion 2.1, but daVinci 2.1 is no longer supported or maintained!
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till MossakowskiHowever, you are encouraged to obtain the latest version of daVinci
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian MaederPresenter (currently 3.0.5) from http://www.b-novative.com that is
760ae19a92dde8249679a674f93f58d26a7c5f6bChristian Maederfree for academic purposes.
88c800932dd7053322501ea2039d9f234be6866cKlaus LuettichLinux: the linux binary release of daVinci 2.1 relies on the old
c0c2380bced8159ff0297ece14eba948bd236471Christian Maedershlibs5 that must be installed on your system (if ./daVinci cannot be
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederfound/executed, then shlibs5 are missing)
c0c2380bced8159ff0297ece14eba948bd236471Christian MaederSolaris: the solaris binary release of daVinci 2.1 should work without
8410667510a76409aca9bb24ff0eda0420088274Christian MaederMacintosh (Darwin): there is no release of daVinci for Macintosh, but
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettichb-novative may have one in the mean time
3474624438293363cada4e49225aae1e292fa597Christian MaederFor best quality, get the latest version of daVinci from b-novative.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederFor hets to find daVinci, the environment variables DAVINCIHOME and
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederUNIDAVINCI must be set to the installation directory of daVinci and to
d67a33b40578beef2e255a274f89bb9c34aaf056Christian Maederthe actual executable, respectively.
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maederexport DAVINCIHOME=<path>/daVinci_V2.1
c72c1e75a969ff4c336e77481c2a8e42603f13eeChristian Maederexport UNIDAVINCI=<path>/daVinci_V2.1/daVinci
6e049108aa87dc46bcff96fae50a4625df1d9648Klaus LuettichA typical call of hets is then: <path>/hets -g Basic/Numbers.casl
5d44c8cecd07b47ce537c7e14bf7b41a39f08507Christian MaederIf you need to rebuild the hets binary follow the instructions in INSTALL
5d44c8cecd07b47ce537c7e14bf7b41a39f08507Christian Maeder(This README belongs a to release created by "make release", in case
c6fcd42c6d6d9dae8c7835c24fcb7ce8531a9050Christian Maederthat you obtained the HetCATS sources as CVS tree)
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till MossakowskiThe heterogeneous tool set (Hets) is mainly maintained by
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus LuettichChristian Maeder (maeder@tzi.de) and Till Mossakowski
7b2177999334c920c5669621bd3c142fe198a8d7Christian Maeder(till@tzi.de). The mailing list is hets@tzi.de.
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederOverview of source modules, with maintainers:
d3ae0072823e2ef0d41d4431fcc768e66489c20eChristian MaederFor more details, see the Haddock documentation in docs/
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder(after generation with "make doc")
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich--------------------------------------------------------
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederLICENCE.txt Licence information (english) (Till Mossakowski)
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederLIZENZ.txt Licence information (german) (Till Mossakowski)
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederINSTALL Installation and compilation instructions (???)
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederMakefile GNU-Makefile to compile sources (Klaus Luettich)
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederREADME This file (Till Mossakowski)
9e748851c150e1022fb952bab3315e869aaf0214Christian Maederhets.hs Top-level Haskell module for hets (Till Mossakowski)
9e748851c150e1022fb952bab3315e869aaf0214Christian Maederversion_nr Current version (Till Mossakowski)
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederATC/ Conversion from and to ATerms (Klaus Luettich)
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederCASL/ Instance of Logic: CASL (Till Mossakowski/Christian Maeder/Martin Kuehl)
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederCommon/ Modules common to all logics
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederCommon/ATerm/ Conversion from and to ATerms (Christian Maeder)
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederCommon/Lib/ Set, Map, Graph, Rel modules (Christian Maeder)
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederCommon/Lib/Parsec/ Parsec combinator parser (Christian Maeder)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederCommon/PrettyPrint.hs pretty printing (Klaus Luettich)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder pretty printing should get an own directory
c0c2380bced8159ff0297ece14eba948bd236471Christian MaederComorphisms/ Comorphisms of the logic graph (Till Mossakowski)
5d44c8cecd07b47ce537c7e14bf7b41a39f08507Christian MaederCspCASL/ Instance of Logic: CspCASL (Markus Roggenbach)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederdoc/ Documentation (Till Mossakowski)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederdocs/ Haddock generated documentation (Klaus Luettich)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederghc/ ghc-specific "coerce" (Christian Maeder)
c0c2380bced8159ff0297ece14eba948bd236471Christian MaederGUI/ GUI for displaying development graphs (Till Mossakowski/Jorina Gerken)
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederHasCASL/ Instance of Logic: HasCASL (Christian Maeder)
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederHaskell/ Instance of Logic: Haskell (Christian Maeder)
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederHaskell/Hatchet/ parsing, printing, analysis of Haskell
9e748851c150e1022fb952bab3315e869aaf0214Christian Maederhetcats/ Command line interface (Klaus Luettich)
9e748851c150e1022fb952bab3315e869aaf0214Christian Maederhugs/ hugs-specific "coerce" (Christian Maeder)
c0c2380bced8159ff0297ece14eba948bd236471Christian MaederIsabelle/ Instance of Logic: Isabelle
549b97cfbe3a6687db74440a550b68b2fc19a272Christian MaederLogic/ Infrastructure for logic independence (Till Mossakowski)
549b97cfbe3a6687db74440a550b68b2fc19a272Christian MaederModal/ Instance of Logic: ModalCASL (Till Mossakowski)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederProofs/ Heterogeneous proof engine (Till Mossakowski/Jorina Gerken)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederStatic/ Heterogeneous development graphs and static analysis (Till Mossakowski/Maciek Makowski)
c0c2380bced8159ff0297ece14eba948bd236471Christian MaederSyntax/ Heterogeneous syntax and parsing (Till Mossakowski, Christian Maeder)
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus LuettichToHaskell/ translation to Haskell (Christian Maeder)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederutils/ Utilities
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederutils/DrIFT-src/ DrIFT (for polytpyic conversion functions) (Klaus Luettich)
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettichutils/GenerateRules/ generate files to be DRIFTed (Klaus Luettich)
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettichutils/inlineAxioms parse inline axioms (Till Mossakowski)