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

Use clearer names for three methods of spot::scc_info

Browse source 
scc_info::used_acc() and spot::info::used_acc_of() have been renamed to
scc_info::marks() and scc_info::marks_of().
scc_info::acc() has been renamed to (the already existing and redundant)
scc_info::acc_sets_of().
Old names have been deprecated.

* spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: implement it.
* spot/twaalgos/dtwasat.cc, spot/twaalgos/isweakscc.cc,
  spot/twaalgos/remfin.cc, spot/twaalgos/sccfilter.cc: update names.
* NEWS: documentate it.
This commit is contained in:
Maximilien Colange 2017-09-14 10:32:36 +02:00
parent 7eb50bc1f8
commit bd5c6920b1
7 changed files with 56 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

2
spot/twaalgos/dtwasat.cc
View file

@ -400,7 +400,7 @@ namespace spot
d.is_weak_scc = sm.weak_sccs();
unsigned scccount = sm.scc_count();
{
auto tmp = sm.used_acc();
auto tmp = sm.marks();
d.scc_marks.reserve(scccount);
for (auto& v: tmp)
{

4
spot/twaalgos/isweakscc.cc
View file

@ -74,7 +74,7 @@ namespace spot
if (map.is_rejecting_scc(scc))
return true;
// If all transitions use the same acceptance set, the SCC is weak.
return map.used_acc_of(scc).size() == 1;
return map.marks_of(scc).size() == 1;
}
bool
@ -117,7 +117,7 @@ namespace spot
// If all transitions use all acceptance conditions, the SCC is weak.
return (map.is_accepting_scc(scc)
&& map.used_acc_of(scc).size() == 1
&& map.marks_of(scc).size() == 1
&& is_complete_scc(map, scc));
}
}

4
spot/twaalgos/remfin.cc
View file

@ -309,7 +309,7 @@ namespace spot
// The main copy is only accepting for inf_alone
// and for all Inf sets that have no matching Fin
// sets in this SCC.
auto scc_pairs = rs_pairs_view(pairs, si.acc(scc));
auto scc_pairs = rs_pairs_view(pairs, si.acc_sets_of(scc));
auto scc_infs_alone = scc_pairs.infs_alone();
for (const auto& e: si.edges_of(scc))
@ -676,7 +676,7 @@ namespace spot
std::vector<unsigned> state_map(nst);
for (unsigned n = 0; n < nscc; ++n)
{
auto m = si.acc(n);
auto m = si.acc_sets_of(n);
auto states = si.states_of(n);
trace << "SCC #" << n << " uses " << m << '\n';

2
spot/twaalgos/sccfilter.cc
View file

@ -223,7 +223,7 @@ namespace spot
"generalized Büchi acceptance");
unsigned scc_count = this->si->scc_count();
auto used_acc = this->si->used_acc();
auto used_acc = this->si->marks();
assert(used_acc.size() == scc_count);
strip_.resize(scc_count);
std::vector<unsigned> cnt(scc_count); // # of useful sets in each SCC

9
spot/twaalgos/sccinfo.cc
View file

@ -318,7 +318,7 @@ namespace spot
}
std::set<acc_cond::mark_t> scc_info::used_acc_of(unsigned scc) const
std::set<acc_cond::mark_t> scc_info::marks_of(unsigned scc) const
{
std::set<acc_cond::mark_t> res;
for (auto& t: inner_edges_of(scc))
@ -326,7 +326,7 @@ namespace spot
return res;
}
std::vector<std::set<acc_cond::mark_t>> scc_info::used_acc() const
std::vector<std::set<acc_cond::mark_t>> scc_info::marks() const
{
unsigned n = aut_->num_states();
std::vector<std::set<acc_cond::mark_t>> result(scc_count());
@ -351,7 +351,7 @@ namespace spot
{
unsigned n = scc_count();
std::vector<bool> result(scc_count());
auto acc = used_acc();
auto acc = marks();
for (unsigned s = 0; s < n; ++s)
result[s] = is_rejecting_scc(s) || acc[s].size() == 1;
return result;
@ -413,7 +413,8 @@ namespace spot
q.pop();
out << " " << state << " [shape=box,"
<< (aut->acc().accepting(m->acc(state)) ? "style=bold," : "")
<< (aut->acc().accepting(m->acc_sets_of(state)) ?
"style=bold," : "")
<< "label=\"" << state;
{
size_t n = m->states_of(state).size();

36
spot/twaalgos/sccinfo.hh
View file

@ -476,9 +476,10 @@ namespace spot
return node(scc).is_trivial();
}
SPOT_DEPRECATED("use acc_sets_of() instead")
acc_cond::mark_t acc(unsigned scc) const
{
return node(scc).acc_marks();
return acc_sets_of(scc);
}
bool is_accepting_scc(unsigned scc) const
@ -505,20 +506,33 @@ namespace spot
return reachable_state(st) && node(scc_of(st)).is_useful();
}
/// \brief Return the set of all used acceptance combinations, for
/// each accepting SCC.
std::vector<std::set<acc_cond::mark_t>> used_acc() const;
/// \brief Returns, for each accepting SCC, the set of all marks appearing
/// in it.
std::vector<std::set<acc_cond::mark_t>> marks() const;
std::set<acc_cond::mark_t> marks_of(unsigned scc) const;
std::set<acc_cond::mark_t> used_acc_of(unsigned scc) const;
/// sets that contain at least one transition of the SCC
acc_cond::mark_t acc_sets_of(unsigned scc) const
// Same as above, with old names.
SPOT_DEPRECATED("use marks() instead")
std::vector<std::set<acc_cond::mark_t>> used_acc() const
{
// FIXME: Why do we have two name for this method?
return acc(scc);
return marks();
}
SPOT_DEPRECATED("use marks_of() instead")
std::set<acc_cond::mark_t> used_acc_of(unsigned scc) const
{
return marks_of(scc);
}
/// sets that contain the entire SCC
/// \brief Returns, for a given SCC, the set of all colors appearing in it.
/// It is the set of colors that appear in some mark among those returned by
/// marks_of().
acc_cond::mark_t acc_sets_of(unsigned scc) const
{
return node(scc).acc_marks();
}
/// Returns, for a given SCC, the set of colors that appear on all of its
/// transitions.
acc_cond::mark_t common_sets_of(unsigned scc) const
{
return node(scc).common_marks();