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