From 2052cf95c1ee4eca54a814422161007041c13d15 Mon Sep 17 00:00:00 2001 From: "Justin M. Seger" Date: Sat, 12 Dec 1998 22:17:48 +0000 Subject: 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 --- math/spin/Makefile | 50 +++++++++++++++++++ math/spin/distinfo | 2 + math/spin/files/patch-aa | 8 +++ math/spin/pkg-comment | 1 + math/spin/pkg-descr | 7 +++ math/spin/pkg-plist | 123 +++++++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 191 insertions(+) create mode 100644 math/spin/Makefile create mode 100644 math/spin/distinfo create mode 100644 math/spin/files/patch-aa create mode 100644 math/spin/pkg-comment create mode 100644 math/spin/pkg-descr create mode 100644 math/spin/pkg-plist (limited to 'math') diff --git a/math/spin/Makefile b/math/spin/Makefile new file mode 100644 index 000000000000..9a99c165d6ea --- /dev/null +++ b/math/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 diff --git a/math/spin/distinfo b/math/spin/distinfo new file mode 100644 index 000000000000..7e4aaee44897 --- /dev/null +++ b/math/spin/distinfo @@ -0,0 +1,2 @@ +MD5 (spin/spin323.tar.gz) = 1ac5fffa78663ba13658ba0c3bce3419 +MD5 (spin/html.tar.gz) = 2988743b1d9db59aff4ddd999573d6b3 diff --git a/math/spin/files/patch-aa b/math/spin/files/patch-aa new file mode 100644 index 000000000000..430dbe1fd181 --- /dev/null +++ b/math/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/math/spin/pkg-comment b/math/spin/pkg-comment new file mode 100644 index 000000000000..3cce122e2137 --- /dev/null +++ b/math/spin/pkg-comment @@ -0,0 +1 @@ +An on-the-fly verification system for asynchronous concurrent systems diff --git a/math/spin/pkg-descr b/math/spin/pkg-descr new file mode 100644 index 000000000000..5cd5f839e550 --- /dev/null +++ b/math/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/math/spin/pkg-plist b/math/spin/pkg-plist new file mode 100644 index 000000000000..a88befe9abeb --- /dev/null +++ b/math/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 -- cgit v1.2.3