* lbtt/: New directory. Contains a patched version of lbtt 1.0.1.

* Makefile.am (MAYBE_LBTT): New variables.
(SUBDIRS): Add $(MAYBE_LBTT).
(EXTRA_DIST): Add m4/lbtt.m4.
* configure.ac: Call AX_CHECK_LBTT.
* m4/lbtt.m4: New file.
* src/tgbatest/Makefile.am (check_PROGRAMS): Add spotlbtt.
(spotlbtt_SOURCES): New variables.
(TESTS): Add spotlbtt.test.
(CLEANFILE): Add config.
* src/tgbatest/defs.in (top_builddir, LBTT, LBTT_TRANSLATE): New
substitutions.
* src/tgbatest/spotlbtt.cc, src/tgbatest/spotlbtt.test: New files.

ChangeLog

@@ -1,5 +1,19 @@
 2003-07-09  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* lbtt/: New directory.  Contains a patched version of lbtt 1.0.1.
+	* Makefile.am (MAYBE_LBTT): New variables.
+	(SUBDIRS): Add $(MAYBE_LBTT).
+	(EXTRA_DIST): Add m4/lbtt.m4.
+	* configure.ac: Call AX_CHECK_LBTT.
+	* m4/lbtt.m4: New file.
+	* src/tgbatest/Makefile.am (check_PROGRAMS): Add spotlbtt.
+	(spotlbtt_SOURCES): New variables.
+	(TESTS): Add spotlbtt.test.
+	(CLEANFILE): Add config.
+	* src/tgbatest/defs.in (top_builddir, LBTT, LBTT_TRANSLATE): New
+	substitutions.
+	* src/tgbatest/spotlbtt.cc, src/tgbatest/spotlbtt.test: New files.
+
 	* src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next):
 	Fix computation of states sharing the same accepting set.
 

Makefile.am

@@ -1,8 +1,11 @@
 if WITH_INCLUDED_BUDDY
   MAYBE_BUDDY = buddy
 endif WITH_INCLUDED_BUDDY
+if WITH_INCLUDED_LBTT
+  MAYBE_LBTT = lbtt
+endif WITH_INCLUDED_LBTT
 
-SUBDIRS = $(MAYBE_BUDDY) doc src wrap iface
+SUBDIRS = $(MAYBE_BUDDY) $(MAYBE_LBTT) doc src wrap iface
 
 ACLOCAL_AMFLAGS = -I m4
-EXTRA_DIST = m4/gccwarn.m4 m4/pypath.m4 m4/buddy.m4 HACKING
+EXTRA_DIST = m4/gccwarn.m4 m4/pypath.m4 m4/buddy.m4 m4/lbtt.m4 HACKING

configure.ac

@@ -13,6 +13,7 @@ AC_PROG_YACC
 AC_LANG(C++)
 
 AX_CHECK_BUDDY
+AX_CHECK_LBTT
 
 AC_PROG_LIBTOOL
 

m4/lbtt.m4

@@ -0,0 +1,26 @@
+AC_DEFUN([AX_CHECK_LBTT], [
+  AC_ARG_WITH([included-lbtt],
+	      [AC_HELP_STRING([--with-included-lbtt],
+			      [use the LBTT program inclued here])])
+  AS_IF([AM_RUN_LOG([lbtt --help | grep spot])],
+        [need_included_lbtt=no],
+	[need_included_lbtt=yes])
+
+  if test "$need_included_lbtt" = yes; then
+     if test "$with_included_lbtt" = no; then
+       AC_MSG_ERROR([Cannot find lbtt.  Please install lbtt first, 
+	             or configure with --with-included-lbtt])
+     else
+	with_included_lbtt=yes
+     fi
+  fi
+
+  if test "$with_included_lbtt" = yes;  then
+     AC_CONFIG_SUBDIRS([lbtt])
+     LBTT='${top_builddir}/lbtt/src/lbtt'
+     LBTT_TRANSLATE='${top_builddir}/lbtt/src/lbtt-translate'
+  fi
+  AM_CONDITIONAL([WITH_INCLUDED_LBTT], [test "$with_included_lbtt" = yes])
+  AC_SUBST([LBTT])
+  AC_SUBST([LBTT_TRANSLATE])
+])

src/tgbatest/.cvsignore

@@ -14,3 +14,4 @@ explprod
 *.dot
 tripprod
 mixprod
+spotlbtt

src/tgbatest/Makefile.am

