From 2ea5de4d680ab90136ef22e19ab46398b8e58c7e Mon Sep 17 00:00:00 2001 From: Pav Lucistnik Date: Sat, 13 Dec 2003 01:22:09 +0000 Subject: 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 --- devel/smv/Makefile | 48 ++++++++++++++++++++++++++++++++++++++ devel/smv/distinfo | 1 + devel/smv/files/patch-bdd.c | 51 +++++++++++++++++++++++++++++++++++++++++ devel/smv/files/patch-hash.c | 17 ++++++++++++++ devel/smv/files/patch-node.c | 19 +++++++++++++++ devel/smv/files/patch-storage.c | 39 +++++++++++++++++++++++++++++++ devel/smv/files/patch-storage.h | 13 +++++++++++ devel/smv/files/patch-string.c | 10 ++++++++ devel/smv/pkg-descr | 14 +++++++++++ devel/smv/pkg-plist | 20 ++++++++++++++++ 10 files changed, 232 insertions(+) create mode 100644 devel/smv/Makefile create mode 100644 devel/smv/distinfo create mode 100644 devel/smv/files/patch-bdd.c create mode 100644 devel/smv/files/patch-hash.c create mode 100644 devel/smv/files/patch-node.c create mode 100644 devel/smv/files/patch-storage.c create mode 100644 devel/smv/files/patch-storage.h create mode 100644 devel/smv/files/patch-string.c create mode 100644 devel/smv/pkg-descr create mode 100644 devel/smv/pkg-plist (limited to 'devel/smv') 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 +# +# $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 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;ileft,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 -- cgit v1.2.3