Commit 073ae6c1 authored by Etienne Renault's avatar Etienne Renault

are_equivalent: remove redundant code

* spot/twacube_algos/convert.cc: Here.
parent fc1d8e50
Pipeline #19110 passed with stage
in 91 minutes and 15 seconds
...@@ -184,7 +184,6 @@ namespace spot ...@@ -184,7 +184,6 @@ namespace spot
return res; return res;
} }
// FIXME this code is very close to twacube_to_twa, can we merge both?
bool are_equivalent(const spot::twacube_ptr twacube, bool are_equivalent(const spot::twacube_ptr twacube,
const spot::const_twa_graph_ptr twa) const spot::const_twa_graph_ptr twa)
{ {
...@@ -206,48 +205,7 @@ namespace spot ...@@ -206,48 +205,7 @@ namespace spot
throw std::runtime_error("are_equivalent: not working on the same " throw std::runtime_error("are_equivalent: not working on the same "
"atomic propositions"); "atomic propositions");
// Grab necessary variables auto res = twacube_to_twa(twacube, twa->get_dict());
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<int> 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());
bool result = are_equivalent(res, twa); bool result = are_equivalent(res, twa);
delete aps_twa; delete aps_twa;
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment