# Copyright 1999-2005 Gentoo Foundation
# Distributed under the terms of the GNU General Public License v2
# $Header: $

inherit eutils

MY_PV="426"
MY_XSPIN_PV="4.2"

S=${WORKDIR}/Spin

DESCRIPTION="Tool for formal verification of distributed software systems"
HOMEPAGE="http://spinroot.com/"
SRC_URI="http://spinroot.com/spin/Src/spin${MY_PV}.tar.gz"

LICENSE="spin"
SLOT="0"
KEYWORDS="~x86"
IUSE="X graphviz" # xspin can use dot to produce prettier graphs

RDEPEND="X? ( dev-lang/tcl
		dev-lang/tk
		graphviz? ( media-gfx/graphviz ) )
		sys-devel/gcc"
DEPEND="dev-util/yacc
		${RDEPEND}"

src_unpack() {
	unpack ${A}

	# correct path to wish
	use X && epatch ${FILESDIR}/${P}-xspin_wish_path.patch
	use X && epatch ${FILESDIR}/${P}-xspin_time_not_found.patch
}

src_compile() {
	cd Src${PV}
	emake || die "Error: emake failed!"
}

src_install() {
	dobin Src${PV}/${PN}
	doman Man/*.1
	dodoc Doc/* README.html

	use X && dobin Xspin${MY_XSPIN_PV}/xspin${MY_PV}.tcl
	use X && dosym /usr/bin/xspin${MY_PV}.tcl /usr/bin/xspin
}

pkg_postinst() {
	einfo "Spin is distributed in source form to encourage research in formal"
	einfo "verification, and to help a support friendly and open exchange of"
	einfo "algorithms, ideas, and tools. The software itself has a copyright"
	einfo "from Lucent Technologies and Bell Laboratories, and is distributed"
	einfo "for research and educational purposes only (i.e., no guarantee of"
	einfo "any kind is implied by the distribution of the code, and all rights"
	einfo "are reserved by the copyright holder). For this general use of"
	einfo "Spin, no license is required."
	einfo
	einfo "Commercial application of the Spin software is also allowed, but"
	einfo "requires the acceptance of a basic license. Refer to the Spin"
	einfo "Public license for details."
	einfo
	einfo "(see /usr/portage/licenses/spin)"
}