diff --git a/doc/spot.bib b/doc/spot.bib index 23d56681f..ddfd746d8 100644 --- a/doc/spot.bib +++ b/doc/spot.bib @@ -31,6 +31,23 @@ doi = {10.1007/978-3-642-39176-7_6} } +@InProceedings{ baier.19.atva, + author = {Christel Baier and Franti\v{s}ek Blahoudek and Alexandre + Duret-Lutz and Joachim Klein and David M\"uller and Jan + Strej\v{c}ek}, + title = {Generic Emptiness Check for Fun and Profit}, + booktitle = {Proceedings of the 17th International Symposium on + Automated Technology for Verification and Analysis + (ATVA'19)}, + year = {2019}, + volume = {?????}, + series = {Lecture Notes in Computer Science}, + pages = {???--???}, + month = oct, + publisher = {Springer}, + note = {To appear} +} + @InProceedings{ beer.01.cav, author = {Ilan Beer and Shoham Ben-David and Cindy Eisner and Dana Fisman and Anna Gringauze and Yoav Rodeh}, diff --git a/spot/twaalgos/genem.hh b/spot/twaalgos/genem.hh index e35b3290d..c6b3d55a2 100644 --- a/spot/twaalgos/genem.hh +++ b/spot/twaalgos/genem.hh @@ -26,6 +26,11 @@ namespace spot { /// \ingroup emptiness_check_algorithms /// \brief Emptiness check of an automaton, for any acceptance condition. + /// + /// Currently only implemented for twa_graph automata, i.e., not automata + /// constructed on-the-fly. + /// + /// \cite baier.19.atva SPOT_API bool generic_emptiness_check(const const_twa_graph_ptr& aut); @@ -33,11 +38,16 @@ namespace spot /// \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. + /// + /// Currently only implemented for twa_graph automata, i.e., not automata + /// constructed on-the-fly. 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. + /// + /// \cite baier.19.atva SPOT_API bool generic_emptiness_check_for_scc(const scc_info& si, unsigned scc); @@ -46,6 +56,8 @@ namespace spot /// /// This version makes it possible to ignore the acceptance /// condition of the automaton, and use \a forced_acc. + /// + /// \cite baier.19.atva SPOT_API bool generic_emptiness_check_for_scc(const scc_info& si, unsigned scc, const acc_cond& forced_acc);