cpet/freebsd-ports
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

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

Browse Source 
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>
This commit is contained in:
Pav Lucistnik 2003-12-13 01:22:09 +00:00
parent 70cd7e885b
commit 2ea5de4d68
Notes: svn2git 2021-03-31 03:12:20 +00:00 
svn path=/head/; revision=95707
11 changed files with 233 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
devel/Makefile
View File

@ -1061,6 +1061,7 @@
SUBDIR += simulavr
SUBDIR += sip
SUBDIR += skalibs
SUBDIR += smv
SUBDIR += soup
SUBDIR += sourcenav
SUBDIR += sparc-rtems-binutils

48
devel/smv/Makefile Normal file
View File

@ -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>

1
devel/smv/distinfo Normal file
View File

@ -0,0 +1 @@
MD5 (smv.r2.5.4.3.tar.gz) = dd1a7ebcbac935845fc73eb8957386cb

51
devel/smv/files/patch-bdd.c Normal file
View File

@ -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));
}
}

17
devel/smv/files/patch-hash.c Normal file
View File

@ -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);
}

19
devel/smv/files/patch-node.c Normal file
View File

@ -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);
}

39
devel/smv/files/patch-storage.c Normal file
View File

@ -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

13
devel/smv/files/patch-storage.h Normal file
View File

@ -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();

10
devel/smv/files/patch-string.c Normal file
View File

@ -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));
}

14
devel/smv/pkg-descr Normal file
View File

@ -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

20
devel/smv/pkg-plist Normal file
View File

@ -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