public.hh 3.26 KB
 Alexandre Duret-Lutz committed Jan 22, 2010 1 2 ``````// Copyright (C) 2010 Laboratoire de Recherche et Développement de // l'Epita (LRDE). `````` Alexandre Duret-Lutz committed Feb 25, 2008 3 4 5 ``````// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. `````` Alexandre Duret-Lutz committed Nov 21, 2003 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 ``````// // 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 Apr 15, 2003 24 25 26 ``````#ifndef SPOT_LTLPARSE_PUBLIC_HH # define SPOT_LTLPARSE_PUBLIC_HH `````` Alexandre Duret-Lutz committed Apr 16, 2003 27 ``````# include "ltlast/formula.hh" `````` Alexandre Duret-Lutz committed Feb 25, 2008 28 29 30 ``````// Unfortunately Bison 2.3 uses the same guards in all parsers :( # undef BISON_LOCATION_HH # undef BISON_POSITION_HH `````` Alexandre Duret-Lutz committed Feb 25, 2008 31 ``````# include "ltlparse/location.hh" `````` Alexandre Duret-Lutz committed Apr 17, 2003 32 33 ``````# include "ltlenv/defaultenv.hh" # include `````` Alexandre Duret-Lutz committed Apr 15, 2003 34 35 ``````# include # include `````` Alexandre Duret-Lutz committed Aug 09, 2004 36 ``````# include `````` Alexandre Duret-Lutz committed Apr 15, 2003 37 `````` `````` Alexandre Duret-Lutz committed Jun 04, 2003 38 ``````namespace spot `````` Alexandre Duret-Lutz committed Apr 15, 2003 39 40 41 ``````{ namespace ltl { `````` Alexandre Duret-Lutz committed Nov 17, 2004 42 43 44 `````` /// \addtogroup ltl_io /// @{ `````` Alexandre Duret-Lutz committed Jan 22, 2010 45 ``````#ifndef SWIG `````` Alexandre Duret-Lutz committed Apr 18, 2003 46 `````` /// \brief A parse diagnostic with its location. `````` Alexandre Duret-Lutz committed Feb 25, 2008 47 `````` typedef std::pair parse_error; `````` Alexandre Duret-Lutz committed Apr 18, 2003 48 `````` /// \brief A list of parser diagnostics, as filled by parse. `````` Alexandre Duret-Lutz committed Apr 15, 2003 49 `````` typedef std::list parse_error_list; `````` Alexandre Duret-Lutz committed Jan 22, 2010 50 51 52 53 ``````#else // Turn parse_error_list into an opaque type for Swig. struct parse_error_list {}; #endif `````` Alexandre Duret-Lutz committed Aug 09, 2004 54 `````` `````` Alexandre Duret-Lutz committed Apr 18, 2003 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 `````` /// \brief Build a formula from an LTL string. /// \param ltl_string The string to parse. /// \param error_list A list that will be filled with /// parse errors that occured during parsing. /// \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 formula built from \a ltl_string, or /// 0 if the input was unparsable. /// /// 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 ltl_string. If you want to make sure \a ltl_string /// was parsed succesfully, check \a error_list for emptiness. /// /// \warning This function is not reentrant. `````` Alexandre Duret-Lutz committed Jun 04, 2003 70 `````` formula* parse(const std::string& ltl_string, `````` Alexandre Duret-Lutz committed Apr 17, 2003 71 72 73 `````` parse_error_list& error_list, environment& env = default_environment::instance(), bool debug = false); `````` Alexandre Duret-Lutz committed Apr 16, 2003 74 `````` `````` Alexandre Duret-Lutz committed Apr 18, 2003 75 76 77 78 79 80 `````` /// \brief Format diagnostics produced by spot::ltl::parse. /// \param os Where diagnostics should be output. /// \param ltl_string The string that were parsed. /// \param error_list The error list filled by spot::ltl::parse while /// parsing \a ltl_string. /// \return \c true iff any diagnostic was output. `````` Alexandre Duret-Lutz committed Apr 16, 2003 81 82 83 `````` bool format_parse_errors(std::ostream& os, const std::string& ltl_string, parse_error_list& error_list); `````` Alexandre Duret-Lutz committed Nov 17, 2004 84 85 `````` /// @} `````` Alexandre Duret-Lutz committed Apr 15, 2003 86 87 88 89 `````` } } #endif // SPOT_LTLPARSE_PUBLIC_HH``````