diff --git a/src/tgbaalgos/mask.cc b/src/tgbaalgos/mask.cc index a769f2d3a..9a82a364e 100644 --- a/src/tgbaalgos/mask.cc +++ b/src/tgbaalgos/mask.cc @@ -32,15 +32,16 @@ namespace spot unsigned tr = to_remove.count(); assert(tr <= na); res->set_acceptance_conditions(na - tr); - transform_mask(in, res, [&](bdd& cond, - acc_cond::mark_t& acc, - unsigned) - { - if (acc & to_remove) - cond = bddfalse; - else - acc = inacc.strip(acc, to_remove); - }); + transform_accessible(in, res, [&](unsigned, + bdd& cond, + acc_cond::mark_t& acc, + unsigned) + { + if (acc & to_remove) + cond = bddfalse; + else + acc = inacc.strip(acc, to_remove); + }); return res; } @@ -55,11 +56,12 @@ namespace spot res->copy_ap_of(in); res->prop_copy(in, { true, true, true, true }); res->copy_acceptance_conditions_of(in); - transform_mask(in, res, [&](bdd& cond, - acc_cond::mark_t&, - unsigned dst) + transform_copy(in, res, [&](unsigned src, + bdd& cond, + acc_cond::mark_t&, + unsigned dst) { - if (!to_keep[dst]) + if (!to_keep[src] || !to_keep[dst]) cond = bddfalse; }, init); return res; diff --git a/src/tgbaalgos/mask.hh b/src/tgbaalgos/mask.hh index 4e9eb42a0..f02ca0d9c 100644 --- a/src/tgbaalgos/mask.hh +++ b/src/tgbaalgos/mask.hh @@ -28,9 +28,10 @@ namespace spot /// /// Copy the transition of the automaton \a old, into the automaton /// \a cpy, creating new states at the same time. The argument \a - /// trans should behave as a fonction with the following prototype: + /// trans should behave as a function with the following prototype: /// - /// void (*trans) (bdd& cond, acc_cond::mark_t& acc, unsigned dst) + /// void (*trans) (unsigned srcbdd& cond, acc_cond::mark_t& acc, + /// unsigned dst) /// /// It can modify either the condition or the acceptance sets of /// the transitions. Set the condition to bddfalse to remove it @@ -39,9 +40,9 @@ namespace spot /// \param init The optional new initial state. template - void transform_mask(const const_tgba_digraph_ptr& old, - tgba_digraph_ptr& cpy, - Trans trans, unsigned int init) + void transform_accessible(const const_tgba_digraph_ptr& old, + tgba_digraph_ptr& cpy, + Trans trans, unsigned int init) { std::vector todo; std::vector seen(old->num_states(), -1U); @@ -72,7 +73,7 @@ namespace spot { bdd cond = t.cond; acc_cond::mark_t acc = t.acc; - trans(cond, acc, t.dst); + trans(t.src, cond, acc, t.dst); if (cond != bddfalse) cpy->new_transition(new_src, @@ -82,12 +83,55 @@ namespace spot } } + /// \brief Copy an automaton and update each transitions. + /// + /// Copy the states of the automaton \a old, into the automaton + /// \a cpy. Each state in \a cpy will have the same id as the ones in \a old. + /// The argument \a trans + /// should behave as a function with the following prototype: + /// + /// void (*trans) (unsigned srcbdd& cond, acc_cond::mark_t& acc, + /// unsigned dst) + /// + /// It can modify either the condition or the acceptance sets of + /// the transitions. Set the condition to bddfalse to remove it. Note that + /// all transtions will be processed. + /// \param init The optional new initial state. template - void transform_mask(const const_tgba_digraph_ptr& old, - tgba_digraph_ptr& cpy, - Trans trans) + void transform_copy(const const_tgba_digraph_ptr& old, + tgba_digraph_ptr& cpy, + Trans trans, unsigned int init) { - transform_mask(old, cpy, trans, old->get_init_state_number()); + // Each state in cpy corresponds to a unique state in old. + cpy->new_states(old->num_states()); + cpy->set_init_state(init); + + for (auto& t: old->transitions()) + { + bdd cond = t.cond; + acc_cond::mark_t acc = t.acc; + trans(t.src, cond, acc, t.dst); + // Having the same number of states should assure that state ids are + // equivilent in old and cpy. + assert(t.src < cpy->num_states() && t.dst < cpy->num_states()); + if (cond != bddfalse) + cpy->new_transition(t.src, t.dst, cond, acc); + } + } + + template + void transform_accessible(const const_tgba_digraph_ptr& old, + tgba_digraph_ptr& cpy, + Trans trans) + { + transform_accessible(old, cpy, trans, old->get_init_state_number()); + } + template + void transform_copy(const const_tgba_digraph_ptr& old, + tgba_digraph_ptr& cpy, + Trans trans) + { + transform_copy(old, cpy, trans, old->get_init_state_number()); } /// \brief Remove all transitions that are in some given acceptance sets. diff --git a/src/tgbatest/maskkeep.test b/src/tgbatest/maskkeep.test index 3ad825795..a5d966a5c 100755 --- a/src/tgbatest/maskkeep.test +++ b/src/tgbatest/maskkeep.test @@ -48,7 +48,7 @@ EOF cat >expect1 <expect2 <output diff output expect1 run 0 ../../bin/autfilt --keep-states=1 input1 -H >output -diff output expect1 +diff output expect2 cat >expect3 <expect4 <