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.
This commit is contained in:
parent
676ab41f6f
commit
89b9cc5fd5
2 changed files with 23 additions and 3 deletions
|
|
@ -325,9 +325,13 @@ namespace spot
|
||||||
|
|
||||||
unsigned num_acc = 0;
|
unsigned num_acc = 0;
|
||||||
is >> num_acc;
|
is >> num_acc;
|
||||||
std::string rest;
|
|
||||||
std::getline(is, rest);
|
int type;
|
||||||
if (rest[0] == 't' || rest[0] == 'T')
|
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,
|
return lbtt_read_tgba(num_states, num_acc, is, error, dict,
|
||||||
env, envacc);
|
env, envacc);
|
||||||
else
|
else
|
||||||
|
|
|
||||||
|
|
@ -65,3 +65,19 @@ test "`cat size | sed -n 's/states: //p'`" = 4
|
||||||
test "`cat size | sed -n 's/transitions: //p'`" = 6
|
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
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue