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
This commit is contained in:
Justin M. Seger
parent
14408aea69
commit
2052cf95c1
Notes:
svn2git
2021-03-31 03:12:20 +00:00
svn path=/head/; revision=15311
50
devel/spin/Makefile
Normal file
50
devel/spin/Makefile
Normal file
@ -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>
|
||||
2
devel/spin/distinfo
Normal file
2
devel/spin/distinfo
Normal file
@ -0,0 +1,2 @@
|
||||
MD5 (spin/spin323.tar.gz) = 1ac5fffa78663ba13658ba0c3bce3419
|
||||
MD5 (spin/html.tar.gz) = 2988743b1d9db59aff4ddd999573d6b3
|
||||
8
devel/spin/files/patch-aa
Normal file
8
devel/spin/files/patch-aa
Normal file
@ -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)
|
||||
1
devel/spin/pkg-comment
Normal file
1
devel/spin/pkg-comment
Normal file
@ -0,0 +1 @@
|
||||
An on-the-fly verification system for asynchronous concurrent systems
|
||||
7
devel/spin/pkg-descr
Normal file
7
devel/spin/pkg-descr
Normal file
@ -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.
|
||||
123
devel/spin/pkg-plist
Normal file
123
devel/spin/pkg-plist
Normal file
@ -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
|
||||
50
math/spin/Makefile
Normal file
50
math/spin/Makefile
Normal file
@ -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>
|
||||
2
math/spin/distinfo
Normal file
2
math/spin/distinfo
Normal file
@ -0,0 +1,2 @@
|
||||
MD5 (spin/spin323.tar.gz) = 1ac5fffa78663ba13658ba0c3bce3419
|
||||
MD5 (spin/html.tar.gz) = 2988743b1d9db59aff4ddd999573d6b3
|
||||
8
math/spin/files/patch-aa
Normal file
8
math/spin/files/patch-aa
Normal file
@ -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)
|
||||
1
math/spin/pkg-comment
Normal file
1
math/spin/pkg-comment
Normal file
@ -0,0 +1 @@
|
||||
An on-the-fly verification system for asynchronous concurrent systems
|
||||
7
math/spin/pkg-descr
Normal file
7
math/spin/pkg-descr
Normal file
@ -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.
|
||||
123
math/spin/pkg-plist
Normal file
123
math/spin/pkg-plist
Normal file
@ -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
|
||||
Loading…
Reference in New Issue
Block a user