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

acc: move unsat_mark in acc_cond

Browse source 
so that we can optimize it when no Fin are used

* spot/twa/acc.cc, spot/twa/acc.hh: Do it.
* spot/twaalgos/complete.cc, spot/twaalgos/strength.cc: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2015-12-09 11:21:41 +01:00
parent 2d3e7cecf5
commit 9bbcf85b3a
4 changed files with 17 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

10
spot/twa/acc.cc
View file

@ -857,12 +857,14 @@ namespace spot
}
std::pair<bool, acc_cond::mark_t>
acc_cond::acc_code::unsat_mark() const
acc_cond::unsat_mark() const
{
if (empty())
if (is_tt())
return {false, 0U};
if (!uses_fin_acceptance())
return {true, 0U};
auto used = acc_cond::acc_code::used_sets();
auto used = code_.used_sets();
unsigned c = used.count();
unsigned max = used.max_set();
@ -884,7 +886,7 @@ namespace spot
}
}
bdd res = to_bdd_rec(&back(), &r[0]);
bdd res = to_bdd_rec(&code_.back(), &r[0]);
if (res == bddtrue)
return {false, 0U};

9
spot/twa/acc.hh
View file

@ -832,10 +832,6 @@ namespace spot
// Return the set of sets appearing in the condition.
acc_cond::mark_t used_sets() const;
// Return (true, m) if there exist some m that does not satisfy
// the acceptance condition. Return (false, 0U) otherwise.
std::pair<bool, acc_cond::mark_t> unsat_mark() const;
// Return the sets used as Inf or Fin in the acceptance condition
std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
@ -958,6 +954,11 @@ namespace spot
return acc_code::inf(m);
}
// Return (true, m) if there exist some acceptance mark m that
// does not satisfy the acceptance condition. Return (false, 0U)
// otherwise.
std::pair<bool, acc_cond::mark_t> unsat_mark() const;
protected:
bool check_fin_acceptance() const;

2
spot/twaalgos/complete.cc
View file

@ -34,7 +34,7 @@ namespace spot
// UM is a pair (bool, mark). If the Boolean is false, the
// acceptance is always satisfiable. Otherwise, MARK is an
// example of unsatisfiable mark.
auto um = aut->get_acceptance().unsat_mark();
auto um = aut->acc().unsat_mark();
if (!um.first)
{
// We cannot safely complete an automaton if its

21
spot/twaalgos/strength.cc
View file

@ -171,26 +171,15 @@ namespace spot
(std::string("unknown option for decompose_strength(): ") + c);
}
auto p = aut->acc().unsat_mark();
bool all_accepting = !p.first;
acc_cond::mark_t wacc = 0U; // Acceptance for weak SCCs
acc_cond::mark_t uacc = 0U; // Acceptance for "needed" SCCs, that
// we only want to traverse.
acc_cond::mark_t uacc = p.second; // Acceptance for "needed" SCCs, that
// we only want to traverse.
// If the acceptance condition is always satisfiable, we will
// consider the automaton has weak (even if that is not the
// consider the automaton as weak (even if that is not the
// case syntactically) and not output any strong part.
bool all_accepting = false;
if (aut->acc().is_tt())
{
all_accepting = true;
}
else if (aut->acc().uses_fin_acceptance())
{
auto p = aut->get_acceptance().unsat_mark();
if (p.first)
uacc = p.second;
else
all_accepting = true;
}
if (all_accepting)
{
keep &= ~Strong;