Add The SMV (Symbolic Model Verifier), a tool for

checking finite state systems against specifications
the temporal logic CTL (Computational Tree Logic).

PR:		ports/59429
Submitted by:	Marc van Woerkom <marc.vanwoerkom@fernuni-hagen.de>

10 files changed, 232 insertions, 0 deletions

diff --git a/devel/smv/Makefile b/devel/smv/Makefile
new file mode 100644
index 000000000000..04956f016459
--- /dev/null
+++ b/devel/smv/Makefile
@@ -0,0 +1,48 @@
+# New ports collection makefile for: smv
+# Date created: 18 November 2003
+# Whom: Marc E.E. van Woerkom <marc.vanwoerkom@fernuni-hagen.de>
+#
+# $FreeBSD$
+#
+
+PORTNAME=	smv
+PORTVERSION=	2.5.4.3
+CATEGORIES=	devel
+MASTER_SITES=	http://www-2.cs.cmu.edu/~modelcheck/smv/
+DISTNAME=	${PORTNAME}.r${PORTVERSION}
+
+MAINTAINER=	marc.vanwoerkom@fernuni-hagen.de
+COMMENT=	Symbolic Model Verifier System for checking finite state systems
+
+WRKSRC=		${WRKDIR}/${PORTNAME}
+ALL_TARGET=	${PORTNAME}
+MAKEFILE=	makefile
+
+MAN1=		smv.1
+
+do-install:
+	${INSTALL_PROGRAM} ${WRKSRC}/smv ${PREFIX}/bin
+	${MKDIR} ${DATADIR}
+	${INSTALL_DATA} ${WRKSRC}/smv-mode.el ${DATADIR}
+	${INSTALL_MAN} ${WRKSRC}/smv.1 ${PREFIX}/man/man1
+.if !defined(NOPORTDOCS)
+	${MKDIR} ${DOCSDIR}
+	${INSTALL_MAN} ${WRKSRC}/NEW ${DOCSDIR}
+	${INSTALL_MAN} ${WRKSRC}/README ${DOCSDIR}
+	${INSTALL_MAN} ${WRKSRC}/doc/smvmanual.ps ${DOCSDIR}
+	${MKDIR} ${EXAMPLESDIR}
+	${INSTALL_MAN} ${WRKSRC}/examples/counter.smv ${EXAMPLESDIR}
+	${INSTALL_MAN} ${WRKSRC}/examples/dme1.smv ${EXAMPLESDIR}
+	${INSTALL_MAN} ${WRKSRC}/examples/dme2.smv ${EXAMPLESDIR}
+	${INSTALL_MAN} ${WRKSRC}/examples/featuring.smv ${EXAMPLESDIR}
+	${INSTALL_MAN} ${WRKSRC}/examples/gigamax.smv ${EXAMPLESDIR}
+	${INSTALL_MAN} ${WRKSRC}/examples/mutex.smv ${EXAMPLESDIR}
+	${INSTALL_MAN} ${WRKSRC}/examples/mutex1.smv ${EXAMPLESDIR}
+	${INSTALL_MAN} ${WRKSRC}/examples/periodic.smv ${EXAMPLESDIR}
+	${INSTALL_MAN} ${WRKSRC}/examples/ring.smv ${EXAMPLESDIR}
+	${INSTALL_MAN} ${WRKSRC}/examples/semaphore.smv ${EXAMPLESDIR}
+	${INSTALL_MAN} ${WRKSRC}/examples/short.smv ${EXAMPLESDIR}
+	${INSTALL_MAN} ${WRKSRC}/examples/syncarb5.smv ${EXAMPLESDIR}
+.endif
+
+.include <bsd.port.mk>
diff --git a/devel/smv/distinfo b/devel/smv/distinfo
new file mode 100644
index 000000000000..1a11eae434b3
--- /dev/null
+++ b/devel/smv/distinfo
@@ -0,0 +1 @@
+MD5 (smv.r2.5.4.3.tar.gz) = dd1a7ebcbac935845fc73eb8957386cb
diff --git a/devel/smv/files/patch-bdd.c b/devel/smv/files/patch-bdd.c
new file mode 100644
index 000000000000..512686ff0fcb
--- /dev/null
+++ b/devel/smv/files/patch-bdd.c
@@ -0,0 +1,51 @@
+--- bdd.c
++++ bdd.c
+@@ -113,7 +113,7 @@
+    /* Initialize a keytable. */
+    kp->n = n;
+    kp->elements_in_table = 0;
+-   kp->hash_table_buf = (bdd_ptr *)malloc(n*sizeof(bdd_ptr));
++   kp->hash_table_buf = (bdd_ptr *)smv_malloc(n*sizeof(bdd_ptr));
+ 
+    {  /* Initialize hash bin list pointers to NULL. */
+       register int i;
+@@ -139,7 +139,7 @@
+    /* Create key tables. */
+    create_keytable(&reduce_table, KEYTABLESIZE);
+    apply_cache_size = APPLY_CACHE_SIZE;
+-   apply_cache = (apply_rec *)malloc(sizeof(apply_rec)*apply_cache_size);
++   apply_cache = (apply_rec *)smv_malloc(sizeof(apply_rec)*apply_cache_size);
+    {
+      int i;
+      for(i=0;i<apply_cache_size;i++)apply_cache[i].op = 0;
+@@ -1446,7 +1446,7 @@
+ }
+ 
+ /* An "infinity" constant - big enough power of 2 not to care about */
+-#define INFINITY 1000
++#define SMV_INFINITY 1000
+ 
+ /* similar to auxcount_bdd, but computes log2 of the fraction */
+ 
+@@ -1457,18 +1457,18 @@
+   union {float a; bdd_ptr b;} temp;     /* very dangerous!!! */
+   double l,r;
+ 
+-  if(d==ZERO)return(-INFINITY); /* = log(0) */
++  if(d==ZERO)return(-SMV_INFINITY); /* = log(0) */
+   if(d==ONE)return(0.0);        /* = log2(1) */
+   temp.b = find_apply(COUNT_OP,d,ZERO);
+   if(temp.b==NULL) {
+     l = auxcount_bdd_log2(d->left,n);
+     r = auxcount_bdd_log2(d->right,n);
+     if(l < r) {
+-      if(r - l > INFINITY) temp.a = r;
++      if(r - l > SMV_INFINITY) temp.a = r;
+       else temp.a = l - 1.0 + log2(1.0 + pow(2.0,r-l));
+     }
+     else {
+-      if(l - r > INFINITY) temp.a = l;
++      if(l - r > SMV_INFINITY) temp.a = l;
+       else temp.a = r - 1.0 + log2(1.0 + pow(2.0,l-r));
+     }
+   }
diff --git a/devel/smv/files/patch-hash.c b/devel/smv/files/patch-hash.c
new file mode 100644
index 000000000000..006e32a1c5b1
--- /dev/null
+++ b/devel/smv/files/patch-hash.c
@@ -0,0 +1,17 @@
+--- hash.c
++++ hash.c
+@@ -7,12 +7,12 @@
+ int (*hash_fun)(),(*eq_fun)();
+ mgr_ptr mgr;
+ {
+-  hash_ptr res = (hash_ptr)malloc(sizeof(struct hash));
++  hash_ptr res = (hash_ptr)smv_malloc(sizeof(struct hash));
+   res->size = init_size;
+   res->hash_fun = hash_fun;
+   res->eq_fun = eq_fun;
+   res->mgr = mgr;
+-  res->tab = (rec_ptr *)malloc(init_size * sizeof(rec_ptr));
++  res->tab = (rec_ptr *)smv_malloc(init_size * sizeof(rec_ptr));
+   bzero(res->tab,init_size * sizeof(rec_ptr));
+   return(res);
+ }
diff --git a/devel/smv/files/patch-node.c b/devel/smv/files/patch-node.c
new file mode 100644
index 000000000000..dd897c152cb8
--- /dev/null
+++ b/devel/smv/files/patch-node.c
@@ -0,0 +1,19 @@
+--- node.c
++++ node.c
+@@ -609,7 +609,7 @@
+ node_ptr n;
+ int col;
+ {
+-  char *buf = (char *)malloc(option_print_node_length + 1);
++  char *buf = (char *)smv_malloc(option_print_node_length + 1);
+   int c,p;
+   if(buf == NULL) rpterr("Out of memory");
+   buf[0] = 0;
+@@ -623,7 +623,7 @@
+   }
+   fprintf(stream,"%s",buf);
+   if(!c)fprintf(stream,"...");
+-  free(buf);
++  smv_free(buf);
+   return(col + p);
+ }
diff --git a/devel/smv/files/patch-storage.c b/devel/smv/files/patch-storage.c
new file mode 100644
index 000000000000..718193d71749
--- /dev/null
+++ b/devel/smv/files/patch-storage.c
@@ -0,0 +1,39 @@
+--- storage.c
++++ storage.c
+@@ -9,7 +9,7 @@
+ {
+ #ifdef MACH
+   mach_init();		/* needed to make sbrk() work */
+-#endif MACH
++#endif
+   /* addrfree points to the first free byte
+      addrlimit points to the memory limit */
+     addrfree = addrlimit = (char *) sbrk(0);
+@@ -34,7 +34,7 @@
+ }
+ 
+ /* provide malloc for miscellaneuos storage allocation */
+-char *malloc(n)
++char* smv_malloc(n)
+ int n;
+ {
+   if(n % 4)n=n+4-(n%4);  /* always allocate multiple of four bytes */
+@@ -47,7 +47,7 @@
+ }
+ 
+ /* very simple implementation of free */
+-void free(p)
++void smv_free(p)
+ char *p;
+ {
+   return;
+@@ -61,7 +61,7 @@
+ mgr_ptr new_mgr(rec_size)
+ int rec_size;
+ {
+-  register mgr_ptr mp = (mgr_ptr)malloc(sizeof(struct mgr));
++  register mgr_ptr mp = (mgr_ptr)smv_malloc(sizeof(struct mgr));
+   mp->free.link = 0;
+   mp->rec_size = rec_size;
+   mp->count = 0;
+diff -ru ./storage.h /usr3/marc/research/hagen/10-ws0304/77075 Model Checking/praktikum/smv/smv/storage.h
diff --git a/devel/smv/files/patch-storage.h b/devel/smv/files/patch-storage.h
new file mode 100644
index 000000000000..4b72cc93ed66
--- /dev/null
+++ b/devel/smv/files/patch-storage.h
@@ -0,0 +1,13 @@
+--- storage.h
++++ storage.h
+@@ -12,8 +12,8 @@
+ #define ALLOCSIZE (2<<15)
+ 
+ void init_storage();
+-char *malloc();
+-void free();
++char* smv_malloc();
++void smv_free();
+ mgr_ptr new_mgr();
+ rec_ptr new_rec(),dup_rec();
+ void free_rec();
diff --git a/devel/smv/files/patch-string.c b/devel/smv/files/patch-string.c
new file mode 100644
index 000000000000..3c5e8e9b54dd
--- /dev/null
+++ b/devel/smv/files/patch-string.c
@@ -0,0 +1,10 @@
+--- string.c
++++ string.c
+@@ -35,7 +35,7 @@
+   string_rec a,*res;
+   a.text = x;
+   if(res = (string_ptr)find_hash(string_hash,&a))return(res);
+-  a.text = (char *)strcpy((char *)malloc(strlen(x)+1),x);
++  a.text = (char *)strcpy((char *)smv_malloc(strlen(x)+1),x);
+   return((string_ptr)insert_hash(string_hash,&a));
+ }
diff --git a/devel/smv/pkg-descr b/devel/smv/pkg-descr
new file mode 100644
index 000000000000..42f263fe9525
--- /dev/null
+++ b/devel/smv/pkg-descr
@@ -0,0 +1,14 @@
+The SMV (Symbolic Model Verifier) system is a tool for 
+checking finite state systems against specifications 
+in the temporal logic CTL (Computational Tree Logic). 
+
+One specifies the finite state system (finite automaton,
+Mealy machine, full adder circuit, ..) as a Kripke 
+structure in the SMV language and provides specificaations 
+in CTL. The model checking algorithm allows to determine 
+if the Kripke structure fulfills the specifications.
+
+WWW: http://www-2.cs.cmu.edu/~modelcheck/smv.html
+
+Marc E.E. van Woerkom
+marc.vanwoerkom@fernuni-hagen.de
diff --git a/devel/smv/pkg-plist b/devel/smv/pkg-plist
new file mode 100644
index 000000000000..61e25ba3026b
--- /dev/null
+++ b/devel/smv/pkg-plist
@@ -0,0 +1,20 @@
+bin/smv
+share/smv/smv-mode.el
+%%PORTDOCS%%%%DOCSDIR%%/NEW
+%%PORTDOCS%%%%DOCSDIR%%/README
+%%PORTDOCS%%%%DOCSDIR%%/smvmanual.ps
+%%PORTDOCS%%%%EXAMPLESDIR%%/counter.smv
+%%PORTDOCS%%%%EXAMPLESDIR%%/dme1.smv
+%%PORTDOCS%%%%EXAMPLESDIR%%/dme2.smv
+%%PORTDOCS%%%%EXAMPLESDIR%%/featuring.smv
+%%PORTDOCS%%%%EXAMPLESDIR%%/gigamax.smv
+%%PORTDOCS%%%%EXAMPLESDIR%%/mutex.smv
+%%PORTDOCS%%%%EXAMPLESDIR%%/mutex1.smv
+%%PORTDOCS%%%%EXAMPLESDIR%%/periodic.smv
+%%PORTDOCS%%%%EXAMPLESDIR%%/ring.smv
+%%PORTDOCS%%%%EXAMPLESDIR%%/semaphore.smv
+%%PORTDOCS%%%%EXAMPLESDIR%%/short.smv
+%%PORTDOCS%%%%EXAMPLESDIR%%/syncarb5.smv
+%%PORTDOCS%%@dirrm %%DOCSDIR%%
+%%PORTDOCS%%@dirrm %%EXAMPLESDIR%%
+@dirrm share/smv