spot  2.4.4
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 32 "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 universal = spot::trival::maybe();
162  spot::trival existential = spot::trival::maybe();
163  spot::trival complete = spot::trival::maybe();
164  bool trans_acc_seen = false;
165 
166  std::map<std::string, spot::location> labels;
167 
168  prop_info prop_is_true(const std::string& p)
169  {
170  auto i = props.find(p);
171  if (i == props.end())
172  return prop_info{spot::location(), false};
173  return i->second;
174  }
175 
176  prop_info prop_is_false(const std::string& p)
177  {
178  auto i = props.find(p);
179  if (i == props.end())
180  return prop_info{spot::location(), false};
181  return prop_info{i->second.loc, !i->second.val};
182  }
183 
184  ~result_()
185  {
186  delete namer;
187  delete acc_mapper;
188  }
189  };
190  }
191 
192 #line 193 "parseaut.hh" // lalr1.cc:377
193 
194 
195 # include <cstdlib> // std::abort
196 # include <iostream>
197 # include <stdexcept>
198 # include <string>
199 # include <vector>
200 # include "stack.hh"
201 
202 
203 
204 #ifndef YY_ATTRIBUTE
205 # if (defined __GNUC__ \
206  && (2 < __GNUC__ || (__GNUC__ == 2 && 96 <= __GNUC_MINOR__))) \
207  || defined __SUNPRO_C && 0x5110 <= __SUNPRO_C
208 # define YY_ATTRIBUTE(Spec) __attribute__(Spec)
209 # else
210 # define YY_ATTRIBUTE(Spec) /* empty */
211 # endif
212 #endif
213 
214 #ifndef YY_ATTRIBUTE_PURE
215 # define YY_ATTRIBUTE_PURE YY_ATTRIBUTE ((__pure__))
216 #endif
217 
218 #ifndef YY_ATTRIBUTE_UNUSED
219 # define YY_ATTRIBUTE_UNUSED YY_ATTRIBUTE ((__unused__))
220 #endif
221 
222 #if !defined _Noreturn \
223  && (!defined __STDC_VERSION__ || __STDC_VERSION__ < 201112)
224 # if defined _MSC_VER && 1200 <= _MSC_VER
225 # define _Noreturn __declspec (noreturn)
226 # else
227 # define _Noreturn YY_ATTRIBUTE ((__noreturn__))
228 # endif
229 #endif
230 
231 /* Suppress unused-variable warnings by "using" E. */
232 #if ! defined lint || defined __GNUC__
233 # define YYUSE(E) ((void) (E))
234 #else
235 # define YYUSE(E) /* empty */
236 #endif
237 
238 #if defined __GNUC__ && 407 <= __GNUC__ * 100 + __GNUC_MINOR__
239 /* Suppress an incorrect diagnostic about yylval being uninitialized. */
240 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
241  _Pragma ("GCC diagnostic push") \
242  _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"")\
243  _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"")
244 # define YY_IGNORE_MAYBE_UNINITIALIZED_END \
245  _Pragma ("GCC diagnostic pop")
246 #else
247 # define YY_INITIAL_VALUE(Value) Value
248 #endif
249 #ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
250 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
251 # define YY_IGNORE_MAYBE_UNINITIALIZED_END
252 #endif
253 #ifndef YY_INITIAL_VALUE
254 # define YY_INITIAL_VALUE(Value) /* Nothing. */
255 #endif
256 
257 /* Debug traces. */
258 #ifndef YYDEBUG
259 # define YYDEBUG 1
260 #endif
261 
262 
263 namespace hoayy {
264 #line 265 "parseaut.hh" // lalr1.cc:377
265 
266 
267 
268 
269 
271  class parser
272  {
273  public:
274 #ifndef YYSTYPE
275  union semantic_type
277  {
278  #line 187 "parseaut.yy" // lalr1.cc:377
279 
280  std::string* str;
281  unsigned int num;
282  int b;
284  pair* p;
285  std::list<pair>* list;
287  std::vector<unsigned>* states;
288 
289 #line 290 "parseaut.hh" // lalr1.cc:377
290  };
291 #else
292  typedef YYSTYPE semantic_type;
293 #endif
294  typedef spot::location location_type;
296 
298  struct syntax_error : std::runtime_error
299  {
300  syntax_error (const location_type& l, const std::string& m);
301  location_type location;
302  };
303 
305  struct token
306  {
307  enum yytokentype
308  {
309  ENDOFFILE = 0,
310  HOA = 258,
311  STATES = 259,
312  START = 260,
313  AP = 261,
314  ALIAS = 262,
315  ACCEPTANCE = 263,
316  ACCNAME = 264,
317  TOOL = 265,
318  NAME = 266,
319  PROPERTIES = 267,
320  BODY = 268,
321  END = 269,
322  STATE = 270,
323  SPOT_HIGHLIGHT_EDGES = 271,
324  SPOT_HIGHLIGHT_STATES = 272,
325  IDENTIFIER = 273,
326  HEADERNAME = 274,
327  ANAME = 275,
328  STRING = 276,
329  INT = 277,
330  DRA = 278,
331  DSA = 279,
332  V2 = 280,
333  EXPLICIT = 281,
334  ACCPAIRS = 282,
335  ACCSIG = 283,
336  ENDOFHEADER = 284,
337  NEVER = 285,
338  SKIP = 286,
339  IF = 287,
340  FI = 288,
341  DO = 289,
342  OD = 290,
343  ARROW = 291,
344  GOTO = 292,
345  FALSE = 293,
346  ATOMIC = 294,
347  ASSERT = 295,
348  FORMULA = 296,
349  ENDAUT = 297,
350  ENDDSTAR = 298,
351  LBTT = 299,
352  INT_S = 300,
353  LBTT_EMPTY = 301,
354  ACC = 302,
355  STATE_NUM = 303,
356  DEST_NUM = 304
357  };
358  };
359 
361  typedef token::yytokentype token_type;
362 
364  typedef int symbol_number_type;
365 
367  enum { empty_symbol = -2 };
368 
370  typedef unsigned char token_number_type;
371 
378  template <typename Base>
379  struct basic_symbol : Base
380  {
382  typedef Base super_type;
383 
385  basic_symbol ();
386 
388  basic_symbol (const basic_symbol& other);
389 
391  basic_symbol (typename Base::kind_type t,
392  const location_type& l);
393 
395  basic_symbol (typename Base::kind_type t,
396  const semantic_type& v,
397  const location_type& l);
398 
400  ~basic_symbol ();
401 
403  void clear ();
404 
406  bool empty () const;
407 
409  void move (basic_symbol& s);
410 
412  semantic_type value;
413 
415  location_type location;
416 
417  private:
419  basic_symbol& operator= (const basic_symbol& other);
420  };
421 
423  struct by_type
424  {
426  by_type ();
427 
429  by_type (const by_type& other);
430 
432  typedef token_type kind_type;
433 
435  by_type (kind_type t);
436 
438  void clear ();
439 
441  void move (by_type& that);
442 
445  symbol_number_type type_get () const;
446 
448  token_type token () const;
449 
453  int type;
454  };
455 
458 
459 
461  parser (void* scanner_yyarg, result_& res_yyarg, spot::location initial_loc_yyarg);
462  virtual ~parser ();
463 
466  virtual int parse ();
467 
468 #if YYDEBUG
469  std::ostream& debug_stream () const YY_ATTRIBUTE_PURE;
472  void set_debug_stream (std::ostream &);
473 
475  typedef int debug_level_type;
477  debug_level_type debug_level () const YY_ATTRIBUTE_PURE;
479  void set_debug_level (debug_level_type l);
480 #endif
481 
485  virtual void error (const location_type& loc, const std::string& msg);
486 
488  void error (const syntax_error& err);
489 
490  private:
492  parser (const parser&);
493  parser& operator= (const parser&);
494 
496  typedef int state_type;
497 
501  virtual std::string yysyntax_error_ (state_type yystate,
502  const symbol_type& yyla) const;
503 
507  state_type yy_lr_goto_state_ (state_type yystate, int yysym);
508 
511  static bool yy_pact_value_is_default_ (int yyvalue);
512 
515  static bool yy_table_value_is_error_ (int yyvalue);
516 
517  static const short int yypact_ninf_;
518  static const signed char yytable_ninf_;
519 
521  static token_number_type yytranslate_ (int t);
522 
523  // Tables.
524  // YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
525  // STATE-NUM.
526  static const short int yypact_[];
527 
528  // YYDEFACT[STATE-NUM] -- Default reduction number in state STATE-NUM.
529  // Performed when YYTABLE does not specify something else to do. Zero
530  // means the default is an error.
531  static const unsigned char yydefact_[];
532 
533  // YYPGOTO[NTERM-NUM].
534  static const short int yypgoto_[];
535 
536  // YYDEFGOTO[NTERM-NUM].
537  static const short int yydefgoto_[];
538 
539  // YYTABLE[YYPACT[STATE-NUM]] -- What to do in state STATE-NUM. If
540  // positive, shift that token. If negative, reduce the rule whose
541  // number is the opposite. If YYTABLE_NINF, syntax error.
542  static const short int yytable_[];
543 
544  static const short int yycheck_[];
545 
546  // YYSTOS[STATE-NUM] -- The (internal number of the) accessing
547  // symbol of state STATE-NUM.
548  static const unsigned char yystos_[];
549 
550  // YYR1[YYN] -- Symbol number of symbol that rule YYN derives.
551  static const unsigned char yyr1_[];
552 
553  // YYR2[YYN] -- Number of symbols on the right hand side of rule YYN.
554  static const unsigned char yyr2_[];
555 
556 
558  static std::string yytnamerr_ (const char *n);
559 
560 
562  static const char* const yytname_[];
563 #if YYDEBUG
564  // YYRLINE[YYN] -- Source line where rule number YYN was defined.
565  static const unsigned short int yyrline_[];
567  virtual void yy_reduce_print_ (int r);
569  virtual void yystack_print_ ();
570 
571  // Debugging.
572  int yydebug_;
573  std::ostream* yycdebug_;
574 
578  template <typename Base>
579  void yy_print_ (std::ostream& yyo, const basic_symbol<Base>& yysym) const;
580 #endif
581 
586  template <typename Base>
587  void yy_destroy_ (const char* yymsg, basic_symbol<Base>& yysym) const;
588 
589  private:
591  struct by_state
592  {
594  by_state ();
595 
597  typedef state_type kind_type;
598 
600  by_state (kind_type s);
601 
603  by_state (const by_state& other);
604 
606  void clear ();
607 
609  void move (by_state& that);
610 
613  symbol_number_type type_get () const;
614 
616  enum { empty_state = -1 };
617 
620  state_type state;
621  };
622 
624  struct stack_symbol_type : basic_symbol<by_state>
625  {
627  typedef basic_symbol<by_state> super_type;
629  stack_symbol_type ();
631  stack_symbol_type (state_type s, symbol_type& sym);
633  stack_symbol_type& operator= (const stack_symbol_type& that);
634  };
635 
638 
640  stack_type yystack_;
641 
647  void yypush_ (const char* m, stack_symbol_type& s);
648 
655  void yypush_ (const char* m, state_type s, symbol_type& sym);
656 
658  void yypop_ (unsigned int n = 1);
659 
661  enum
662  {
663  yyeof_ = 0,
664  yylast_ = 235,
665  yynnts_ = 82,
666  yyfinal_ = 24,
667  yyterror_ = 1,
668  yyerrcode_ = 256,
669  yyntokens_ = 65
670  };
671 
672 
673  // User arguments.
674  void* scanner;
675  result_& res;
676  spot::location initial_loc;
677  };
678 
679 
680 
681 } // hoayy
682 #line 683 "parseaut.hh" // lalr1.cc:377
683 
684 
685 
686 
687 #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:276
semantic_type value
The semantic value.
Definition: parseaut.hh:412
Syntax errors thrown from user actions.
Definition: parseaut.hh:298
Definition: formula.hh:1678
Definition: parseaut.hh:92
Definition: ngraph.hh:32
token::yytokentype token_type
(External) token type, as returned by yylex.
Definition: parseaut.hh:361
Definition: parseaut.hh:263
Definition: public.hh:92
Definition: parseaut.hh:115
Tokens.
Definition: parseaut.hh:305
Type access provider for token (enum) based symbols.
Definition: parseaut.hh:423
token_type kind_type
The symbol type as needed by the constructor.
Definition: parseaut.hh:432
Base super_type
Alias to Base.
Definition: parseaut.hh:382
unsigned char token_number_type
Internal symbol number for tokens (subsumed by symbol_number_type).
Definition: parseaut.hh:370
A class implementing Kleene&#39;s three-valued logic.
Definition: trival.hh:33
int type
Definition: parseaut.hh:453
basic_symbol< by_type > symbol_type
"External" symbols: returned by the scanner.
Definition: parseaut.hh:457
spot::location location_type
Symbol locations.
Definition: parseaut.hh:295
Definition: parseaut.hh:67
A Bison parser.
Definition: parseaut.hh:271
Definition: parseaut.hh:379
Definition: acc.hh:335
location_type location
The location.
Definition: parseaut.hh:415
int symbol_number_type
Symbol type: an internal symbol number.
Definition: parseaut.hh:364
Definition: acc.hh:39
int debug_level_type
Type for debugging levels.
Definition: parseaut.hh:475

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Mon Dec 25 2017 14:51:14 for spot by doxygen 1.8.13