spot  2.12
parse.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) by the Spot authors, see the AUTHORS file for details.
3 //
4 // This file is part of Spot, a model checking library.
5 //
6 // Spot is free software; you can redistribute it and/or modify it
7 // under the terms of the GNU General Public License as published by
8 // the Free Software Foundation; either version 3 of the License, or
9 // (at your option) any later version.
10 //
11 // Spot is distributed in the hope that it will be useful, but WITHOUT
12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 // License for more details.
15 //
16 // You should have received a copy of the GNU General Public License
17 // along with this program. If not, see <http://www.gnu.org/licenses/>.
18 
19 #pragma once
20 
21 #include <spot/tl/formula.hh>
22 #include <spot/misc/location.hh>
23 #include <spot/tl/defaultenv.hh>
24 #include <string>
25 #include <list>
26 #include <utility>
27 #include <iosfwd>
28 
29 namespace spot
30 {
33 
34 #ifndef SWIG
36  typedef std::pair<location, std::string> one_parse_error;
38  typedef std::list<one_parse_error> parse_error_list;
39 #else
40  // Turn parse_error_list into an opaque type for Swig.
41  struct parse_error_list {};
42 #endif
43 
45  struct SPOT_API parsed_formula final
46  {
50  formula f = nullptr;
51 
53  std::string input;
54 
62 
63  parsed_formula(const std::string& str = "")
64  : input(str)
65  {
66  }
67 
72  bool format_errors(std::ostream& os);
73 
92  bool format_errors(std::ostream& os,
93  const std::string& input,
94  unsigned shift);
95  };
96 
97 
116  SPOT_API
117  parsed_formula parse_infix_psl(const std::string& ltl_string,
118  environment& env =
120  bool debug = false,
121  bool lenient = false);
122 
139  SPOT_API
140  parsed_formula parse_infix_boolean(const std::string& ltl_string,
141  environment& env =
143  bool debug = false,
144  bool lenient = false);
145 
164  SPOT_API
165  parsed_formula parse_prefix_ltl(const std::string& ltl_string,
166  environment& env =
168  bool debug = false);
169 
176  SPOT_API formula
177  parse_formula(const std::string& ltl_string,
179 
197  SPOT_API
198  parsed_formula parse_infix_sere(const std::string& sere_string,
199  environment& env =
201  bool debug = false,
202  bool lenient = false);
203 
226  SPOT_API
227  void
228  fix_utf8_locations(const std::string& input_string,
229  parse_error_list& error_list);
230 
232 }
static default_environment & instance()
Get the sole instance of spot::default_environment.
An environment that describes atomic propositions.
Definition: environment.hh:29
Main class for temporal logic formula.
Definition: formula.hh:732
LTL/PSL formula interface.
parsed_formula parse_infix_boolean(const std::string &ltl_string, environment &env=default_environment::instance(), bool debug=false, bool lenient=false)
Build a Boolean formula from a string.
std::pair< location, std::string > one_parse_error
A parse diagnostic with its location.
Definition: parse.hh:36
parsed_formula parse_prefix_ltl(const std::string &ltl_string, environment &env=default_environment::instance(), bool debug=false)
Build a formula from an LTL string in LBT's format.
formula parse_formula(const std::string &ltl_string, environment &env=default_environment::instance())
A simple wrapper to parse_infix_psl() and parse_prefix_ltl().
parsed_formula parse_infix_sere(const std::string &sere_string, environment &env=default_environment::instance(), bool debug=false, bool lenient=false)
Build a formula from a string representing a SERE.
parsed_formula parse_infix_psl(const std::string &ltl_string, environment &env=default_environment::instance(), bool debug=false, bool lenient=false)
Build a formula from an LTL string.
void fix_utf8_locations(const std::string &input_string, parse_error_list &error_list)
Fix location of diagnostics assuming the input is utf8.
std::list< one_parse_error > parse_error_list
A list of parser diagnostics, as filled by parse.
Definition: parse.hh:38
Definition: automata.hh:26
The result of a formula parser.
Definition: parse.hh:46
parse_error_list errors
Syntax errors that occurred during parsing.
Definition: parse.hh:61
std::string input
The input text, before parsing.
Definition: parse.hh:53
bool format_errors(std::ostream &os, const std::string &input, unsigned shift)
Format shifted diagnostics.
bool format_errors(std::ostream &os)
Format diagnostics.

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1