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

minor code cleanups

Browse source 
* spot/twaalgos/cobuchi.cc, spot/twaalgos/totgba.cc: Here.
This commit is contained in:
Alexandre Duret-Lutz 2018-02-18 08:09:39 +01:00
parent 386a1c32be
commit 69f31c89c6
2 changed files with 43 additions and 39 deletions
Download patch file Download diff file Expand all files Collapse all files

35
spot/twaalgos/cobuchi.cc
View file

@ -219,7 +219,7 @@ namespace spot
named_states_(named_states), named_states_(named_states),
res_(aug_subset_cons(ref_prod, ref_power, named_states_, pmap_)), res_(aug_subset_cons(ref_prod, ref_power, named_states_, pmap_)),
res_map_(res_->get_named_prop<product_states>("product-states")), res_map_(res_->get_named_prop<product_states>("product-states")),
si_(scc_info(res_, scc_info_options::TRACK_STATES si_(res_, (scc_info_options::TRACK_STATES
| scc_info_options::TRACK_SUCCS)), | scc_info_options::TRACK_SUCCS)),
nb_states_(res_->num_states()), nb_states_(res_->num_states()),
was_rabin_(was_rabin), was_rabin_(was_rabin),
@ -474,7 +474,7 @@ namespace spot
} }
} }
} }
debug << "All_states:\n" << *bv_aut_trans_ << std::endl; debug << "All_states:\n" << *bv_aut_trans_ << '\n';
twa_graph_ptr res = make_twa_graph(aut_->get_dict()); twa_graph_ptr res = make_twa_graph(aut_->get_dict());
res->copy_ap_of(aut_); res->copy_ap_of(aut_);
@ -561,10 +561,14 @@ namespace spot
bv_trans_mark->at(l) |= bv_aut_trans_->at(s * nc + l); bv_trans_mark->at(l) |= bv_aut_trans_->at(s * nc + l);
toclean_.push_back(bv_trans_mark); toclean_.push_back(bv_trans_mark);
debug << "src:" << top.second << std::endl; debug << "src:" << top.second;
if (named_states)
debug << ' ' << (*state_name)[top.second];
debug << '\n';
for (unsigned l = 0; l < nc; ++l) for (unsigned l = 0; l < nc; ++l)
{ {
debug << "l:" debug << "l: "
<< bdd_format_formula(aut_->get_dict(), num2bdd_[l]) << bdd_format_formula(aut_->get_dict(), num2bdd_[l])
<< '\n'; << '\n';
@ -591,8 +595,7 @@ namespace spot
(top.first.first + 1) % (nb_copy_ + 1) (top.first.first + 1) % (nb_copy_ + 1)
: top.first.first; : top.first.first;
debug << "dest\n" << *bv_res << "i: " << i debug << "dest\n" << *bv_res << "i: " << i << '\n';
<< std::endl;
res->new_edge(top.second, res->new_edge(top.second,
new_state(std::make_pair(i, bv_res)), new_state(std::make_pair(i, bv_res)),
num2bdd_[l]); num2bdd_[l]);
@ -600,15 +603,18 @@ namespace spot
debug << '\n'; debug << '\n';
} }
// Set accepting states. // Set rejecting states.
scc_info si(res); scc_info si(res);
bool state_based = (bool)aut_->prop_state_acc(); bool state_based = (bool)aut_->prop_state_acc();
unsigned res_size = res->num_states(); unsigned res_size = res->num_states();
for (unsigned s = 0; s < res_size; ++s) for (unsigned s = 0; s < res_size; ++s)
{
unsigned s_scc = si.scc_of(s);
if (num_2_bv_[s].second->at(1).is_fully_clear()) if (num_2_bv_[s].second->at(1).is_fully_clear())
for (auto& edge : res->out(s)) for (auto& edge : res->out(s))
if (si.scc_of(edge.dst) == si.scc_of(s) || state_based) if (state_based || si.scc_of(edge.dst) == s_scc)
edge.acc = acc_cond::mark_t({0}); edge.acc = acc_cond::mark_t({0});
}
// Delete all bitvect arrays allocated by this method (run). // Delete all bitvect arrays allocated by this method (run).
for (auto v: toclean_) for (auto v: toclean_)
@ -624,7 +630,7 @@ namespace spot
twa_graph_ptr twa_graph_ptr
nsa_to_dca(const_twa_graph_ptr aut, bool named_states) nsa_to_dca(const_twa_graph_ptr aut, bool named_states)
{ {
debug << "NSA_to_dca" << std::endl; debug << "NSA_to_dca\n";
std::vector<acc_cond::rs_pair> pairs; std::vector<acc_cond::rs_pair> pairs;
if (!aut->acc().is_streett_like(pairs) && !aut->acc().is_parity()) if (!aut->acc().is_streett_like(pairs) && !aut->acc().is_parity())
throw std::runtime_error("nsa_to_dca() only works with Streett-like or " throw std::runtime_error("nsa_to_dca() only works with Streett-like or "
@ -640,10 +646,10 @@ namespace spot
nsa_to_nca(aut, named_states, &nca_info); nsa_to_nca(aut, named_states, &nca_info);
#if DEBUG #if DEBUG
debug << "PRINTING INFO" << std::endl; debug << "PRINTING INFO\n";
for (unsigned i = 0; i < nca_info.size(); ++i) for (unsigned i = 0; i < nca_info.size(); ++i)
debug << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num debug << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num
<< ',' << nca_info[i]->all_dst << '>' << std::endl; << ',' << *nca_info[i]->all_dst << ">\n";
#endif #endif
dca_breakpoint_cons dca(aut, &nca_info, 0); dca_breakpoint_cons dca(aut, &nca_info, 0);
@ -654,9 +660,8 @@ namespace spot
twa_graph_ptr twa_graph_ptr
dnf_to_dca(const_twa_graph_ptr aut, bool named_states) dnf_to_dca(const_twa_graph_ptr aut, bool named_states)
{ {
debug << "DNF_to_dca" << std::endl; debug << "DNF_to_dca\n";
const acc_cond::acc_code& code = aut->get_acceptance(); const acc_cond::acc_code& code = aut->get_acceptance();
std::vector<acc_cond::rs_pair> pairs;
if (!code.is_dnf()) if (!code.is_dnf())
throw std::runtime_error("dnf_to_dca() only works with DNF (Rabin-like " throw std::runtime_error("dnf_to_dca() only works with DNF (Rabin-like "
"included) acceptance condition"); "included) acceptance condition");
@ -671,10 +676,10 @@ namespace spot
dnf_to_nca(aut, false, &nca_info); dnf_to_nca(aut, false, &nca_info);
#if DEBUG #if DEBUG
debug << "PRINTING INFO" << std::endl; debug << "PRINTING INFO\n";
for (unsigned i = 0; i < nca_info.size(); ++i) for (unsigned i = 0; i < nca_info.size(); ++i)
debug << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num debug << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num
<< ',' << nca_info[i]->all_dst << '>' << std::endl; << ',' << *nca_info[i]->all_dst << ">\n";
#endif #endif
unsigned nb_copy = 0; unsigned nb_copy = 0;

31
spot/twaalgos/totgba.cc
View file

@ -126,18 +126,18 @@ namespace spot
for (unsigned i = 0; i < all_clauses_.size(); ++i) for (unsigned i = 0; i < all_clauses_.size(); ++i)
{ {
debug << i << " Fin:" << all_clauses_[i].first << " Inf:" debug << i << " Fin:" << all_clauses_[i].first << " Inf:"
<< all_clauses_[i].second << std::endl; << all_clauses_[i].second << '\n';
} }
#endif #endif
} }
// Compute all the acceptance sets that will be needed: // Compute all the acceptance sets that will be needed:
// -Inf(x) will be converted to (Inf(x) | Fin(y)) with y appearing // -Inf(x) will be converted to (Inf(x) | Fin(y)) with y appearing
// on every edge. // on every edge of the associated clone.
// -Fin(x) will be converted to (Inf(y) | Fin(x)) with y appearing // -Fin(x) will be converted to (Inf(y) | Fin(x)) with y appearing
// nowhere. // nowhere.
// // In the second form, Inf(y) with no occurrence of y, can be
// All the previous 'y' are the new sets assigned. // reused multiple times. It's called "missing_set" below.
void void
assign_new_sets() assign_new_sets()
{ {
@ -151,7 +151,7 @@ namespace spot
{ {
if ((int)missing_set < 0) if ((int)missing_set < 0)
{ {
while (all_m & acc_cond::mark_t({next_set})) while (all_m.has(next_set))
++next_set; ++next_set;
missing_set = next_set++; missing_set = next_set++;
} }
@ -160,13 +160,13 @@ namespace spot
} }
else if (all_inf_.has(set)) else if (all_inf_.has(set))
{ {
while (all_m & acc_cond::mark_t({next_set})) while (all_m.has(next_set))
++next_set; ++next_set;
assigned_sets_[set] = next_set++; assigned_sets_[set] = next_set++;
} }
num_sets_res_ = next_set > max_set_in_ ? next_set : max_set_in_; num_sets_res_ = std::max(next_set, max_set_in_);
} }
// Precompute: // Precompute:
@ -239,15 +239,15 @@ namespace spot
} }
} }
#if DEBUG #if DEBUG
debug << "accepting clauses" << std::endl; debug << "accepting clauses\n";
for (unsigned i = 0; i < res.size(); ++i) for (unsigned i = 0; i < res.size(); ++i)
{ {
debug << "scc(" << i << ") --> "; debug << "scc(" << i << ") --> ";
for (auto elt : res[i]) for (auto elt : res[i])
debug << elt << ','; debug << elt << ',';
debug << std::endl; debug << '\n'
} }
debug << std::endl; debug << '\n';
#endif #endif
} }
@ -257,7 +257,7 @@ namespace spot
void void
add_state(unsigned st) add_state(unsigned st)
{ {
debug << "add_state(" << st << ')' << std::endl; debug << "add_state(" << st << ")\n";
if (st_repr_[st].empty()) if (st_repr_[st].empty())
{ {
unsigned st_scc = si_.scc_of(st); unsigned st_scc = si_.scc_of(st);
@ -270,7 +270,7 @@ namespace spot
else else
st_repr_[st].emplace_back(-1U, res_->new_state()); st_repr_[st].emplace_back(-1U, res_->new_state());
debug << "added" << std::endl; debug << "added\n";
} }
} }
@ -317,7 +317,7 @@ namespace spot
init_st_in_(in->get_init_state_number()), init_st_in_(in->get_init_state_number()),
init_reachable_(is_init_reachable()) init_reachable_(is_init_reachable())
{ {
debug << "State based ? " << state_based_ << std::endl; debug << "State based ? " << state_based_ << '\n';
std::tie(all_inf_, all_fin_) = code.used_inf_fin_sets(); std::tie(all_inf_, all_fin_) = code.used_inf_fin_sets();
split_dnf_clauses(code); split_dnf_clauses(code);
find_set_to_add(); find_set_to_add();
@ -346,8 +346,7 @@ namespace spot
add_state(st); add_state(st);
for (const auto& e : in_->out(st)) for (const auto& e : in_->out(st))
{ {
debug << "working_on_edge(" << st << ',' << e.dst << ')' debug << "working_on_edge(" << st << ',' << e.dst << ")\n";
<< std::endl;
unsigned dst_scc = si_.scc_of(e.dst); unsigned dst_scc = si_.scc_of(e.dst);
if (!si_.is_useful_scc(dst_scc)) if (!si_.is_useful_scc(dst_scc))
@ -368,7 +367,7 @@ namespace spot
for (const auto& p_dst : st_repr_[e.dst]) for (const auto& p_dst : st_repr_[e.dst])
{ {
debug << "repr(" << p_src.second << ',' debug << "repr(" << p_src.second << ','
<< p_dst.second << ')' << std::endl; << p_dst.second << ")\n";
if (same_scc && p_src.first == p_dst.first) if (same_scc && p_src.first == p_dst.first)
res_->new_edge(p_src.second, p_dst.second, e.cond, res_->new_edge(p_src.second, p_dst.second, e.cond,