alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

pdegen & toparity: minor refactor

Browse source 
* spot/twaalgos/degen.hh (is_partially_degeneralizable): Pass the
forbid vector by reference, and document it.  I hope that not passing
forbid by copy will get rid of a spurious "potential nullptr" warning
by gcc on Arch Linux.
* spot/twaalgos/degen.cc: Adjust, and refactor the code a bit.
* spot/twaalgos/toparity.cc: Likewise.
This commit is contained in:
Alexandre Duret-Lutz 2024-05-14 10:20:45 +02:00
parent ed91f59bbd
commit 2bd2abd4c9
3 changed files with 126 additions and 128 deletions
Download patch file Download diff file Expand all files Collapse all files

27
spot/twaalgos/degen.cc
View file

@ -872,7 +872,7 @@ namespace spot
acc_cond::mark_t
is_partially_degeneralizable(const const_twa_graph_ptr& aut,
bool allow_inf, bool allow_fin,
std::vector<acc_cond::mark_t> forbid)
const std::vector<acc_cond::mark_t>& forbid)
{
auto& code = aut->get_acceptance();
@ -881,16 +881,19 @@ namespace spot
acc_cond::mark_t res = {};
unsigned res_sz = -1U;
auto update = [&](const acc_cond::mark_t& m)
auto keep_smallest_mark = [&](const acc_cond::mark_t& m)
{
if (std::find(forbid.begin(), forbid.end(), m) != forbid.end())
return false;
unsigned sz = m.count();
if (sz > 1 && sz < res_sz)
{
res_sz = sz;
res = m;
}
// If we have found a pair to degeneralize, we
// won't find
// If we have found a pair to degeneralize, we won't find a
// smaller one.
return res_sz == 2;
};
@ -906,22 +909,14 @@ namespace spot
case acc_cond::acc_op::Fin:
case acc_cond::acc_op::FinNeg:
pos -= 2;
if (allow_fin)
{
auto m = code[pos].mark;
if (!std::count(forbid.begin(), forbid.end(), m) && update(m))
return res;
}
if (allow_fin && keep_smallest_mark(code[pos].mark))
return res;
break;
case acc_cond::acc_op::Inf:
case acc_cond::acc_op::InfNeg:
pos -= 2;
if (allow_inf)
{
auto m = code[pos].mark;
if (!std::count(forbid.begin(), forbid.end(), m) && update(m))
return res;
}
if (allow_inf && keep_smallest_mark(code[pos].mark))
return res;
break;
}
}

9
spot/twaalgos/degen.hh
View file

@ -158,11 +158,14 @@ namespace spot
///
/// The optional arguments \a allow_inf and \a allow_fin, can be set
/// to false to disallow one type of match.
///
/// If you need to disallow certain marks from being returned, pass
/// them in the \a forbid vector.
SPOT_API acc_cond::mark_t
is_partially_degeneralizable(const const_twa_graph_ptr& aut,
bool allow_inf = true,
bool allow_fin = true,
std::vector<acc_cond::mark_t> forbid = {});
bool allow_inf = true, bool allow_fin = true,
const std::vector<acc_cond::mark_t>&
forbid = {});
/// \ingroup twa_algorithms
/// \brief Propagate marks around the automaton

218
spot/twaalgos/toparity.cc
View file

