Date: Tue, 18 Nov 2003 19:35:31 +0100 (CET) From: Marc van Woerkom <woerkom@es-i2.fernuni-hagen.de> To: FreeBSD-gnats-submit@FreeBSD.org Subject: ports/59429: [NEW PORT] smv - a model checker for CTL Message-ID: <20031118183531.BF759608D@es-i2.fernuni-hagen.de> Resent-Message-ID: <200311181840.hAIIeAZ5058477@freefall.freebsd.org>
next in thread | raw e-mail | index | archive | help
>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@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@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@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@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@dirrm share/smv END-of-smv/pkg-plist exit >Release-Note: >Audit-Trail: >Unformatted:
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?20031118183531.BF759608D>