aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--devel/Makefile1
-rw-r--r--devel/smv/Makefile48
-rw-r--r--devel/smv/distinfo1
-rw-r--r--devel/smv/files/patch-bdd.c51
-rw-r--r--devel/smv/files/patch-hash.c17
-rw-r--r--devel/smv/files/patch-node.c19
-rw-r--r--devel/smv/files/patch-storage.c39
-rw-r--r--devel/smv/files/patch-storage.h13
-rw-r--r--devel/smv/files/patch-string.c10
-rw-r--r--devel/smv/pkg-descr14
-rw-r--r--devel/smv/pkg-plist20
11 files changed, 233 insertions, 0 deletions
diff --git a/devel/Makefile b/devel/Makefile
index d2b5a83111e9..41bfb8d04f2b 100644
--- a/devel/Makefile
+++ b/devel/Makefile
@@ -1061,6 +1061,7 @@
SUBDIR += simulavr
SUBDIR += sip
SUBDIR += skalibs
+ SUBDIR += smv
SUBDIR += soup
SUBDIR += sourcenav
SUBDIR += sparc-rtems-binutils
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-01 14:41:06 +0000