From b1dbfed17f19b8d417233dabee1349acb9e6abb4 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 6 Nov 2010 15:56:50 +0100
Subject: [PATCH] * src/tgbatest/neverclaimread.test: Check that Spot can read
 the neverclaims it outputs.

---
 ChangeLog                        | 5 +++++
 src/tgbatest/neverclaimread.test | 5 ++---
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 522aab474..fd9bb3e52 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,8 @@
+2010-11-06  Alexandre Duret-Lutz  <adl@gnu.org>
+
+	* src/tgbatest/neverclaimread.test: Check that Spot can read the
+	neverclaims it outputs.
+
 2010-11-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Do not output a counterexample by default in ltl2tgba, introduce
diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test
index 28d72a7d8..28ec275a2 100755
--- a/src/tgbatest/neverclaimread.test
+++ b/src/tgbatest/neverclaimread.test
@@ -95,9 +95,6 @@ EOF
 grep input: stderr >> stderrfilt
 diff stderrfilt expected
 
-# Skip the rest of this test if neither Spin nor ltl2ba are installed.
-test -n "$SPIN$LTL2BA" || exit
-
 cat >formulae<<EOF
 a
 <>[] a
@@ -116,4 +113,6 @@ do
 	$LTL2BA -f "$f" > f.ltl2ba
 	run 0 ../ltl2tgba -E -Pf.tgba -XN f.ltl2ba
     fi
+    run 0 ../ltl2tgba -DS -NN -f "$f" > f.spot
+    run 0 ../ltl2tgba -E -Pf.tgba -XN f.spot
 done  <formulae