From owner-freebsd-ports Fri Dec 11 18:50:02 1998 Return-Path: Received: (from majordom@localhost) by hub.freebsd.org (8.8.8/8.8.8) id SAA04219 for freebsd-ports-outgoing; Fri, 11 Dec 1998 18:50:02 -0800 (PST) (envelope-from owner-freebsd-ports@FreeBSD.ORG) Received: from freefall.freebsd.org (freefall.FreeBSD.ORG [204.216.27.21]) by hub.freebsd.org (8.8.8/8.8.8) with ESMTP id SAA04177 for ; Fri, 11 Dec 1998 18:49:59 -0800 (PST) (envelope-from gnats@FreeBSD.org) Received: (from Unknown UID 563@localhost) by freefall.freebsd.org (8.8.8/8.8.5) id SAA13733; Fri, 11 Dec 1998 18:50:01 -0800 (PST) Received: from cr1003333-a.crdva1.bc.wave.home.com (cr1003333-a.crdva1.bc.wave.home.com [24.113.51.240]) by hub.freebsd.org (8.8.8/8.8.8) with ESMTP id SAA03869 for ; Fri, 11 Dec 1998 18:46:17 -0800 (PST) (envelope-from jh@cr1003333-a.crdva1.bc.wave.home.com) Received: (from jh@localhost) by cr1003333-a.crdva1.bc.wave.home.com (8.9.1/8.9.1) id SAA08739; Fri, 11 Dec 1998 18:46:03 -0800 (PST) (envelope-from jh) Message-Id: <199812120246.SAA08739@cr1003333-a.crdva1.bc.wave.home.com> Date: Fri, 11 Dec 1998 18:46:03 -0800 (PST) From: Jonathan Hanna Reply-To: pangolin@home.com To: FreeBSD-gnats-submit@FreeBSD.ORG X-Send-Pr-Version: 3.2 Subject: ports/9058: New port (resubmitted): spin - Verification system for asynchronous concurrent systems. Sender: owner-freebsd-ports@FreeBSD.ORG Precedence: bulk X-Loop: FreeBSD.org >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 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