diff options
| author | Brendan Fabeny <bf@FreeBSD.org> | 2011-05-27 18:11:32 +0000 |
|---|---|---|
| committer | Brendan Fabeny <bf@FreeBSD.org> | 2011-05-27 18:11:32 +0000 |
| commit | dc711f5047a170fc538e72f013ff1eeb838ac1f7 (patch) | |
| tree | 40dcae70a6dd4c7e6181bead6f4c360adb7fb2ea /math/ltl2ba | |
| parent | 55452e601aee06d7e661223420d628c27e0c21e6 (diff) | |
| download | ports-dc711f5047a170fc538e72f013ff1eeb838ac1f7.tar.gz ports-dc711f5047a170fc538e72f013ff1eeb838ac1f7.zip | |
Add ltl2ba 1.1, fast translation from LTL formulae to Buechi automata.
Notes
Notes:
svn path=/head/; revision=274737
Diffstat (limited to 'math/ltl2ba')
| -rw-r--r-- | math/ltl2ba/Makefile | 28 | ||||
| -rw-r--r-- | math/ltl2ba/distinfo | 2 | ||||
| -rw-r--r-- | math/ltl2ba/pkg-descr | 11 |
3 files changed, 41 insertions, 0 deletions
diff --git a/math/ltl2ba/Makefile b/math/ltl2ba/Makefile new file mode 100644 index 000000000000..03bda7785bee --- /dev/null +++ b/math/ltl2ba/Makefile @@ -0,0 +1,28 @@ +# New ports collection makefile for: ltl2ba +# Date created: 25 May 2011 +# Whom: b.f. <bf@FreeBSD.org> +# +# $FreeBSD$ +# + +PORTNAME= ltl2ba +PORTVERSION= 1.1 +CATEGORIES= math +MASTER_SITES= http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ LOCAL/bf + +MAINTAINER= bf@FreeBSD.org +COMMENT= Fast translation from LTL formulae to Buechi automata + +LICENSE= GPLv2 + +ALL_TARGET= ltl2ba +CFLAGS+= -DNXT +PLIST_FILES= bin/ltl2ba + +post-patch: + ${REINPLACE_CMD} -e '/^CC=/d' -e '/^CFLAGS=/d' ${WRKSRC}/Makefile + +do-install: + ${INSTALL_PROGRAM} ${WRKSRC}/ltl2ba ${PREFIX}/bin/ + +.include <bsd.port.mk> diff --git a/math/ltl2ba/distinfo b/math/ltl2ba/distinfo new file mode 100644 index 000000000000..249400dcc978 --- /dev/null +++ b/math/ltl2ba/distinfo @@ -0,0 +1,2 @@ +SHA256 (ltl2ba-1.1.tar.gz) = a66bf05bc3fd030f19fd0114623d263870d864793b1b0a2ccf6ab6a40e7be09b +SIZE (ltl2ba-1.1.tar.gz) = 29629 diff --git a/math/ltl2ba/pkg-descr b/math/ltl2ba/pkg-descr new file mode 100644 index 000000000000..68a2cfafde00 --- /dev/null +++ b/math/ltl2ba/pkg-descr @@ -0,0 +1,11 @@ +ltl2ba implements an algorithm of P. Gastin and D. Oddoux to generate +Buechi automata from linear temporal logic (LTL) formulae. This +algorithm generates a very weak alternating automaton and then +transforms it into a Buechi automaton, using a generalized Buechi +automaton as an intermediate step. Each automaton is simplified +on-the-fly in order to save memory and time. As usual the LTL formula +is simplified before any treatment. ltl2ba is more efficient than +Spin 3.4.1, with regard to the the size of the resulting automaton, +the time of the computation, and the memory used. + +WWW: http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ |