diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index a86c47e3a..bc65d2048 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -169,9 +169,7 @@ namespace spot const ltl::formula* af = acc_f[n] = envacc.require(s.str()); aut->declare_acceptance_condition(af->clone()); } - std::vector acc_b(num_acc); - for (unsigned n = 0; n < num_acc; ++n) - acc_b[n] = aut->get_acceptance_condition(acc_f[n]); + std::map acc_b; for (unsigned n = 0; n < num_states; ++n) { @@ -197,13 +195,25 @@ namespace spot is >> acc_n; if (acc_n == -1) break; - if (acc_n < 0 || (unsigned)acc_n >= num_acc) + std::map::const_iterator i = acc_b.find(acc_n); + if (i != acc_b.end()) { - error += "invalid acceptance set"; - goto fail; + acc |= i->second; + } + else + { + size_t s = acc_b.size(); + if (s >= num_acc) + { + error += "more acceptance sets used than declared"; + goto fail; + } + bdd a = aut->get_acceptance_condition(acc_f[s]); + acc_b[acc_n] = a; + acc |= a; } - acc |= acc_b[acc_n]; } + std::string guard; std::getline(is, guard); ltl::parse_error_list pel; @@ -242,9 +252,7 @@ namespace spot const ltl::formula* af = acc_f[n] = envacc.require(s.str()); aut->declare_acceptance_condition(af->clone()); } - std::vector acc_b(num_acc); - for (unsigned n = 0; n < num_acc; ++n) - acc_b[n] = aut->get_acceptance_condition(acc_f[n]); + std::map acc_b; for (unsigned n = 0; n < num_states; ++n) { @@ -262,12 +270,23 @@ namespace spot is >> acc_n; if (acc_n == -1) break; - if (acc_n < 0 || (unsigned)acc_n >= num_acc) + std::map::const_iterator i = acc_b.find(acc_n); + if (i != acc_b.end()) { - error += "invalid acceptance set"; - goto fail; + acc |= i->second; + } + else + { + size_t s = acc_b.size(); + if (s >= num_acc) + { + error += "more acceptance sets used than declared"; + goto fail; + } + bdd a = aut->get_acceptance_condition(acc_f[s]); + acc_b[acc_n] = a; + acc |= a; } - acc |= acc_b[acc_n]; } // Read the transitions. diff --git a/src/tgbatest/lbttparse.test b/src/tgbatest/lbttparse.test index 6f3970619..ff552e94b 100755 --- a/src/tgbatest/lbttparse.test +++ b/src/tgbatest/lbttparse.test @@ -81,3 +81,21 @@ 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 +# Another example from wring2lbtt (or modella), showing that the +# acceptance set of the state is not always numbered from 0. +cat >wring2lbtt2 < size +test "`cat size | sed -n 's/states: //p'`" = 6 +test "`cat size | sed -n 's/transitions: //p'`" = 9