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

genem: greatly simplify code

Browse source 
* spot/twaalgos/genem.cc: Simplify the code to be more
aligned to the Python version in genem.py.
This commit is contained in:
Alexandre Duret-Lutz 2019-03-30 16:38:43 +01:00
parent 55db24e00e
commit 8aafe74acf
1 changed files with 59 additions and 146 deletions
Download patch file Download diff file Expand all files Collapse all files

205
spot/twaalgos/genem.cc
View file

@ -25,189 +25,102 @@ namespace spot
{ {
namespace namespace
{ {
class temporary_acc_set static bool
is_scc_empty(const scc_info& si, unsigned scc,
const acc_cond& autacc, twa_run_ptr run,
acc_cond::mark_t tocut = {});
static bool
scc_split_check(const scc_info& si, unsigned scc, const acc_cond& acc,
twa_run_ptr run, acc_cond::mark_t tocut)
{ {
twa_graph_ptr aut_;
acc_cond old_acc_;
public:
temporary_acc_set(const const_twa_graph_ptr& aut,
acc_cond new_acc)
: aut_(std::const_pointer_cast<twa_graph>(aut)),
old_acc_(aut->acc())
{
set(new_acc);
}
void set(acc_cond new_acc)
{
aut_->set_acceptance(new_acc);
}
~temporary_acc_set()
{
aut_->set_acceptance(old_acc_);
}
};
bool scc_split_check(const scc_info& si, unsigned scc, twa_run_ptr run,
acc_cond::mark_t tocut,
bool (*ec_scc)(const scc_info& si,
unsigned scc,
twa_run_ptr run,
acc_cond::mark_t tocut))
{
// We want to remove tocut from the acceptance condition right
// now, because hopefully this will convert the acceptance
// condition into a Fin-less one, and then we do not have to
// recurse it.
auto& autacc = si.get_aut()->acc();
acc_cond acc = autacc.restrict_to(si.acc_sets_of(scc) - tocut);
acc = acc.remove(si.common_sets_of(scc), false);
scc_and_mark_filter filt(si, scc, tocut); scc_and_mark_filter filt(si, scc, tocut);
filt.override_acceptance(acc); filt.override_acceptance(acc);
scc_info upper_si(filt, scc_info_options::STOP_ON_ACC); scc_info upper_si(filt, scc_info_options::STOP_ON_ACC);
const int accepting_scc = upper_si.one_accepting_scc(); const int accepting_scc = upper_si.one_accepting_scc();
if (accepting_scc >= 0) if (accepting_scc >= 0)
{ {
if (run) if (run)
upper_si.get_accepting_run(accepting_scc, run); upper_si.get_accepting_run(accepting_scc, run);
return false; return false;
} }
if (!acc.uses_fin_acceptance()) if (!acc.uses_fin_acceptance())
return true; return true;
unsigned nscc = upper_si.scc_count(); unsigned nscc = upper_si.scc_count();
for (unsigned scc = 0; scc < nscc; ++scc) for (unsigned scc = 0; scc < nscc; ++scc)
if (!ec_scc(upper_si, scc, run, tocut)) if (!is_scc_empty(upper_si, scc, acc, run, tocut))
return false; return false;
return true; return true;
} }
template <bool deal_with_disjunct> static bool
bool generic_emptiness_check_for_scc_nocopy(const scc_info& si, is_scc_empty(const scc_info& si, unsigned scc,
unsigned scc, const acc_cond& autacc, twa_run_ptr run,
twa_run_ptr run, acc_cond::mark_t tocut)
acc_cond::mark_t
tocut = {})
{ {
if (si.is_rejecting_scc(scc)) if (si.is_rejecting_scc(scc))
return true; return true;
acc_cond::mark_t sets = si.acc_sets_of(scc); acc_cond::mark_t sets = si.acc_sets_of(scc);
auto& autacc = si.get_aut()->acc();
acc_cond acc = autacc.restrict_to(sets); acc_cond acc = autacc.restrict_to(sets);
acc = acc.remove(si.common_sets_of(scc), false); acc = acc.remove(si.common_sets_of(scc), false);
if (acc.is_f())
return true;
if (acc.is_t())
{
if (run)
si.get_accepting_run(scc, run);
return false;
}
temporary_acc_set tmp(si.get_aut(), acc);
if (acc_cond::mark_t fu = acc.fin_unit())
return scc_split_check
(si, scc, run, tocut | fu,
generic_emptiness_check_for_scc_nocopy<deal_with_disjunct>);
if (deal_with_disjunct) for (const acc_cond& disjunct: acc.top_disjuncts())
{ if (acc_cond::mark_t fu = disjunct.fin_unit())
acc_cond::acc_code& code = acc.get_acceptance(); {
assert(!code.empty()); if (!scc_split_check
auto pos = &code.back(); (si, scc, disjunct.remove(fu, true), run, fu))
auto start = &code.front(); return false;
assert(pos - pos->sub.size == start); }
if (pos->sub.op == acc_cond::acc_op::Or) else
{ {
do int fo = acc.fin_one();
{ assert(fo >= 0);
--pos; // Try to accept when Fin(fo) == true
acc_cond::acc_code one(pos); acc_cond::mark_t fo_m = {(unsigned) fo};
// This sets the acceptance of the automaton we if (!scc_split_check
// are working on. (si, scc, disjunct.remove(fo_m, true), run, fo_m))
tmp.set(one); return false;
// Because we use scc_info with STOP_ON_ACC and test // Try to accept when Fin(fo) == false
// for this, every clauses should contain a Fin. Also if (!is_scc_empty(si, scc, disjunct.force_inf(fo_m), run, tocut))
assert(si.get_aut()->acc().uses_fin_acceptance()); return false;
acc_cond::mark_t plus = {}; }
if (acc_cond::mark_t fu = one.fin_unit()) return true;
plus = fu;
if (!scc_split_check
(si, scc, run, tocut | plus,
generic_emptiness_check_for_scc_nocopy
<deal_with_disjunct>))
return false;
pos -= pos->sub.size;
}
while (pos > start);
return true;
}
if (pos->sub.op == acc_cond::acc_op::Fin)
{
tmp.set(acc_cond::acc_code());
for (unsigned d: pos[-1].mark.sets())
if (!scc_split_check
(si, scc, run,
tocut | acc_cond::mark_t({d}),
generic_emptiness_check_for_scc_nocopy
<deal_with_disjunct>))
return false;
return true;
}
}
int fo = acc.fin_one();
assert(fo >= 0);
// Try to accept when Fin(fo) == true
if (!scc_split_check
(si, scc, run, tocut | acc_cond::mark_t({(unsigned) fo}),
generic_emptiness_check_for_scc_nocopy
<deal_with_disjunct>))
return false;
// Try to accept when Fin(fo) == false
tmp.set(acc.force_inf({(unsigned) fo}));
return generic_emptiness_check_for_scc_nocopy
<deal_with_disjunct>(si, scc, run, tocut);
} }
template <bool deal_with_disjunct> static bool
bool generic_emptiness_check_main_nocopy(const twa_graph_ptr& aut, generic_emptiness_check_main(const twa_graph_ptr& aut,
twa_run_ptr run) twa_run_ptr run)
{ {
cleanup_acceptance_here(aut, false); cleanup_acceptance_here(aut, false);
auto& aut_acc = aut->acc(); auto& aut_acc = aut->acc();
if (aut_acc.is_f()) if (aut_acc.is_f())
return true; return true;
if (!aut->acc().uses_fin_acceptance()) if (!aut_acc.uses_fin_acceptance())
{
if (run)
{ {
auto p = aut->accepting_run(); if (!run)
if (p) return aut->is_empty();
{ if (auto p = aut->accepting_run())
*run = *p; {
return false; *run = *p;
} return false;
}
return true; return true;
} }
return aut->is_empty();
}
scc_info si(aut, scc_info_options::STOP_ON_ACC); scc_info si(aut, scc_info_options::STOP_ON_ACC);
const int accepting_scc = si.one_accepting_scc(); const int accepting_scc = si.one_accepting_scc();
if (accepting_scc >= 0) if (accepting_scc >= 0)
{ {
if (run) if (run)
si.get_accepting_run(accepting_scc, run); si.get_accepting_run(accepting_scc, run);
return false; return false;
} }
unsigned nscc = si.scc_count(); unsigned nscc = si.scc_count();
for (unsigned scc = 0; scc < nscc; ++scc) for (unsigned scc = 0; scc < nscc; ++scc)
if (!generic_emptiness_check_for_scc_nocopy if (!is_scc_empty(si, scc, aut_acc, run))
<deal_with_disjunct>(si, scc, run))
return false; return false;
return true; return true;
} }
@ -220,7 +133,7 @@ namespace spot
"does not support alternating automata"); "does not support alternating automata");
auto aut_ = std::const_pointer_cast<twa_graph>(aut); auto aut_ = std::const_pointer_cast<twa_graph>(aut);
acc_cond old = aut_->acc(); acc_cond old = aut_->acc();
bool res = generic_emptiness_check_main_nocopy<true>(aut_, nullptr); bool res = generic_emptiness_check_main(aut_, nullptr);
aut_->set_acceptance(old); aut_->set_acceptance(old);
return res; return res;
} }
@ -233,7 +146,7 @@ namespace spot
auto aut_ = std::const_pointer_cast<twa_graph>(aut); auto aut_ = std::const_pointer_cast<twa_graph>(aut);
acc_cond old = aut_->acc(); acc_cond old = aut_->acc();
twa_run_ptr run = std::make_shared<twa_run>(aut_); twa_run_ptr run = std::make_shared<twa_run>(aut_);
bool res = generic_emptiness_check_main_nocopy<true>(aut_, run); bool res = generic_emptiness_check_main(aut_, run);
aut_->set_acceptance(old); aut_->set_acceptance(old);
if (!res) if (!res)
return run; return run;
@ -246,6 +159,6 @@ namespace spot
if (SPOT_UNLIKELY(!si.get_aut()->is_existential())) if (SPOT_UNLIKELY(!si.get_aut()->is_existential()))
throw std::runtime_error("generic_emptiness_check_for_scc() " throw std::runtime_error("generic_emptiness_check_for_scc() "
"does not support alternating automata"); "does not support alternating automata");
return generic_emptiness_check_for_scc_nocopy<true>(si, scc, nullptr); return is_scc_empty(si, scc, si.get_aut()->acc(), nullptr);
} }
} }