acc: get rid of join()
* spot/twa/acc.hh: Here. Also make sure << takes an unsigned argument. * spot/twa/twaproduct.cc, spot/twaalgos/compsusp.cc, spot/twaalgos/product.cc, spot/twaalgos/remfin.cc, spot/twaalgos/totgba.cc, spot/tests/acc.cc: Adjust.
This commit is contained in:
Alexandre Duret-Lutz
parent
94cca9de3d
commit
fd6ad9913f
7 changed files with 27 additions and 48 deletions
|
|
@ -91,11 +91,11 @@ int main()
|
|||
ac3.set_generalized_buchi();
|
||||
std::cout << ac.num_sets() << " + "
|
||||
<< ac2.num_sets() << " = " << ac3.num_sets() << '\n';
|
||||
auto m5 = ac3.join(ac, m2, ac2, m3);
|
||||
auto m5 = m2 | (m3 << ac.num_sets());
|
||||
check(ac3, m5);
|
||||
auto m6 = ac3.join(ac, ac.comp(m2 & m3), ac2, m3);
|
||||
auto m6 = ac.comp(m2 & m3) | (m3 << ac.num_sets());
|
||||
check(ac3, m6);
|
||||
auto m7 = ac3.join(ac, ac.comp(m2 & m3), ac2, ac2.all_sets());
|
||||
auto m7 = ac.comp(m2 & m3) | (ac.all_sets() << ac.num_sets());
|
||||
check(ac3, m7);
|
||||
|
||||
const char* comma = "";
|
||||
|
|
|
|||
|
|
@ -167,23 +167,23 @@ namespace spot
|
|||
return id ^ r.id;
|
||||
}
|
||||
|
||||
mark_t operator<<(int i) const
|
||||
mark_t operator<<(unsigned i) const
|
||||
{
|
||||
return id << i;
|
||||
}
|
||||
|
||||
mark_t& operator<<=(int i)
|
||||
mark_t& operator<<=(unsigned i)
|
||||
{
|
||||
id <<= i;
|
||||
return *this;
|
||||
}
|
||||
|
||||
mark_t operator>>(int i) const
|
||||
mark_t operator>>(unsigned i) const
|
||||
{
|
||||
return id >> i;
|
||||
}
|
||||
|
||||
mark_t& operator>>=(int i)
|
||||
mark_t& operator>>=(unsigned i)
|
||||
{
|
||||
id >>= i;
|
||||
return *this;
|
||||
|
|
@ -1072,15 +1072,8 @@ namespace spot
|
|||
|
||||
mark_t mark(unsigned u) const
|
||||
{
|
||||
return mark_(u);
|
||||
}
|
||||
|
||||
mark_t join(const acc_cond& la, mark_t lm,
|
||||
const acc_cond& ra, mark_t rm) const
|
||||
{
|
||||
assert(la.num_sets() + ra.num_sets() == num_sets());
|
||||
(void)ra;
|
||||
return lm.id | (rm.id << la.num_sets());
|
||||
assert(u < num_sets());
|
||||
return 1U << u;
|
||||
}
|
||||
|
||||
mark_t comp(mark_t l) const
|
||||
|
|
@ -1151,12 +1144,6 @@ namespace spot
|
|||
}
|
||||
|
||||
protected:
|
||||
mark_t::value_t mark_(unsigned u) const
|
||||
{
|
||||
assert(u < num_sets());
|
||||
return 1U << u;
|
||||
}
|
||||
|
||||
mark_t::value_t all_sets_() const
|
||||
{
|
||||
if (num_ == 0)
|
||||
|
|
|
|||
|
|
@ -203,12 +203,8 @@ namespace spot
|
|||
|
||||
acc_cond::mark_t acc() const
|
||||
{
|
||||
return
|
||||
prod_->acc().join(prod_->left_acc(),
|
||||
left_->acc(),
|
||||
prod_->right_acc(),
|
||||
right_->acc());
|
||||
}
|
||||
return left_->acc() | (right_->acc() << prod_->left_acc().num_sets());
|
||||
}
|
||||
|
||||
protected:
|
||||
bdd current_cond_;
|
||||
|
|
|
|||
|
|
@ -168,11 +168,10 @@ namespace spot
|
|||
dict->register_all_variables_of(right, res);
|
||||
dict->unregister_variable(bdd_var(v), res);
|
||||
|
||||
const acc_cond& la = left->acc();
|
||||
const acc_cond& ra = right->acc();
|
||||
res->set_generalized_buchi(la.num_sets() + ra.num_sets());
|
||||
unsigned lsets = left->num_sets();
|
||||
res->set_generalized_buchi(lsets + right->num_sets());
|
||||
|
||||
acc_cond::mark_t radd = ra.all_sets();
|
||||
acc_cond::mark_t radd = right->acc().all_sets();
|
||||
|
||||
pair_map seen;
|
||||
pair_queue todo;
|
||||
|
|
@ -246,9 +245,7 @@ namespace spot
|
|||
todo.push_back(d);
|
||||
}
|
||||
|
||||
acc_cond::mark_t a =
|
||||
res->acc().join(la, li->acc(),
|
||||
ra, racc);
|
||||
acc_cond::mark_t a = li->acc() | (racc << lsets);
|
||||
res->new_edge(src, dest, bdd_exist(cond, v), a);
|
||||
|
||||
if (ri)
|
||||
|
|
|
|||
|
|
@ -96,8 +96,7 @@ namespace spot
|
|||
continue;
|
||||
auto dst = new_state(l.dst, r.dst);
|
||||
res->new_edge(top.second, dst, cond,
|
||||
res->acc().join(left->acc(), l.acc,
|
||||
right->acc(), r.acc));
|
||||
l.acc | (r.acc << left_num));
|
||||
// If right is deterministic, we can abort immediately!
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -63,7 +63,7 @@ namespace spot
|
|||
// Let f=[F₁,F₂,...] and i=[I₁,I₂,...] be bitvectors where bit
|
||||
// Fᵢ (resp. Iᵢ) indicates that Fᵢ (resp. Iᵢ) has been visited
|
||||
// in the SCC.
|
||||
acc_cond::mark_t f = (sets << 1) & inf_pairs;
|
||||
acc_cond::mark_t f = (sets << 1U) & inf_pairs;
|
||||
acc_cond::mark_t i = sets & inf_pairs;
|
||||
// If we have i&!f = [0,0,...] that means that the cycle formed
|
||||
// by the entire SCC is not accepting. However that does not
|
||||
|
|
@ -168,7 +168,7 @@ namespace spot
|
|||
acc_cond::mark_t inf;
|
||||
std::tie(inf, fin) = aut->get_acceptance().used_inf_fin_sets();
|
||||
assert(inf == (inf_pairs | inf_alone));
|
||||
assert(fin == ((inf_pairs >> 1) | fin_alone));
|
||||
assert(fin == ((inf_pairs >> 1U) | fin_alone));
|
||||
#endif
|
||||
ba_final_states.resize(aut->num_states(), false);
|
||||
ba_type = true; // until proven otherwise
|
||||
|
|
@ -254,7 +254,7 @@ namespace spot
|
|||
// and for all Inf sets that have no matching Fin
|
||||
// sets in this SCC.
|
||||
acc_cond::mark_t sccsets = si.acc(n);
|
||||
acc_cond::mark_t f = (sccsets << 1) & inf_pairs;
|
||||
acc_cond::mark_t f = (sccsets << 1U) & inf_pairs;
|
||||
acc_cond::mark_t i = sccsets & (inf_pairs | inf_alone);
|
||||
i -= f;
|
||||
for (auto s: states)
|
||||
|
|
@ -264,7 +264,7 @@ namespace spot
|
|||
res->new_acc_edge(s, t.dst, t.cond, acc);
|
||||
}
|
||||
|
||||
auto rem = sccsets & ((inf_pairs >> 1) | fin_alone);
|
||||
auto rem = sccsets & ((inf_pairs >> 1U) | fin_alone);
|
||||
assert(rem != 0U);
|
||||
auto sets = rem.sets();
|
||||
|
||||
|
|
@ -347,7 +347,7 @@ namespace spot
|
|||
o2 != acc_cond::acc_op::Inf ||
|
||||
m1.count() != 1 ||
|
||||
m2.count() != 1 ||
|
||||
m2 != (m1 << 1))
|
||||
m2 != (m1 << 1U))
|
||||
return nullptr;
|
||||
inf_pairs |= m2;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -126,7 +126,7 @@ namespace spot
|
|||
acc_cond::mark_t inf;
|
||||
acc_cond::mark_t fin;
|
||||
std::tie(inf, fin) = in->get_acceptance().used_inf_fin_sets();
|
||||
assert((inf >> 1) == fin);
|
||||
assert((inf >> 1U) == fin);
|
||||
|
||||
scc_info si(in);
|
||||
|
||||
|
|
@ -139,8 +139,8 @@ namespace spot
|
|||
auto acc = si.acc_sets_of(s); // {0,1,2,3,4,6,7,9}
|
||||
auto acc_fin = acc & fin; // {0, 2, 4,6}
|
||||
auto acc_inf = acc & inf; // { 1, 3, 7,9}
|
||||
auto fin_wo_inf = acc_fin - (acc_inf >> 1); // {4}
|
||||
auto inf_wo_fin = acc_inf - (acc_fin << 1); // {9}
|
||||
auto fin_wo_inf = acc_fin - (acc_inf >> 1U); // {4}
|
||||
auto inf_wo_fin = acc_inf - (acc_fin << 1U); // {9}
|
||||
sccfi.emplace_back(fin_wo_inf, inf_wo_fin, acc_fin == 0U);
|
||||
}
|
||||
|
||||
|
|
@ -199,7 +199,7 @@ namespace spot
|
|||
continue;
|
||||
// For any Fin set we see, we want to see the
|
||||
// corresponding Inf set.
|
||||
pend |= (t.acc & fin) << 1;
|
||||
pend |= (t.acc & fin) << 1U;
|
||||
pend -= t.acc & inf;
|
||||
// Label this transition with all non-pending
|
||||
// inf sets. The strip will shift everything
|
||||
|
|
@ -212,7 +212,7 @@ namespace spot
|
|||
auto a = in->state_acc_sets(t.dst);
|
||||
if (a & scc_fin_wo_inf)
|
||||
continue;
|
||||
pend |= (a & fin) << 1;
|
||||
pend |= (a & fin) << 1U;
|
||||
pend -= a & inf;
|
||||
}
|
||||
pend |= scc_inf_wo_fin;
|
||||
|
|
@ -250,7 +250,7 @@ namespace spot
|
|||
auto a = in->state_acc_sets(t.dst);
|
||||
if (a & scc_fin_wo_inf)
|
||||
continue;
|
||||
pend = (a & fin) << 1;
|
||||
pend = (a & fin) << 1U;
|
||||
pend -= a & inf;
|
||||
}
|
||||
st2gba_state d(t.dst, pend | scc_inf_wo_fin);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue