ports/59429: [NEW PORT] smv - a model checker for CTL
Marc van Woerkom
woerkom at es-i2.fernuni-hagen.de
Tue Nov 18 18:40:15 UTC 2003
>Number: 59429
>Category: ports
>Synopsis: [NEW PORT] smv - a model checker for CTL
>Confidential: no
>Severity: non-critical
>Priority: low
>Responsible: freebsd-ports-bugs
>State: open
>Quarter:
>Keywords:
>Date-Required:
>Class: change-request
>Submitter-Id: current-users
>Arrival-Date: Tue Nov 18 10:40:09 PST 2003
>Closed-Date:
>Last-Modified:
>Originator: Marc van Woerkom
>Release: FreeBSD 4.9-RELEASE i386
>Organization:
FernUniversitaet Hagen
>Environment:
System: FreeBSD es-i2.fernuni-hagen.de 4.9-RELEASE FreeBSD 4.9-RELEASE #0: Mon Oct 27 07:38:24 CET 2003 root at es-i2.fernuni-hagen.de:/usr/obj/usr/src/sys/Compaq-ES i386
>Description:
[NEW PORT] smv - a model checker for CTL
>How-To-Repeat:
>Fix:
Here is the port
Regards,
Marc
# 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:
#
# smv
# smv/distinfo
# smv/Makefile
# smv/pkg-descr
# smv/files
# smv/files/patch-bdd.c
# smv/files/patch-storage.c
# smv/files/patch-hash.c
# smv/files/patch-node.c
# smv/files/patch-makefile
# smv/files/patch-storage.h
# smv/files/patch-string.c
# smv/pkg-plist
#
echo c - smv
mkdir -p smv > /dev/null 2>&1
echo x - smv/distinfo
sed 's/^X//' >smv/distinfo << 'END-of-smv/distinfo'
XMD5 (smv.r2.5.4.3.tar.gz) = dd1a7ebcbac935845fc73eb8957386cb
END-of-smv/distinfo
echo x - smv/Makefile
sed 's/^X//' >smv/Makefile << 'END-of-smv/Makefile'
X# New ports collection makefile for: smv
X# Date created: 18 November 2003
X# Whom: Marc E.E. van Woerkom <marc.vanwoerkom at fernuni-hagen.de>
X#
X# $FreeBSD$
X#
X
XPORTNAME= smv
XPORTVERSION= 2.5.4.3
XCATEGORIES= devel
XMASTER_SITES= http://www-2.cs.cmu.edu/~modelcheck/smv/
XDISTNAME= ${PORTNAME}.r${PORTVERSION}
X
XMAINTAINER= marc.vanwoerkom at fernuni-hagen.de
XCOMMENT= A model checker
X
XWRKSRC= ${WRKDIR}/smv
XALL_TARGET= smv
X
XMAN1= smv.1
X
XMANCOMPRESSED=no
X
Xpost-patch:
X @${MV} ${WRKSRC}/makefile ${WRKSRC}/Makefile
X
Xdo-install:
X ${INSTALL_PROGRAM} ${WRKSRC}/smv ${PREFIX}/bin
X ${MKDIR} ${PREFIX}/share/smv
X ${INSTALL_DATA} ${WRKSRC}/smv-mode.el ${DATADIR}
X
Xpost-install:
X.if !defined(NOPORTDOCS)
X ${INSTALL_MAN} ${WRKSRC}/smv.1 ${PREFIX}/man/man1
X ${MKDIR} ${DOCSDIR}
X ${INSTALL_MAN} ${WRKSRC}/NEW ${DOCSDIR}
X ${INSTALL_MAN} ${WRKSRC}/README ${DOCSDIR}
X ${INSTALL_MAN} ${WRKSRC}/doc/smvmanual.ps ${DOCSDIR}
X ${MKDIR} ${EXAMPLESDIR}
X ${INSTALL_MAN} ${WRKSRC}/examples/counter.smv ${EXAMPLESDIR}
X ${INSTALL_MAN} ${WRKSRC}/examples/dme1.smv ${EXAMPLESDIR}
X ${INSTALL_MAN} ${WRKSRC}/examples/dme2.smv ${EXAMPLESDIR}
X ${INSTALL_MAN} ${WRKSRC}/examples/featuring.smv ${EXAMPLESDIR}
X ${INSTALL_MAN} ${WRKSRC}/examples/gigamax.smv ${EXAMPLESDIR}
X ${INSTALL_MAN} ${WRKSRC}/examples/mutex.smv ${EXAMPLESDIR}
X ${INSTALL_MAN} ${WRKSRC}/examples/mutex1.smv ${EXAMPLESDIR}
X ${INSTALL_MAN} ${WRKSRC}/examples/periodic.smv ${EXAMPLESDIR}
X ${INSTALL_MAN} ${WRKSRC}/examples/ring.smv ${EXAMPLESDIR}
X ${INSTALL_MAN} ${WRKSRC}/examples/semaphore.smv ${EXAMPLESDIR}
X ${INSTALL_MAN} ${WRKSRC}/examples/short.smv ${EXAMPLESDIR}
X ${INSTALL_MAN} ${WRKSRC}/examples/syncarb5.smv ${EXAMPLESDIR}
X.endif
X
X.include <bsd.port.mk>
END-of-smv/Makefile
echo x - smv/pkg-descr
sed 's/^X//' >smv/pkg-descr << 'END-of-smv/pkg-descr'
XThe SMV (Symbolic Model Verifier) system is a tool for
Xchecking finite state systems against specifications
Xin the temporal logic CTL (Computational Tree Logic).
X
XOne specifies the finite state system (finite automaton,
XMealy machine, full adder circuit, ..) as a Kripke
Xstructure in the SMV language and provides specificaations
Xin CTL. The model checking algorithm allows to determine
Xif the Kripke structure fulfills the specifications.
X
XWWW: http://www-2.cs.cmu.edu/~modelcheck/smv.html
X
XMarc E.E. van Woerkom
Xmarc.vanwoerkom at fernuni-hagen.de
END-of-smv/pkg-descr
echo c - smv/files
mkdir -p smv/files > /dev/null 2>&1
echo x - smv/files/patch-bdd.c
sed 's/^X//' >smv/files/patch-bdd.c << 'END-of-smv/files/patch-bdd.c'
X--- bdd.c
X+++ bdd.c
X@@ -113,7 +113,7 @@
X /* Initialize a keytable. */
X kp->n = n;
X kp->elements_in_table = 0;
X- kp->hash_table_buf = (bdd_ptr *)malloc(n*sizeof(bdd_ptr));
X+ kp->hash_table_buf = (bdd_ptr *)smv_malloc(n*sizeof(bdd_ptr));
X
X { /* Initialize hash bin list pointers to NULL. */
X register int i;
X@@ -139,7 +139,7 @@
X /* Create key tables. */
X create_keytable(&reduce_table, KEYTABLESIZE);
X apply_cache_size = APPLY_CACHE_SIZE;
X- apply_cache = (apply_rec *)malloc(sizeof(apply_rec)*apply_cache_size);
X+ apply_cache = (apply_rec *)smv_malloc(sizeof(apply_rec)*apply_cache_size);
X {
X int i;
X for(i=0;i<apply_cache_size;i++)apply_cache[i].op = 0;
X@@ -1446,7 +1446,7 @@
X }
X
X /* An "infinity" constant - big enough power of 2 not to care about */
X-#define INFINITY 1000
X+#define SMV_INFINITY 1000
X
X /* similar to auxcount_bdd, but computes log2 of the fraction */
X
X@@ -1457,18 +1457,18 @@
X union {float a; bdd_ptr b;} temp; /* very dangerous!!! */
X double l,r;
X
X- if(d==ZERO)return(-INFINITY); /* = log(0) */
X+ if(d==ZERO)return(-SMV_INFINITY); /* = log(0) */
X if(d==ONE)return(0.0); /* = log2(1) */
X temp.b = find_apply(COUNT_OP,d,ZERO);
X if(temp.b==NULL) {
X l = auxcount_bdd_log2(d->left,n);
X r = auxcount_bdd_log2(d->right,n);
X if(l < r) {
X- if(r - l > INFINITY) temp.a = r;
X+ if(r - l > SMV_INFINITY) temp.a = r;
X else temp.a = l - 1.0 + log2(1.0 + pow(2.0,r-l));
X }
X else {
X- if(l - r > INFINITY) temp.a = l;
X+ if(l - r > SMV_INFINITY) temp.a = l;
X else temp.a = r - 1.0 + log2(1.0 + pow(2.0,l-r));
X }
X }
END-of-smv/files/patch-bdd.c
echo x - smv/files/patch-storage.c
sed 's/^X//' >smv/files/patch-storage.c << 'END-of-smv/files/patch-storage.c'
X--- storage.c
X+++ storage.c
X@@ -9,7 +9,7 @@
X {
X #ifdef MACH
X mach_init(); /* needed to make sbrk() work */
X-#endif MACH
X+#endif
X /* addrfree points to the first free byte
X addrlimit points to the memory limit */
X addrfree = addrlimit = (char *) sbrk(0);
X@@ -34,7 +34,7 @@
X }
X
X /* provide malloc for miscellaneuos storage allocation */
X-char *malloc(n)
X+char* smv_malloc(n)
X int n;
X {
X if(n % 4)n=n+4-(n%4); /* always allocate multiple of four bytes */
X@@ -47,7 +47,7 @@
X }
X
X /* very simple implementation of free */
X-void free(p)
X+void smv_free(p)
X char *p;
X {
X return;
X@@ -61,7 +61,7 @@
X mgr_ptr new_mgr(rec_size)
X int rec_size;
X {
X- register mgr_ptr mp = (mgr_ptr)malloc(sizeof(struct mgr));
X+ register mgr_ptr mp = (mgr_ptr)smv_malloc(sizeof(struct mgr));
X mp->free.link = 0;
X mp->rec_size = rec_size;
X mp->count = 0;
Xdiff -ru ./storage.h /usr3/marc/research/hagen/10-ws0304/77075 Model Checking/praktikum/smv/smv/storage.h
END-of-smv/files/patch-storage.c
echo x - smv/files/patch-hash.c
sed 's/^X//' >smv/files/patch-hash.c << 'END-of-smv/files/patch-hash.c'
X--- hash.c
X+++ hash.c
X@@ -7,12 +7,12 @@
X int (*hash_fun)(),(*eq_fun)();
X mgr_ptr mgr;
X {
X- hash_ptr res = (hash_ptr)malloc(sizeof(struct hash));
X+ hash_ptr res = (hash_ptr)smv_malloc(sizeof(struct hash));
X res->size = init_size;
X res->hash_fun = hash_fun;
X res->eq_fun = eq_fun;
X res->mgr = mgr;
X- res->tab = (rec_ptr *)malloc(init_size * sizeof(rec_ptr));
X+ res->tab = (rec_ptr *)smv_malloc(init_size * sizeof(rec_ptr));
X bzero(res->tab,init_size * sizeof(rec_ptr));
X return(res);
X }
END-of-smv/files/patch-hash.c
echo x - smv/files/patch-node.c
sed 's/^X//' >smv/files/patch-node.c << 'END-of-smv/files/patch-node.c'
X--- node.c
X+++ node.c
X@@ -609,7 +609,7 @@
X node_ptr n;
X int col;
X {
X- char *buf = (char *)malloc(option_print_node_length + 1);
X+ char *buf = (char *)smv_malloc(option_print_node_length + 1);
X int c,p;
X if(buf == NULL) rpterr("Out of memory");
X buf[0] = 0;
X@@ -623,7 +623,7 @@
X }
X fprintf(stream,"%s",buf);
X if(!c)fprintf(stream,"...");
X- free(buf);
X+ smv_free(buf);
X return(col + p);
X }
END-of-smv/files/patch-node.c
echo x - smv/files/patch-makefile
sed 's/^X//' >smv/files/patch-makefile << 'END-of-smv/files/patch-makefile'
X--- makefile
X+++ makefile
X@@ -50,8 +50,8 @@
X input.c: input.lex
X $(LEX) $(LEXFLAGS) input.lex; mv lex.yy.c input.c
X
X-# Recompile main.c if makefile changes. This may be the change of version.
X-main.o: main.c init.h makefile
X+# Recompile main.c if Makefile changes. This may be the change of version.
X+main.o: main.c init.h Makefile
X init.o: init.c init.h y.tab.h assoc.h storage.h bdd.h hash.h node.h string.h
X assoc.o: assoc.c assoc.h storage.h hash.h node.h
X bdd.o: bdd.c assoc.h storage.h bdd.h hash.h node.h y.tab.h
X@@ -66,7 +66,7 @@
X clean:
X rm -f *.o grammar.c grammar.y input.lex input.c y.tab.h
X SRC= \
X- makefile \
X+ Makefile \
X README \
X assoc.c \
X assoc.h \
END-of-smv/files/patch-makefile
echo x - smv/files/patch-storage.h
sed 's/^X//' >smv/files/patch-storage.h << 'END-of-smv/files/patch-storage.h'
X--- storage.h
X+++ storage.h
X@@ -12,8 +12,8 @@
X #define ALLOCSIZE (2<<15)
X
X void init_storage();
X-char *malloc();
X-void free();
X+char* smv_malloc();
X+void smv_free();
X mgr_ptr new_mgr();
X rec_ptr new_rec(),dup_rec();
X void free_rec();
END-of-smv/files/patch-storage.h
echo x - smv/files/patch-string.c
sed 's/^X//' >smv/files/patch-string.c << 'END-of-smv/files/patch-string.c'
X--- string.c
X+++ string.c
X@@ -35,7 +35,7 @@
X string_rec a,*res;
X a.text = x;
X if(res = (string_ptr)find_hash(string_hash,&a))return(res);
X- a.text = (char *)strcpy((char *)malloc(strlen(x)+1),x);
X+ a.text = (char *)strcpy((char *)smv_malloc(strlen(x)+1),x);
X return((string_ptr)insert_hash(string_hash,&a));
X }
END-of-smv/files/patch-string.c
echo x - smv/pkg-plist
sed 's/^X//' >smv/pkg-plist << 'END-of-smv/pkg-plist'
Xbin/smv
Xshare/smv/smv-mode.el
X%%PORTDOCS%%%%DOCSDIR%%/NEW
X%%PORTDOCS%%%%DOCSDIR%%/README
X%%PORTDOCS%%%%DOCSDIR%%/smvmanual.ps
X%%PORTDOCS%%%%EXAMPLESDIR%%/counter.smv
X%%PORTDOCS%%%%EXAMPLESDIR%%/dme1.smv
X%%PORTDOCS%%%%EXAMPLESDIR%%/dme2.smv
X%%PORTDOCS%%%%EXAMPLESDIR%%/featuring.smv
X%%PORTDOCS%%%%EXAMPLESDIR%%/gigamax.smv
X%%PORTDOCS%%%%EXAMPLESDIR%%/mutex.smv
X%%PORTDOCS%%%%EXAMPLESDIR%%/mutex1.smv
X%%PORTDOCS%%%%EXAMPLESDIR%%/periodic.smv
X%%PORTDOCS%%%%EXAMPLESDIR%%/ring.smv
X%%PORTDOCS%%%%EXAMPLESDIR%%/semaphore.smv
X%%PORTDOCS%%%%EXAMPLESDIR%%/short.smv
X%%PORTDOCS%%%%EXAMPLESDIR%%/syncarb5.smv
X%%PORTDOCS%%@dirrm %%DOCSDIR%%
X%%PORTDOCS%%@dirrm %%EXAMPLESDIR%%
X at dirrm share/smv
END-of-smv/pkg-plist
exit
>Release-Note:
>Audit-Trail:
>Unformatted:
More information about the freebsd-ports-bugs
mailing list