Initial import of spin version 5.2.5 into the Packages Collection.

	To verify a design, a formal model is built using PROMELA, Spin's
	input language.  PROMELA is a non-deterministic language, loosely
	based on Dijkstra's guarded command language notation and borrowing
	the notation for I/O operations from Hoare's CSP language.

	Spin can be used in four main modes:

	1.  as a simulator, allowing for rapid prototyping with a random,
	guided, or interactive simulations

	2.  as an exhaustive verifier, capable of rigorously proving the
	validity of user specified correctness requirements (using partial
	order reduction theory to optimize the search)

	3.  as proof approximation system that can validate even very large
	system models with maximal coverage of the state space.

	4.  as a driver for swarm verification (a new form of swarm
	computing), which can make optimal use of large numbers of available
	compute cores to leverage parallelism and search diversification
	techniques, which increases the chance of locating defects in very
	large verification models.

With thanks to the plan9 guys for the nudge

4 files changed, 54 insertions, 0 deletions

diff --git a/devel/spin/DESCR b/devel/spin/DESCR
new file mode 100644
index 00000000000..94fd7dd83f3
--- /dev/null
+++ b/devel/spin/DESCR
@@ -0,0 +1,22 @@
+To verify a design, a formal model is built using PROMELA, Spin's
+input language.  PROMELA is a non-deterministic language, loosely
+based on Dijkstra's guarded command language notation and borrowing
+the notation for I/O operations from Hoare's CSP language.
+
+Spin can be used in four main modes:
+
+1.  as a simulator, allowing for rapid prototyping with a random,
+guided, or interactive simulations
+
+2.  as an exhaustive verifier, capable of rigorously proving the
+validity of user specified correctness requirements (using partial
+order reduction theory to optimize the search)
+
+3.  as proof approximation system that can validate even very large
+system models with maximal coverage of the state space.
+
+4.  as a driver for swarm verification (a new form of swarm
+computing), which can make optimal use of large numbers of available
+compute cores to leverage parallelism and search diversification
+techniques, which increases the chance of locating defects in very
+large verification models.
diff --git a/devel/spin/Makefile b/devel/spin/Makefile
new file mode 100644
index 00000000000..39c5534a105
--- /dev/null
+++ b/devel/spin/Makefile
@@ -0,0 +1,24 @@
+# $NetBSD: Makefile,v 1.1.1.1 2010/10/24 18:54:12 agc Exp $
+
+DISTNAME=	spin525
+PKGNAME=	spin-5.2.5
+CATEGORIES=	devel
+MASTER_SITES=	http://spinroot.com/spin/Src/
+
+MAINTAINER=	agc@NetBSD.org
+HOMEPAGE=	http://spinroot.com/spin/whatispin.html
+COMMENT=	Formal correctness prover
+LICENSE=	spin-license
+
+PKG_DESTDIR_SUPPORT=	user-destdir
+INSTALLATION_DIRS=	bin ${PKGMANDIR}/man1
+
+WRKSRC=		${WRKDIR}/Spin/Src5.2.5
+MAKE_FILE=	makefile
+BUILD_TARGET=	spin
+
+do-install:
+	${INSTALL_PROGRAM} ${WRKSRC}/spin ${DESTDIR}${PREFIX}/bin/spin
+	${INSTALL_MAN} ${WRKDIR}/Spin/Man/spin.1 ${DESTDIR}${PREFIX}/${PKGMANDIR}/man1/spin.1
+
+.include "../../mk/bsd.pkg.mk"
diff --git a/devel/spin/PLIST b/devel/spin/PLIST
new file mode 100644
index 00000000000..a2d9c84ef4b
--- /dev/null
+++ b/devel/spin/PLIST
@@ -0,0 +1,3 @@
+@comment $NetBSD: PLIST,v 1.1.1.1 2010/10/24 18:54:12 agc Exp $
+bin/spin
+${PKGMANDIR}/man1/spin.1
diff --git a/devel/spin/distinfo b/devel/spin/distinfo
new file mode 100644
index 00000000000..0e4b8803b7e
--- /dev/null
+++ b/devel/spin/distinfo
@@ -0,0 +1,5 @@
+$NetBSD: distinfo,v 1.1.1.1 2010/10/24 18:54:12 agc Exp $
+
+SHA1 (spin525.tar.gz) = 274649628c0c8ae3414b863c27a1b8d98a8e9921
+RMD160 (spin525.tar.gz) = 8d01f8dd0da8c8013fbb8c6d6e9a8c40b8c5f33f
+Size (spin525.tar.gz) = 413406 bytes