public.hh 3.02 KB
 Alexandre Duret-Lutz committed Jan 03, 2005 1 ``````// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), `````` Alexandre Duret-Lutz committed Nov 21, 2003 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 ``````// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // 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 2 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 Spot; see the file COPYING. If not, write to the Free // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. `````` Alexandre Duret-Lutz committed Jun 05, 2003 22 23 24 25 ``````#ifndef SPOT_TGBAPARSE_PUBLIC_HH # define SPOT_TGBAPARSE_PUBLIC_HH # include "tgba/tgbaexplicit.hh" `````` Alexandre Duret-Lutz committed Jun 26, 2003 26 ``````# include "ltlparse/location.hh" `````` Alexandre Duret-Lutz committed Jun 05, 2003 27 28 29 30 ``````# include "ltlenv/defaultenv.hh" # include # include # include `````` Alexandre Duret-Lutz committed Aug 09, 2004 31 ``````# include `````` Alexandre Duret-Lutz committed Jun 05, 2003 32 33 34 `````` namespace spot { `````` Alexandre Duret-Lutz committed Nov 17, 2004 35 36 37 `````` /// \addtogroup tgba_io /// @{ `````` Alexandre Duret-Lutz committed Jun 05, 2003 38 `````` /// \brief A parse diagnostic with its location. `````` Alexandre Duret-Lutz committed Feb 01, 2005 39 `````` typedef std::pair tgba_parse_error; `````` Alexandre Duret-Lutz committed Jun 05, 2003 40 41 42 43 44 45 46 `````` /// \brief A list of parser diagnostics, as filled by parse. typedef std::list tgba_parse_error_list; /// \brief Build a spot::tgba_explicit from a text file. /// \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. `````` Alexandre Duret-Lutz committed Jul 14, 2003 47 `````` /// \param dict The BDD dictionary where to use. `````` Alexandre Duret-Lutz committed Jun 05, 2003 48 49 50 51 52 53 54 55 56 57 58 59 60 `````` /// \param env The environment 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. tgba_explicit* tgba_parse(const std::string& filename, tgba_parse_error_list& error_list, `````` Alexandre Duret-Lutz committed Jul 14, 2003 61 `````` bdd_dict* dict, `````` Alexandre Duret-Lutz committed Jun 05, 2003 62 63 64 65 66 67 `````` ltl::environment& env = ltl::default_environment::instance(), bool debug = false); /// \brief Format diagnostics produced by spot::tgba_parse. /// \param os Where diagnostics should be output. `````` Alexandre Duret-Lutz committed Jan 03, 2005 68 `````` /// \param filename The filename that should appear in the diagnostics. `````` Alexandre Duret-Lutz committed Jun 05, 2003 69 70 71 72 `````` /// \param error_list The error list filled by spot::ltl::parse while /// parsing \a ltl_string. /// \return \c true iff any diagnostic was output. bool format_tgba_parse_errors(std::ostream& os, `````` Alexandre Duret-Lutz committed Dec 16, 2004 73 `````` const std::string& filename, `````` Alexandre Duret-Lutz committed Jun 05, 2003 74 `````` tgba_parse_error_list& error_list); `````` Alexandre Duret-Lutz committed Nov 17, 2004 75 76 `````` /// @} `````` Alexandre Duret-Lutz committed Jun 05, 2003 77 78 79 ``````} #endif // SPOT_TGBAPARSE_PUBLIC_HH``````