diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc index 9fb382f98..3258bf8c7 100644 --- a/spot/twaalgos/genem.cc +++ b/spot/twaalgos/genem.cc @@ -50,10 +50,11 @@ namespace spot } }; - bool scc_split_check(const scc_info& si, unsigned scc, + 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)) { struct filter_data_t { @@ -85,14 +86,21 @@ namespace spot acc = acc.remove(si.common_sets_of(scc), false); temporary_acc_set tmp(si.get_aut(), acc); scc_info upper_si(si.get_aut(), si.one_state_of(scc), filter, &data, - scc_info_options::STOP_ON_ACC); - if (upper_si.one_accepting_scc() >= 0) + scc_info_options::STOP_ON_ACC + | scc_info_options::TRACK_STATES); + + const int accepting_scc = upper_si.one_accepting_scc(); + if (accepting_scc >= 0) + { + if (run) + upper_si.get_accepting_run(accepting_scc, run); return false; + } if (!acc.uses_fin_acceptance()) return true; unsigned nscc = upper_si.scc_count(); for (unsigned scc = 0; scc < nscc; ++scc) - if (!ec_scc(upper_si, scc, tocut)) + if (!ec_scc(upper_si, scc, run, tocut)) return false; return true; } @@ -100,6 +108,7 @@ namespace spot template bool generic_emptiness_check_for_scc_nocopy(const scc_info& si, unsigned scc, + twa_run_ptr run, acc_cond::mark_t tocut = {}) { @@ -112,11 +121,15 @@ namespace spot 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, tocut | fu, + (si, scc, run, tocut | fu, generic_emptiness_check_for_scc_nocopy); if (deal_with_disjunct) @@ -141,7 +154,7 @@ namespace spot if (acc_cond::mark_t fu = one.fin_unit()) plus = fu; if (!scc_split_check - (si, scc, tocut | plus, + (si, scc, run, tocut | plus, generic_emptiness_check_for_scc_nocopy )) return false; @@ -157,7 +170,7 @@ namespace spot tmp.set(acc_cond::acc_code()); for (unsigned d: pos[-1].mark.sets()) if (!scc_split_check - (si, scc, + (si, scc, run, tocut | acc_cond::mark_t({d}), generic_emptiness_check_for_scc_nocopy )) @@ -170,36 +183,54 @@ namespace spot assert(fo >= 0); // Try to accept when Fin(fo) == true if (!scc_split_check - (si, scc, tocut | acc_cond::mark_t({(unsigned) fo}), + (si, scc, run, tocut | acc_cond::mark_t({(unsigned) fo}), generic_emptiness_check_for_scc_nocopy )) return false; // Try to accept when Fin(fo) == false tmp.set(acc.force_inf({(unsigned) fo})); return generic_emptiness_check_for_scc_nocopy - (si, scc, tocut); - return true; + (si, scc, run, tocut); } template - bool generic_emptiness_check_main_nocopy(const twa_graph_ptr& aut) + bool generic_emptiness_check_main_nocopy(const twa_graph_ptr& aut, + twa_run_ptr run) { cleanup_acceptance_here(aut, false); auto& aut_acc = aut->acc(); if (aut_acc.is_f()) return true; if (!aut->acc().uses_fin_acceptance()) + { + if (run) + { + auto p = aut->accepting_run(); + if (p) + { + *run = *p; + return false; + } + return true; + } return aut->is_empty(); + } scc_info si(aut, scc_info_options::STOP_ON_ACC | scc_info_options::TRACK_STATES); - if (si.one_accepting_scc() >= 0) + + const int accepting_scc = si.one_accepting_scc(); + if (accepting_scc >= 0) + { + if (run) + si.get_accepting_run(accepting_scc, run); return false; + } unsigned nscc = si.scc_count(); for (unsigned scc = 0; scc < nscc; ++scc) if (!generic_emptiness_check_for_scc_nocopy - (si, scc)) + (si, scc, run)) return false; return true; } @@ -212,17 +243,35 @@ namespace spot "does not support alternating automata"); auto aut_ = std::const_pointer_cast(aut); acc_cond old = aut_->acc(); - bool res = generic_emptiness_check_main_nocopy(aut_); + bool res = generic_emptiness_check_main_nocopy(aut_, nullptr); aut_->set_acceptance(old); return res; } + twa_run_ptr generic_accepting_run(const const_twa_graph_ptr& aut) + { + if (SPOT_UNLIKELY(!aut->is_existential())) + throw std::runtime_error("generic_accepting_run() " + "does not support alternating automata"); + auto aut_ = std::const_pointer_cast(aut); + acc_cond old = aut_->acc(); + + twa_run_ptr run = std::make_shared(aut_); + bool res = generic_emptiness_check_main_nocopy(aut_, run); + + aut_->set_acceptance(old); + + if (!res) + return run; + return nullptr; + } + bool generic_emptiness_check_for_scc(const scc_info& si, unsigned scc) { if (SPOT_UNLIKELY(!si.get_aut()->is_existential())) throw std::runtime_error("generic_emptiness_check_for_scc() " "does not support alternating automata"); - return generic_emptiness_check_for_scc_nocopy(si, scc); + return generic_emptiness_check_for_scc_nocopy(si, scc, nullptr); } } diff --git a/spot/twaalgos/genem.hh b/spot/twaalgos/genem.hh index bdc8d7889..2f8a625f7 100644 --- a/spot/twaalgos/genem.hh +++ b/spot/twaalgos/genem.hh @@ -19,6 +19,7 @@ #pragma once +#include #include namespace spot @@ -28,6 +29,13 @@ namespace spot SPOT_API bool generic_emptiness_check(const const_twa_graph_ptr& aut); + /// \ingroup emptiness_check_algorithms + /// \brief Accepting run search in an automaton, for any acceptance condition. + /// \return An accepting run over the automaton, or nullptr if the language is + /// empty. + SPOT_API twa_run_ptr + generic_accepting_run(const const_twa_graph_ptr& aut); + /// \ingroup emptiness_check_algorithms /// \brief Emptiness check of one SCC, for any acceptance condition. SPOT_API bool diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index e7c9b08ac..bd9335c55 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -23,11 +23,11 @@ #include #include #include +#include #include #include #include - namespace spot { void scc_info::report_need_track_states() @@ -461,6 +461,141 @@ namespace spot determine_usefulness(); } + // Describes an explicit spot::twa_run::step + struct exp_step + { + unsigned src; + bdd cond; + acc_cond::mark_t acc; + }; + + // A reimplementation of spot::bfs_steps for explicit automata. + // bool filter(const twa_graph::edge_storage_t&) returns true if the + // transition has to be filtered out. + // bool match(struct exp_step&, unsigned dest) returns true if the BFS has to + // stop after this transition. + // Returns the destination of the matched transition, or -1 if no match has + // been found. + static int explicit_bfs_steps(const const_twa_graph_ptr aut, unsigned start, + twa_run::steps& steps, + std::function filter, + std::function match) + { + std::unordered_map backlinks; + std::deque bfs_queue; + bfs_queue.emplace_back(start); + + while (!bfs_queue.empty()) + { + unsigned src = bfs_queue.front(); + bfs_queue.pop_front(); + for (auto& t: aut->out(src)) + { + if (filter(t)) + continue; + + exp_step s = { src, t.cond, t.acc }; + if (match(s, t.dst)) + { + twa_run::steps path; + for (;;) + { + path.emplace_front(aut->state_from_number(s.src), s.cond, s.acc); + if (s.src == start) + break; + const auto& i = backlinks.find(s.src); + assert(i != backlinks.end()); + s = i->second; + } + steps.splice(steps.end(), path); + return t.dst; + } + + if (backlinks.emplace(t.dst, s).second) + bfs_queue.push_back(t.dst); + } + } + return -1; + } + + void scc_info::get_accepting_run(unsigned scc, twa_run_ptr r) const + { + const scc_info::scc_node& node = node_[scc]; + + if (!node.is_accepting()) + throw std::runtime_error("scc_info::get_accepting_cycle needs to be " + "called on an accepting scc"); + acc_cond actual_cond = aut_->acc().restrict_to(node.acc_marks()) + .force_inf(node.acc_marks()); + assert(!actual_cond.uses_fin_acceptance()); + + // List of states of the SCC + const std::set scc_states(node.states().cbegin(), + node.states().cend()); + + // Prefix search + + r->prefix.clear(); + + int init = aut_->get_init_state_number(); + int substart; + + if (scc_states.find(init) != scc_states.end()) + { + // The initial state is in the SCC + substart = init; + } + else + { + substart = explicit_bfs_steps(aut_, init, r->prefix, + [](const twa_graph::edge_storage_t&) + { + return false; // Do not filter. + }, + [&](exp_step&, unsigned dst) + { + // Match any state in the SCC. + return scc_states.find(dst) != scc_states.end(); + }); + } + + const unsigned start = (unsigned)substart; + + // Cycle search + + acc_cond::mark_t acc_to_see = actual_cond.accepting_sets(node.acc_marks()); + + r->cycle.clear(); + + do + { + substart = explicit_bfs_steps(aut_, substart, r->cycle, + [&](const twa_graph::edge_storage_t& t) + { + if (scc_states.find(t.dst) == scc_states.end()) + return true; // Destination is not in the SCC. + if (filter_) + // Filter out ignored and cut transitions. + return filter_(t, t.dst, filter_data_) + != edge_filter_choice::keep; + return false; + }, + [&](exp_step& st, unsigned dst) + { + if (!acc_to_see) // We have seen all the marks, go back to start. + return dst == start; + if (st.acc & acc_to_see) + { + acc_to_see -= st.acc; + return true; + } + return false; + }); + assert(0 <= substart); + } + while (acc_to_see || (unsigned)substart != start); + } + std::ostream& dump_scc_info_dot(std::ostream& out, const_twa_graph_ptr aut, scc_info* sccinfo) diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index 0acc69dfa..b114823fd 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -21,6 +21,7 @@ #include #include +#include namespace spot { @@ -595,6 +596,11 @@ namespace spot /// determine_unknown_acceptance(). bool check_scc_emptiness(unsigned n); + /// \brief Retrieves an accepting run of the automaton whose cycle is in the + /// SCC. + /// \param scc an accepting scc + void get_accepting_run(unsigned scc, twa_run_ptr r) const; + bool is_useful_scc(unsigned scc) const { if (SPOT_UNLIKELY(!!(options_ & scc_info_options::STOP_ON_ACC))) diff --git a/tests/python/genem.py b/tests/python/genem.py index 8eb6d96d5..58db36910 100644 --- a/tests/python/genem.py +++ b/tests/python/genem.py @@ -189,5 +189,8 @@ def run_bench(automata): res = str(res1)[0] + str(res2)[0] + str(res3)[0] print(res) assert res in ('TTT', 'FFF') + if res == 'FFF': + run3 = spot.generic_accepting_run(aut) + assert run3.replay(spot.get_cout()) is True run_bench([a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a11, a360])