automata.hh 5.21 KB
 Maximilien Colange committed Apr 21, 2017 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 // -*- coding: utf-8 -*- // Copyright (C) 2017 Laboratoire de Recherche et Developpement de // l'EPITA (LRDE). // // This file is part of Spot, a model checking library. // // Spot is free software; you can redistribute it and/or modify it // under the terms of the GNU General Public License as published by // the Free Software Foundation; either version 3 of the License, or // (at your option) any later version. // // Spot is distributed in the hope that it will be useful, but WITHOUT // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public // License for more details. // // You should have received a copy of the GNU General Public License // along with this program. If not, see . #pragma once  Alexandre Duret-Lutz committed Apr 28, 2017 22 23 #include #include  Alexandre Duret-Lutz committed Apr 28, 2017 24 #include  Maximilien Colange committed Apr 21, 2017 25 26 27 28 29  namespace spot { namespace gen {  Alexandre Duret-Lutz committed Apr 28, 2017 30 31 32 33  enum aut_pattern_id { AUT_BEGIN = 256, /// \brief A family of co-Büchi automata. ///  Alexandre Duret-Lutz committed Apr 28, 2017 34 35 36  /// Builds a co-Büchi automaton of size 2n+1 that is /// good-for-games and that has no equivalent deterministic /// co-Büchi automaton with less than 2^n / (2n+1) states.  Alexandre Duret-Lutz committed Apr 28, 2017 37  ///  Alexandre Duret-Lutz committed Sep 03, 2017 38  /// Only defined for n>0.  Alexandre Duret-Lutz committed Apr 28, 2017 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53  /// /** \verbatim @InProceedings{ kuperberg.15.icalp, author = {Denis Kuperberg and Micha{\l} Skrzypczak }, title = {On Determinisation of Good-for-Games Automata}, booktitle = {Proceedings of the 42nd International Colloquium on Automata, Languages, and Programming (ICALP'15)}, pages = {299--310}, year = {2015}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 9135, doi = {10.1007/978-3-662-47666-6_24} } \endverbatim */  Alexandre Duret-Lutz committed Sep 03, 2017 54  AUT_KS_NCA = AUT_BEGIN,  Alexandre Duret-Lutz committed Apr 28, 2017 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83  /// \brief Hard-to-complement non-deterministic Büchi automata /// /// Build a non-deterministic Büchi automaton with 3n+1 states /// and whose complementary language requires an automaton with /// at least n! states if Streett acceptance is used. /// /// Only defined for n>0. The automaton constructed corresponds /// to the right part of Fig.1 in the following paper, except /// that only state q_1 is initial. (The fact that states q_2, /// q_3, ..., and q_n are not initial as in the paper does not /// change the recognized language.) /// /** \verbatim @InProceedings{loding.99.fstts, author = {Christof L{\"o}ding}, title = {Optimal Bounds for Transformations of $\omega$-Automata}, booktitle = {Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'99)}, year = 1999, publisher = {Springer}, pages = {97--109}, series = {Lecture Notes in Computer Science}, volume = 1738, doi = {10.1007/3-540-46691-6_8} } \endverbatim */ AUT_L_NBA,  Alexandre Duret-Lutz committed Apr 28, 2017 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111  /// \brief DSA hard to convert to DRA. /// /// Build a deterministic Streett automaton 4n states, and n /// acceptance pairs, such that an equivalent deterministic Rabin /// automaton would require at least n! states. /// /// Only defined for 1