@@ -12,7 +12,8 @@ check_PROGRAMS = \
   bddprod \
   explprod \
   tripprod \
-  mixprod
+  mixprod \
+  spotlbtt
 
 # Keep this sorted alphabetically.
 bddprod_SOURCES  = ltlprod.cc
@@ -25,6 +26,7 @@ mixprod_SOURCES  = mixprod.cc
 readsave_SOURCES = readsave.cc
 tgbaread_SOURCES = tgbaread.cc
 tripprod_SOURCES = tripprod.cc
+spotlbtt_SOURCES = spotlbtt.cc
 
 # Keep this sorted by STRENGTH.  Test basic things first,
 # because such failures will be easier to diagnose and fix.
@@ -37,8 +39,9 @@ TESTS = \
   bddprod.test \
   explprod.test \
   tripprod.test \
-  mixprod.test
+  mixprod.test \
+  spotlbtt.test
 
 EXTRA_DIST = $(TESTS)
 
-CLEANFILES = input input1 input2 input3 stdout expected
+CLEANFILES = input input1 input2 input3 stdout expected config

src/tgbatest/defs.in

@@ -26,6 +26,9 @@ test -z "$VERBOSE" && exec >/dev/null 2>&1
 echo "== Running test $0"
 
 DOT='@DOT@'
+top_builddir='@top_builddir@'
+LBTT="@LBTT@"
+LBTT_TRANSLATE="@LBTT_TRANSLATE@"
 
 # Turn on shell traces when VERBOSE=x.
 if test "x$VERBOSE" = xx; then

src/tgbatest/spotlbtt.cc

@@ -0,0 +1,63 @@
+#include <iostream>
+#include <fstream>
+#include <cassert>
+#include <string>
+#include "ltlvisit/destroy.hh"
+#include "ltlast/allnodes.hh"
+#include "ltlparse/public.hh"
+#include "tgbaalgos/ltl2tgba.hh"
+#include "tgbaalgos/lbtt.hh"
+
+
+void
+syntax(char* prog)
+{
+  std::cerr << "Usage: "<< prog << " file" << std::endl;
+  exit(2);
+}
+
+int
+main(int argc, char** argv)
+{
+  int exit_code = 0;
+
+  if (argc !=  2)
+    syntax(argv[0]);
+
+  std::ifstream fin(argv[1]);
+  if (! fin)
+    {
+      std::cerr << "Cannot open " << argv[1] << std::endl;
+      exit(2);
+    }
+
+  std::string input;
+  if (! std::getline(fin, input, '\0'))
+    {
+      std::cerr << "Cannot read " << argv[1] << std::endl;
+      exit(2);      
+    }
+
+  spot::ltl::environment& env(spot::ltl::default_environment::instance());
+  spot::ltl::parse_error_list pel;
+  spot::ltl::formula* f = spot::ltl::parse(input, pel, env);
+
+  exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel);
+
+  if (f)
+    {
+      spot::tgba_bdd_concrete a = spot::ltl_to_tgba(f);
+      spot::ltl::destroy(f);
+      spot::lbtt_reachable(std::cout, a);
+    }
+  else
+    {
+      exit_code = 1;
+    }
+
+  assert(spot::ltl::atomic_prop::instance_count() == 0);
+  assert(spot::ltl::unop::instance_count() == 0);
+  assert(spot::ltl::binop::instance_count() == 0);
+  assert(spot::ltl::multop::instance_count() == 0);
+  return exit_code;
+}

src/tgbatest/spotlbtt.test

@@ -0,0 +1,45 @@
+#!/bin/sh
+
+. ./defs
+
+set -e
+
+cat > config <<EOF
+Algorithm
+{
+   Name = "Spot"
+   Path = "${LBTT_TRANSLATE} --spot ./spotlbtt"
+   Enabled = yes
+}
+
+GlobalOptions
+{
+   Rounds = 1
+   Interactive = Never
+#   Verbosity = 5
+}
+
+FormulaOptions
+{
+
+  AbbreviatedOperators = Yes
+  GenerateMode = Normal
+  OutputMode = Normal
+  PropositionPriority = 50
+
+  TruePriority = 1
+  FalsePriority = 1
+
+  AndPriority = 10
+  OrPriority = 10
+  
+  BeforePriority = 0
+  StrongReleasePriority = 0
+  WeakUntilPriority = 0
+
+  DefaultOperatorPriority = 5
+}
+EOF
+
+${LBTT}
+rm config