spot  2.10.2.dev
parseaut.hh
Go to the documentation of this file.
1 // A Bison parser, made by GNU Bison 3.8.2.
2 
3 // Skeleton interface for Bison LALR(1) parsers in C++
4 
5 // Copyright (C) 2002-2015, 2018-2021 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 <https://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 
33 
39 // C++ LALR(1) parser skeleton written by Akim Demaille.
40 
41 // DO NOT RELY ON FEATURES THAT ARE NOT DOCUMENTED in the manual,
42 // especially those whose name start with YY_ or yy_. They are
43 // private implementation details that can be changed or removed.
44 
45 #ifndef YY_HOAYY_PARSEAUT_HH_INCLUDED
46 # define YY_HOAYY_PARSEAUT_HH_INCLUDED
47 // "%code requires" blocks.
48 #line 33 "parseaut.yy"
49 
50 #include "config.h"
51 #include <spot/misc/common.hh>
52 #include <spot/priv/robin_hood.hh>
53 #include <string>
54 #include <cstring>
55 #include <sstream>
56 #include <unordered_map>
57 #include <algorithm>
58 #include <spot/twa/formula2bdd.hh>
59 #include <spot/parseaut/public.hh>
60 #include "spot/priv/accmap.hh"
61 #include <spot/tl/parse.hh>
62 #include <spot/twaalgos/alternation.hh>
63 
64 using namespace std::string_literals;
65 
66 #ifndef HAVE_STRVERSCMP
67 // If the libc does not have this, a version is compiled in lib/.
68 extern "C" int strverscmp(const char *s1, const char *s2);
69 #endif
70 
71 // Work around Bison not letting us write
72 // %lex-param { res.h->errors, res.fcache }
73 #define PARSE_ERROR_LIST res.h->errors, res.fcache
74 
75  inline namespace hoayy_support
76  {
77  typedef std::map<int, bdd> map_t;
78 
79  /* Cache parsed formulae. Labels on arcs are frequently identical
80  and it would be a waste of time to parse them to formula
81  over and over, and to register all their atomic_propositions in
82  the bdd_dict. Keep the bdd result around so we can reuse
83  it. */
84  typedef robin_hood::unordered_flat_map<std::string, bdd> formula_cache;
85 
86  typedef std::pair<int, std::string*> pair;
87  typedef spot::twa_graph::namer<std::string> named_tgba_t;
88 
89  // Note: because this parser is meant to be used on a stream of
90  // automata, it tries hard to recover from errors, so that we get a
91  // chance to reach the end of the current automaton in order to
92  // process the next one. Several variables below are used to keep
93  // track of various error conditions.
94  enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels,
95  Implicit_Labels };
96  enum acc_style_t { Mixed_Acc, State_Acc, Trans_Acc };
97 
98  struct result_
99  {
100  struct state_info
101  {
102  bool declared = false;
103  bool used = false;
104  spot::location used_loc;
105  };
106  spot::parsed_aut_ptr h;
107  spot::twa_ptr aut_or_ks;
109  std::string format_version;
110  spot::location format_version_loc;
111  spot::environment* env;
112  formula_cache fcache;
113  named_tgba_t* namer = nullptr;
114  spot::acc_mapper_int* acc_mapper = nullptr;
115  std::vector<int> ap;
116  std::vector<bdd> guards;
117  std::vector<bdd>::const_iterator cur_guard;
118  // If "Alias: ..." occurs before "AP: ..." in the HOA format we
119  // are in trouble because the parser would like to turn each
120  // alias into a BDD, yet the atomic proposition have not been
121  // declared yet. We solve that by using arbitrary BDD variables
122  // numbers (in fact we use the same number given in the Alias:
123  // definition) and keeping track of the highest variable number
124  // we have seen (unknown_ap_max). Once AP: is encountered,
125  // we can remap everything. If AP: is never encountered an
126  // unknown_ap_max is non-negative, then we can signal an error.
127  int unknown_ap_max = -1;
128  spot::location unknown_ap_max_location;
129  bool in_alias = false;
130  map_t dest_map;
131  std::vector<state_info> info_states; // States declared and used.
132  std::vector<std::pair<spot::location,
133  std::vector<unsigned>>> start; // Initial states;
134  std::unordered_map<std::string, bdd> alias;
135  struct prop_info
136  {
137  spot::location loc;
138  bool val;
139  operator bool() const
140  {
141  return val;
142  };
143  };
144  std::unordered_map<std::string, prop_info> props;
145  spot::location states_loc;
146  spot::location ap_loc;
147  spot::location state_label_loc;
148  spot::location accset_loc;
149  spot::acc_cond::mark_t acc_state;
150  spot::acc_cond::mark_t neg_acc_sets = {};
151  spot::acc_cond::mark_t pos_acc_sets = {};
152  int plus;
153  int minus;
154  std::vector<std::string>* state_names = nullptr;
155  std::map<unsigned, unsigned>* highlight_edges = nullptr;
156  std::map<unsigned, unsigned>* highlight_states = nullptr;
157  std::map<unsigned, unsigned> states_map;
158  std::vector<bool>* state_player = nullptr;
159  spot::location state_player_loc;
160  std::set<int> ap_set;
161  unsigned cur_state;
162  int states = -1;
163  int ap_count = -1;
164  int accset = -1;
165  bdd state_label;
166  bdd cur_label;
167  bool has_state_label = false;
168  bool ignore_more_ap = false; // Set to true after the first "AP:"
169  // line has been read.
170  bool ignore_acc = false; // Set to true in case of missing
171  // Acceptance: lines.
172  bool ignore_acc_silent = false;
173  bool ignore_more_acc = false; // Set to true after the first
174  // "Acceptance:" line has been read.
175 
176  label_style_t label_style = Mixed_Labels;
177  acc_style_t acc_style = Mixed_Acc;
178 
179  bool accept_all_needed = false;
180  bool accept_all_seen = false;
181  bool aliased_states = false;
182 
183  spot::trival universal = spot::trival::maybe();
184  spot::trival existential = spot::trival::maybe();
185  spot::trival complete = spot::trival::maybe();
186  bool trans_acc_seen = false;
187 
188  std::map<std::string, spot::location> labels;
189 
190  prop_info prop_is_true(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 i->second;
196  }
197 
198  prop_info prop_is_false(const std::string& p)
199  {
200  auto i = props.find(p);
201  if (i == props.end())
202  return prop_info{spot::location(), false};
203  return prop_info{i->second.loc, !i->second.val};
204  }
205 
206  ~result_()
207  {
208  delete namer;
209  delete acc_mapper;
210  }
211  };
212  }
213 
214 #line 215 "parseaut.hh"
215 
216 
217 # include <cstdlib> // std::abort
218 # include <iostream>
219 # include <stdexcept>
220 # include <string>
221 # include <vector>
222 
223 #if defined __cplusplus
224 # define YY_CPLUSPLUS __cplusplus
225 #else
226 # define YY_CPLUSPLUS 199711L
227 #endif
228 
229 // Support move semantics when possible.
230 #if 201103L <= YY_CPLUSPLUS
231 # define YY_MOVE std::move
232 # define YY_MOVE_OR_COPY move
233 # define YY_MOVE_REF(Type) Type&&
234 # define YY_RVREF(Type) Type&&
235 # define YY_COPY(Type) Type
236 #else
237 # define YY_MOVE
238 # define YY_MOVE_OR_COPY copy
239 # define YY_MOVE_REF(Type) Type&
240 # define YY_RVREF(Type) const Type&
241 # define YY_COPY(Type) const Type&
242 #endif
243 
244 // Support noexcept when possible.
245 #if 201103L <= YY_CPLUSPLUS
246 # define YY_NOEXCEPT noexcept
247 # define YY_NOTHROW
248 #else
249 # define YY_NOEXCEPT
250 # define YY_NOTHROW throw ()
251 #endif
252 
253 // Support constexpr when possible.
254 #if 201703 <= YY_CPLUSPLUS
255 # define YY_CONSTEXPR constexpr
256 #else
257 # define YY_CONSTEXPR
258 #endif
259 
260 
261 
262 #ifndef YY_ATTRIBUTE_PURE
263 # if defined __GNUC__ && 2 < __GNUC__ + (96 <= __GNUC_MINOR__)
264 # define YY_ATTRIBUTE_PURE __attribute__ ((__pure__))
265 # else
266 # define YY_ATTRIBUTE_PURE
267 # endif
268 #endif
269 
270 #ifndef YY_ATTRIBUTE_UNUSED
271 # if defined __GNUC__ && 2 < __GNUC__ + (7 <= __GNUC_MINOR__)
272 # define YY_ATTRIBUTE_UNUSED __attribute__ ((__unused__))
273 # else
274 # define YY_ATTRIBUTE_UNUSED
275 # endif
276 #endif
277 
278 /* Suppress unused-variable warnings by "using" E. */
279 #if ! defined lint || defined __GNUC__
280 # define YY_USE(E) ((void) (E))
281 #else
282 # define YY_USE(E) /* empty */
283 #endif
284 
285 /* Suppress an incorrect diagnostic about yylval being uninitialized. */
286 #if defined __GNUC__ && ! defined __ICC && 406 <= __GNUC__ * 100 + __GNUC_MINOR__
287 # if __GNUC__ * 100 + __GNUC_MINOR__ < 407
288 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
289  _Pragma ("GCC diagnostic push") \
290  _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"")
291 # else
292 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
293  _Pragma ("GCC diagnostic push") \
294  _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"") \
295  _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"")
296 # endif
297 # define YY_IGNORE_MAYBE_UNINITIALIZED_END \
298  _Pragma ("GCC diagnostic pop")
299 #else
300 # define YY_INITIAL_VALUE(Value) Value
301 #endif
302 #ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
303 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
304 # define YY_IGNORE_MAYBE_UNINITIALIZED_END
305 #endif
306 #ifndef YY_INITIAL_VALUE
307 # define YY_INITIAL_VALUE(Value) /* Nothing. */
308 #endif
309 
310 #if defined __cplusplus && defined __GNUC__ && ! defined __ICC && 6 <= __GNUC__
311 # define YY_IGNORE_USELESS_CAST_BEGIN \
312  _Pragma ("GCC diagnostic push") \
313  _Pragma ("GCC diagnostic ignored \"-Wuseless-cast\"")
314 # define YY_IGNORE_USELESS_CAST_END \
315  _Pragma ("GCC diagnostic pop")
316 #endif
317 #ifndef YY_IGNORE_USELESS_CAST_BEGIN
318 # define YY_IGNORE_USELESS_CAST_BEGIN
319 # define YY_IGNORE_USELESS_CAST_END
320 #endif
321 
322 # ifndef YY_CAST
323 # ifdef __cplusplus
324 # define YY_CAST(Type, Val) static_cast<Type> (Val)
325 # define YY_REINTERPRET_CAST(Type, Val) reinterpret_cast<Type> (Val)
326 # else
327 # define YY_CAST(Type, Val) ((Type) (Val))
328 # define YY_REINTERPRET_CAST(Type, Val) ((Type) (Val))
329 # endif
330 # endif
331 # ifndef YY_NULLPTR
332 # if defined __cplusplus
333 # if 201103L <= __cplusplus
334 # define YY_NULLPTR nullptr
335 # else
336 # define YY_NULLPTR 0
337 # endif
338 # else
339 # define YY_NULLPTR ((void*)0)
340 # endif
341 # endif
342 
343 /* Debug traces. */
344 #ifndef HOAYYDEBUG
345 # if defined YYDEBUG
346 #if YYDEBUG
347 # define HOAYYDEBUG 1
348 # else
349 # define HOAYYDEBUG 0
350 # endif
351 # else /* ! defined YYDEBUG */
352 # define HOAYYDEBUG 1
353 # endif /* ! defined YYDEBUG */
354 #endif /* ! defined HOAYYDEBUG */
355 
356 namespace hoayy {
357 #line 358 "parseaut.hh"
358 
359 
360 
361 
363  class parser
364  {
365  public:
366 #ifdef HOAYYSTYPE
367 # ifdef __GNUC__
368 # pragma GCC message "bison: do not #define HOAYYSTYPE in C++, use %define api.value.type"
369 # endif
370  typedef HOAYYSTYPE value_type;
371 #else
374  {
375 #line 205 "parseaut.yy"
376 
377  std::string* str;
378  unsigned int num;
379  int b;
381  pair* p;
382  std::list<pair>* list;
384  std::vector<unsigned>* states;
385 
386 #line 387 "parseaut.hh"
387 
388  };
389 #endif
392 
394  typedef spot::location location_type;
395 
397  struct syntax_error : std::runtime_error
398  {
399  syntax_error (const location_type& l, const std::string& m)
400  : std::runtime_error (m)
401  , location (l)
402  {}
403 
404  syntax_error (const syntax_error& s)
405  : std::runtime_error (s.what ())
406  , location (s.location)
407  {}
408 
409  ~syntax_error () YY_NOEXCEPT YY_NOTHROW;
410 
411  location_type location;
412  };
413 
415  struct token
416  {
417  enum token_kind_type
418  {
419  HOAYYEMPTY = -2,
420  ENDOFFILE = 0, // "end of file"
421  HOAYYerror = 256, // error
422  HOAYYUNDEF = 257, // "invalid token"
423  HOA = 258, // "HOA:"
424  STATES = 259, // "States:"
425  START = 260, // "Start:"
426  AP = 261, // "AP:"
427  ALIAS = 262, // "Alias:"
428  ACCEPTANCE = 263, // "Acceptance:"
429  ACCNAME = 264, // "acc-name:"
430  TOOL = 265, // "tool:"
431  NAME = 266, // "name:"
432  PROPERTIES = 267, // "properties:"
433  BODY = 268, // "--BODY--"
434  END = 269, // "--END--"
435  STATE = 270, // "State:"
436  SPOT_HIGHLIGHT_EDGES = 271, // "spot.highlight.edges:"
437  SPOT_HIGHLIGHT_STATES = 272, // "spot.highlight.states:"
438  SPOT_STATE_PLAYER = 273, // "spot.state-player:"
439  IDENTIFIER = 274, // "identifier"
440  HEADERNAME = 275, // "header name"
441  ANAME = 276, // "alias name"
442  STRING = 277, // "string"
443  INT = 278, // "integer"
444  DRA = 279, // "DRA"
445  DSA = 280, // "DSA"
446  V2 = 281, // "v2"
447  EXPLICIT = 282, // "explicit"
448  ACCPAIRS = 283, // "Acceptance-Pairs:"
449  ACCSIG = 284, // "Acc-Sig:"
450  ENDOFHEADER = 285, // "---"
451  LINEDIRECTIVE = 286, // "#line"
452  BDD = 287, // BDD
453  NEVER = 288, // "never"
454  SKIP = 289, // "skip"
455  IF = 290, // "if"
456  FI = 291, // "fi"
457  DO = 292, // "do"
458  OD = 293, // "od"
459  ARROW = 294, // "->"
460  GOTO = 295, // "goto"
461  FALSE = 296, // "false"
462  ATOMIC = 297, // "atomic"
463  ASSERT = 298, // "assert"
464  FORMULA = 299, // "boolean formula"
465  ENDAUT = 300, // "-1"
466  ENDDSTAR = 301, // "end of DSTAR automaton"
467  LBTT = 302, // "LBTT header"
468  INT_S = 303, // "state acceptance"
469  LBTT_EMPTY = 304, // "acceptance sets for empty automaton"
470  ACC = 305, // "acceptance set"
471  STATE_NUM = 306, // "state number"
472  DEST_NUM = 307 // "destination number"
473  };
475  typedef token_kind_type yytokentype;
476  };
477 
479  typedef token::token_kind_type token_kind_type;
480 
482  typedef token_kind_type token_type;
483 
485  struct symbol_kind
486  {
488  {
489  YYNTOKENS = 68,
490  S_YYEMPTY = -2,
491  S_YYEOF = 0, // "end of file"
492  S_YYerror = 1, // error
493  S_YYUNDEF = 2, // "invalid token"
494  S_HOA = 3, // "HOA:"
495  S_STATES = 4, // "States:"
496  S_START = 5, // "Start:"
497  S_AP = 6, // "AP:"
498  S_ALIAS = 7, // "Alias:"
499  S_ACCEPTANCE = 8, // "Acceptance:"
500  S_ACCNAME = 9, // "acc-name:"
501  S_TOOL = 10, // "tool:"
502  S_NAME = 11, // "name:"
503  S_PROPERTIES = 12, // "properties:"
504  S_BODY = 13, // "--BODY--"
505  S_END = 14, // "--END--"
506  S_STATE = 15, // "State:"
507  S_SPOT_HIGHLIGHT_EDGES = 16, // "spot.highlight.edges:"
508  S_SPOT_HIGHLIGHT_STATES = 17, // "spot.highlight.states:"
509  S_SPOT_STATE_PLAYER = 18, // "spot.state-player:"
510  S_IDENTIFIER = 19, // "identifier"
511  S_HEADERNAME = 20, // "header name"
512  S_ANAME = 21, // "alias name"
513  S_STRING = 22, // "string"
514  S_INT = 23, // "integer"
515  S_24_ = 24, // '['
516  S_DRA = 25, // "DRA"
517  S_DSA = 26, // "DSA"
518  S_V2 = 27, // "v2"
519  S_EXPLICIT = 28, // "explicit"
520  S_ACCPAIRS = 29, // "Acceptance-Pairs:"
521  S_ACCSIG = 30, // "Acc-Sig:"
522  S_ENDOFHEADER = 31, // "---"
523  S_LINEDIRECTIVE = 32, // "#line"
524  S_BDD = 33, // BDD
525  S_34_ = 34, // '|'
526  S_35_ = 35, // '&'
527  S_36_ = 36, // '!'
528  S_NEVER = 37, // "never"
529  S_SKIP = 38, // "skip"
530  S_IF = 39, // "if"
531  S_FI = 40, // "fi"
532  S_DO = 41, // "do"
533  S_OD = 42, // "od"
534  S_ARROW = 43, // "->"
535  S_GOTO = 44, // "goto"
536  S_FALSE = 45, // "false"
537  S_ATOMIC = 46, // "atomic"
538  S_ASSERT = 47, // "assert"
539  S_FORMULA = 48, // "boolean formula"
540  S_ENDAUT = 49, // "-1"
541  S_ENDDSTAR = 50, // "end of DSTAR automaton"
542  S_LBTT = 51, // "LBTT header"
543  S_INT_S = 52, // "state acceptance"
544  S_LBTT_EMPTY = 53, // "acceptance sets for empty automaton"
545  S_ACC = 54, // "acceptance set"
546  S_STATE_NUM = 55, // "state number"
547  S_DEST_NUM = 56, // "destination number"
548  S_57_t_ = 57, // 't'
549  S_58_f_ = 58, // 'f'
550  S_59_ = 59, // '('
551  S_60_ = 60, // ')'
552  S_61_ = 61, // ']'
553  S_62_ = 62, // '{'
554  S_63_ = 63, // '}'
555  S_64_ = 64, // '+'
556  S_65_ = 65, // '-'
557  S_66_ = 66, // ';'
558  S_67_ = 67, // ':'
559  S_YYACCEPT = 68, // $accept
560  S_aut = 69, // aut
561  S_70_1 = 70, // $@1
562  S_71_aut_1 = 71, // aut-1
563  S_hoa = 72, // hoa
564  S_string_opt = 73, // string_opt
565  S_BOOLEAN = 74, // BOOLEAN
566  S_header = 75, // header
567  S_version = 76, // version
568  S_77_format_version = 77, // format-version
569  S_78_2 = 78, // $@2
570  S_aps = 79, // aps
571  S_80_3 = 80, // $@3
572  S_81_header_items = 81, // header-items
573  S_82_header_item = 82, // header-item
574  S_83_4 = 83, // $@4
575  S_84_5 = 84, // $@5
576  S_85_6 = 85, // $@6
577  S_86_7 = 86, // $@7
578  S_87_8 = 87, // $@8
579  S_88_ap_names = 88, // ap-names
580  S_89_ap_name = 89, // ap-name
581  S_90_acc_spec = 90, // acc-spec
582  S_properties = 91, // properties
583  S_92_highlight_edges = 92, // highlight-edges
584  S_93_highlight_states = 93, // highlight-states
585  S_94_state_player = 94, // state-player
586  S_95_header_spec = 95, // header-spec
587  S_96_state_conj_2 = 96, // state-conj-2
588  S_97_init_state_conj_2 = 97, // init-state-conj-2
589  S_98_label_expr = 98, // label-expr
590  S_99_acc_set = 99, // acc-set
591  S_100_acceptance_cond = 100, // acceptance-cond
592  S_body = 101, // body
593  S_102_state_num = 102, // state-num
594  S_103_checked_state_num = 103, // checked-state-num
595  S_states = 104, // states
596  S_state = 105, // state
597  S_106_state_name = 106, // state-name
598  S_label = 107, // label
599  S_108_state_label_opt = 108, // state-label_opt
600  S_109_trans_label = 109, // trans-label
601  S_110_acc_sig = 110, // acc-sig
602  S_111_acc_sets = 111, // acc-sets
603  S_112_state_acc_opt = 112, // state-acc_opt
604  S_113_trans_acc_opt = 113, // trans-acc_opt
605  S_114_labeled_edges = 114, // labeled-edges
606  S_115_some_labeled_edges = 115, // some-labeled-edges
607  S_116_incorrectly_unlabeled_edge = 116, // incorrectly-unlabeled-edge
608  S_117_labeled_edge = 117, // labeled-edge
609  S_118_state_conj_checked = 118, // state-conj-checked
610  S_119_unlabeled_edges = 119, // unlabeled-edges
611  S_120_unlabeled_edge = 120, // unlabeled-edge
612  S_121_incorrectly_labeled_edge = 121, // incorrectly-labeled-edge
613  S_dstar = 122, // dstar
614  S_dstar_type = 123, // dstar_type
615  S_dstar_header = 124, // dstar_header
616  S_dstar_sizes = 125, // dstar_sizes
617  S_dstar_state_id = 126, // dstar_state_id
618  S_sign = 127, // sign
619  S_dstar_accsigs = 128, // dstar_accsigs
620  S_dstar_state_accsig = 129, // dstar_state_accsig
621  S_dstar_transitions = 130, // dstar_transitions
622  S_dstar_states = 131, // dstar_states
623  S_never = 132, // never
624  S_133_9 = 133, // $@9
625  S_134_nc_states = 134, // nc-states
626  S_135_nc_one_ident = 135, // nc-one-ident
627  S_136_nc_ident_list = 136, // nc-ident-list
628  S_137_nc_transition_block = 137, // nc-transition-block
629  S_138_nc_state = 138, // nc-state
630  S_139_nc_transitions = 139, // nc-transitions
631  S_140_nc_formula_or_ident = 140, // nc-formula-or-ident
632  S_141_nc_formula = 141, // nc-formula
633  S_142_nc_opt_dest = 142, // nc-opt-dest
634  S_143_nc_src_dest = 143, // nc-src-dest
635  S_144_nc_transition = 144, // nc-transition
636  S_lbtt = 145, // lbtt
637  S_146_lbtt_header_states = 146, // lbtt-header-states
638  S_147_lbtt_header = 147, // lbtt-header
639  S_148_lbtt_body = 148, // lbtt-body
640  S_149_lbtt_states = 149, // lbtt-states
641  S_150_lbtt_state = 150, // lbtt-state
642  S_151_lbtt_acc = 151, // lbtt-acc
643  S_152_lbtt_guard = 152, // lbtt-guard
644  S_153_lbtt_transitions = 153 // lbtt-transitions
645  };
646  };
647 
650 
652  static const symbol_kind_type YYNTOKENS = symbol_kind::YYNTOKENS;
653 
660  template <typename Base>
661  struct basic_symbol : Base
662  {
664  typedef Base super_type;
665 
667  basic_symbol () YY_NOEXCEPT
668  : value ()
669  , location ()
670  {}
671 
672 #if 201103L <= YY_CPLUSPLUS
674  basic_symbol (basic_symbol&& that)
675  : Base (std::move (that))
676  , value (std::move (that.value))
677  , location (std::move (that.location))
678  {}
679 #endif
680 
682  basic_symbol (const basic_symbol& that);
684  basic_symbol (typename Base::kind_type t,
685  YY_MOVE_REF (location_type) l);
686 
688  basic_symbol (typename Base::kind_type t,
689  YY_RVREF (value_type) v,
690  YY_RVREF (location_type) l);
691 
694  {
695  clear ();
696  }
697 
698 
699 
701  void clear () YY_NOEXCEPT
702  {
703  Base::clear ();
704  }
705 
707  std::string name () const YY_NOEXCEPT
708  {
709  return parser::symbol_name (this->kind ());
710  }
711 
713  symbol_kind_type type_get () const YY_NOEXCEPT;
714 
716  bool empty () const YY_NOEXCEPT;
717 
719  void move (basic_symbol& s);
720 
722  value_type value;
723 
725  location_type location;
726 
727  private:
728 #if YY_CPLUSPLUS < 201103L
730  basic_symbol& operator= (const basic_symbol& that);
731 #endif
732  };
733 
735  struct by_kind
736  {
738  typedef token_kind_type kind_type;
739 
741  by_kind () YY_NOEXCEPT;
742 
743 #if 201103L <= YY_CPLUSPLUS
745  by_kind (by_kind&& that) YY_NOEXCEPT;
746 #endif
747 
749  by_kind (const by_kind& that) YY_NOEXCEPT;
750 
752  by_kind (kind_type t) YY_NOEXCEPT;
753 
754 
755 
757  void clear () YY_NOEXCEPT;
758 
760  void move (by_kind& that);
761 
764  symbol_kind_type kind () const YY_NOEXCEPT;
765 
767  symbol_kind_type type_get () const YY_NOEXCEPT;
768 
772  };
773 
775  typedef by_kind by_type;
776 
779  {};
780 
782  parser (void* scanner_yyarg, result_& res_yyarg, spot::location initial_loc_yyarg);
783  virtual ~parser ();
784 
785 #if 201103L <= YY_CPLUSPLUS
787  parser (const parser&) = delete;
789  parser& operator= (const parser&) = delete;
790 #endif
791 
794  int operator() ();
795 
798  virtual int parse ();
799 
800 #if HOAYYDEBUG
802  std::ostream& debug_stream () const YY_ATTRIBUTE_PURE;
804  void set_debug_stream (std::ostream &);
805 
807  typedef int debug_level_type;
809  debug_level_type debug_level () const YY_ATTRIBUTE_PURE;
811  void set_debug_level (debug_level_type l);
812 #endif
813 
817  virtual void error (const location_type& loc, const std::string& msg);
818 
820  void error (const syntax_error& err);
821 
824  static std::string symbol_name (symbol_kind_type yysymbol);
825 
826 
827 
828  class context
829  {
830  public:
831  context (const parser& yyparser, const symbol_type& yyla);
832  const symbol_type& lookahead () const YY_NOEXCEPT { return yyla_; }
833  symbol_kind_type token () const YY_NOEXCEPT { return yyla_.kind (); }
834  const location_type& location () const YY_NOEXCEPT { return yyla_.location; }
835 
839  int expected_tokens (symbol_kind_type yyarg[], int yyargn) const;
840 
841  private:
842  const parser& yyparser_;
843  const symbol_type& yyla_;
844  };
845 
846  private:
847 #if YY_CPLUSPLUS < 201103L
849  parser (const parser&);
851  parser& operator= (const parser&);
852 #endif
853 
854 
856  typedef short state_type;
857 
859  int yy_syntax_error_arguments_ (const context& yyctx,
860  symbol_kind_type yyarg[], int yyargn) const;
861 
864  virtual std::string yysyntax_error_ (const context& yyctx) const;
868  static state_type yy_lr_goto_state_ (state_type yystate, int yysym);
869 
872  static bool yy_pact_value_is_default_ (int yyvalue) YY_NOEXCEPT;
873 
876  static bool yy_table_value_is_error_ (int yyvalue) YY_NOEXCEPT;
877 
878  static const short yypact_ninf_;
879  static const short yytable_ninf_;
880 
884  static symbol_kind_type yytranslate_ (int t) YY_NOEXCEPT;
885 
887  static std::string yytnamerr_ (const char *yystr);
888 
890  static const char* const yytname_[];
891 
892 
893  // Tables.
894  // YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
895  // STATE-NUM.
896  static const short yypact_[];
897 
898  // YYDEFACT[STATE-NUM] -- Default reduction number in state STATE-NUM.
899  // Performed when YYTABLE does not specify something else to do. Zero
900  // means the default is an error.
901  static const unsigned char yydefact_[];
902 
903  // YYPGOTO[NTERM-NUM].
904  static const short yypgoto_[];
905 
906  // YYDEFGOTO[NTERM-NUM].
907  static const short yydefgoto_[];
908 
909  // YYTABLE[YYPACT[STATE-NUM]] -- What to do in state STATE-NUM. If
910  // positive, shift that token. If negative, reduce the rule whose
911  // number is the opposite. If YYTABLE_NINF, syntax error.
912  static const short yytable_[];
913 
914  static const short yycheck_[];
915 
916  // YYSTOS[STATE-NUM] -- The symbol kind of the accessing symbol of
917  // state STATE-NUM.
918  static const unsigned char yystos_[];
919 
920  // YYR1[RULE-NUM] -- Symbol kind of the left-hand side of rule RULE-NUM.
921  static const unsigned char yyr1_[];
922 
923  // YYR2[RULE-NUM] -- Number of symbols on the right-hand side of rule RULE-NUM.
924  static const signed char yyr2_[];
925 
926 
927 #if HOAYYDEBUG
928  // YYRLINE[YYN] -- Source line where rule number YYN was defined.
929  static const short yyrline_[];
931  virtual void yy_reduce_print_ (int r) const;
933  virtual void yy_stack_print_ () const;
934 
936  int yydebug_;
938  std::ostream* yycdebug_;
939 
943  template <typename Base>
944  void yy_print_ (std::ostream& yyo, const basic_symbol<Base>& yysym) const;
945 #endif
946 
951  template <typename Base>
952  void yy_destroy_ (const char* yymsg, basic_symbol<Base>& yysym) const;
953 
954  private:
956  struct by_state
957  {
959  by_state () YY_NOEXCEPT;
960 
962  typedef state_type kind_type;
963 
965  by_state (kind_type s) YY_NOEXCEPT;
966 
968  by_state (const by_state& that) YY_NOEXCEPT;
969 
971  void clear () YY_NOEXCEPT;
972 
974  void move (by_state& that);
975 
978  symbol_kind_type kind () const YY_NOEXCEPT;
979 
982  enum { empty_state = 0 };
983 
986  state_type state;
987  };
988 
990  struct stack_symbol_type : basic_symbol<by_state>
991  {
993  typedef basic_symbol<by_state> super_type;
995  stack_symbol_type ();
997  stack_symbol_type (YY_RVREF (stack_symbol_type) that);
999  stack_symbol_type (state_type s, YY_MOVE_REF (symbol_type) sym);
1000 #if YY_CPLUSPLUS < 201103L
1003  stack_symbol_type& operator= (stack_symbol_type& that);
1004 
1007  stack_symbol_type& operator= (const stack_symbol_type& that);
1008 #endif
1009  };
1010 
1012  template <typename T, typename S = std::vector<T> >
1013  class stack
1014  {
1015  public:
1016  // Hide our reversed order.
1017  typedef typename S::iterator iterator;
1018  typedef typename S::const_iterator const_iterator;
1019  typedef typename S::size_type size_type;
1020  typedef typename std::ptrdiff_t index_type;
1021 
1022  stack (size_type n = 200) YY_NOEXCEPT
1023  : seq_ (n)
1024  {}
1025 
1026 #if 201103L <= YY_CPLUSPLUS
1028  stack (const stack&) = delete;
1030  stack& operator= (const stack&) = delete;
1031 #endif
1032 
1036  const T&
1037  operator[] (index_type i) const
1038  {
1039  return seq_[size_type (size () - 1 - i)];
1040  }
1041 
1045  T&
1046  operator[] (index_type i)
1047  {
1048  return seq_[size_type (size () - 1 - i)];
1049  }
1050 
1054  void
1055  push (YY_MOVE_REF (T) t)
1056  {
1057  seq_.push_back (T ());
1058  operator[] (0).move (t);
1059  }
1060 
1062  void
1063  pop (std::ptrdiff_t n = 1) YY_NOEXCEPT
1064  {
1065  for (; 0 < n; --n)
1066  seq_.pop_back ();
1067  }
1068 
1070  void
1071  clear () YY_NOEXCEPT
1072  {
1073  seq_.clear ();
1074  }
1075 
1077  index_type
1078  size () const YY_NOEXCEPT
1079  {
1080  return index_type (seq_.size ());
1081  }
1082 
1084  const_iterator
1085  begin () const YY_NOEXCEPT
1086  {
1087  return seq_.begin ();
1088  }
1089 
1091  const_iterator
1092  end () const YY_NOEXCEPT
1093  {
1094  return seq_.end ();
1095  }
1096 
1098  class slice
1099  {
1100  public:
1101  slice (const stack& stack, index_type range) YY_NOEXCEPT
1102  : stack_ (stack)
1103  , range_ (range)
1104  {}
1105 
1106  const T&
1107  operator[] (index_type i) const
1108  {
1109  return stack_[range_ - i];
1110  }
1111 
1112  private:
1113  const stack& stack_;
1114  index_type range_;
1115  };
1116 
1117  private:
1118 #if YY_CPLUSPLUS < 201103L
1120  stack (const stack&);
1122  stack& operator= (const stack&);
1123 #endif
1125  S seq_;
1126  };
1127 
1128 
1130  typedef stack<stack_symbol_type> stack_type;
1131 
1133  stack_type yystack_;
1134 
1140  void yypush_ (const char* m, YY_MOVE_REF (stack_symbol_type) sym);
1141 
1148  void yypush_ (const char* m, state_type s, YY_MOVE_REF (symbol_type) sym);
1149 
1151  void yypop_ (int n = 1) YY_NOEXCEPT;
1152 
1154  enum
1155  {
1156  yylast_ = 245,
1157  yynnts_ = 86,
1158  yyfinal_ = 26
1159  };
1160 
1161 
1162  // User arguments.
1163  void* scanner;
1164  result_& res;
1165  spot::location initial_loc;
1166 
1167  };
1168 
1169 
1170 } // hoayy
1171 #line 1172 "parseaut.hh"
1172 
1173 
1174 
1175 
1176 #endif // !YY_HOAYY_PARSEAUT_HH_INCLUDED
Definition: parseaut.hh:829
int expected_tokens(symbol_kind_type yyarg[], int yyargn) const
Present a slice of the top of a stack.
Definition: parseaut.hh:1099
A Bison parser.
Definition: parseaut.hh:364
void error(const syntax_error &err)
Report a syntax error.
token_kind_type token_type
Backward compatibility alias (Bison 3.6).
Definition: parseaut.hh:482
symbol_kind::symbol_kind_type symbol_kind_type
(Internal) symbol kind.
Definition: parseaut.hh:649
token::token_kind_type token_kind_type
Token kind, as returned by yylex.
Definition: parseaut.hh:479
std::ostream & debug_stream() const
The current debugging stream.
spot::location location_type
Symbol locations.
Definition: parseaut.hh:394
virtual int parse()
static std::string symbol_name(symbol_kind_type yysymbol)
int debug_level_type
Type for debugging levels.
Definition: parseaut.hh:807
value_type semantic_type
Backward compatibility (Bison 3.8).
Definition: parseaut.hh:391
virtual void error(const location_type &loc, const std::string &msg)
parser(void *scanner_yyarg, result_ &res_yyarg, spot::location initial_loc_yyarg)
Build a parser object.
An environment that describes atomic propositions.
Definition: environment.hh:33
Definition: ngraph.hh:33
A class implementing Kleene's three-valued logic.
Definition: trival.hh:34
Definition: parseaut.hh:662
Base super_type
Alias to Base.
Definition: parseaut.hh:664
basic_symbol()
Default constructor.
Definition: parseaut.hh:667
symbol_kind_type type_get() const
Backward compatibility (Bison 3.6).
void clear()
Destroy contents, and record that is empty.
Definition: parseaut.hh:701
basic_symbol(const basic_symbol &that)
Copy constructor.
basic_symbol(typename Base::kind_type t, const value_type &v, const location_type &l)
Constructor for symbols with semantic value.
basic_symbol(typename Base::kind_type t, location_type &l)
Constructor for valueless symbols.
std::string name() const
The user-facing name of this symbol.
Definition: parseaut.hh:707
~basic_symbol()
Destroy the symbol.
Definition: parseaut.hh:693
Type access provider for token (enum) based symbols.
Definition: parseaut.hh:736
by_kind()
Default constructor.
void clear()
Record that this symbol is empty.
by_kind(kind_type t)
Constructor from (external) token numbers.
by_kind(const by_kind &that)
Copy constructor.
token_kind_type kind_type
The symbol kind as needed by the constructor.
Definition: parseaut.hh:738
Symbol kinds.
Definition: parseaut.hh:486
symbol_kind_type
Definition: parseaut.hh:488
"External" symbols: returned by the scanner.
Definition: parseaut.hh:779
Syntax errors thrown from user actions.
Definition: parseaut.hh:398
Token kinds.
Definition: parseaut.hh:416
token_kind_type yytokentype
Backward compatibility alias (Bison 3.6).
Definition: parseaut.hh:475
Definition: parseaut.hh:136
Definition: parseaut.hh:101
Definition: parseaut.hh:99
An acceptance formula.
Definition: acc.hh:487
An acceptance mark.
Definition: acc.hh:89
Definition: public.hh:93
Symbol semantic values.
Definition: parseaut.hh:374

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