From 89b9cc5fd56decb926d84eb39822a46e5840b602 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 18 Oct 2012 13:58:38 +0200
Subject: [PATCH] lbttparse: make sure we parse wring2lbtt's output

* src/tgbaalgos/lbtt.cc: Do not expect a new line after the number of
acceptance conditions.
* src/tgbatest/lbttparse.test: Add a test case.
---
 src/tgbaalgos/lbtt.cc       | 10 +++++++---
 src/tgbatest/lbttparse.test | 16 ++++++++++++++++
 2 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc
index 19d8b06de..a86c47e3a 100644
--- a/src/tgbaalgos/lbtt.cc
+++ b/src/tgbaalgos/lbtt.cc
@@ -325,9 +325,13 @@ namespace spot
 
     unsigned num_acc = 0;
     is >> num_acc;
-    std::string rest;
-    std::getline(is, rest);
-    if (rest[0] == 't' || rest[0] == 'T')
+
+    int type;
+    type = is.peek();
+    if (type == 't' || type == 'T' || type == 's' || type == 'S')
+      type = is.get();
+
+    if (type == 't' || type == 'T')
       return lbtt_read_tgba(num_states, num_acc, is, error, dict,
 			    env, envacc);
     else
diff --git a/src/tgbatest/lbttparse.test b/src/tgbatest/lbttparse.test
index ed8fd082a..6f3970619 100755
--- a/src/tgbatest/lbttparse.test
+++ b/src/tgbatest/lbttparse.test
@@ -65,3 +65,19 @@ test "`cat size | sed -n 's/states: //p'`" = 4
 test "`cat size | sed -n 's/transitions: //p'`" = 6
 
 
+# This kind of output is returned by wring2lbtt, on the same formula.
+# (Newer versions of LBTT reject this input with missing new lines.)
+cat >wring2lbtt <<EOF
+4 1 0 1 -1 1 p0
+2 p1
+-1 1 0 -1 1 p0
+2 p1
+-1 2 0 0 -1 3 t
+-1 3 0 0 -1 3 t
+-1
+EOF
+
+run 0 ../ltl2tgba -ks -XL wring2lbtt > size
+test "`cat size | sed -n 's/states: //p'`" = 4
+test "`cat size | sed -n 's/transitions: //p'`" = 6
+