From 1b4002401a72abd00122be60b644ab2018db15b8 Mon Sep 17 00:00:00 2001 From: Alexandre GBAGUIDI AISSE Date: Tue, 10 Oct 2017 15:20:08 +0200 Subject: [PATCH] spot: small factorisations, improvements and typos * spot/tl/hierarchy.cc: Factorisations, improvements. * spot/twaalgos/totgba.cc: Typos. --- spot/tl/hierarchy.cc | 6 +++--- spot/twaalgos/totgba.cc | 1 - 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/spot/tl/hierarchy.cc b/spot/tl/hierarchy.cc index f3c90f652..08ff27a52 100644 --- a/spot/tl/hierarchy.cc +++ b/spot/tl/hierarchy.cc @@ -41,9 +41,9 @@ namespace spot twa_graph_ptr cobuchi = nullptr; std::vector pairs; if (aut->acc().is_streett_like(pairs) || aut->acc().is_parity()) - cobuchi = nsa_to_dca(aut, false); + cobuchi = nsa_to_nca(aut, false); else if (aut->get_acceptance().is_dnf()) - cobuchi = dnf_to_dca(aut, false); + cobuchi = dnf_to_nca(aut, false); else throw std::runtime_error("cobuchi_realizable() only works with " "Streett-like, Parity or any " @@ -107,7 +107,7 @@ namespace spot { if (aut_given && !is_persistence) return prcheck::via_Rabin; - else if ((aut_given && is_persistence) || !aut_given) + else if (is_persistence || !aut_given) return prcheck::via_CoBuchi; else SPOT_UNREACHABLE(); diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index ecf8b1c60..8e9b37c81 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -84,7 +84,6 @@ namespace spot if (code[s].sub.op == acc_cond::acc_op::And || ((one_conjunction = root_op == acc_cond::acc_op::And))) { - debug << "WABA" << std::endl; s = one_conjunction ? s + 1 : s; const unsigned short size = code[s].sub.size; acc_cond::mark_t fin = 0u;