Import of math spin:

Spin is an efficient on-the-fly verification system
(a `model checker') for asynchronous concurrent systems,
such as data communication protocols, distributed operating
systems, database systems, etc.
It can be used to prove both safety and liveness properties,
including all correctness requirements expressible in linear
time temporal logic.

PR:		ports/9058
Submitted by:	pangolin@home.com

6 files changed, 191 insertions, 0 deletions

diff --git a/devel/spin/Makefile b/devel/spin/Makefile
new file mode 100644
index 00000000000..9a99c165d6e
--- /dev/null
+++ b/devel/spin/Makefile
@@ -0,0 +1,50 @@
+# Ports collection makefile for: spin
+# Version required:	3.23
+# Date created:		Oct 23, 1997
+# Whom:			jhanna@home.com
+#
+# $Id$
+#
+
+DISTNAME=	spin-3.23
+CATEGORIES=	math
+MASTER_SITES=	ftp://netlib.bell-labs.com/netlib/spin/ \
+		ftp://www.netlib.org/spin/ \
+		ftp://www.enseeiht.fr/NetLib/spin/ \
+		ftp://wcarchive.cdrom.com/netlib/spin/
+DISTFILES=	spin323.tar.gz html.tar.gz
+
+MAINTAINER=	jhanna@home.com
+
+DIST_SUBDIR=	spin
+WRKSRC=		${WRKDIR}/Src3.2
+MAKEFILE=	makefile
+ALL_TARGET=	spin
+
+post-extract:
+	@cd ${WRKDIR}/Test && ${SH} ${WRKDIR}/Test/examples
+
+pre-build:
+	cd ${WRKSRC} && ${MAKE} clean
+
+do-install:
+	${INSTALL_PROGRAM} ${WRKSRC}/spin ${PREFIX}/bin
+	${INSTALL_SCRIPT} ${WRKDIR}/Xspin3.2/xspin323.tcl ${PREFIX}/bin
+	${RM} -f ${PREFIX}/bin/xspin
+	ln -s ${PREFIX}/bin/xspin323.tcl ${PREFIX}/bin/xspin
+
+.if !defined(NOPORTDOCS)
+	${MKDIR} ${PREFIX}/share/doc/spin/Doc
+	${MKDIR} ${PREFIX}/share/doc/spin/Examples
+	${MKDIR} ${PREFIX}/share/doc/spin/HTML
+	${MKDIR} ${PREFIX}/share/doc/spin/Test
+	${INSTALL_DATA} ${WRKDIR}/Doc/* ${PREFIX}/share/doc/spin/Doc
+	${INSTALL_DATA} ${WRKDIR}/Test/ex.* ${PREFIX}/share/doc/spin/Examples
+	${INSTALL_DATA} ${WRKDIR}/HTML/* ${PREFIX}/share/doc/spin/HTML
+.for i in README.tests erathostenes hello leader leader2 loops pftp \
+	priorities snoopy sort
+	${INSTALL_DATA} ${WRKDIR}/Test/$i ${PREFIX}/share/doc/spin/Test
+.endfor
+.endif
+
+.include <bsd.port.mk>
diff --git a/devel/spin/distinfo b/devel/spin/distinfo
new file mode 100644
index 00000000000..7e4aaee4489
--- /dev/null
+++ b/devel/spin/distinfo
@@ -0,0 +1,2 @@
+MD5 (spin/spin323.tar.gz) = 1ac5fffa78663ba13658ba0c3bce3419
+MD5 (spin/html.tar.gz) = 2988743b1d9db59aff4ddd999573d6b3
diff --git a/devel/spin/files/patch-aa b/devel/spin/files/patch-aa
new file mode 100644
index 00000000000..430dbe1fd18
--- /dev/null
+++ b/devel/spin/files/patch-aa
@@ -0,0 +1,8 @@
+--- ../Xspin3.2/xspin323.tcl.orig	Wed Dec 17 10:11:57 1997
++++ ../Xspin3.2/xspin323.tcl	Sun Dec 21 13:20:41 1997
+@@ -1,4 +1,4 @@
+-#!/usr/local/bin/wish -f
++#!/usr/local/bin/wish8.0 -f
+ #	Installation Notes (see also the README file):
+ # 1. On Unix systems: change the 1st above line to point to the wish
+ #    executable you want to use (e.g., wish4.2 or /usr/local/bin/wish8.0)
diff --git a/devel/spin/pkg-comment b/devel/spin/pkg-comment
new file mode 100644
index 00000000000..3cce122e213
--- /dev/null
+++ b/devel/spin/pkg-comment
@@ -0,0 +1 @@
+An on-the-fly verification system for asynchronous concurrent systems
diff --git a/devel/spin/pkg-descr b/devel/spin/pkg-descr
new file mode 100644
index 00000000000..5cd5f839e55
--- /dev/null
+++ b/devel/spin/pkg-descr
@@ -0,0 +1,7 @@
+Spin is an efficient on-the-fly verification system
+(a `model checker') for asynchronous concurrent systems,
+such as data communication protocols, distributed operating
+systems, database systems, etc.
+It can be used to prove both safety and liveness properties,
+including all correctness requirements expressible in linear
+time temporal logic.
diff --git a/devel/spin/pkg-plist b/devel/spin/pkg-plist
new file mode 100644
index 00000000000..a88befe9abe
--- /dev/null
+++ b/devel/spin/pkg-plist
@@ -0,0 +1,123 @@
+bin/spin
+bin/xspin
+bin/xspin323.tcl
+share/doc/spin/Doc/Book.Ch6.add
+share/doc/spin/Doc/Book.Errata
+share/doc/spin/Doc/Book.answers
+share/doc/spin/Doc/Book.samples
+share/doc/spin/Doc/V1.Updates
+share/doc/spin/Doc/V2.Updates
+share/doc/spin/Doc/V3.Updates
+share/doc/spin/Examples/ex.1a
+share/doc/spin/Examples/ex.1b
+share/doc/spin/Examples/ex.1c
+share/doc/spin/Examples/ex.2
+share/doc/spin/Examples/ex.3
+share/doc/spin/Examples/ex.4b
+share/doc/spin/Examples/ex.4c
+share/doc/spin/Examples/ex.5a
+share/doc/spin/Examples/ex.5b
+share/doc/spin/Examples/ex.6
+share/doc/spin/Examples/ex.7
+share/doc/spin/Examples/ex.8
+share/doc/spin/Examples/ex.9
+share/doc/spin/Examples/ex.9b
+share/doc/spin/Examples/ex.9c
+share/doc/spin/Examples/ex.readme
+share/doc/spin/HTML/Exercises.html
+share/doc/spin/HTML/GettingStarted.html
+share/doc/spin/HTML/Intro.html
+share/doc/spin/HTML/Manual.html
+share/doc/spin/HTML/Pan.html
+share/doc/spin/HTML/Quick.html
+share/doc/spin/HTML/README.html
+share/doc/spin/HTML/Roadmap.html
+share/doc/spin/HTML/Spin.html
+share/doc/spin/HTML/WhatsNew.html
+share/doc/spin/HTML/_.html
+share/doc/spin/HTML/_last.html
+share/doc/spin/HTML/_pid.html
+share/doc/spin/HTML/accept.html
+share/doc/spin/HTML/active.html
+share/doc/spin/HTML/arrays.html
+share/doc/spin/HTML/assert.html
+share/doc/spin/HTML/assign.html
+share/doc/spin/HTML/atomic.html
+share/doc/spin/HTML/break.html
+share/doc/spin/HTML/chan.html
+share/doc/spin/HTML/comments.html
+share/doc/spin/HTML/cond_expr.html
+share/doc/spin/HTML/condition.html
+share/doc/spin/HTML/d_step.html
+share/doc/spin/HTML/datatypes.html
+share/doc/spin/HTML/do.html
+share/doc/spin/HTML/else.html
+share/doc/spin/HTML/empty.html
+share/doc/spin/HTML/enabled.html
+share/doc/spin/HTML/end.html
+share/doc/spin/HTML/eval.html
+share/doc/spin/HTML/false.html
+share/doc/spin/HTML/float.html
+share/doc/spin/HTML/full.html
+share/doc/spin/HTML/goto.html
+share/doc/spin/HTML/grammar.html
+share/doc/spin/HTML/hidden.html
+share/doc/spin/HTML/hierarchy.html
+share/doc/spin/HTML/if.html
+share/doc/spin/HTML/index.html
+share/doc/spin/HTML/init.html
+share/doc/spin/HTML/inline.html
+share/doc/spin/HTML/labels.html
+share/doc/spin/HTML/len.html
+share/doc/spin/HTML/ltl.html
+share/doc/spin/HTML/macros.html
+share/doc/spin/HTML/mtype.html
+share/doc/spin/HTML/nempty.html
+share/doc/spin/HTML/never.html
+share/doc/spin/HTML/nfull.html
+share/doc/spin/HTML/notrace.html
+share/doc/spin/HTML/np_.html
+share/doc/spin/HTML/pc_value.html
+share/doc/spin/HTML/pointers.html
+share/doc/spin/HTML/poll.html
+share/doc/spin/HTML/printf.html
+share/doc/spin/HTML/priority.html
+share/doc/spin/HTML/probabilities.html
+share/doc/spin/HTML/procedures.html
+share/doc/spin/HTML/proctype.html
+share/doc/spin/HTML/progress.html
+share/doc/spin/HTML/promela.html
+share/doc/spin/HTML/provided.html
+share/doc/spin/HTML/rand.html
+share/doc/spin/HTML/realtime.html
+share/doc/spin/HTML/receive.html
+share/doc/spin/HTML/remoterefs.html
+share/doc/spin/HTML/run.html
+share/doc/spin/HTML/scanf.html
+share/doc/spin/HTML/send.html
+share/doc/spin/HTML/separators.html
+share/doc/spin/HTML/sequence.html
+share/doc/spin/HTML/show.html
+share/doc/spin/HTML/skip.html
+share/doc/spin/HTML/timeout.html
+share/doc/spin/HTML/trace.html
+share/doc/spin/HTML/true.html
+share/doc/spin/HTML/typedef.html
+share/doc/spin/HTML/unless.html
+share/doc/spin/HTML/xr.html
+share/doc/spin/HTML/xs.html
+share/doc/spin/Test/README.tests
+share/doc/spin/Test/erathostenes
+share/doc/spin/Test/hello
+share/doc/spin/Test/leader
+share/doc/spin/Test/leader2
+share/doc/spin/Test/loops
+share/doc/spin/Test/pftp
+share/doc/spin/Test/priorities
+share/doc/spin/Test/snoopy
+share/doc/spin/Test/sort
+@dirrm share/doc/spin/Test
+@dirrm share/doc/spin/HTML
+@dirrm share/doc/spin/Examples
+@dirrm share/doc/spin/Doc
+@dirrm share/doc/spin