diff options
| -rw-r--r-- | math/Makefile | 1 | ||||
| -rw-r--r-- | math/ltl2ba/Makefile | 28 | ||||
| -rw-r--r-- | math/ltl2ba/distinfo | 2 | ||||
| -rw-r--r-- | math/ltl2ba/pkg-descr | 11 |
4 files changed, 42 insertions, 0 deletions
diff --git a/math/Makefile b/math/Makefile index 3573a3313f7d..782c51a5acbd 100644 --- a/math/Makefile +++ b/math/Makefile @@ -176,6 +176,7 @@ SUBDIR += lll_spect SUBDIR += lp_solve SUBDIR += ltl + SUBDIR += ltl2ba SUBDIR += lybniz SUBDIR += matharray SUBDIR += mathomatic 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/ |