Allow lbtt not to be built, and skip relevant tests.

* m4/lbtt.m4: Turn the missing lbtt error into a warning,
and do not configure lbtt wen --without-included-lbtt is specified.
* bench/ltl2tgba/defs.in: Abort if lbtt is missing.
* src/tgbatest/defs.in (need_lbtt): New function to skip
tests that require lbtt.
* src/tgbatest/babiak.test, src/tgbatest/ltl2neverclaim.test,
src/tgbatest/spotlbtt.test: Call need_lbtt.

bench/ltl2tgba/defs.in

@@ -1,6 +1,6 @@
-# -*- shell-script; coding: utf-8 -*-
-# Copyright (C) 2012 Laboratoire de Recherche et Développement de
-# l'Epita (LRDE).
+# -*- mode: shell-script; coding: utf-8 -*-
+# Copyright (C) 2012 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
 # Copyright (C) 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
@@ -48,6 +48,11 @@ MODELLA="@MODELLA@"
 SPIN="@SPIN@"
 WRING2LBTT="@WRING2LBTT@"
 
+($LBTT --version) >/dev/null 2>&1 || {
+  echo "$LBTT not available.  Try configuring with --with-included-lbtt."
+  exit 77
+}
+
 for var in LBT LTL2BA LTL3BA LTL2NBA MODELLA SPIN WRING2LBTT
 do
   if eval 'test -z "$'$var'"'; then

m4/lbtt.m4

@@ -8,8 +8,8 @@ AC_DEFUN([AX_CHECK_LBTT], [
 
   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])
+       AC_MSG_WARN([Cannot find lbtt, needed for test-suite and benchmarks.
+Please install lbtt first, or configure with --with-included-lbtt.])
      else
        with_included_lbtt=yes
      fi
@@ -22,10 +22,17 @@ AC_DEFUN([AX_CHECK_LBTT], [
      LBTT=lbtt
      LBTT_TRANSLATE=lbtt-translate
   fi
-  # We always configure lbtt, this is needed to ensure
-  # it gets distributed properly.  Whether with_included_buddy is
-  # set or not affects whether we *use* or *build* lbtt.
+
+  # We always configure lbtt, even if it is not built to ensure it
+  # gets distributed properly.  However, when someone uses
+  # --without-included-lbtt explicitely, we assume he might be trying
+  # to build Spot on a system where lbtt cannot build (e.g. MinGW) and
+  # where lbtt/configure will fail.  So we don't run the sub-configure
+  # only in this case.  On such a setup, "make distcheck" will break,
+  # but so probably isn't important.
+  if test "$with_included_lbtt" != no; then
     AC_CONFIG_SUBDIRS([lbtt])
+  fi
 
   AM_CONDITIONAL([WITH_INCLUDED_LBTT], [test "$with_included_lbtt" = yes])
   AC_SUBST([LBTT])

src/tgbatest/babiak.test

@@ -1,5 +1,6 @@
 #!/bin/sh
-# Copyright (C) 2011 Laboratoire de Recherche et Développement
+# -*- coding: utf-8 -*-
+# Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -28,6 +29,7 @@
 # buildfarm will timeout if it does).
 
 . ./defs
+need_lbtt
 
 set -e
 
@@ -110,6 +112,3 @@ EOF
 
 ${LBTT} --formulafile=formulae
 rm config
-
-
-

src/tgbatest/defs.in

@@ -1,8 +1,8 @@
-# -*- shell-script -*-
-# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+# -*- mode: shell-script; coding: utf-8 -*-
+# Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 # Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
-# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
 # This file is part of Spot, a model checking library.
@@ -51,11 +51,10 @@ rm -rf $testSubDir > /dev/null 2>&1
 mkdir $testSubDir
 cd $testSubDir
 
-# Adjust srcdir now that we are in a subdirectory.  We still want to
-# source directory corresponding to the build directory that contains
-# $testSubDir.
+# Adjust srcdir now that we are in a subdirectory.  We still want
+# $srcdir to point to the source directory corresponding to the build
+# directory that contains $testSubDir.
 case $srcdir in
-  # I
   [\\/$]* | ?:[\\/]* );;
   *) srcdir=../$srcdir
 esac
@@ -68,6 +67,12 @@ VALGRIND='@VALGRIND@'
 SPIN='@SPIN@'
 LTL2BA='@LTL2BA@'
 
+need_lbtt()
+{
+  # LBTT may not have been installed or compiled.
+  ("$LBTT" --version) || exit 77
+}
+
 run()
 {
   expected_exitcode=$1

src/tgbatest/ltl2neverclaim.test

@@ -1,5 +1,6 @@
 #!/bin/sh
-# Copyright (C) 2010 Laboratoire de Recherche et Développement
+# -*- coding: utf-8 -*-
+# Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -19,7 +20,7 @@
 # Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
 # 02111-1307, USA.
 
-# Do some quick translations to make sure the neverclaim produced by
+# Do some quick translations to make sure the neverclaims produced by
 # spot actually look correct!
 
 # This test is separate from spotlbtt.test, because lbtt-translate
@@ -27,6 +28,7 @@
 # Spin.
 
 . ./defs
+need_lbtt
 
 set -e
 

src/tgbatest/spotlbtt.test

@@ -27,6 +27,7 @@
 echo 'This test can take as long as 15 minutes on a 2GHz Pentium 4.'
 
 . ./defs
+need_lbtt
 
 set -e