diff --git a/spot/twacube_algos/convert.cc b/spot/twacube_algos/convert.cc index e49194b90..1c25fe19a 100644 --- a/spot/twacube_algos/convert.cc +++ b/spot/twacube_algos/convert.cc @@ -184,7 +184,6 @@ namespace spot return res; } - // FIXME this code is very close to twacube_to_twa, can we merge both? bool are_equivalent(const spot::twacube_ptr twacube, const spot::const_twa_graph_ptr twa) { @@ -206,48 +205,7 @@ namespace spot throw std::runtime_error("are_equivalent: not working on the same " "atomic propositions"); - // Grab necessary variables - auto& theg = twacube->get_graph(); - spot::cubeset cs = twacube->get_cubeset(); - - auto d = twa->get_dict(); - auto res = make_twa_graph(d); - - // Fix the acceptance of the resulting automaton - res->acc() = twacube->acc(); - - // Grep bdd id for each atomic propositions - std::vector bdds_ref; - for (unsigned i = 0; i < aps_twacube.size(); ++i) - bdds_ref.push_back(res->register_ap(twacube->ap()[i])); - - // Build all resulting states - for (unsigned int i = 0; i < theg.num_states(); ++i) - { - unsigned st = res->new_state(); - (void) st; - assert(st == i); - } - - // Build all resulting conditions. - for (unsigned int i = 1; i <= theg.num_edges(); ++i) - { - bdd cond = bddtrue; - for (unsigned j = 0; j < cs.size(); ++j) - { - if (cs.is_true_var(theg.edge_data(i).cube_, j)) - cond &= bdd_ithvar(bdds_ref[j]); - else if (cs.is_false_var(theg.edge_data(i).cube_, j)) - cond &= bdd_nithvar(bdds_ref[j]); - // otherwise it 's a free variable do nothing - } - - res->new_edge(theg.edge_storage(i).src, theg.edge_storage(i).dst, - cond, theg.edge_data(i).acc_); - } - - // Fix the initial state - res->set_init_state(twacube->get_initial()); + auto res = twacube_to_twa(twacube, twa->get_dict()); bool result = are_equivalent(res, twa); delete aps_twa;