spot  2.7.3
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 33 "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 using namespace std::string_literals;
59 
60 #ifndef HAVE_STRVERSCMP
61 // If the libc does not have this, a version is compiled in lib/.
62 extern "C" int strverscmp(const char *s1, const char *s2);
63 #endif
64 
65 // Work around Bison not letting us write
66 // %lex-param { res.h->errors }
67 #define PARSE_ERROR_LIST res.h->errors
68 
69  inline namespace hoayy_support
70  {
71  typedef std::map<int, bdd> map_t;
72 
73  /* Cache parsed formulae. Labels on arcs are frequently identical
74  and it would be a waste of time to parse them to formula
75  over and over, and to register all their atomic_propositions in
76  the bdd_dict. Keep the bdd result around so we can reuse
77  it. */
78  typedef std::map<std::string, bdd> formula_cache;
79 
80  typedef std::pair<int, std::string*> pair;
81  typedef spot::twa_graph::namer<std::string> named_tgba_t;
82 
83  // Note: because this parser is meant to be used on a stream of
84  // automata, it tries hard to recover from errors, so that we get a
85  // chance to reach the end of the current automaton in order to
86  // process the next one. Several variables below are used to keep
87  // track of various error conditions.
88  enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels,
89  Implicit_Labels };
90  enum acc_style_t { Mixed_Acc, State_Acc, Trans_Acc };
91 
92  struct result_
93  {
94  struct state_info
95  {
96  bool declared = false;
97  bool used = false;
98  spot::location used_loc;
99  };
100  spot::parsed_aut_ptr h;
101  spot::twa_ptr aut_or_ks;
103  std::string format_version;
104  spot::location format_version_loc;
105  spot::environment* env;
106  formula_cache fcache;
107  named_tgba_t* namer = nullptr;
108  spot::acc_mapper_int* acc_mapper = nullptr;
109  std::vector<int> ap;
110  std::vector<bdd> guards;
111  std::vector<bdd>::const_iterator cur_guard;
112  // If "Alias: ..." occurs before "AP: ..." in the HOA format we
113  // are in trouble because the parser would like to turn each
114  // alias into a BDD, yet the atomic proposition have not been
115  // declared yet. We solve that by using arbitrary BDD variables
116  // numbers (in fact we use the same number given in the Alias:
117  // definition) and keeping track of the highest variable number
118  // we have seen (unknown_ap_max). Once AP: is encountered,
119  // we can remap everything. If AP: is never encountered an
120  // unknown_ap_max is non-negative, then we can signal an error.
121  int unknown_ap_max = -1;
122  spot::location unknown_ap_max_location;
123  bool in_alias = false;
124  map_t dest_map;
125  std::vector<state_info> info_states; // States declared and used.
126  std::vector<std::pair<spot::location,
127  std::vector<unsigned>>> start; // Initial states;
128  std::unordered_map<std::string, bdd> alias;
129  struct prop_info
130  {
131  spot::location loc;
132  bool val;
133  operator bool() const
134  {
135  return val;
136  };
137  };
138  std::unordered_map<std::string, prop_info> props;
139  spot::location states_loc;
140  spot::location ap_loc;
141  spot::location state_label_loc;
142  spot::location accset_loc;
143  spot::acc_cond::mark_t acc_state;
144  spot::acc_cond::mark_t neg_acc_sets = {};
145  spot::acc_cond::mark_t pos_acc_sets = {};
146  int plus;
147  int minus;
148  std::vector<std::string>* state_names = nullptr;
149  std::map<unsigned, unsigned>* highlight_edges = nullptr;
150  std::map<unsigned, unsigned>* highlight_states = nullptr;
151  std::map<unsigned, unsigned> states_map;
152  std::set<int> ap_set;
153  unsigned cur_state;
154  int states = -1;
155  int ap_count = -1;
156  int accset = -1;
157  bdd state_label;
158  bdd cur_label;
159  bool has_state_label = false;
160  bool ignore_more_ap = false; // Set to true after the first "AP:"
161  // line has been read.
162  bool ignore_acc = false; // Set to true in case of missing
163  // Acceptance: lines.
164  bool ignore_acc_silent = false;
165  bool ignore_more_acc = false; // Set to true after the first
166  // "Acceptance:" line has been read.
167 
168  label_style_t label_style = Mixed_Labels;
169  acc_style_t acc_style = Mixed_Acc;
170 
171  bool accept_all_needed = false;
172  bool accept_all_seen = false;
173  bool aliased_states = false;
174 
175  spot::trival universal = spot::trival::maybe();
176  spot::trival existential = spot::trival::maybe();
177  spot::trival complete = spot::trival::maybe();
178  bool trans_acc_seen = false;
179 
180  std::map<std::string, spot::location> labels;
181 
182  prop_info prop_is_true(const std::string& p)
183  {
184  auto i = props.find(p);
185  if (i == props.end())
186  return prop_info{spot::location(), false};
187  return i->second;
188  }
189 
190  prop_info prop_is_false(const std::string& p)
191  {
192  auto i = props.find(p);
193  if (i == props.end())
194  return prop_info{spot::location(), false};
195  return prop_info{i->second.loc, !i->second.val};
196  }
197 
198  ~result_()
199  {
200  delete namer;
201  delete acc_mapper;
202  }
203  };
204  }
205 
206 #line 207 "parseaut.hh" // lalr1.cc:377
207 
208 
209 # include <cstdlib> // std::abort
210 # include <iostream>
211 # include <stdexcept>
212 # include <string>
213 # include <vector>
214 # include "stack.hh"
215 
216 
217 
218 #ifndef YY_ATTRIBUTE
219 # if (defined __GNUC__ \
220  && (2 < __GNUC__ || (__GNUC__ == 2 && 96 <= __GNUC_MINOR__))) \
221  || defined __SUNPRO_C && 0x5110 <= __SUNPRO_C
222 # define YY_ATTRIBUTE(Spec) __attribute__(Spec)
223 # else
224 # define YY_ATTRIBUTE(Spec) /* empty */
225 # endif
226 #endif
227 
228 #ifndef YY_ATTRIBUTE_PURE
229 # define YY_ATTRIBUTE_PURE YY_ATTRIBUTE ((__pure__))
230 #endif
231 
232 #ifndef YY_ATTRIBUTE_UNUSED
233 # define YY_ATTRIBUTE_UNUSED YY_ATTRIBUTE ((__unused__))
234 #endif
235 
236 #if !defined _Noreturn \
237  && (!defined __STDC_VERSION__ || __STDC_VERSION__ < 201112)
238 # if defined _MSC_VER && 1200 <= _MSC_VER
239 # define _Noreturn __declspec (noreturn)
240 # else
241 # define _Noreturn YY_ATTRIBUTE ((__noreturn__))
242 # endif
243 #endif
244 
245 /* Suppress unused-variable warnings by "using" E. */
246 #if ! defined lint || defined __GNUC__
247 # define YYUSE(E) ((void) (E))
248 #else
249 # define YYUSE(E) /* empty */
250 #endif
251 
252 #if defined __GNUC__ && 407 <= __GNUC__ * 100 + __GNUC_MINOR__
253 /* Suppress an incorrect diagnostic about yylval being uninitialized. */
254 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
255  _Pragma ("GCC diagnostic push") \
256  _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"")\
257  _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"")
258 # define YY_IGNORE_MAYBE_UNINITIALIZED_END \
259  _Pragma ("GCC diagnostic pop")
260 #else
261 # define YY_INITIAL_VALUE(Value) Value
262 #endif
263 #ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
264 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
265 # define YY_IGNORE_MAYBE_UNINITIALIZED_END
266 #endif
267 #ifndef YY_INITIAL_VALUE
268 # define YY_INITIAL_VALUE(Value) /* Nothing. */
269 #endif
270 
271 /* Debug traces. */
272 #ifndef YYDEBUG
273 # define YYDEBUG 1
274 #endif
275 
276 
277 namespace hoayy {
278 #line 279 "parseaut.hh" // lalr1.cc:377
279 
280 
281 
282 
283 
285  class parser
286  {
287  public:
288 #ifndef YYSTYPE
289  union semantic_type
291  {
292  #line 202 "parseaut.yy" // lalr1.cc:377
293 
294  std::string* str;
295  unsigned int num;
296  int b;
298  pair* p;
299  std::list<pair>* list;
301  std::vector<unsigned>* states;
302 
303 #line 304 "parseaut.hh" // lalr1.cc:377
304  };
305 #else
306  typedef YYSTYPE semantic_type;
307 #endif
308  typedef spot::location location_type;
310 
312  struct syntax_error : std::runtime_error
313  {
314  syntax_error (const location_type& l, const std::string& m);
315  location_type location;
316  };
317 
319  struct token
320  {
321  enum yytokentype
322  {
323  ENDOFFILE = 0,
324  HOA = 258,
325  STATES = 259,
326  START = 260,
327  AP = 261,
328  ALIAS = 262,
329  ACCEPTANCE = 263,
330  ACCNAME = 264,
331  TOOL = 265,
332  NAME = 266,
333  PROPERTIES = 267,
334  BODY = 268,
335  END = 269,
336  STATE = 270,
337  SPOT_HIGHLIGHT_EDGES = 271,
338  SPOT_HIGHLIGHT_STATES = 272,
339  IDENTIFIER = 273,
340  HEADERNAME = 274,
341  ANAME = 275,
342  STRING = 276,
343  INT = 277,
344  DRA = 278,
345  DSA = 279,
346  V2 = 280,
347  EXPLICIT = 281,
348  ACCPAIRS = 282,
349  ACCSIG = 283,
350  ENDOFHEADER = 284,
351  NEVER = 285,
352  SKIP = 286,
353  IF = 287,
354  FI = 288,
355  DO = 289,
356  OD = 290,
357  ARROW = 291,
358  GOTO = 292,
359  FALSE = 293,
360  ATOMIC = 294,
361  ASSERT = 295,
362  FORMULA = 296,
363  ENDAUT = 297,
364  ENDDSTAR = 298,
365  LBTT = 299,
366  INT_S = 300,
367  LBTT_EMPTY = 301,
368  ACC = 302,
369  STATE_NUM = 303,
370  DEST_NUM = 304
371  };
372  };
373 
375  typedef token::yytokentype token_type;
376 
378  typedef int symbol_number_type;
379 
381  enum { empty_symbol = -2 };
382 
384  typedef unsigned char token_number_type;
385 
392  template <typename Base>
393  struct basic_symbol : Base
394  {
396  typedef Base super_type;
397 
399  basic_symbol ();
400 
402  basic_symbol (const basic_symbol& other);
403 
405  basic_symbol (typename Base::kind_type t,
406  const location_type& l);
407 
409  basic_symbol (typename Base::kind_type t,
410  const semantic_type& v,
411  const location_type& l);
412 
414  ~basic_symbol ();
415 
417  void clear ();
418 
420  bool empty () const;
421 
423  void move (basic_symbol& s);
424 
426  semantic_type value;
427 
429  location_type location;
430 
431  private:
433  basic_symbol& operator= (const basic_symbol& other);
434  };
435 
437  struct by_type
438  {
440  by_type ();
441 
443  by_type (const by_type& other);
444 
446  typedef token_type kind_type;
447 
449  by_type (kind_type t);
450 
452  void clear ();
453 
455  void move (by_type& that);
456 
459  symbol_number_type type_get () const;
460 
462  token_type token () const;
463 
467  int type;
468  };
469 
472 
473 
475  parser (void* scanner_yyarg, result_& res_yyarg, spot::location initial_loc_yyarg);
476  virtual ~parser ();
477 
480  virtual int parse ();
481 
482 #if YYDEBUG
483  std::ostream& debug_stream () const YY_ATTRIBUTE_PURE;
486  void set_debug_stream (std::ostream &);
487 
489  typedef int debug_level_type;
491  debug_level_type debug_level () const YY_ATTRIBUTE_PURE;
493  void set_debug_level (debug_level_type l);
494 #endif
495 
499  virtual void error (const location_type& loc, const std::string& msg);
500 
502  void error (const syntax_error& err);
503 
504  private:
506  parser (const parser&);
507  parser& operator= (const parser&);
508 
510  typedef int state_type;
511 
515  virtual std::string yysyntax_error_ (state_type yystate,
516  const symbol_type& yyla) const;
517 
521  state_type yy_lr_goto_state_ (state_type yystate, int yysym);
522 
525  static bool yy_pact_value_is_default_ (int yyvalue);
526 
529  static bool yy_table_value_is_error_ (int yyvalue);
530 
531  static const short int yypact_ninf_;
532  static const signed char yytable_ninf_;
533 
535  static token_number_type yytranslate_ (int t);
536 
537  // Tables.
538  // YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
539  // STATE-NUM.
540  static const short int yypact_[];
541 
542  // YYDEFACT[STATE-NUM] -- Default reduction number in state STATE-NUM.
543  // Performed when YYTABLE does not specify something else to do. Zero
544  // means the default is an error.
545  static const unsigned char yydefact_[];
546 
547  // YYPGOTO[NTERM-NUM].
548  static const short int yypgoto_[];
549 
550  // YYDEFGOTO[NTERM-NUM].
551  static const short int yydefgoto_[];
552 
553  // YYTABLE[YYPACT[STATE-NUM]] -- What to do in state STATE-NUM. If
554  // positive, shift that token. If negative, reduce the rule whose
555  // number is the opposite. If YYTABLE_NINF, syntax error.
556  static const short int yytable_[];
557 
558  static const short int yycheck_[];
559 
560  // YYSTOS[STATE-NUM] -- The (internal number of the) accessing
561  // symbol of state STATE-NUM.
562  static const unsigned char yystos_[];
563 
564  // YYR1[YYN] -- Symbol number of symbol that rule YYN derives.
565  static const unsigned char yyr1_[];
566 
567  // YYR2[YYN] -- Number of symbols on the right hand side of rule YYN.
568  static const unsigned char yyr2_[];
569 
570 
572  static std::string yytnamerr_ (const char *n);
573 
574 
576  static const char* const yytname_[];
577 #if YYDEBUG
578  // YYRLINE[YYN] -- Source line where rule number YYN was defined.
579  static const unsigned short int yyrline_[];
581  virtual void yy_reduce_print_ (int r);
583  virtual void yystack_print_ ();
584 
585  // Debugging.
586  int yydebug_;
587  std::ostream* yycdebug_;
588 
592  template <typename Base>
593  void yy_print_ (std::ostream& yyo, const basic_symbol<Base>& yysym) const;
594 #endif
595 
600  template <typename Base>
601  void yy_destroy_ (const char* yymsg, basic_symbol<Base>& yysym) const;
602 
603  private:
605  struct by_state
606  {
608  by_state ();
609 
611  typedef state_type kind_type;
612 
614  by_state (kind_type s);
615 
617  by_state (const by_state& other);
618 
620  void clear ();
621 
623  void move (by_state& that);
624 
627  symbol_number_type type_get () const;
628 
630  enum { empty_state = -1 };
631 
634  state_type state;
635  };
636 
638  struct stack_symbol_type : basic_symbol<by_state>
639  {
641  typedef basic_symbol<by_state> super_type;
643  stack_symbol_type ();
645  stack_symbol_type (state_type s, symbol_type& sym);
647  stack_symbol_type& operator= (const stack_symbol_type& that);
648  };
649 
652 
654  stack_type yystack_;
655 
661  void yypush_ (const char* m, stack_symbol_type& s);
662 
669  void yypush_ (const char* m, state_type s, symbol_type& sym);
670 
672  void yypop_ (unsigned int n = 1);
673 
675  enum
676  {
677  yyeof_ = 0,
678  yylast_ = 235,
679  yynnts_ = 83,
680  yyfinal_ = 24,
681  yyterror_ = 1,
682  yyerrcode_ = 256,
683  yyntokens_ = 65
684  };
685 
686 
687  // User arguments.
688  void* scanner;
689  result_& res;
690  spot::location initial_loc;
691  };
692 
693 
694 
695 } // hoayy
696 #line 697 "parseaut.hh" // lalr1.cc:377
697 
698 
699 
700 
701 #endif // !YY_HOAYY_PARSEAUT_HH_INCLUDED
Definition: parseaut.hh:92
An environment that describes atomic propositions.
Definition: environment.hh:32
Symbol semantic values.
Definition: parseaut.hh:290
semantic_type value
The semantic value.
Definition: parseaut.hh:426
Syntax errors thrown from user actions.
Definition: parseaut.hh:312
Definition: bitset.hh:405
Definition: parseaut.hh:94
Definition: ngraph.hh:32
token::yytokentype token_type
(External) token type, as returned by yylex.
Definition: parseaut.hh:375
Definition: parseaut.hh:277
Definition: public.hh:92
Definition: parseaut.hh:129
Tokens.
Definition: parseaut.hh:319
Type access provider for token (enum) based symbols.
Definition: parseaut.hh:437
token_type kind_type
The symbol type as needed by the constructor.
Definition: parseaut.hh:446
Base super_type
Alias to Base.
Definition: parseaut.hh:396
unsigned char token_number_type
Internal symbol number for tokens (subsumed by symbol_number_type).
Definition: parseaut.hh:384
A class implementing Kleene&#39;s three-valued logic.
Definition: trival.hh:33
int type
Definition: parseaut.hh:467
basic_symbol< by_type > symbol_type
"External" symbols: returned by the scanner.
Definition: parseaut.hh:471
spot::location location_type
Symbol locations.
Definition: parseaut.hh:309
Definition: parseaut.hh:69
A Bison parser.
Definition: parseaut.hh:285
Definition: parseaut.hh:393
An acceptance formula.
Definition: acc.hh:444
location_type location
The location.
Definition: parseaut.hh:429
int symbol_number_type
Symbol type: an internal symbol number.
Definition: parseaut.hh:378
An acceptance mark.
Definition: acc.hh:81
int debug_level_type
Type for debugging levels.
Definition: parseaut.hh:489

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.8.13