Date: Fri, 11 Dec 1998 18:46:03 -0800 (PST) From: Jonathan Hanna <jh@cr1003333-a.crdva1.bc.wave.home.com> To: FreeBSD-gnats-submit@FreeBSD.ORG Subject: ports/9058: New port (resubmitted): spin - Verification system for asynchronous concurrent systems. Message-ID: <199812120246.SAA08739@cr1003333-a.crdva1.bc.wave.home.com>
next in thread | raw e-mail | index | archive | help
>Number: 9058 >Category: ports >Synopsis: New port (resubmitted): spin - Verification system for asynchronous concurrent systems. >Confidential: no >Severity: non-critical >Priority: low >Responsible: freebsd-ports >State: open >Quarter: >Keywords: >Date-Required: >Class: change-request >Submitter-Id: current-users >Arrival-Date: Fri Dec 11 18:50:01 PST 1998 >Last-Modified: >Originator: Jonathan Hanna >Organization: >Release: FreeBSD 3.0-CURRENT i386 >Environment: >Description: 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. Has TCL front-end (not required). >How-To-Repeat: >Fix: # This is a shell archive. Save it in a file, remove anything before # this line, and then unpack it by entering "sh file". Note, it may # create directories; files and directories will be owned by you and # have default permissions. # # This archive contains: # # spin # spin/pkg # spin/pkg/PLIST # spin/pkg/COMMENT # spin/pkg/DESCR # spin/files # spin/files/md5 # spin/patches # spin/patches/patch-aa # spin/Makefile # echo c - spin mkdir -p spin > /dev/null 2>&1 echo c - spin/pkg mkdir -p spin/pkg > /dev/null 2>&1 echo x - spin/pkg/PLIST sed 's/^X//' >spin/pkg/PLIST << 'END-of-spin/pkg/PLIST' Xbin/spin Xbin/xspin323.tcl Xbin/xspin Xshare/doc/spin/Doc/Book.Ch6.add Xshare/doc/spin/Doc/Book.Errata Xshare/doc/spin/Doc/Book.answers Xshare/doc/spin/Doc/Book.samples Xshare/doc/spin/Doc/V1.Updates Xshare/doc/spin/Doc/V2.Updates Xshare/doc/spin/Doc/V3.Updates Xshare/doc/spin/Examples/ex.readme Xshare/doc/spin/Examples/ex.1a Xshare/doc/spin/Examples/ex.1b Xshare/doc/spin/Examples/ex.1c Xshare/doc/spin/Examples/ex.2 Xshare/doc/spin/Examples/ex.3 Xshare/doc/spin/Examples/ex.4b Xshare/doc/spin/Examples/ex.4c Xshare/doc/spin/Examples/ex.5a Xshare/doc/spin/Examples/ex.5b Xshare/doc/spin/Examples/ex.6 Xshare/doc/spin/Examples/ex.7 Xshare/doc/spin/Examples/ex.8 Xshare/doc/spin/Examples/ex.9 Xshare/doc/spin/Examples/ex.9b Xshare/doc/spin/Examples/ex.9c Xshare/doc/spin/HTML/Exercises.html Xshare/doc/spin/HTML/GettingStarted.html Xshare/doc/spin/HTML/Intro.html Xshare/doc/spin/HTML/Manual.html Xshare/doc/spin/HTML/Pan.html Xshare/doc/spin/HTML/Quick.html Xshare/doc/spin/HTML/README.html Xshare/doc/spin/HTML/Roadmap.html Xshare/doc/spin/HTML/Spin.html Xshare/doc/spin/HTML/WhatsNew.html Xshare/doc/spin/HTML/_.html Xshare/doc/spin/HTML/_last.html Xshare/doc/spin/HTML/_pid.html Xshare/doc/spin/HTML/accept.html Xshare/doc/spin/HTML/active.html Xshare/doc/spin/HTML/arrays.html Xshare/doc/spin/HTML/assert.html Xshare/doc/spin/HTML/assign.html Xshare/doc/spin/HTML/atomic.html Xshare/doc/spin/HTML/break.html Xshare/doc/spin/HTML/chan.html Xshare/doc/spin/HTML/comments.html Xshare/doc/spin/HTML/cond_expr.html Xshare/doc/spin/HTML/condition.html Xshare/doc/spin/HTML/d_step.html Xshare/doc/spin/HTML/datatypes.html Xshare/doc/spin/HTML/do.html Xshare/doc/spin/HTML/else.html Xshare/doc/spin/HTML/empty.html Xshare/doc/spin/HTML/enabled.html Xshare/doc/spin/HTML/end.html Xshare/doc/spin/HTML/eval.html Xshare/doc/spin/HTML/false.html Xshare/doc/spin/HTML/float.html Xshare/doc/spin/HTML/full.html Xshare/doc/spin/HTML/goto.html Xshare/doc/spin/HTML/grammar.html Xshare/doc/spin/HTML/hidden.html Xshare/doc/spin/HTML/hierarchy.html Xshare/doc/spin/HTML/if.html Xshare/doc/spin/HTML/index.html Xshare/doc/spin/HTML/init.html Xshare/doc/spin/HTML/labels.html Xshare/doc/spin/HTML/len.html Xshare/doc/spin/HTML/ltl.html Xshare/doc/spin/HTML/macros.html Xshare/doc/spin/HTML/mtype.html Xshare/doc/spin/HTML/nempty.html Xshare/doc/spin/HTML/never.html Xshare/doc/spin/HTML/nfull.html Xshare/doc/spin/HTML/notrace.html Xshare/doc/spin/HTML/np_.html Xshare/doc/spin/HTML/pc_value.html Xshare/doc/spin/HTML/pointers.html Xshare/doc/spin/HTML/poll.html Xshare/doc/spin/HTML/printf.html Xshare/doc/spin/HTML/priority.html Xshare/doc/spin/HTML/probabilities.html Xshare/doc/spin/HTML/procedures.html Xshare/doc/spin/HTML/proctype.html Xshare/doc/spin/HTML/progress.html Xshare/doc/spin/HTML/promela.html Xshare/doc/spin/HTML/provided.html Xshare/doc/spin/HTML/rand.html Xshare/doc/spin/HTML/realtime.html Xshare/doc/spin/HTML/receive.html Xshare/doc/spin/HTML/remoterefs.html Xshare/doc/spin/HTML/run.html Xshare/doc/spin/HTML/scanf.html Xshare/doc/spin/HTML/send.html Xshare/doc/spin/HTML/xr.html Xshare/doc/spin/HTML/separators.html Xshare/doc/spin/HTML/sequence.html Xshare/doc/spin/HTML/show.html Xshare/doc/spin/HTML/skip.html Xshare/doc/spin/HTML/timeout.html Xshare/doc/spin/HTML/trace.html Xshare/doc/spin/HTML/true.html Xshare/doc/spin/HTML/typedef.html Xshare/doc/spin/HTML/unless.html Xshare/doc/spin/HTML/xs.html Xshare/doc/spin/Test/README.tests Xshare/doc/spin/Test/erathostenes Xshare/doc/spin/Test/hello Xshare/doc/spin/Test/leader Xshare/doc/spin/Test/leader2 Xshare/doc/spin/Test/loops Xshare/doc/spin/Test/pftp Xshare/doc/spin/Test/priorities Xshare/doc/spin/Test/snoopy Xshare/doc/spin/Test/sort X@dirrm share/doc/spin/Doc X@dirrm share/doc/spin/HTML X@dirrm share/doc/spin/Examples X@dirrm share/doc/spin/Test X@dirrm share/doc/spin END-of-spin/pkg/PLIST echo x - spin/pkg/COMMENT sed 's/^X//' >spin/pkg/COMMENT << 'END-of-spin/pkg/COMMENT' XAn efficient on-the-fly verification system for asynchronous concurrent systems. END-of-spin/pkg/COMMENT echo x - spin/pkg/DESCR sed 's/^X//' >spin/pkg/DESCR << 'END-of-spin/pkg/DESCR' XSpin is an efficient on-the-fly verification system X(a `model checker') for asynchronous concurrent systems, Xsuch as data communication protocols, distributed operating Xsystems, database systems, etc. XIt can be used to prove both safety and liveness properties, Xincluding all correctness requirements expressible in linear Xtime temporal logic. END-of-spin/pkg/DESCR echo c - spin/files mkdir -p spin/files > /dev/null 2>&1 echo x - spin/files/md5 sed 's/^X//' >spin/files/md5 << 'END-of-spin/files/md5' XMD5 (spin/spin323.tar.gz) = 1ac5fffa78663ba13658ba0c3bce3419 XMD5 (spin/html.tar.gz) = 3dfcfa218a425943586dc9608d44a175 END-of-spin/files/md5 echo c - spin/patches mkdir -p spin/patches > /dev/null 2>&1 echo x - spin/patches/patch-aa sed 's/^X//' >spin/patches/patch-aa << 'END-of-spin/patches/patch-aa' X--- ../Xspin3.2/xspin323.tcl.orig Wed Dec 17 10:11:57 1997 X+++ ../Xspin3.2/xspin323.tcl Sun Dec 21 13:20:41 1997 X@@ -1,4 +1,4 @@ X-#!/usr/local/bin/wish -f X+#!/usr/local/bin/wish8.0 -f X # Installation Notes (see also the README file): X # 1. On Unix systems: change the 1st above line to point to the wish X # executable you want to use (e.g., wish4.2 or /usr/local/bin/wish8.0) END-of-spin/patches/patch-aa echo x - spin/Makefile sed 's/^X//' >spin/Makefile << 'END-of-spin/Makefile' X# X# Ports collection makefile for: spin X# Version required: 3.23 X# Date created: Oct 23, 1997 X# Whom: jhanna@home.com X# X# $Id$ X# X XDISTNAME= spin-3.23 XCATEGORIES= lang X# X# netlib mirrors don't seem to keep in sync, can't just list all of them X# XMASTER_SITES= ftp://netlib.bell-labs.com/netlib/spin/ XMASTER_SITES+= ftp://www.netlib.org/spin/ XMASTER_SITES+= ftp://www.enseeiht.fr/NetLib/spin/ XMASTER_SITES+= ftp://wcarchive.cdrom.com/netlib/spin/ XDISTFILES= spin323.tar.gz html.tar.gz X XMAINTAINER= jhanna@home.com X XDIST_SUBDIR= spin XEXTRACT_ONLY= spin323.tar.gz XWRKSRC= ${WRKDIR}/Src3.2 XMAKEFILE= makefile XALL_TARGET= spin X X# X# Objects may be included in the distfile. X# Xpre-build: X cd ${WRKSRC} ; ${MAKE} clean X Xdo-install: X # X # Program X # X ${INSTALL_PROGRAM} ${WRKSRC}/spin ${PREFIX}/bin X ${INSTALL_SCRIPT} ${WRKDIR}/Xspin3.2/xspin323.tcl ${PREFIX}/bin X cd ${PREFIX}/bin ; \ X ${RM} -f xspin ; ln -s xspin323.tcl xspin ; \ X chown -h ${BINOWN}.${BINGRP} xspin X.if !defined(NOPORTDOCS) X # X # Documentation, Examples X # X ${MKDIR} ${PREFIX}/share/doc/spin X chown -h ${SHAREOWN}.${SHAREGRP} ${PREFIX}/share/doc/spin X ${MKDIR} ${PREFIX}/share/doc/spin/Doc X chown -h ${SHAREOWN}.${SHAREGRP} ${PREFIX}/share/doc/spin/Doc X ${INSTALL_DATA} ${WRKDIR}/Doc/* ${PREFIX}/share/doc/spin/Doc X ${MKDIR} ${PREFIX}/share/doc/spin/Examples X chown -h ${SHAREOWN}.${SHAREGRP} ${PREFIX}/share/doc/spin/Examples X cd ${PREFIX}/share/doc/spin/Examples ; \ X sh ${WRKDIR}/Test/examples ; \ X chown ${SHAREOWN}.${SHAREGRP} * X cd ${PREFIX}/share/doc/spin ; \ X tar -xzvf ${DISTDIR}/${DIST_SUBDIR}/html.tar.gz ; \ X chown ${SHAREOWN}.${SHAREGRP} HTML HTML/* X ${MKDIR} ${PREFIX}/share/doc/spin/Test X chown -h ${SHAREOWN}.${SHAREGRP} ${PREFIX}/share/doc/spin/Test X.for i in README.tests erathostenes hello leader leader2 loops pftp \ X priorities snoopy sort X ${INSTALL_DATA} ${WRKDIR}/Test/$i ${PREFIX}/share/doc/spin/Test X.endfor X.endif X X.include <bsd.port.mk> END-of-spin/Makefile exit >Audit-Trail: >Unformatted: To Unsubscribe: send mail to majordomo@FreeBSD.org with "unsubscribe freebsd-ports" in the body of the message
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?199812120246.SAA08739>