From fc609057d6e435036ddbe40e16dc5ad1d47ef9ae Mon Sep 17 00:00:00 2001 From: Thomas Medioni Date: Tue, 20 Jun 2017 11:50:16 +0200 Subject: [PATCH] streett_like: clear the pair vector when non Streett-like When an acceptance condition is not Streett-like, is_streett_like now clears the rs_pair vector parameter before returning. Fixes #270. * spot/twa/acc.cc: Clear the pair vector. * spot/twaalgos/totgba.cc: Stop calling streett_to_generalized_buchi() when the acceptance condition is not Streett-like. --- spot/twa/acc.cc | 21 +++++++++++++++------ spot/twaalgos/totgba.cc | 4 ++-- 2 files changed, 17 insertions(+), 8 deletions(-) diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index b1c4a0d73..be3837658 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -479,9 +479,9 @@ namespace spot s = 5; } else if (mainop != highop) - { - return false; - } + { + return false; + } while (s) { auto op = code[--s].sub.op; @@ -494,7 +494,10 @@ namespace spot acc_cond::mark_t inf(0U); if (op == singleop && m.count() != 1) - return false; + { + pairs.clear(); + return false; + } for (unsigned mark: m.sets()) { if (op == acc_cond::acc_op::Fin) @@ -507,7 +510,10 @@ namespace spot else { if (op != lowop || size != 4) - return false; + { + pairs.clear(); + return false; + } auto o1 = code[--s].sub.op; auto m1 = code[--s].mark; @@ -527,7 +533,10 @@ namespace spot || o2 != acc_cond::acc_op::Inf || m1.count() != 1 || m2.count() != 1) - return false; + { + pairs.clear(); + return false; + } pairs.emplace_back(m1, m2); } } diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index d74d1d27c..01bbc0c5d 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -331,8 +331,8 @@ namespace spot }(); std::vector pairs; - in->acc().is_streett_like(pairs); - if (min == 0 || min > pairs.size()) + bool res = in->acc().is_streett_like(pairs); + if (!res || min == 0 || min > pairs.size()) return nullptr; else return streett_to_generalized_buchi(in);