spot  2.6
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  // If "Alias: ..." occurs before "AP: ..." in the HOA format we
111  // are in trouble because the parser would like to turn each
112  // alias into a BDD, yet the atomic proposition have not been
113  // declared yet. We solve that by using arbitrary BDD variables
114  // numbers (in fact we use the same number given in the Alias:
115  // definition) and keeping track of the highest variable number
116  // we have seen (unknown_ap_max). Once AP: is encountered,
117  // we can remap everything. If AP: is never encountered an
118  // unknown_ap_max is non-negative, then we can signal an error.
119  int unknown_ap_max = -1;
120  spot::location unknown_ap_max_location;
121  bool in_alias = false;
122  map_t dest_map;
123  std::vector<state_info> info_states; // States declared and used.
124  std::vector<std::pair<spot::location,
125  std::vector<unsigned>>> start; // Initial states;
126  std::unordered_map<std::string, bdd> alias;
127  struct prop_info
128  {
129  spot::location loc;
130  bool val;
131  operator bool() const
132  {
133  return val;
134  };
135  };
136  std::unordered_map<std::string, prop_info> props;
137  spot::location states_loc;
138  spot::location ap_loc;
139  spot::location state_label_loc;
140  spot::location accset_loc;
141  spot::acc_cond::mark_t acc_state;
142  spot::acc_cond::mark_t neg_acc_sets = {};
143  spot::acc_cond::mark_t pos_acc_sets = {};
144  int plus;
145  int minus;
146  std::vector<std::string>* state_names = nullptr;
147  std::map<unsigned, unsigned>* highlight_edges = nullptr;
148  std::map<unsigned, unsigned>* highlight_states = nullptr;
149  std::map<unsigned, unsigned> states_map;
150  std::set<int> ap_set;
151  unsigned cur_state;
152  int states = -1;
153  int ap_count = -1;
154  int accset = -1;
155  bdd state_label;
156  bdd cur_label;
157  bool has_state_label = false;
158  bool ignore_more_ap = false; // Set to true after the first "AP:"
159  // line has been read.
160  bool ignore_acc = false; // Set to true in case of missing
161  // Acceptance: lines.
162  bool ignore_acc_silent = false;
163  bool ignore_more_acc = false; // Set to true after the first
164  // "Acceptance:" line has been read.
165 
166  label_style_t label_style = Mixed_Labels;
167  acc_style_t acc_style = Mixed_Acc;
168 
169  bool accept_all_needed = false;
170  bool accept_all_seen = false;
171  bool aliased_states = false;
172 
173  spot::trival universal = spot::trival::maybe();
174  spot::trival existential = spot::trival::maybe();
175  spot::trival complete = spot::trival::maybe();
176  bool trans_acc_seen = false;
177 
178  std::map<std::string, spot::location> labels;
179 
180  prop_info prop_is_true(const std::string& p)
181  {
182  auto i = props.find(p);
183  if (i == props.end())
184  return prop_info{spot::location(), false};
185  return i->second;
186  }
187 
188  prop_info prop_is_false(const std::string& p)
189  {
190  auto i = props.find(p);
191  if (i == props.end())
192  return prop_info{spot::location(), false};
193  return prop_info{i->second.loc, !i->second.val};
194  }
195 
196  ~result_()
197  {
198  delete namer;
199  delete acc_mapper;
200  }
201  };
202  }
203 
204 #line 205 "parseaut.hh" // lalr1.cc:377
205 
206 
207 # include <cstdlib> // std::abort
208 # include <iostream>
209 # include <stdexcept>
210 # include <string>
211 # include <vector>
212 # include "stack.hh"
213 
214 
215 
216 #ifndef YY_ATTRIBUTE
217 # if (defined __GNUC__ \
218  && (2 < __GNUC__ || (__GNUC__ == 2 && 96 <= __GNUC_MINOR__))) \
219  || defined __SUNPRO_C && 0x5110 <= __SUNPRO_C
220 # define YY_ATTRIBUTE(Spec) __attribute__(Spec)
221 # else
222 # define YY_ATTRIBUTE(Spec) /* empty */
223 # endif
224 #endif
225 
226 #ifndef YY_ATTRIBUTE_PURE
227 # define YY_ATTRIBUTE_PURE YY_ATTRIBUTE ((__pure__))
228 #endif
229 
230 #ifndef YY_ATTRIBUTE_UNUSED
231 # define YY_ATTRIBUTE_UNUSED YY_ATTRIBUTE ((__unused__))
232 #endif
233 
234 #if !defined _Noreturn \
235  && (!defined __STDC_VERSION__ || __STDC_VERSION__ < 201112)
236 # if defined _MSC_VER && 1200 <= _MSC_VER
237 # define _Noreturn __declspec (noreturn)
238 # else
239 # define _Noreturn YY_ATTRIBUTE ((__noreturn__))
240 # endif
241 #endif
242 
243 /* Suppress unused-variable warnings by "using" E. */
244 #if ! defined lint || defined __GNUC__
245 # define YYUSE(E) ((void) (E))
246 #else
247 # define YYUSE(E) /* empty */
248 #endif
249 
250 #if defined __GNUC__ && 407 <= __GNUC__ * 100 + __GNUC_MINOR__
251 /* Suppress an incorrect diagnostic about yylval being uninitialized. */
252 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
253  _Pragma ("GCC diagnostic push") \
254  _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"")\
255  _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"")
256 # define YY_IGNORE_MAYBE_UNINITIALIZED_END \
257  _Pragma ("GCC diagnostic pop")
258 #else
259 # define YY_INITIAL_VALUE(Value) Value
260 #endif
261 #ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
262 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
263 # define YY_IGNORE_MAYBE_UNINITIALIZED_END
264 #endif
265 #ifndef YY_INITIAL_VALUE
266 # define YY_INITIAL_VALUE(Value) /* Nothing. */
267 #endif
268 
269 /* Debug traces. */
270 #ifndef YYDEBUG
271 # define YYDEBUG 1
272 #endif
273 
274 
275 namespace hoayy {
276 #line 277 "parseaut.hh" // lalr1.cc:377
277 
278 
279 
280 
281 
283  class parser
284  {
285  public:
286 #ifndef YYSTYPE
287  union semantic_type
289  {
290  #line 199 "parseaut.yy" // lalr1.cc:377
291 
292  std::string* str;
293  unsigned int num;
294  int b;
296  pair* p;
297  std::list<pair>* list;
299  std::vector<unsigned>* states;
300 
301 #line 302 "parseaut.hh" // lalr1.cc:377
302  };
303 #else
304  typedef YYSTYPE semantic_type;
305 #endif
306  typedef spot::location location_type;
308 
310  struct syntax_error : std::runtime_error
311  {
312  syntax_error (const location_type& l, const std::string& m);
313  location_type location;
314  };
315 
317  struct token
318  {
319  enum yytokentype
320  {
321  ENDOFFILE = 0,
322  HOA = 258,
323  STATES = 259,
324  START = 260,
325  AP = 261,
326  ALIAS = 262,
327  ACCEPTANCE = 263,
328  ACCNAME = 264,
329  TOOL = 265,
330  NAME = 266,
331  PROPERTIES = 267,
332  BODY = 268,
333  END = 269,
334  STATE = 270,
335  SPOT_HIGHLIGHT_EDGES = 271,
336  SPOT_HIGHLIGHT_STATES = 272,
337  IDENTIFIER = 273,
338  HEADERNAME = 274,
339  ANAME = 275,
340  STRING = 276,
341  INT = 277,
342  DRA = 278,
343  DSA = 279,
344  V2 = 280,
345  EXPLICIT = 281,
346  ACCPAIRS = 282,
347  ACCSIG = 283,
348  ENDOFHEADER = 284,
349  NEVER = 285,
350  SKIP = 286,
351  IF = 287,
352  FI = 288,
353  DO = 289,
354  OD = 290,
355  ARROW = 291,
356  GOTO = 292,
357  FALSE = 293,
358  ATOMIC = 294,
359  ASSERT = 295,
360  FORMULA = 296,
361  ENDAUT = 297,
362  ENDDSTAR = 298,
363  LBTT = 299,
364  INT_S = 300,
365  LBTT_EMPTY = 301,
366  ACC = 302,
367  STATE_NUM = 303,
368  DEST_NUM = 304
369  };
370  };
371 
373  typedef token::yytokentype token_type;
374 
376  typedef int symbol_number_type;
377 
379  enum { empty_symbol = -2 };
380 
382  typedef unsigned char token_number_type;
383 
390  template <typename Base>
391  struct basic_symbol : Base
392  {
394  typedef Base super_type;
395 
397  basic_symbol ();
398 
400  basic_symbol (const basic_symbol& other);
401 
403  basic_symbol (typename Base::kind_type t,
404  const location_type& l);
405 
407  basic_symbol (typename Base::kind_type t,
408  const semantic_type& v,
409  const location_type& l);
410 
412  ~basic_symbol ();
413 
415  void clear ();
416 
418  bool empty () const;
419 
421  void move (basic_symbol& s);
422 
424  semantic_type value;
425 
427  location_type location;
428 
429  private:
431  basic_symbol& operator= (const basic_symbol& other);
432  };
433 
435  struct by_type
436  {
438  by_type ();
439 
441  by_type (const by_type& other);
442 
444  typedef token_type kind_type;
445 
447  by_type (kind_type t);
448 
450  void clear ();
451 
453  void move (by_type& that);
454 
457  symbol_number_type type_get () const;
458 
460  token_type token () const;
461 
465  int type;
466  };
467 
470 
471 
473  parser (void* scanner_yyarg, result_& res_yyarg, spot::location initial_loc_yyarg);
474  virtual ~parser ();
475 
478  virtual int parse ();
479 
480 #if YYDEBUG
481  std::ostream& debug_stream () const YY_ATTRIBUTE_PURE;
484  void set_debug_stream (std::ostream &);
485 
487  typedef int debug_level_type;
489  debug_level_type debug_level () const YY_ATTRIBUTE_PURE;
491  void set_debug_level (debug_level_type l);
492 #endif
493 
497  virtual void error (const location_type& loc, const std::string& msg);
498 
500  void error (const syntax_error& err);
501 
502  private:
504  parser (const parser&);
505  parser& operator= (const parser&);
506 
508  typedef int state_type;
509 
513  virtual std::string yysyntax_error_ (state_type yystate,
514  const symbol_type& yyla) const;
515 
519  state_type yy_lr_goto_state_ (state_type yystate, int yysym);
520 
523  static bool yy_pact_value_is_default_ (int yyvalue);
524 
527  static bool yy_table_value_is_error_ (int yyvalue);
528 
529  static const short int yypact_ninf_;
530  static const signed char yytable_ninf_;
531 
533  static token_number_type yytranslate_ (int t);
534 
535  // Tables.
536  // YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
537  // STATE-NUM.
538  static const short int yypact_[];
539 
540  // YYDEFACT[STATE-NUM] -- Default reduction number in state STATE-NUM.
541  // Performed when YYTABLE does not specify something else to do. Zero
542  // means the default is an error.
543  static const unsigned char yydefact_[];
544 
545  // YYPGOTO[NTERM-NUM].
546  static const short int yypgoto_[];
547 
548  // YYDEFGOTO[NTERM-NUM].
549  static const short int yydefgoto_[];
550 
551  // YYTABLE[YYPACT[STATE-NUM]] -- What to do in state STATE-NUM. If
552  // positive, shift that token. If negative, reduce the rule whose
553  // number is the opposite. If YYTABLE_NINF, syntax error.
554  static const short int yytable_[];
555 
556  static const short int yycheck_[];
557 
558  // YYSTOS[STATE-NUM] -- The (internal number of the) accessing
559  // symbol of state STATE-NUM.
560  static const unsigned char yystos_[];
561 
562  // YYR1[YYN] -- Symbol number of symbol that rule YYN derives.
563  static const unsigned char yyr1_[];
564 
565  // YYR2[YYN] -- Number of symbols on the right hand side of rule YYN.
566  static const unsigned char yyr2_[];
567 
568 
570  static std::string yytnamerr_ (const char *n);
571 
572 
574  static const char* const yytname_[];
575 #if YYDEBUG
576  // YYRLINE[YYN] -- Source line where rule number YYN was defined.
577  static const unsigned short int yyrline_[];
579  virtual void yy_reduce_print_ (int r);
581  virtual void yystack_print_ ();
582 
583  // Debugging.
584  int yydebug_;
585  std::ostream* yycdebug_;
586 
590  template <typename Base>
591  void yy_print_ (std::ostream& yyo, const basic_symbol<Base>& yysym) const;
592 #endif
593 
598  template <typename Base>
599  void yy_destroy_ (const char* yymsg, basic_symbol<Base>& yysym) const;
600 
601  private:
603  struct by_state
604  {
606  by_state ();
607 
609  typedef state_type kind_type;
610 
612  by_state (kind_type s);
613 
615  by_state (const by_state& other);
616 
618  void clear ();
619 
621  void move (by_state& that);
622 
625  symbol_number_type type_get () const;
626 
628  enum { empty_state = -1 };
629 
632  state_type state;
633  };
634 
636  struct stack_symbol_type : basic_symbol<by_state>
637  {
639  typedef basic_symbol<by_state> super_type;
641  stack_symbol_type ();
643  stack_symbol_type (state_type s, symbol_type& sym);
645  stack_symbol_type& operator= (const stack_symbol_type& that);
646  };
647 
650 
652  stack_type yystack_;
653 
659  void yypush_ (const char* m, stack_symbol_type& s);
660 
667  void yypush_ (const char* m, state_type s, symbol_type& sym);
668 
670  void yypop_ (unsigned int n = 1);
671 
673  enum
674  {
675  yyeof_ = 0,
676  yylast_ = 235,
677  yynnts_ = 83,
678  yyfinal_ = 24,
679  yyterror_ = 1,
680  yyerrcode_ = 256,
681  yyntokens_ = 65
682  };
683 
684 
685  // User arguments.
686  void* scanner;
687  result_& res;
688  spot::location initial_loc;
689  };
690 
691 
692 
693 } // hoayy
694 #line 695 "parseaut.hh" // lalr1.cc:377
695 
696 
697 
698 
699 #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:288
semantic_type value
The semantic value.
Definition: parseaut.hh:424
Syntax errors thrown from user actions.
Definition: parseaut.hh:310
Definition: bitset.hh:405
Definition: parseaut.hh:92
Definition: ngraph.hh:32
token::yytokentype token_type
(External) token type, as returned by yylex.
Definition: parseaut.hh:373
Definition: parseaut.hh:275
Definition: public.hh:92
Definition: parseaut.hh:127
Tokens.
Definition: parseaut.hh:317
Type access provider for token (enum) based symbols.
Definition: parseaut.hh:435
token_type kind_type
The symbol type as needed by the constructor.
Definition: parseaut.hh:444
Base super_type
Alias to Base.
Definition: parseaut.hh:394
unsigned char token_number_type
Internal symbol number for tokens (subsumed by symbol_number_type).
Definition: parseaut.hh:382
A class implementing Kleene&#39;s three-valued logic.
Definition: trival.hh:33
int type
Definition: parseaut.hh:465
basic_symbol< by_type > symbol_type
"External" symbols: returned by the scanner.
Definition: parseaut.hh:469
spot::location location_type
Symbol locations.
Definition: parseaut.hh:307
Definition: parseaut.hh:67
A Bison parser.
Definition: parseaut.hh:283
Definition: parseaut.hh:391
Definition: acc.hh:378
location_type location
The location.
Definition: parseaut.hh:427
int symbol_number_type
Symbol type: an internal symbol number.
Definition: parseaut.hh:376
Definition: acc.hh:55
int debug_level_type
Type for debugging levels.
Definition: parseaut.hh:487

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