@ -2198,17 +2198,17 @@ namespace spot
return true;
std::vector<acc_cond::rs_pair> pairs;
if (deg->acc().is_rabin_like(pairs))
{
remove_duplicates(pairs);
if (pairs.size() < nb_col_orig)
return true;
}
{
remove_duplicates(pairs);
if (pairs.size() < nb_col_orig)
return true;
}
if (deg->acc().is_streett_like(pairs))
{
remove_duplicates(pairs);
if (pairs.size() < nb_col_orig)
return true;
}
{
remove_duplicates(pairs);
if (pairs.size() < nb_col_orig)
return true;
}
return false;
}
@ -2223,118 +2223,118 @@ namespace spot
max_color_scc_ = 0;
// If the sub_automaton is "empty", we don't need to apply an algorithm.
if (sub_aut->num_edges() == 0)
{
apply_copy(sub_aut, {}, none_algo);
return;
}
{
apply_copy(sub_aut, {}, none_algo);
return;
}
bool tried_emptiness = false;
bool changed_structure = true;
while (true)
{
auto cond_before_simpl = sub_aut->acc();
if (opt_.acc_clean)
simplify_acceptance_here(sub_aut);
if (opt_.propagate_col)
{
propagate_marks_here(sub_aut);
auto cond_before_simpl = sub_aut->acc();
if (opt_.acc_clean)
simplify_acceptance_here(sub_aut);
}
if (opt_.datas && sub_aut->acc() != cond_before_simpl)
algo_used_ |= algorithm::ACC_CLEAN;
if (opt_.parity_equiv || opt_.parity_prefix)
{
// If we don't try to find a parity prefix, we can stop
// to construct the tree when it has not parity shape.
zielonka_tree_options zopt = zielonka_tree_options::MERGE_SUBTREES
| zielonka_tree_options::CHECK_PARITY;
if (!opt_.parity_prefix)
zopt = zopt | zielonka_tree_options::ABORT_WRONG_SHAPE;
auto tree = zielonka_tree(sub_aut->acc(), zopt);
// If it is not parity shape, tree.nodes_ will be empty
if (tree.num_branches() != 0 && opt_.parity_equiv
&& try_parity_equivalence(tree, sub_aut))
return;
if (opt_.parity_prefix && try_parity_prefix(tree, sub_aut))
return;
}
if (changed_structure && opt_.parity_prefix_general
&& try_parity_prefix_general(sub_aut))
return;
if (opt_.generic_emptiness && !tried_emptiness
&& try_emptiness(sub_aut, tried_emptiness))
return;
// Buchi_type_to_buchi is more general that Rabin_to_buchi so
// we just call rabin_to_buchi if buchi_type_to_buchi is false.
if (!opt_.buchi_type_to_buchi && !opt_.parity_type_to_parity
&& opt_.rabin_to_buchi
&& try_rabin_to_buchi(sub_aut))
return;
// As parity_type_to_parity is stronger, we don't
// try if this option is used.
if (opt_.buchi_type_to_buchi && !opt_.parity_type_to_parity
&& try_buchi_type(sub_aut))
return;
// We don't do it if parity_prefix_general is true as on a parity-type
// automaton parity_prefix_general removes all the transitions and
// we also get a parity-type automaton.
if (!opt_.parity_prefix_general && opt_.parity_type_to_parity
&& try_parity_type(sub_aut))
return;
if (opt_.partial_degen
&& is_partially_degeneralizable(sub_aut, true, true))
{
auto deg = sub_aut;
std::vector<acc_cond::mark_t> forbid;
auto m = is_partially_degeneralizable(sub_aut, true, true, forbid);
bool changed = false;
while (m)
{
auto tmp = partial_degeneralize(deg, m);
simplify_acceptance_here(tmp);
if (keep_deg(deg, tmp))
if (opt_.propagate_col)
{
algo_used_ |= algorithm::PARTIAL_DEGEN;
deg = tmp;
changed = true;
changed_structure = true;
propagate_marks_here(sub_aut);
if (opt_.acc_clean)
simplify_acceptance_here(sub_aut);
}
else
forbid.emplace_back(m);
m = is_partially_degeneralizable(deg, true, true, forbid);
}
if (opt_.datas && sub_aut->acc() != cond_before_simpl)
algo_used_ |= algorithm::ACC_CLEAN;
if (changed)
{
sub_aut = deg;
continue;
}
if (opt_.parity_equiv || opt_.parity_prefix)
{
// If we don't try to find a parity prefix, we can stop
// to construct the tree when it has not parity shape.
zielonka_tree_options zopt =
zielonka_tree_options::MERGE_SUBTREES
| zielonka_tree_options::CHECK_PARITY;
if (!opt_.parity_prefix)
zopt = zopt | zielonka_tree_options::ABORT_WRONG_SHAPE;
auto tree = zielonka_tree(sub_aut->acc(), zopt);
// If it is not parity shape, tree.nodes_ will be empty
if (tree.num_branches() != 0 && opt_.parity_equiv
&& try_parity_equivalence(tree, sub_aut))
return;
if (opt_.parity_prefix && try_parity_prefix(tree, sub_aut))
return;
}
if (changed_structure && opt_.parity_prefix_general
&& try_parity_prefix_general(sub_aut))
return;
if (opt_.generic_emptiness
&& !tried_emptiness && try_emptiness(sub_aut, tried_emptiness))
return;
// Buchi_type_to_buchi is more general that Rabin_to_buchi so
// we just call rabin_to_buchi if buchi_type_to_buchi is false.
if (!opt_.buchi_type_to_buchi
&& !opt_.parity_type_to_parity && opt_.rabin_to_buchi
&& try_rabin_to_buchi(sub_aut))
return;
// As parity_type_to_parity is stronger, we don't
// try if this option is used.
if (opt_.buchi_type_to_buchi
&& !opt_.parity_type_to_parity && try_buchi_type(sub_aut))
return;
// We don't do it if parity_prefix_general is true as on a parity-type
// automaton parity_prefix_general removes all the transitions and
// we also get a parity-type automaton.
if (!opt_.parity_prefix_general && opt_.parity_type_to_parity
&& try_parity_type(sub_aut))
return;
if (opt_.partial_degen)
{
twa_graph_ptr deg = sub_aut;
std::vector<acc_cond::mark_t> forbid;
bool changed = false;
while (acc_cond::mark_t m =
is_partially_degeneralizable(deg, true, true, forbid))
{
twa_graph_ptr tmp = partial_degeneralize(deg, m);
simplify_acceptance_here(tmp);
if (keep_deg(deg, tmp))
{
algo_used_ |= algorithm::PARTIAL_DEGEN;
deg = tmp;
changed = true;
changed_structure = true;
}
else
{
forbid.emplace_back(m);
}
}
if (changed)
{
sub_aut = deg;
continue;
}
}
break;
}
break;
}
if (opt_.use_generalized_rabin)
{
auto gen_rab = to_generalized_rabin(sub_aut);
// to_generalized_rabin does not propagate original-states.
auto sub_aut_orig =
{
auto gen_rab = to_generalized_rabin(sub_aut);
// to_generalized_rabin does not propagate original-states.
auto sub_aut_orig =
sub_aut->get_named_prop<std::vector<unsigned>>("original-states");
assert(sub_aut_orig);
auto orig = new std::vector<unsigned>();
const auto sub_aut_num_states = sub_aut->num_states();
orig->reserve(sub_aut_num_states);
gen_rab->set_named_prop("original-states", orig);
for (unsigned i = 0; i < sub_aut_num_states; ++i)
orig->push_back((*sub_aut_orig)[i]);
sub_aut = partial_degeneralize(gen_rab);
}
assert(sub_aut_orig);
auto orig = new std::vector<unsigned>();
const auto sub_aut_num_states = sub_aut->num_states();
orig->reserve(sub_aut_num_states);
gen_rab->set_named_prop("original-states", orig);
for (unsigned i = 0; i < sub_aut_num_states; ++i)
orig->push_back((*sub_aut_orig)[i]);
sub_aut = partial_degeneralize(gen_rab);
}
std::vector<acc_cond::rs_pair> pairs;
algorithm algo = choose_lar(sub_aut->acc(), pairs, sub_aut->num_edges());
if (opt_.datas)