spot  2.10.6.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 #include <spot/twaalgos/game.hh>
64 
65 using namespace std::string_literals;
66 
67 #ifndef HAVE_STRVERSCMP
68 // If the libc does not have this, a version is compiled in lib/.
69 extern "C" int strverscmp(const char *s1, const char *s2);
70 #endif
71 
72 // Work around Bison not letting us write
73 // %lex-param { res.h->errors, res.fcache }
74 #define PARSE_ERROR_LIST res.h->errors, res.fcache
75 
76  inline namespace hoayy_support
77  {
78  typedef std::map<int, bdd> map_t;
79 
80  /* Cache parsed formulae. Labels on arcs are frequently identical
81  and it would be a waste of time to parse them to formula
82  over and over, and to register all their atomic_propositions in
83  the bdd_dict. Keep the bdd result around so we can reuse
84  it. */
85  typedef robin_hood::unordered_flat_map<std::string, bdd> formula_cache;
86 
87  typedef std::pair<int, std::string*> pair;
88  typedef spot::twa_graph::namer<std::string> named_tgba_t;
89 
90  // Note: because this parser is meant to be used on a stream of
91  // automata, it tries hard to recover from errors, so that we get a
92  // chance to reach the end of the current automaton in order to
93  // process the next one. Several variables below are used to keep
94  // track of various error conditions.
95  enum label_style_t { Mixed_Labels, State_Labels, Trans_Labels,
96  Implicit_Labels };
97  enum acc_style_t { Mixed_Acc, State_Acc, Trans_Acc };
98 
99  struct result_
100  {
101  struct state_info
102  {
103  bool declared = false;
104  bool used = false;
105  spot::location used_loc;
106  };
107  spot::parsed_aut_ptr h;
108  spot::twa_ptr aut_or_ks;
110  std::string format_version;
111  spot::location format_version_loc;
112  spot::environment* env;
113  formula_cache fcache;
114  named_tgba_t* namer = nullptr;
115  spot::acc_mapper_int* acc_mapper = nullptr;
116  std::vector<int> ap;
117  std::vector<int> controllable_ap;
118  bool has_controllable_ap = false;
119  std::vector<spot::location> controllable_ap_loc;
120  spot::location controllable_aps_loc;
121  std::vector<bdd> guards;
122  std::vector<bdd>::const_iterator cur_guard;
123  // If "Alias: ..." occurs before "AP: ..." in the HOA format we
124  // are in trouble because the parser would like to turn each
125  // alias into a BDD, yet the atomic proposition have not been
126  // declared yet. We solve that by using arbitrary BDD variables
127  // numbers (in fact we use the same number given in the Alias:
128  // definition) and keeping track of the highest variable number
129  // we have seen (unknown_ap_max). Once AP: is encountered,
130  // we can remap everything. If AP: is never encountered an
131  // unknown_ap_max is non-negative, then we can signal an error.
132  int unknown_ap_max = -1;
133  spot::location unknown_ap_max_location;
134  bool in_alias = false;
135  map_t dest_map;
136  std::vector<state_info> info_states; // States declared and used.
137  std::vector<std::pair<spot::location,
138  std::vector<unsigned>>> start; // Initial states;
139  std::unordered_map<std::string, bdd> alias;
140  std::vector<std::string> alias_order;
141  struct prop_info
142  {
143  spot::location loc;
144  bool val;
145  operator bool() const
146  {
147  return val;
148  };
149  };
150  std::unordered_map<std::string, prop_info> props;
151  spot::location states_loc;
152  spot::location ap_loc;
153  spot::location state_label_loc;
154  spot::location accset_loc;
155  spot::acc_cond::mark_t acc_state;
156  spot::acc_cond::mark_t neg_acc_sets = {};
157  spot::acc_cond::mark_t pos_acc_sets = {};
158  int plus;
159  int minus;
160  std::vector<std::string>* state_names = nullptr;
161  std::map<unsigned, unsigned>* highlight_edges = nullptr;
162  std::map<unsigned, unsigned>* highlight_states = nullptr;
163  std::map<unsigned, unsigned> states_map;
164  std::vector<bool>* state_player = nullptr;
165  spot::location state_player_loc;
166  std::set<int> ap_set;
167  unsigned cur_state;
168  int states = -1;
169  int ap_count = -1;
170  int accset = -1;
171  bdd state_label;
172  bdd cur_label;
173  bool has_state_label = false;
174  bool ignore_more_ap = false; // Set to true after the first "AP:"
175  // line has been read.
176  bool ignore_acc = false; // Set to true in case of missing
177  // Acceptance: lines.
178  bool ignore_acc_silent = false;
179  bool ignore_more_acc = false; // Set to true after the first
180  // "Acceptance:" line has been read.
181 
182  label_style_t label_style = Mixed_Labels;
183  acc_style_t acc_style = Mixed_Acc;
184 
185  bool accept_all_needed = false;
186  bool accept_all_seen = false;
187  bool aliased_states = false;
188 
189  spot::trival universal = spot::trival::maybe();
190  spot::trival existential = spot::trival::maybe();
191  spot::trival complete = spot::trival::maybe();
192  bool trans_acc_seen = false;
193 
194  std::map<std::string, spot::location> labels;
195 
196  prop_info prop_is_true(const std::string& p)
197  {
198  auto i = props.find(p);
199  if (i == props.end())
200  return prop_info{spot::location(), false};
201  return i->second;
202  }
203 
204  prop_info prop_is_false(const std::string& p)
205  {
206  auto i = props.find(p);
207  if (i == props.end())
208  return prop_info{spot::location(), false};
209  return prop_info{i->second.loc, !i->second.val};
210  }
211 
212  ~result_()
213  {
214  delete namer;
215  delete acc_mapper;
216  }
217  };
218  }
219 
220 #line 221 "parseaut.hh"
221 
222 
223 # include <cstdlib> // std::abort
224 # include <iostream>
225 # include <stdexcept>
226 # include <string>
227 # include <vector>
228 
229 #if defined __cplusplus
230 # define YY_CPLUSPLUS __cplusplus
231 #else
232 # define YY_CPLUSPLUS 199711L
233 #endif
234 
235 // Support move semantics when possible.
236 #if 201103L <= YY_CPLUSPLUS
237 # define YY_MOVE std::move
238 # define YY_MOVE_OR_COPY move
239 # define YY_MOVE_REF(Type) Type&&
240 # define YY_RVREF(Type) Type&&
241 # define YY_COPY(Type) Type
242 #else
243 # define YY_MOVE
244 # define YY_MOVE_OR_COPY copy
245 # define YY_MOVE_REF(Type) Type&
246 # define YY_RVREF(Type) const Type&
247 # define YY_COPY(Type) const Type&
248 #endif
249 
250 // Support noexcept when possible.
251 #if 201103L <= YY_CPLUSPLUS
252 # define YY_NOEXCEPT noexcept
253 # define YY_NOTHROW
254 #else
255 # define YY_NOEXCEPT
256 # define YY_NOTHROW throw ()
257 #endif
258 
259 // Support constexpr when possible.
260 #if 201703 <= YY_CPLUSPLUS
261 # define YY_CONSTEXPR constexpr
262 #else
263 # define YY_CONSTEXPR
264 #endif
265 
266 
267 
268 #ifndef YY_ATTRIBUTE_PURE
269 # if defined __GNUC__ && 2 < __GNUC__ + (96 <= __GNUC_MINOR__)
270 # define YY_ATTRIBUTE_PURE __attribute__ ((__pure__))
271 # else
272 # define YY_ATTRIBUTE_PURE
273 # endif
274 #endif
275 
276 #ifndef YY_ATTRIBUTE_UNUSED
277 # if defined __GNUC__ && 2 < __GNUC__ + (7 <= __GNUC_MINOR__)
278 # define YY_ATTRIBUTE_UNUSED __attribute__ ((__unused__))
279 # else
280 # define YY_ATTRIBUTE_UNUSED
281 # endif
282 #endif
283 
284 /* Suppress unused-variable warnings by "using" E. */
285 #if ! defined lint || defined __GNUC__
286 # define YY_USE(E) ((void) (E))
287 #else
288 # define YY_USE(E) /* empty */
289 #endif
290 
291 /* Suppress an incorrect diagnostic about yylval being uninitialized. */
292 #if defined __GNUC__ && ! defined __ICC && 406 <= __GNUC__ * 100 + __GNUC_MINOR__
293 # if __GNUC__ * 100 + __GNUC_MINOR__ < 407
294 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
295  _Pragma ("GCC diagnostic push") \
296  _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"")
297 # else
298 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
299  _Pragma ("GCC diagnostic push") \
300  _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"") \
301  _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"")
302 # endif
303 # define YY_IGNORE_MAYBE_UNINITIALIZED_END \
304  _Pragma ("GCC diagnostic pop")
305 #else
306 # define YY_INITIAL_VALUE(Value) Value
307 #endif
308 #ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
309 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
310 # define YY_IGNORE_MAYBE_UNINITIALIZED_END
311 #endif
312 #ifndef YY_INITIAL_VALUE
313 # define YY_INITIAL_VALUE(Value) /* Nothing. */
314 #endif
315 
316 #if defined __cplusplus && defined __GNUC__ && ! defined __ICC && 6 <= __GNUC__
317 # define YY_IGNORE_USELESS_CAST_BEGIN \
318  _Pragma ("GCC diagnostic push") \
319  _Pragma ("GCC diagnostic ignored \"-Wuseless-cast\"")
320 # define YY_IGNORE_USELESS_CAST_END \
321  _Pragma ("GCC diagnostic pop")
322 #endif
323 #ifndef YY_IGNORE_USELESS_CAST_BEGIN
324 # define YY_IGNORE_USELESS_CAST_BEGIN
325 # define YY_IGNORE_USELESS_CAST_END
326 #endif
327 
328 # ifndef YY_CAST
329 # ifdef __cplusplus
330 # define YY_CAST(Type, Val) static_cast<Type> (Val)
331 # define YY_REINTERPRET_CAST(Type, Val) reinterpret_cast<Type> (Val)
332 # else
333 # define YY_CAST(Type, Val) ((Type) (Val))
334 # define YY_REINTERPRET_CAST(Type, Val) ((Type) (Val))
335 # endif
336 # endif
337 # ifndef YY_NULLPTR
338 # if defined __cplusplus
339 # if 201103L <= __cplusplus
340 # define YY_NULLPTR nullptr
341 # else
342 # define YY_NULLPTR 0
343 # endif
344 # else
345 # define YY_NULLPTR ((void*)0)
346 # endif
347 # endif
348 
349 /* Debug traces. */
350 #ifndef HOAYYDEBUG
351 # if defined YYDEBUG
352 #if YYDEBUG
353 # define HOAYYDEBUG 1
354 # else
355 # define HOAYYDEBUG 0
356 # endif
357 # else /* ! defined YYDEBUG */
358 # define HOAYYDEBUG 1
359 # endif /* ! defined YYDEBUG */
360 #endif /* ! defined HOAYYDEBUG */
361 
362 namespace hoayy {
363 #line 364 "parseaut.hh"
364 
365 
366 
367 
369  class parser
370  {
371  public:
372 #ifdef HOAYYSTYPE
373 # ifdef __GNUC__
374 # pragma GCC message "bison: do not #define HOAYYSTYPE in C++, use %define api.value.type"
375 # endif
376  typedef HOAYYSTYPE value_type;
377 #else
380  {
381 #line 211 "parseaut.yy"
382 
383  std::string* str;
384  unsigned int num;
385  int b;
387  pair* p;
388  std::list<pair>* list;
390  std::vector<unsigned>* states;
391 
392 #line 393 "parseaut.hh"
393 
394  };
395 #endif
398 
400  typedef spot::location location_type;
401 
403  struct syntax_error : std::runtime_error
404  {
405  syntax_error (const location_type& l, const std::string& m)
406  : std::runtime_error (m)
407  , location (l)
408  {}
409 
410  syntax_error (const syntax_error& s)
411  : std::runtime_error (s.what ())
412  , location (s.location)
413  {}
414 
415  ~syntax_error () YY_NOEXCEPT YY_NOTHROW;
416 
417  location_type location;
418  };
419 
421  struct token
422  {
423  enum token_kind_type
424  {
425  HOAYYEMPTY = -2,
426  ENDOFFILE = 0, // "end of file"
427  HOAYYerror = 256, // error
428  HOAYYUNDEF = 257, // "invalid token"
429  HOA = 258, // "HOA:"
430  STATES = 259, // "States:"
431  START = 260, // "Start:"
432  AP = 261, // "AP:"
433  ALIAS = 262, // "Alias:"
434  ACCEPTANCE = 263, // "Acceptance:"
435  ACCNAME = 264, // "acc-name:"
436  CONTROLLABLE_AP = 265, // "controllable-AP:"
437  TOOL = 266, // "tool:"
438  NAME = 267, // "name:"
439  PROPERTIES = 268, // "properties:"
440  BODY = 269, // "--BODY--"
441  END = 270, // "--END--"
442  STATE = 271, // "State:"
443  SPOT_HIGHLIGHT_EDGES = 272, // "spot.highlight.edges:"
444  SPOT_HIGHLIGHT_STATES = 273, // "spot.highlight.states:"
445  SPOT_STATE_PLAYER = 274, // "spot.state-player:"
446  IDENTIFIER = 275, // "identifier"
447  HEADERNAME = 276, // "header name"
448  ANAME = 277, // "alias name"
449  STRING = 278, // "string"
450  INT = 279, // "integer"
451  LINEDIRECTIVE = 280, // "#line"
452  BDD = 281, // BDD
453  ENDDSTAR = 282, // "end of DSTAR automaton"
454  DRA = 283, // "DRA"
455  DSA = 284, // "DSA"
456  V2 = 285, // "v2"
457  EXPLICIT = 286, // "explicit"
458  ACCPAIRS = 287, // "Acceptance-Pairs:"
459  ACCSIG = 288, // "Acc-Sig:"
460  ENDOFHEADER = 289, // "---"
461  NEVER = 290, // "never"
462  SKIP = 291, // "skip"
463  IF = 292, // "if"
464  FI = 293, // "fi"
465  DO = 294, // "do"
466  OD = 295, // "od"
467  ARROW = 296, // "->"
468  GOTO = 297, // "goto"
469  FALSE = 298, // "false"
470  ATOMIC = 299, // "atomic"
471  ASSERT = 300, // "assert"
472  FORMULA = 301, // "boolean formula"
473  PGAME = 302, // "start of PGSolver game"
474  ENDPGAME = 303, // "end of PGSolver game"
475  ENDAUT = 304, // "-1"
476  LBTT = 305, // "LBTT header"
477  INT_S = 306, // "state acceptance"
478  LBTT_EMPTY = 307, // "acceptance sets for empty automaton"
479  ACC = 308, // "acceptance set"
480  STATE_NUM = 309, // "state number"
481  DEST_NUM = 310 // "destination number"
482  };
484  typedef token_kind_type yytokentype;
485  };
486 
488  typedef token::token_kind_type token_kind_type;
489 
491  typedef token_kind_type token_type;
492 
494  struct symbol_kind
495  {
497  {
498  YYNTOKENS = 72,
499  S_YYEMPTY = -2,
500  S_YYEOF = 0, // "end of file"
501  S_YYerror = 1, // error
502  S_YYUNDEF = 2, // "invalid token"
503  S_HOA = 3, // "HOA:"
504  S_STATES = 4, // "States:"
505  S_START = 5, // "Start:"
506  S_AP = 6, // "AP:"
507  S_ALIAS = 7, // "Alias:"
508  S_ACCEPTANCE = 8, // "Acceptance:"
509  S_ACCNAME = 9, // "acc-name:"
510  S_CONTROLLABLE_AP = 10, // "controllable-AP:"
511  S_TOOL = 11, // "tool:"
512  S_NAME = 12, // "name:"
513  S_PROPERTIES = 13, // "properties:"
514  S_BODY = 14, // "--BODY--"
515  S_END = 15, // "--END--"
516  S_STATE = 16, // "State:"
517  S_SPOT_HIGHLIGHT_EDGES = 17, // "spot.highlight.edges:"
518  S_SPOT_HIGHLIGHT_STATES = 18, // "spot.highlight.states:"
519  S_SPOT_STATE_PLAYER = 19, // "spot.state-player:"
520  S_IDENTIFIER = 20, // "identifier"
521  S_HEADERNAME = 21, // "header name"
522  S_ANAME = 22, // "alias name"
523  S_STRING = 23, // "string"
524  S_INT = 24, // "integer"
525  S_25_ = 25, // '['
526  S_LINEDIRECTIVE = 26, // "#line"
527  S_BDD = 27, // BDD
528  S_ENDDSTAR = 28, // "end of DSTAR automaton"
529  S_DRA = 29, // "DRA"
530  S_DSA = 30, // "DSA"
531  S_V2 = 31, // "v2"
532  S_EXPLICIT = 32, // "explicit"
533  S_ACCPAIRS = 33, // "Acceptance-Pairs:"
534  S_ACCSIG = 34, // "Acc-Sig:"
535  S_ENDOFHEADER = 35, // "---"
536  S_36_ = 36, // '|'
537  S_37_ = 37, // '&'
538  S_38_ = 38, // '!'
539  S_NEVER = 39, // "never"
540  S_SKIP = 40, // "skip"
541  S_IF = 41, // "if"
542  S_FI = 42, // "fi"
543  S_DO = 43, // "do"
544  S_OD = 44, // "od"
545  S_ARROW = 45, // "->"
546  S_GOTO = 46, // "goto"
547  S_FALSE = 47, // "false"
548  S_ATOMIC = 48, // "atomic"
549  S_ASSERT = 49, // "assert"
550  S_FORMULA = 50, // "boolean formula"
551  S_PGAME = 51, // "start of PGSolver game"
552  S_ENDPGAME = 52, // "end of PGSolver game"
553  S_ENDAUT = 53, // "-1"
554  S_LBTT = 54, // "LBTT header"
555  S_INT_S = 55, // "state acceptance"
556  S_LBTT_EMPTY = 56, // "acceptance sets for empty automaton"
557  S_ACC = 57, // "acceptance set"
558  S_STATE_NUM = 58, // "state number"
559  S_DEST_NUM = 59, // "destination number"
560  S_60_t_ = 60, // 't'
561  S_61_f_ = 61, // 'f'
562  S_62_ = 62, // '('
563  S_63_ = 63, // ')'
564  S_64_ = 64, // ']'
565  S_65_ = 65, // '{'
566  S_66_ = 66, // '}'
567  S_67_ = 67, // '+'
568  S_68_ = 68, // '-'
569  S_69_ = 69, // ';'
570  S_70_ = 70, // ','
571  S_71_ = 71, // ':'
572  S_YYACCEPT = 72, // $accept
573  S_aut = 73, // aut
574  S_74_1 = 74, // $@1
575  S_75_aut_1 = 75, // aut-1
576  S_hoa = 76, // hoa
577  S_string_opt = 77, // string_opt
578  S_BOOLEAN = 78, // BOOLEAN
579  S_header = 79, // header
580  S_version = 80, // version
581  S_81_format_version = 81, // format-version
582  S_82_2 = 82, // $@2
583  S_83_controllable_aps = 83, // controllable-aps
584  S_aps = 84, // aps
585  S_85_3 = 85, // $@3
586  S_86_header_items = 86, // header-items
587  S_87_header_item = 87, // header-item
588  S_88_4 = 88, // $@4
589  S_89_5 = 89, // $@5
590  S_90_6 = 90, // $@6
591  S_91_7 = 91, // $@7
592  S_92_8 = 92, // $@8
593  S_93_ap_names = 93, // ap-names
594  S_94_ap_name = 94, // ap-name
595  S_95_acc_spec = 95, // acc-spec
596  S_properties = 96, // properties
597  S_97_highlight_edges = 97, // highlight-edges
598  S_98_highlight_states = 98, // highlight-states
599  S_99_state_player = 99, // state-player
600  S_100_header_spec = 100, // header-spec
601  S_101_state_conj_2 = 101, // state-conj-2
602  S_102_init_state_conj_2 = 102, // init-state-conj-2
603  S_103_label_expr = 103, // label-expr
604  S_104_acc_set = 104, // acc-set
605  S_105_acceptance_cond = 105, // acceptance-cond
606  S_body = 106, // body
607  S_107_state_num = 107, // state-num
608  S_108_checked_state_num = 108, // checked-state-num
609  S_states = 109, // states
610  S_state = 110, // state
611  S_111_state_name = 111, // state-name
612  S_label = 112, // label
613  S_113_state_label_opt = 113, // state-label_opt
614  S_114_trans_label = 114, // trans-label
615  S_115_acc_sig = 115, // acc-sig
616  S_116_acc_sets = 116, // acc-sets
617  S_117_state_acc_opt = 117, // state-acc_opt
618  S_118_trans_acc_opt = 118, // trans-acc_opt
619  S_119_labeled_edges = 119, // labeled-edges
620  S_120_some_labeled_edges = 120, // some-labeled-edges
621  S_121_incorrectly_unlabeled_edge = 121, // incorrectly-unlabeled-edge
622  S_122_labeled_edge = 122, // labeled-edge
623  S_123_state_conj_checked = 123, // state-conj-checked
624  S_124_unlabeled_edges = 124, // unlabeled-edges
625  S_125_unlabeled_edge = 125, // unlabeled-edge
626  S_126_incorrectly_labeled_edge = 126, // incorrectly-labeled-edge
627  S_dstar = 127, // dstar
628  S_dstar_type = 128, // dstar_type
629  S_dstar_header = 129, // dstar_header
630  S_dstar_sizes = 130, // dstar_sizes
631  S_dstar_state_id = 131, // dstar_state_id
632  S_sign = 132, // sign
633  S_dstar_accsigs = 133, // dstar_accsigs
634  S_dstar_state_accsig = 134, // dstar_state_accsig
635  S_dstar_transitions = 135, // dstar_transitions
636  S_dstar_states = 136, // dstar_states
637  S_pgamestart = 137, // pgamestart
638  S_pgame = 138, // pgame
639  S_pgame_nodes = 139, // pgame_nodes
640  S_pgame_succs = 140, // pgame_succs
641  S_pgame_node = 141, // pgame_node
642  S_never = 142, // never
643  S_143_9 = 143, // $@9
644  S_144_nc_states = 144, // nc-states
645  S_145_nc_one_ident = 145, // nc-one-ident
646  S_146_nc_ident_list = 146, // nc-ident-list
647  S_147_nc_transition_block = 147, // nc-transition-block
648  S_148_nc_state = 148, // nc-state
649  S_149_nc_transitions = 149, // nc-transitions
650  S_150_nc_formula_or_ident = 150, // nc-formula-or-ident
651  S_151_nc_formula = 151, // nc-formula
652  S_152_nc_opt_dest = 152, // nc-opt-dest
653  S_153_nc_src_dest = 153, // nc-src-dest
654  S_154_nc_transition = 154, // nc-transition
655  S_lbtt = 155, // lbtt
656  S_156_lbtt_header_states = 156, // lbtt-header-states
657  S_157_lbtt_header = 157, // lbtt-header
658  S_158_lbtt_body = 158, // lbtt-body
659  S_159_lbtt_states = 159, // lbtt-states
660  S_160_lbtt_state = 160, // lbtt-state
661  S_161_lbtt_acc = 161, // lbtt-acc
662  S_162_lbtt_guard = 162, // lbtt-guard
663  S_163_lbtt_transitions = 163 // lbtt-transitions
664  };
665  };
666 
669 
671  static const symbol_kind_type YYNTOKENS = symbol_kind::YYNTOKENS;
672 
679  template <typename Base>
680  struct basic_symbol : Base
681  {
683  typedef Base super_type;
684 
686  basic_symbol () YY_NOEXCEPT
687  : value ()
688  , location ()
689  {}
690 
691 #if 201103L <= YY_CPLUSPLUS
693  basic_symbol (basic_symbol&& that)
694  : Base (std::move (that))
695  , value (std::move (that.value))
696  , location (std::move (that.location))
697  {}
698 #endif
699 
701  basic_symbol (const basic_symbol& that);
703  basic_symbol (typename Base::kind_type t,
704  YY_MOVE_REF (location_type) l);
705 
707  basic_symbol (typename Base::kind_type t,
708  YY_RVREF (value_type) v,
709  YY_RVREF (location_type) l);
710 
713  {
714  clear ();
715  }
716 
717 
718 
720  void clear () YY_NOEXCEPT
721  {
722  Base::clear ();
723  }
724 
726  std::string name () const YY_NOEXCEPT
727  {
728  return parser::symbol_name (this->kind ());
729  }
730 
732  symbol_kind_type type_get () const YY_NOEXCEPT;
733 
735  bool empty () const YY_NOEXCEPT;
736 
738  void move (basic_symbol& s);
739 
741  value_type value;
742 
744  location_type location;
745 
746  private:
747 #if YY_CPLUSPLUS < 201103L
749  basic_symbol& operator= (const basic_symbol& that);
750 #endif
751  };
752 
754  struct by_kind
755  {
757  typedef token_kind_type kind_type;
758 
760  by_kind () YY_NOEXCEPT;
761 
762 #if 201103L <= YY_CPLUSPLUS
764  by_kind (by_kind&& that) YY_NOEXCEPT;
765 #endif
766 
768  by_kind (const by_kind& that) YY_NOEXCEPT;
769 
771  by_kind (kind_type t) YY_NOEXCEPT;
772 
773 
774 
776  void clear () YY_NOEXCEPT;
777 
779  void move (by_kind& that);
780 
783  symbol_kind_type kind () const YY_NOEXCEPT;
784 
786  symbol_kind_type type_get () const YY_NOEXCEPT;
787 
791  };
792 
794  typedef by_kind by_type;
795 
798  {};
799 
801  parser (void* scanner_yyarg, result_& res_yyarg, spot::location initial_loc_yyarg);
802  virtual ~parser ();
803 
804 #if 201103L <= YY_CPLUSPLUS
806  parser (const parser&) = delete;
808  parser& operator= (const parser&) = delete;
809 #endif
810 
813  int operator() ();
814 
817  virtual int parse ();
818 
819 #if HOAYYDEBUG
821  std::ostream& debug_stream () const YY_ATTRIBUTE_PURE;
823  void set_debug_stream (std::ostream &);
824 
826  typedef int debug_level_type;
828  debug_level_type debug_level () const YY_ATTRIBUTE_PURE;
830  void set_debug_level (debug_level_type l);
831 #endif
832 
836  virtual void error (const location_type& loc, const std::string& msg);
837 
839  void error (const syntax_error& err);
840 
843  static std::string symbol_name (symbol_kind_type yysymbol);
844 
845 
846 
847  class context
848  {
849  public:
850  context (const parser& yyparser, const symbol_type& yyla);
851  const symbol_type& lookahead () const YY_NOEXCEPT { return yyla_; }
852  symbol_kind_type token () const YY_NOEXCEPT { return yyla_.kind (); }
853  const location_type& location () const YY_NOEXCEPT { return yyla_.location; }
854 
858  int expected_tokens (symbol_kind_type yyarg[], int yyargn) const;
859 
860  private:
861  const parser& yyparser_;
862  const symbol_type& yyla_;
863  };
864 
865  private:
866 #if YY_CPLUSPLUS < 201103L
868  parser (const parser&);
870  parser& operator= (const parser&);
871 #endif
872 
873 
875  typedef short state_type;
876 
878  int yy_syntax_error_arguments_ (const context& yyctx,
879  symbol_kind_type yyarg[], int yyargn) const;
880 
883  virtual std::string yysyntax_error_ (const context& yyctx) const;
887  static state_type yy_lr_goto_state_ (state_type yystate, int yysym);
888 
891  static bool yy_pact_value_is_default_ (int yyvalue) YY_NOEXCEPT;
892 
895  static bool yy_table_value_is_error_ (int yyvalue) YY_NOEXCEPT;
896 
897  static const short yypact_ninf_;
898  static const short yytable_ninf_;
899 
903  static symbol_kind_type yytranslate_ (int t) YY_NOEXCEPT;
904 
906  static std::string yytnamerr_ (const char *yystr);
907 
909  static const char* const yytname_[];
910 
911 
912  // Tables.
913  // YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
914  // STATE-NUM.
915  static const short yypact_[];
916 
917  // YYDEFACT[STATE-NUM] -- Default reduction number in state STATE-NUM.
918  // Performed when YYTABLE does not specify something else to do. Zero
919  // means the default is an error.
920  static const unsigned char yydefact_[];
921 
922  // YYPGOTO[NTERM-NUM].
923  static const short yypgoto_[];
924 
925  // YYDEFGOTO[NTERM-NUM].
926  static const short yydefgoto_[];
927 
928  // YYTABLE[YYPACT[STATE-NUM]] -- What to do in state STATE-NUM. If
929  // positive, shift that token. If negative, reduce the rule whose
930  // number is the opposite. If YYTABLE_NINF, syntax error.
931  static const short yytable_[];
932 
933  static const short yycheck_[];
934 
935  // YYSTOS[STATE-NUM] -- The symbol kind of the accessing symbol of
936  // state STATE-NUM.
937  static const unsigned char yystos_[];
938 
939  // YYR1[RULE-NUM] -- Symbol kind of the left-hand side of rule RULE-NUM.
940  static const unsigned char yyr1_[];
941 
942  // YYR2[RULE-NUM] -- Number of symbols on the right-hand side of rule RULE-NUM.
943  static const signed char yyr2_[];
944 
945 
946 #if HOAYYDEBUG
947  // YYRLINE[YYN] -- Source line where rule number YYN was defined.
948  static const short yyrline_[];
950  virtual void yy_reduce_print_ (int r) const;
952  virtual void yy_stack_print_ () const;
953 
955  int yydebug_;
957  std::ostream* yycdebug_;
958 
962  template <typename Base>
963  void yy_print_ (std::ostream& yyo, const basic_symbol<Base>& yysym) const;
964 #endif
965 
970  template <typename Base>
971  void yy_destroy_ (const char* yymsg, basic_symbol<Base>& yysym) const;
972 
973  private:
975  struct by_state
976  {
978  by_state () YY_NOEXCEPT;
979 
981  typedef state_type kind_type;
982 
984  by_state (kind_type s) YY_NOEXCEPT;
985 
987  by_state (const by_state& that) YY_NOEXCEPT;
988 
990  void clear () YY_NOEXCEPT;
991 
993  void move (by_state& that);
994 
997  symbol_kind_type kind () const YY_NOEXCEPT;
998 
1001  enum { empty_state = 0 };
1002 
1005  state_type state;
1006  };
1007 
1009  struct stack_symbol_type : basic_symbol<by_state>
1010  {
1012  typedef basic_symbol<by_state> super_type;
1014  stack_symbol_type ();
1016  stack_symbol_type (YY_RVREF (stack_symbol_type) that);
1018  stack_symbol_type (state_type s, YY_MOVE_REF (symbol_type) sym);
1019 #if YY_CPLUSPLUS < 201103L
1022  stack_symbol_type& operator= (stack_symbol_type& that);
1023 
1026  stack_symbol_type& operator= (const stack_symbol_type& that);
1027 #endif
1028  };
1029 
1031  template <typename T, typename S = std::vector<T> >
1032  class stack
1033  {
1034  public:
1035  // Hide our reversed order.
1036  typedef typename S::iterator iterator;
1037  typedef typename S::const_iterator const_iterator;
1038  typedef typename S::size_type size_type;
1039  typedef typename std::ptrdiff_t index_type;
1040 
1041  stack (size_type n = 200) YY_NOEXCEPT
1042  : seq_ (n)
1043  {}
1044 
1045 #if 201103L <= YY_CPLUSPLUS
1047  stack (const stack&) = delete;
1049  stack& operator= (const stack&) = delete;
1050 #endif
1051 
1055  const T&
1056  operator[] (index_type i) const
1057  {
1058  return seq_[size_type (size () - 1 - i)];
1059  }
1060 
1064  T&
1065  operator[] (index_type i)
1066  {
1067  return seq_[size_type (size () - 1 - i)];
1068  }
1069 
1073  void
1074  push (YY_MOVE_REF (T) t)
1075  {
1076  seq_.push_back (T ());
1077  operator[] (0).move (t);
1078  }
1079 
1081  void
1082  pop (std::ptrdiff_t n = 1) YY_NOEXCEPT
1083  {
1084  for (; 0 < n; --n)
1085  seq_.pop_back ();
1086  }
1087 
1089  void
1090  clear () YY_NOEXCEPT
1091  {
1092  seq_.clear ();
1093  }
1094 
1096  index_type
1097  size () const YY_NOEXCEPT
1098  {
1099  return index_type (seq_.size ());
1100  }
1101 
1103  const_iterator
1104  begin () const YY_NOEXCEPT
1105  {
1106  return seq_.begin ();
1107  }
1108 
1110  const_iterator
1111  end () const YY_NOEXCEPT
1112  {
1113  return seq_.end ();
1114  }
1115 
1117  class slice
1118  {
1119  public:
1120  slice (const stack& stack, index_type range) YY_NOEXCEPT
1121  : stack_ (stack)
1122  , range_ (range)
1123  {}
1124 
1125  const T&
1126  operator[] (index_type i) const
1127  {
1128  return stack_[range_ - i];
1129  }
1130 
1131  private:
1132  const stack& stack_;
1133  index_type range_;
1134  };
1135 
1136  private:
1137 #if YY_CPLUSPLUS < 201103L
1139  stack (const stack&);
1141  stack& operator= (const stack&);
1142 #endif
1144  S seq_;
1145  };
1146 
1147 
1149  typedef stack<stack_symbol_type> stack_type;
1150 
1152  stack_type yystack_;
1153 
1159  void yypush_ (const char* m, YY_MOVE_REF (stack_symbol_type) sym);
1160 
1167  void yypush_ (const char* m, state_type s, YY_MOVE_REF (symbol_type) sym);
1168 
1170  void yypop_ (int n = 1) YY_NOEXCEPT;
1171 
1173  enum
1174  {
1175  yylast_ = 271,
1176  yynnts_ = 92,
1177  yyfinal_ = 29
1178  };
1179 
1180 
1181  // User arguments.
1182  void* scanner;
1183  result_& res;
1184  spot::location initial_loc;
1185 
1186  };
1187 
1188 
1189 } // hoayy
1190 #line 1191 "parseaut.hh"
1191 
1192 
1193 
1194 
1195 #endif // !YY_HOAYY_PARSEAUT_HH_INCLUDED
Definition: parseaut.hh:848
int expected_tokens(symbol_kind_type yyarg[], int yyargn) const
Present a slice of the top of a stack.
Definition: parseaut.hh:1118
A Bison parser.
Definition: parseaut.hh:370
void error(const syntax_error &err)
Report a syntax error.
token_kind_type token_type
Backward compatibility alias (Bison 3.6).
Definition: parseaut.hh:491
symbol_kind::symbol_kind_type symbol_kind_type
(Internal) symbol kind.
Definition: parseaut.hh:668
token::token_kind_type token_kind_type
Token kind, as returned by yylex.
Definition: parseaut.hh:488
std::ostream & debug_stream() const
The current debugging stream.
spot::location location_type
Symbol locations.
Definition: parseaut.hh:400
virtual int parse()
static std::string symbol_name(symbol_kind_type yysymbol)
int debug_level_type
Type for debugging levels.
Definition: parseaut.hh:826
value_type semantic_type
Backward compatibility (Bison 3.8).
Definition: parseaut.hh:397
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:681
Base super_type
Alias to Base.
Definition: parseaut.hh:683
basic_symbol()
Default constructor.
Definition: parseaut.hh:686
symbol_kind_type type_get() const
Backward compatibility (Bison 3.6).
void clear()
Destroy contents, and record that is empty.
Definition: parseaut.hh:720
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:726
~basic_symbol()
Destroy the symbol.
Definition: parseaut.hh:712
Type access provider for token (enum) based symbols.
Definition: parseaut.hh:755
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:757
Symbol kinds.
Definition: parseaut.hh:495
symbol_kind_type
Definition: parseaut.hh:497
"External" symbols: returned by the scanner.
Definition: parseaut.hh:798
Syntax errors thrown from user actions.
Definition: parseaut.hh:404
Token kinds.
Definition: parseaut.hh:422
token_kind_type yytokentype
Backward compatibility alias (Bison 3.6).
Definition: parseaut.hh:484
Definition: parseaut.hh:142
Definition: parseaut.hh:102
Definition: parseaut.hh:100
An acceptance formula.
Definition: acc.hh:488
An acceptance mark.
Definition: acc.hh:90
Definition: public.hh:100
Symbol semantic values.
Definition: parseaut.hh:380

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