From 1df5f0e2c75d249d2fdeb43067ff9962ce2d6e44 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 23 Oct 2021 01:23:24 +0200 Subject: [PATCH] synthesis: simplify split_2step_fast_here * spot/twaalgos/synthesis.cc (split_2step_fast_here): Do not use a temporary vector to iterate over the original edges. --- spot/twaalgos/synthesis.cc | 37 +++++++++++++++++-------------------- 1 file changed, 17 insertions(+), 20 deletions(-) diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 08cb4264d..3bfeba5b7 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -363,26 +363,23 @@ namespace spot return ns; }; - std::vector to_treat(aut->num_edges()); - std::transform(aut->edges().begin(), aut->edges().end(), - to_treat.begin(), [&](const auto& e) - { return aut->edge_number(e); }); - - std::for_each(to_treat.begin(), to_treat.end(), - [&](unsigned eidx) - { - const auto& e = aut->edge_storage(eidx); - bdd incond = bdd_exist(e.cond, output_bdd); - bdd outcond = bdd_existcomp(e.cond, output_bdd); - assert(((incond&outcond) == e.cond) - && "Precondition violated"); - // Modify - // Create new state and trans - unsigned new_dst = get_ps(e.dst, outcond, e.acc); - // redirect - aut->edge_storage(eidx).dst = new_dst; - aut->edge_storage(eidx).cond = incond; - }); + unsigned ne = aut->edge_vector().size(); + for (unsigned eidx = 1; eidx < ne; ++eidx) + { + const auto& e = aut->edge_storage(eidx); + if (e.next_succ == eidx) // dead edge + continue; + bdd incond = bdd_exist(e.cond, output_bdd); + bdd outcond = bdd_existcomp(e.cond, output_bdd); + assert(((incond&outcond) == e.cond) && "Precondition violated"); + // Create new state and trans + // this may invalidate "e". + unsigned new_dst = get_ps(e.dst, outcond, e.acc); + // redirect + auto& e2 = aut->edge_storage(eidx); + e2.dst = new_dst; + e2.cond = incond; + } auto* sp_ptr = aut->get_or_set_named_prop>("state-player");