public.hh 5.34 KB
 Alexandre Duret-Lutz committed Aug 23, 2013 1 ``````// -*- coding: utf-8 -*- `````` Alexandre Duret-Lutz committed Feb 05, 2014 2 3 ``````// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement // de l'Epita (LRDE). `````` Alexandre Duret-Lutz committed Aug 23, 2013 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 ``````// // 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 . #ifndef SPOT_DSTARPARSE_PUBLIC_HH # define SPOT_DSTARPARSE_PUBLIC_HH `````` Alexandre Duret-Lutz committed Aug 06, 2014 23 ``````# include "tgba/tgbagraph.hh" `````` Alexandre Duret-Lutz committed Aug 23, 2013 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 ``````# include "misc/location.hh" # include "ltlenv/defaultenv.hh" # include # include # include # include # include namespace spot { /// \addtogroup tgba_io /// @{ /// \brief A parse diagnostic with its location. typedef std::pair dstar_parse_error; /// \brief A list of parser diagnostics, as filled by parse. typedef std::list dstar_parse_error_list; enum dstar_type { Rabin, Streett }; /// \brief Temporary encoding of an omega automaton produced by /// ltl2dstar. struct SPOT_API dstar_aut { // Transition structure of the automaton. // This is encoded as a TGBA without acceptance condition. `````` Alexandre Duret-Lutz committed Aug 06, 2014 50 `````` tgba_digraph* aut; `````` Alexandre Duret-Lutz committed Aug 23, 2013 51 52 53 54 55 56 57 `````` /// Type of the acceptance. dstar_type type; /// Number of acceptance pairs. size_t accpair_count; /// \brief acceptance sets encoded as 2*num_state bit-vectors of /// num_pairs bits /// `````` Alexandre Duret-Lutz committed Feb 05, 2014 58 59 60 `````` /// Assuming F={(L₀,U₀),…,(Lᵢ,Uᵢ),…}, /// s∈Lᵢ iff accsets->at(s * 2).get(i), /// s∈Uᵢ iff accsets->at(s * 2 + 1).get(i). `````` Alexandre Duret-Lutz committed Aug 23, 2013 61 62 63 64 65 66 67 68 69 70 `````` bitvect_array* accsets; ~dstar_aut() { delete aut; delete accsets; } }; `````` Alexandre Duret-Lutz committed Aug 06, 2014 71 `````` /// \brief Build a spot::tgba_digraph from ltl2dstar's output. `````` Alexandre Duret-Lutz committed Aug 23, 2013 72 73 74 75 76 77 78 79 80 81 82 83 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 `````` /// \param filename The name of the file to parse. /// \param error_list A list that will be filled with /// parse errors that occured during parsing. /// \param dict The BDD dictionary where to use. /// \param env The environment of atomic proposition into which parsing /// should take place. /// \param debug When true, causes the parser to trace its execution. /// \return A pointer to the tgba built from \a filename, or /// 0 if the file could not be opened. /// /// Note that the parser usually tries to recover from errors. It can /// return an non zero value even if it encountered error during the /// parsing of \a filename. If you want to make sure \a filename /// was parsed succesfully, check \a error_list for emptiness. /// /// \warning This function is not reentrant. SPOT_API dstar_aut* dstar_parse(const std::string& filename, dstar_parse_error_list& error_list, bdd_dict* dict, ltl::environment& env = ltl::default_environment::instance(), bool debug = false); /// \brief Format diagnostics produced by spot::dstar_parse. /// \param os Where diagnostics should be output. /// \param filename The filename that should appear in the diagnostics. /// \param error_list The error list filled by spot::ltl::parse while /// parsing \a ltl_string. /// \return \c true iff any diagnostic was output. SPOT_API bool format_dstar_parse_errors(std::ostream& os, const std::string& filename, dstar_parse_error_list& error_list); /// \brief Convert a non-deterministic Rabin automaton into a /// non-deterministic Büchi automaton. `````` Alexandre Duret-Lutz committed Aug 12, 2014 109 `````` SPOT_API tgba_digraph* `````` Alexandre Duret-Lutz committed Aug 23, 2013 110 111 112 113 114 115 `````` nra_to_nba(const dstar_aut* nra); /// \brief Convert a non-deterministic Rabin automaton into a /// non-deterministic Büchi automaton. /// /// This version simply ignores all states in \a ignore. `````` Alexandre Duret-Lutz committed Aug 12, 2014 116 `````` SPOT_API tgba_digraph* `````` Alexandre Duret-Lutz committed Aug 23, 2013 117 118 119 `````` nra_to_nba(const dstar_aut* nra, const state_set* ignore); /// \brief Convert a deterministic Rabin automaton into a `````` Alexandre Duret-Lutz committed Aug 26, 2013 120 `````` /// Büchi automaton, deterministic when possible. `````` Alexandre Duret-Lutz committed Aug 23, 2013 121 122 123 `````` /// /// See "Deterministic ω-automata vis-a-vis Deterministic Büchi /// Automata", S. Krishnan, A. Puri, and R. Brayton (ISAAC'94) for `````` Alexandre Duret-Lutz committed Aug 26, 2013 124 `````` /// more details about a DRA->DBA construction. `````` Alexandre Duret-Lutz committed Aug 23, 2013 125 `````` /// `````` Alexandre Duret-Lutz committed Aug 26, 2013 126 127 128 129 130 131 132 133 134 `````` /// We essentially apply this method SCC-wise. If an SCC is /// DBA-realizable, we duplicate it in the output, fixing just /// the acceptance states. If an SCC is not DBA-realizable, /// then we apply the more usual conversion from Rabin to NBA /// for this part. /// /// If the optional \a dba_output argument is non-null, the /// pointed Boolean will be updated to indicate whether the /// returned Büchi automaton is deterministic. `````` Alexandre Duret-Lutz committed Aug 12, 2014 135 `````` SPOT_API tgba_digraph* `````` Alexandre Duret-Lutz committed Aug 26, 2013 136 `````` dra_to_ba(const dstar_aut* dra, bool* dba_output = 0); `````` Alexandre Duret-Lutz committed Aug 23, 2013 137 138 139 `````` /// \brief Convert a non-deterministic Streett automaton into a /// non-deterministic tgba. `````` Alexandre Duret-Lutz committed Aug 12, 2014 140 `````` SPOT_API tgba_digraph* `````` Alexandre Duret-Lutz committed Aug 23, 2013 141 142 143 144 `````` nsa_to_tgba(const dstar_aut* nra); /// \brief Convert a Rabin or Streett automaton into a TGBA. /// `````` Alexandre Duret-Lutz committed Aug 26, 2013 145 `````` /// This function calls dra_to_ba() or nsa_to_tgba(). `````` Alexandre Duret-Lutz committed Aug 12, 2014 146 `````` SPOT_API tgba_digraph* `````` Alexandre Duret-Lutz committed Aug 23, 2013 147 148 `````` dstar_to_tgba(const dstar_aut* dstar); `````` Alexandre Duret-Lutz committed Aug 23, 2013 149 150 151 152 153 `````` /// @} } #endif // SPOT_DSTARPARSE_PUBLIC_HH``````