spot  2.3.5
parseaut.hh
Go to the documentation of this file.
1 // A Bison parser, made by GNU Bison 3.0.4.
2 
3 // Skeleton interface for Bison LALR(1) parsers in C++
4 
5 // Copyright (C) 2002-2015 Free Software Foundation, Inc.
6 
7 // This program is free software: you can redistribute it and/or modify
8 // it under the terms of the GNU General Public License as published by
9 // the Free Software Foundation, either version 3 of the License, or
10 // (at your option) any later version.
11 
12 // This program is distributed in the hope that it will be useful,
13 // but WITHOUT ANY WARRANTY; without even the implied warranty of
14 // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 // GNU General Public License for more details.
16 
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19 
20 // As a special exception, you may create a larger work that contains
21 // part or all of the Bison parser skeleton and distribute that work
22 // under terms of your choice, so long as that work isn't itself a
23 // parser generator using the skeleton or a modified version thereof
24 // as a parser skeleton. Alternatively, if you modify or redistribute
25 // the parser skeleton itself, you may (at your option) remove this
26 // special exception, which will cause the skeleton and the resulting
27 // Bison output files to be licensed under the GNU General Public
28 // License without this special exception.
29 
30 // This special exception was added by the Free Software Foundation in
31 // version 2.2 of Bison.
32 
38 // C++ LALR(1) parser skeleton written by Akim Demaille.
39 
40 #ifndef YY_HOAYY_PARSEAUT_HH_INCLUDED
41 # define YY_HOAYY_PARSEAUT_HH_INCLUDED
42 // // "%code requires" blocks.
43 #line 31 "parseaut.yy" // lalr1.cc:377
44 
45 #include "config.h"
46 #include <spot/misc/common.hh>
47 #include <string>
48 #include <cstring>
49 #include <sstream>
50 #include <unordered_map>
51 #include <algorithm>
52 #include <spot/twa/formula2bdd.hh>
53 #include <spot/parseaut/public.hh>
54 #include "spot/priv/accmap.hh"
55 #include <spot/tl/parse.hh>
56 #include <spot/twaalgos/alternation.hh>
57 
58 #ifndef HAVE_STRVERSCMP
59 // If the libc does not have this, a version is compiled in lib/.
60 extern "C" int strverscmp(const char *s1, const char *s2);
61 #endif
62 
63 // Work around Bison not letting us write
64 // %lex-param { res.h->errors }
65 #define PARSE_ERROR_LIST res.h->errors
66 
67  inline namespace hoayy_support
68  {
69  typedef std::map<int, bdd> map_t;
70 
71  /* Cache parsed formulae. Labels on arcs are frequently identical
72  and it would be a waste of time to parse them to formula
73  over and over, and to register all their atomic_propositions in
74  the bdd_dict. Keep the bdd result around so we can reuse
75  it. */
76  typedef std::map<std::string, bdd> formula_cache;
77 
78  typedef std::pair<int, std::string*> pair;
79  typedef spot::twa_graph::namer<std::string> named_tgba_t;
80 
81  // Note: because this parser is meant to be used on a stream of
82  // automata, it tries hard to recover from errors, so that we get a
83  // chance to reach the end of the current automaton in order to
84  // process the next one. Several variables below are used to keep
85  // track of various error conditions.
86  enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels,
87  Implicit_Labels };
88  enum acc_style_t { Mixed_Acc, State_Acc, Trans_Acc };
89 
90  struct result_
91  {
92  struct state_info
93  {
94  bool declared = false;
95  bool used = false;
96  spot::location used_loc;
97  };
98  spot::parsed_aut_ptr h;
99  spot::twa_ptr aut_or_ks;
101  std::string format_version;
102  spot::location format_version_loc;
103  spot::environment* env;
104  formula_cache fcache;
105  named_tgba_t* namer = nullptr;
106  spot::acc_mapper_int* acc_mapper = nullptr;
107  std::vector<int> ap;
108  std::vector<bdd> guards;
109  std::vector<bdd>::const_iterator cur_guard;
110  map_t dest_map;
111  std::vector<state_info> info_states; // States declared and used.
112  std::vector<std::pair<spot::location,
113  std::vector<unsigned>>> start; // Initial states;
114  std::unordered_map<std::string, bdd> alias;
115  struct prop_info
116  {
117  spot::location loc;
118  bool val;
119  operator bool() const
120  {
121  return val;
122  };
123  };
124  std::unordered_map<std::string, prop_info> props;
125  spot::location states_loc;
126  spot::location ap_loc;
127  spot::location state_label_loc;
128  spot::location accset_loc;
129  spot::acc_cond::mark_t acc_state;
130  spot::acc_cond::mark_t neg_acc_sets = 0U;
131  spot::acc_cond::mark_t pos_acc_sets = 0U;
132  int plus;
133  int minus;
134  std::vector<std::string>* state_names = nullptr;
135  std::map<unsigned, unsigned>* highlight_edges = nullptr;
136  std::map<unsigned, unsigned>* highlight_states = nullptr;
137  std::map<unsigned, unsigned> states_map;
138  std::set<int> ap_set;
139  unsigned cur_state;
140  int states = -1;
141  int ap_count = -1;
142  int accset = -1;
143  bdd state_label;
144  bdd cur_label;
145  bool has_state_label = false;
146  bool ignore_more_ap = false; // Set to true after the first "AP:"
147  // line has been read.
148  bool ignore_acc = false; // Set to true in case of missing
149  // Acceptance: lines.
150  bool ignore_acc_silent = false;
151  bool ignore_more_acc = false; // Set to true after the first
152  // "Acceptance:" line has been read.
153 
154  label_style_t label_style = Mixed_Labels;
155  acc_style_t acc_style = Mixed_Acc;
156 
157  bool accept_all_needed = false;
158  bool accept_all_seen = false;
159  bool aliased_states = false;
160 
161  spot::trival deterministic = spot::trival::maybe();
162  bool complete = false;
163  bool trans_acc_seen = false;
164 
165  std::map<std::string, spot::location> labels;
166 
167  prop_info prop_is_true(const std::string& p)
168  {
169  auto i = props.find(p);
170  if (i == props.end())
171  return prop_info{spot::location(), false};
172  return i->second;
173  }
174 
175  prop_info prop_is_false(const std::string& p)
176  {
177  auto i = props.find(p);
178  if (i == props.end())
179  return prop_info{spot::location(), false};
180  return prop_info{i->second.loc, !i->second.val};
181  }
182 
183  ~result_()
184  {
185  delete namer;
186  delete acc_mapper;
187  }
188  };
189  }
190 
191 #line 192 "parseaut.hh" // lalr1.cc:377
192 
193 
194 # include <cstdlib> // std::abort
195 # include <iostream>
196 # include <stdexcept>
197 # include <string>
198 # include <vector>
199 # include "stack.hh"
200 
201 
202 
203 #ifndef YY_ATTRIBUTE
204 # if (defined __GNUC__ \
205  && (2 < __GNUC__ || (__GNUC__ == 2 && 96 <= __GNUC_MINOR__))) \
206  || defined __SUNPRO_C && 0x5110 <= __SUNPRO_C
207 # define YY_ATTRIBUTE(Spec) __attribute__(Spec)
208 # else
209 # define YY_ATTRIBUTE(Spec) /* empty */
210 # endif
211 #endif
212 
213 #ifndef YY_ATTRIBUTE_PURE
214 # define YY_ATTRIBUTE_PURE YY_ATTRIBUTE ((__pure__))
215 #endif
216 
217 #ifndef YY_ATTRIBUTE_UNUSED
218 # define YY_ATTRIBUTE_UNUSED YY_ATTRIBUTE ((__unused__))
219 #endif
220 
221 #if !defined _Noreturn \
222  && (!defined __STDC_VERSION__ || __STDC_VERSION__ < 201112)
223 # if defined _MSC_VER && 1200 <= _MSC_VER
224 # define _Noreturn __declspec (noreturn)
225 # else
226 # define _Noreturn YY_ATTRIBUTE ((__noreturn__))
227 # endif
228 #endif
229 
230 /* Suppress unused-variable warnings by "using" E. */
231 #if ! defined lint || defined __GNUC__
232 # define YYUSE(E) ((void) (E))
233 #else
234 # define YYUSE(E) /* empty */
235 #endif
236 
237 #if defined __GNUC__ && 407 <= __GNUC__ * 100 + __GNUC_MINOR__
238 /* Suppress an incorrect diagnostic about yylval being uninitialized. */
239 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
240  _Pragma ("GCC diagnostic push") \
241  _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"")\
242  _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"")
243 # define YY_IGNORE_MAYBE_UNINITIALIZED_END \
244  _Pragma ("GCC diagnostic pop")
245 #else
246 # define YY_INITIAL_VALUE(Value) Value
247 #endif
248 #ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
249 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
250 # define YY_IGNORE_MAYBE_UNINITIALIZED_END
251 #endif
252 #ifndef YY_INITIAL_VALUE
253 # define YY_INITIAL_VALUE(Value) /* Nothing. */
254 #endif
255 
256 /* Debug traces. */
257 #ifndef YYDEBUG
258 # define YYDEBUG 1
259 #endif
260 
261 
262 namespace hoayy {
263 #line 264 "parseaut.hh" // lalr1.cc:377
264 
265 
266 
267 
268 
270  class parser
271  {
272  public:
273 #ifndef YYSTYPE
274  union semantic_type
276  {
277  #line 185 "parseaut.yy" // lalr1.cc:377
278 
279  std::string* str;
280  unsigned int num;
281  int b;
283  pair* p;
284  std::list<pair>* list;
286  std::vector<unsigned>* states;
287 
288 #line 289 "parseaut.hh" // lalr1.cc:377
289  };
290 #else
291  typedef YYSTYPE semantic_type;
292 #endif
293  typedef spot::location location_type;
295 
297  struct syntax_error : std::runtime_error
298  {
299  syntax_error (const location_type& l, const std::string& m);
300  location_type location;
301  };
302 
304  struct token
305  {
306  enum yytokentype
307  {
308  ENDOFFILE = 0,
309  HOA = 258,
310  STATES = 259,
311  START = 260,
312  AP = 261,
313  ALIAS = 262,
314  ACCEPTANCE = 263,
315  ACCNAME = 264,
316  TOOL = 265,
317  NAME = 266,
318  PROPERTIES = 267,
319  BODY = 268,
320  END = 269,
321  STATE = 270,
322  SPOT_HIGHLIGHT_EDGES = 271,
323  SPOT_HIGHLIGHT_STATES = 272,
324  IDENTIFIER = 273,
325  HEADERNAME = 274,
326  ANAME = 275,
327  STRING = 276,
328  INT = 277,
329  DRA = 278,
330  DSA = 279,
331  V2 = 280,
332  EXPLICIT = 281,
333  ACCPAIRS = 282,
334  ACCSIG = 283,
335  ENDOFHEADER = 284,
336  NEVER = 285,
337  SKIP = 286,
338  IF = 287,
339  FI = 288,
340  DO = 289,
341  OD = 290,
342  ARROW = 291,
343  GOTO = 292,
344  FALSE = 293,
345  ATOMIC = 294,
346  ASSERT = 295,
347  FORMULA = 296,
348  ENDAUT = 297,
349  ENDDSTAR = 298,
350  LBTT = 299,
351  INT_S = 300,
352  LBTT_EMPTY = 301,
353  ACC = 302,
354  STATE_NUM = 303,
355  DEST_NUM = 304
356  };
357  };
358 
360  typedef token::yytokentype token_type;
361 
363  typedef int symbol_number_type;
364 
366  enum { empty_symbol = -2 };
367 
369  typedef unsigned char token_number_type;
370 
377  template <typename Base>
378  struct basic_symbol : Base
379  {
381  typedef Base super_type;
382 
384  basic_symbol ();
385 
387  basic_symbol (const basic_symbol& other);
388 
390  basic_symbol (typename Base::kind_type t,
391  const location_type& l);
392 
394  basic_symbol (typename Base::kind_type t,
395  const semantic_type& v,
396  const location_type& l);
397 
399  ~basic_symbol ();
400 
402  void clear ();
403 
405  bool empty () const;
406 
408  void move (basic_symbol& s);
409 
411  semantic_type value;
412 
414  location_type location;
415 
416  private:
418  basic_symbol& operator= (const basic_symbol& other);
419  };
420 
422  struct by_type
423  {
425  by_type ();
426 
428  by_type (const by_type& other);
429 
431  typedef token_type kind_type;
432 
434  by_type (kind_type t);
435 
437  void clear ();
438 
440  void move (by_type& that);
441 
444  symbol_number_type type_get () const;
445 
447  token_type token () const;
448 
452  int type;
453  };
454 
457 
458 
460  parser (result_& res_yyarg, spot::location initial_loc_yyarg);
461  virtual ~parser ();
462 
465  virtual int parse ();
466 
467 #if YYDEBUG
468  std::ostream& debug_stream () const YY_ATTRIBUTE_PURE;
471  void set_debug_stream (std::ostream &);
472 
474  typedef int debug_level_type;
476  debug_level_type debug_level () const YY_ATTRIBUTE_PURE;
478  void set_debug_level (debug_level_type l);
479 #endif
480 
484  virtual void error (const location_type& loc, const std::string& msg);
485 
487  void error (const syntax_error& err);
488 
489  private:
491  parser (const parser&);
492  parser& operator= (const parser&);
493 
495  typedef int state_type;
496 
500  virtual std::string yysyntax_error_ (state_type yystate,
501  const symbol_type& yyla) const;
502 
506  state_type yy_lr_goto_state_ (state_type yystate, int yysym);
507 
510  static bool yy_pact_value_is_default_ (int yyvalue);
511 
514  static bool yy_table_value_is_error_ (int yyvalue);
515 
516  static const short int yypact_ninf_;
517  static const signed char yytable_ninf_;
518 
520  static token_number_type yytranslate_ (int t);
521 
522  // Tables.
523  // YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
524  // STATE-NUM.
525  static const short int yypact_[];
526 
527  // YYDEFACT[STATE-NUM] -- Default reduction number in state STATE-NUM.
528  // Performed when YYTABLE does not specify something else to do. Zero
529  // means the default is an error.
530  static const unsigned char yydefact_[];
531 
532  // YYPGOTO[NTERM-NUM].
533  static const short int yypgoto_[];
534 
535  // YYDEFGOTO[NTERM-NUM].
536  static const short int yydefgoto_[];
537 
538  // YYTABLE[YYPACT[STATE-NUM]] -- What to do in state STATE-NUM. If
539  // positive, shift that token. If negative, reduce the rule whose
540  // number is the opposite. If YYTABLE_NINF, syntax error.
541  static const short int yytable_[];
542 
543  static const short int yycheck_[];
544 
545  // YYSTOS[STATE-NUM] -- The (internal number of the) accessing
546  // symbol of state STATE-NUM.
547  static const unsigned char yystos_[];
548 
549  // YYR1[YYN] -- Symbol number of symbol that rule YYN derives.
550  static const unsigned char yyr1_[];
551 
552  // YYR2[YYN] -- Number of symbols on the right hand side of rule YYN.
553  static const unsigned char yyr2_[];
554 
555 
557  static std::string yytnamerr_ (const char *n);
558 
559 
561  static const char* const yytname_[];
562 #if YYDEBUG
563  // YYRLINE[YYN] -- Source line where rule number YYN was defined.
564  static const unsigned short int yyrline_[];
566  virtual void yy_reduce_print_ (int r);
568  virtual void yystack_print_ ();
569 
570  // Debugging.
571  int yydebug_;
572  std::ostream* yycdebug_;
573 
577  template <typename Base>
578  void yy_print_ (std::ostream& yyo, const basic_symbol<Base>& yysym) const;
579 #endif
580 
585  template <typename Base>
586  void yy_destroy_ (const char* yymsg, basic_symbol<Base>& yysym) const;
587 
588  private:
590  struct by_state
591  {
593  by_state ();
594 
596  typedef state_type kind_type;
597 
599  by_state (kind_type s);
600 
602  by_state (const by_state& other);
603 
605  void clear ();
606 
608  void move (by_state& that);
609 
612  symbol_number_type type_get () const;
613 
615  enum { empty_state = -1 };
616 
619  state_type state;
620  };
621 
623  struct stack_symbol_type : basic_symbol<by_state>
624  {
626  typedef basic_symbol<by_state> super_type;
628  stack_symbol_type ();
630  stack_symbol_type (state_type s, symbol_type& sym);
632  stack_symbol_type& operator= (const stack_symbol_type& that);
633  };
634 
637 
639  stack_type yystack_;
640 
646  void yypush_ (const char* m, stack_symbol_type& s);
647 
654  void yypush_ (const char* m, state_type s, symbol_type& sym);
655 
657  void yypop_ (unsigned int n = 1);
658 
660  enum
661  {
662  yyeof_ = 0,
663  yylast_ = 235,
664  yynnts_ = 82,
665  yyfinal_ = 24,
666  yyterror_ = 1,
667  yyerrcode_ = 256,
668  yyntokens_ = 65
669  };
670 
671 
672  // User arguments.
673  result_& res;
674  spot::location initial_loc;
675  };
676 
677 
678 
679 } // hoayy
680 #line 681 "parseaut.hh" // lalr1.cc:377
681 
682 
683 
684 
685 #endif // !YY_HOAYY_PARSEAUT_HH_INCLUDED
Definition: parseaut.hh:90
An environment that describes atomic propositions.
Definition: environment.hh:32
Symbol semantic values.
Definition: parseaut.hh:275
semantic_type value
The semantic value.
Definition: parseaut.hh:411
Syntax errors thrown from user actions.
Definition: parseaut.hh:297
Definition: formula.hh:1671
Definition: parseaut.hh:92
Definition: ngraph.hh:32
token::yytokentype token_type
(External) token type, as returned by yylex.
Definition: parseaut.hh:360
Definition: parseaut.hh:262
Definition: public.hh:92
Definition: parseaut.hh:115
Tokens.
Definition: parseaut.hh:304
Type access provider for token (enum) based symbols.
Definition: parseaut.hh:422
token_type kind_type
The symbol type as needed by the constructor.
Definition: parseaut.hh:431
Base super_type
Alias to Base.
Definition: parseaut.hh:381
unsigned char token_number_type
Internal symbol number for tokens (subsumed by symbol_number_type).
Definition: parseaut.hh:369
A class implementing Kleene&#39;s three-valued logic.
Definition: trival.hh:33
int type
Definition: parseaut.hh:452
basic_symbol< by_type > symbol_type
"External" symbols: returned by the scanner.
Definition: parseaut.hh:456
spot::location location_type
Symbol locations.
Definition: parseaut.hh:294
Definition: parseaut.hh:67
A Bison parser.
Definition: parseaut.hh:270
Definition: parseaut.hh:378
Definition: acc.hh:300
location_type location
The location.
Definition: parseaut.hh:414
int symbol_number_type
Symbol type: an internal symbol number.
Definition: parseaut.hh:363
Definition: acc.hh:34
int debug_level_type
Type for debugging levels.
Definition: parseaut.hh:474

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Thu Jun 22 2017 07:46:14 for spot by doxygen 1.8.13