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

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