aboutsummaryrefslogtreecommitdiff
path: root/math/ltl2ba
diff options
context:
space:
mode:
authorBrendan Fabeny <bf@FreeBSD.org>2011-05-27 18:11:32 +0000
committerBrendan Fabeny <bf@FreeBSD.org>2011-05-27 18:11:32 +0000
commitdc711f5047a170fc538e72f013ff1eeb838ac1f7 (patch)
tree40dcae70a6dd4c7e6181bead6f4c360adb7fb2ea /math/ltl2ba
parent55452e601aee06d7e661223420d628c27e0c21e6 (diff)
downloadports-dc711f5047a170fc538e72f013ff1eeb838ac1f7.tar.gz
ports-dc711f5047a170fc538e72f013ff1eeb838ac1f7.zip
Notes
Diffstat (limited to 'math/ltl2ba')
-rw-r--r--math/ltl2ba/Makefile28
-rw-r--r--math/ltl2ba/distinfo2
-rw-r--r--math/ltl2ba/pkg-descr11
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/