spot  2.11.6
parseaut.hh
Go to the documentation of this file.
1 // A Bison parser, made by GNU Bison 3.7.5.
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 <http://www.gnu.org/licenses/>.
19 
20 // As a special exception, you may create a larger work that contains
21 // part or all of the Bison parser skeleton and distribute that work
22 // under terms of your choice, so long as that work isn't itself a
23 // parser generator using the skeleton or a modified version thereof
24 // as a parser skeleton. Alternatively, if you modify or redistribute
25 // the parser skeleton itself, you may (at your option) remove this
26 // special exception, which will cause the skeleton and the resulting
27 // Bison output files to be licensed under the GNU General Public
28 // License without this special exception.
29 
30 // This special exception was added by the Free Software Foundation in
31 // version 2.2 of Bison.
32 
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 #if defined __GNUC__ && ! defined __ICC && 407 <= __GNUC__ * 100 + __GNUC_MINOR__
292 /* Suppress an incorrect diagnostic about yylval being uninitialized. */
293 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
294  _Pragma ("GCC diagnostic push") \
295  _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"") \
296  _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"")
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 #ifndef HOAYYSTYPE
369  {
370 #line 211 "parseaut.yy"
371 
372  std::string* str;
373  unsigned int num;
374  int b;
376  pair* p;
377  std::list<pair>* list;
379  std::vector<unsigned>* states;
380 
381 #line 382 "parseaut.hh"
382 
383  };
384 #else
385  typedef HOAYYSTYPE semantic_type;
386 #endif
388  typedef spot::location location_type;
389 
391  struct syntax_error : std::runtime_error
392  {
393  syntax_error (const location_type& l, const std::string& m)
394  : std::runtime_error (m)
395  , location (l)
396  {}
397 
398  syntax_error (const syntax_error& s)
399  : std::runtime_error (s.what ())
400  , location (s.location)
401  {}
402 
403  ~syntax_error () YY_NOEXCEPT YY_NOTHROW;
404 
405  location_type location;
406  };
407 
409  struct token
410  {
411  enum token_kind_type
412  {
413  HOAYYEMPTY = -2,
414  ENDOFFILE = 0, // "end of file"
415  HOAYYerror = 256, // error
416  HOAYYUNDEF = 257, // "invalid token"
417  HOA = 258, // "HOA:"
418  STATES = 259, // "States:"
419  START = 260, // "Start:"
420  AP = 261, // "AP:"
421  ALIAS = 262, // "Alias:"
422  ACCEPTANCE = 263, // "Acceptance:"
423  ACCNAME = 264, // "acc-name:"
424  CONTROLLABLE_AP = 265, // "controllable-AP:"
425  TOOL = 266, // "tool:"
426  NAME = 267, // "name:"
427  PROPERTIES = 268, // "properties:"
428  BODY = 269, // "--BODY--"
429  END = 270, // "--END--"
430  STATE = 271, // "State:"
431  SPOT_HIGHLIGHT_EDGES = 272, // "spot.highlight.edges:"
432  SPOT_HIGHLIGHT_STATES = 273, // "spot.highlight.states:"
433  SPOT_STATE_PLAYER = 274, // "spot.state-player:"
434  IDENTIFIER = 275, // "identifier"
435  HEADERNAME = 276, // "header name"
436  ANAME = 277, // "alias name"
437  STRING = 278, // "string"
438  INT = 279, // "integer"
439  LINEDIRECTIVE = 280, // "#line"
440  BDD = 281, // BDD
441  ENDDSTAR = 282, // "end of DSTAR automaton"
442  DRA = 283, // "DRA"
443  DSA = 284, // "DSA"
444  V2 = 285, // "v2"
445  EXPLICIT = 286, // "explicit"
446  ACCPAIRS = 287, // "Acceptance-Pairs:"
447  ACCSIG = 288, // "Acc-Sig:"
448  ENDOFHEADER = 289, // "---"
449  NEVER = 290, // "never"
450  SKIP = 291, // "skip"
451  IF = 292, // "if"
452  FI = 293, // "fi"
453  DO = 294, // "do"
454  OD = 295, // "od"
455  ARROW = 296, // "->"
456  GOTO = 297, // "goto"
457  FALSE = 298, // "false"
458  ATOMIC = 299, // "atomic"
459  ASSERT = 300, // "assert"
460  FORMULA = 301, // "boolean formula"
461  PGAME = 302, // "start of PGSolver game"
462  ENDPGAME = 303, // "end of PGSolver game"
463  ENDAUT = 304, // "-1"
464  LBTT = 305, // "LBTT header"
465  INT_S = 306, // "state acceptance"
466  LBTT_EMPTY = 307, // "acceptance sets for empty automaton"
467  ACC = 308, // "acceptance set"
468  STATE_NUM = 309, // "state number"
469  DEST_NUM = 310 // "destination number"
470  };
472  typedef token_kind_type yytokentype;
473  };
474 
476  typedef token::yytokentype token_kind_type;
477 
479  typedef token_kind_type token_type;
480 
482  struct symbol_kind
483  {
485  {
486  YYNTOKENS = 72,
487  S_YYEMPTY = -2,
488  S_YYEOF = 0, // "end of file"
489  S_YYerror = 1, // error
490  S_YYUNDEF = 2, // "invalid token"
491  S_HOA = 3, // "HOA:"
492  S_STATES = 4, // "States:"
493  S_START = 5, // "Start:"
494  S_AP = 6, // "AP:"
495  S_ALIAS = 7, // "Alias:"
496  S_ACCEPTANCE = 8, // "Acceptance:"
497  S_ACCNAME = 9, // "acc-name:"
498  S_CONTROLLABLE_AP = 10, // "controllable-AP:"
499  S_TOOL = 11, // "tool:"
500  S_NAME = 12, // "name:"
501  S_PROPERTIES = 13, // "properties:"
502  S_BODY = 14, // "--BODY--"
503  S_END = 15, // "--END--"
504  S_STATE = 16, // "State:"
505  S_SPOT_HIGHLIGHT_EDGES = 17, // "spot.highlight.edges:"
506  S_SPOT_HIGHLIGHT_STATES = 18, // "spot.highlight.states:"
507  S_SPOT_STATE_PLAYER = 19, // "spot.state-player:"
508  S_IDENTIFIER = 20, // "identifier"
509  S_HEADERNAME = 21, // "header name"
510  S_ANAME = 22, // "alias name"
511  S_STRING = 23, // "string"
512  S_INT = 24, // "integer"
513  S_25_ = 25, // '['
514  S_LINEDIRECTIVE = 26, // "#line"
515  S_BDD = 27, // BDD
516  S_ENDDSTAR = 28, // "end of DSTAR automaton"
517  S_DRA = 29, // "DRA"
518  S_DSA = 30, // "DSA"
519  S_V2 = 31, // "v2"
520  S_EXPLICIT = 32, // "explicit"
521  S_ACCPAIRS = 33, // "Acceptance-Pairs:"
522  S_ACCSIG = 34, // "Acc-Sig:"
523  S_ENDOFHEADER = 35, // "---"
524  S_36_ = 36, // '|'
525  S_37_ = 37, // '&'
526  S_38_ = 38, // '!'
527  S_NEVER = 39, // "never"
528  S_SKIP = 40, // "skip"
529  S_IF = 41, // "if"
530  S_FI = 42, // "fi"
531  S_DO = 43, // "do"
532  S_OD = 44, // "od"
533  S_ARROW = 45, // "->"
534  S_GOTO = 46, // "goto"
535  S_FALSE = 47, // "false"
536  S_ATOMIC = 48, // "atomic"
537  S_ASSERT = 49, // "assert"
538  S_FORMULA = 50, // "boolean formula"
539  S_PGAME = 51, // "start of PGSolver game"
540  S_ENDPGAME = 52, // "end of PGSolver game"
541  S_ENDAUT = 53, // "-1"
542  S_LBTT = 54, // "LBTT header"
543  S_INT_S = 55, // "state acceptance"
544  S_LBTT_EMPTY = 56, // "acceptance sets for empty automaton"
545  S_ACC = 57, // "acceptance set"
546  S_STATE_NUM = 58, // "state number"
547  S_DEST_NUM = 59, // "destination number"
548  S_60_t_ = 60, // 't'
549  S_61_f_ = 61, // 'f'
550  S_62_ = 62, // '('
551  S_63_ = 63, // ')'
552  S_64_ = 64, // ']'
553  S_65_ = 65, // '{'
554  S_66_ = 66, // '}'
555  S_67_ = 67, // '+'
556  S_68_ = 68, // '-'
557  S_69_ = 69, // ';'
558  S_70_ = 70, // ','
559  S_71_ = 71, // ':'
560  S_YYACCEPT = 72, // $accept
561  S_aut = 73, // aut
562  S_74_1 = 74, // $@1
563  S_75_aut_1 = 75, // aut-1
564  S_hoa = 76, // hoa
565  S_string_opt = 77, // string_opt
566  S_BOOLEAN = 78, // BOOLEAN
567  S_header = 79, // header
568  S_version = 80, // version
569  S_81_format_version = 81, // format-version
570  S_82_2 = 82, // $@2
571  S_83_controllable_aps = 83, // controllable-aps
572  S_aps = 84, // aps
573  S_85_3 = 85, // $@3
574  S_86_header_items = 86, // header-items
575  S_87_header_item = 87, // header-item
576  S_88_4 = 88, // $@4
577  S_89_5 = 89, // $@5
578  S_90_6 = 90, // $@6
579  S_91_7 = 91, // $@7
580  S_92_8 = 92, // $@8
581  S_93_ap_names = 93, // ap-names
582  S_94_ap_name = 94, // ap-name
583  S_95_acc_spec = 95, // acc-spec
584  S_properties = 96, // properties
585  S_97_highlight_edges = 97, // highlight-edges
586  S_98_highlight_states = 98, // highlight-states
587  S_99_state_player = 99, // state-player
588  S_100_header_spec = 100, // header-spec
589  S_101_state_conj_2 = 101, // state-conj-2
590  S_102_init_state_conj_2 = 102, // init-state-conj-2
591  S_103_label_expr = 103, // label-expr
592  S_104_acc_set = 104, // acc-set
593  S_105_acceptance_cond = 105, // acceptance-cond
594  S_body = 106, // body
595  S_107_state_num = 107, // state-num
596  S_108_checked_state_num = 108, // checked-state-num
597  S_states = 109, // states
598  S_state = 110, // state
599  S_111_state_name = 111, // state-name
600  S_label = 112, // label
601  S_113_state_label_opt = 113, // state-label_opt
602  S_114_trans_label = 114, // trans-label
603  S_115_acc_sig = 115, // acc-sig
604  S_116_acc_sets = 116, // acc-sets
605  S_117_state_acc_opt = 117, // state-acc_opt
606  S_118_trans_acc_opt = 118, // trans-acc_opt
607  S_119_labeled_edges = 119, // labeled-edges
608  S_120_some_labeled_edges = 120, // some-labeled-edges
609  S_121_incorrectly_unlabeled_edge = 121, // incorrectly-unlabeled-edge
610  S_122_labeled_edge = 122, // labeled-edge
611  S_123_state_conj_checked = 123, // state-conj-checked
612  S_124_unlabeled_edges = 124, // unlabeled-edges
613  S_125_unlabeled_edge = 125, // unlabeled-edge
614  S_126_incorrectly_labeled_edge = 126, // incorrectly-labeled-edge
615  S_dstar = 127, // dstar
616  S_dstar_type = 128, // dstar_type
617  S_dstar_header = 129, // dstar_header
618  S_dstar_sizes = 130, // dstar_sizes
619  S_dstar_state_id = 131, // dstar_state_id
620  S_sign = 132, // sign
621  S_dstar_accsigs = 133, // dstar_accsigs
622  S_dstar_state_accsig = 134, // dstar_state_accsig
623  S_dstar_transitions = 135, // dstar_transitions
624  S_dstar_states = 136, // dstar_states
625  S_pgamestart = 137, // pgamestart
626  S_pgame = 138, // pgame
627  S_pgame_nodes = 139, // pgame_nodes
628  S_pgame_succs = 140, // pgame_succs
629  S_pgame_node = 141, // pgame_node
630  S_never = 142, // never
631  S_143_9 = 143, // $@9
632  S_144_nc_states = 144, // nc-states
633  S_145_nc_one_ident = 145, // nc-one-ident
634  S_146_nc_ident_list = 146, // nc-ident-list
635  S_147_nc_transition_block = 147, // nc-transition-block
636  S_148_nc_state = 148, // nc-state
637  S_149_nc_transitions = 149, // nc-transitions
638  S_150_nc_formula_or_ident = 150, // nc-formula-or-ident
639  S_151_nc_formula = 151, // nc-formula
640  S_152_nc_opt_dest = 152, // nc-opt-dest
641  S_153_nc_src_dest = 153, // nc-src-dest
642  S_154_nc_transition = 154, // nc-transition
643  S_lbtt = 155, // lbtt
644  S_156_lbtt_header_states = 156, // lbtt-header-states
645  S_157_lbtt_header = 157, // lbtt-header
646  S_158_lbtt_body = 158, // lbtt-body
647  S_159_lbtt_states = 159, // lbtt-states
648  S_160_lbtt_state = 160, // lbtt-state
649  S_161_lbtt_acc = 161, // lbtt-acc
650  S_162_lbtt_guard = 162, // lbtt-guard
651  S_163_lbtt_transitions = 163 // lbtt-transitions
652  };
653  };
654 
657 
659  static const symbol_kind_type YYNTOKENS = symbol_kind::YYNTOKENS;
660 
667  template <typename Base>
668  struct basic_symbol : Base
669  {
671  typedef Base super_type;
672 
675  : value ()
676  , location ()
677  {}
678 
679 #if 201103L <= YY_CPLUSPLUS
681  basic_symbol (basic_symbol&& that)
682  : Base (std::move (that))
683  , value (std::move (that.value))
684  , location (std::move (that.location))
685  {}
686 #endif
687 
689  basic_symbol (const basic_symbol& that);
691  basic_symbol (typename Base::kind_type t,
692  YY_MOVE_REF (location_type) l);
693 
695  basic_symbol (typename Base::kind_type t,
696  YY_RVREF (semantic_type) v,
697  YY_RVREF (location_type) l);
698 
701  {
702  clear ();
703  }
704 
706  void clear () YY_NOEXCEPT
707  {
708  Base::clear ();
709  }
710 
712  std::string name () const YY_NOEXCEPT
713  {
714  return parser::symbol_name (this->kind ());
715  }
716 
718  symbol_kind_type type_get () const YY_NOEXCEPT;
719 
721  bool empty () const YY_NOEXCEPT;
722 
724  void move (basic_symbol& s);
725 
728 
730  location_type location;
731 
732  private:
733 #if YY_CPLUSPLUS < 201103L
735  basic_symbol& operator= (const basic_symbol& that);
736 #endif
737  };
738 
740  struct by_kind
741  {
744 
745 #if 201103L <= YY_CPLUSPLUS
747  by_kind (by_kind&& that);
748 #endif
749 
751  by_kind (const by_kind& that);
752 
754  typedef token_kind_type kind_type;
755 
757  by_kind (kind_type t);
758 
760  void clear () YY_NOEXCEPT;
761 
763  void move (by_kind& that);
764 
767  symbol_kind_type kind () const YY_NOEXCEPT;
768 
770  symbol_kind_type type_get () const YY_NOEXCEPT;
771 
775  };
776 
778  typedef by_kind by_type;
779 
782  {};
783 
785  parser (void* scanner_yyarg, result_& res_yyarg, spot::location initial_loc_yyarg);
786  virtual ~parser ();
787 
788 #if 201103L <= YY_CPLUSPLUS
790  parser (const parser&) = delete;
792  parser& operator= (const parser&) = delete;
793 #endif
794 
797  int operator() ();
798 
801  virtual int parse ();
802 
803 #if HOAYYDEBUG
805  std::ostream& debug_stream () const YY_ATTRIBUTE_PURE;
807  void set_debug_stream (std::ostream &);
808 
810  typedef int debug_level_type;
812  debug_level_type debug_level () const YY_ATTRIBUTE_PURE;
814  void set_debug_level (debug_level_type l);
815 #endif
816 
820  virtual void error (const location_type& loc, const std::string& msg);
821 
823  void error (const syntax_error& err);
824 
827  static std::string symbol_name (symbol_kind_type yysymbol);
828 
829 
830 
831  class context
832  {
833  public:
834  context (const parser& yyparser, const symbol_type& yyla);
835  const symbol_type& lookahead () const YY_NOEXCEPT { return yyla_; }
836  symbol_kind_type token () const YY_NOEXCEPT { return yyla_.kind (); }
837  const location_type& location () const YY_NOEXCEPT { return yyla_.location; }
838 
842  int expected_tokens (symbol_kind_type yyarg[], int yyargn) const;
843 
844  private:
845  const parser& yyparser_;
846  const symbol_type& yyla_;
847  };
848 
849  private:
850 #if YY_CPLUSPLUS < 201103L
852  parser (const parser&);
854  parser& operator= (const parser&);
855 #endif
856 
857 
859  typedef short state_type;
860 
862  int yy_syntax_error_arguments_ (const context& yyctx,
863  symbol_kind_type yyarg[], int yyargn) const;
864 
867  virtual std::string yysyntax_error_ (const context& yyctx) const;
871  static state_type yy_lr_goto_state_ (state_type yystate, int yysym);
872 
875  static bool yy_pact_value_is_default_ (int yyvalue);
876 
879  static bool yy_table_value_is_error_ (int yyvalue);
880 
881  static const short yypact_ninf_;
882  static const short yytable_ninf_;
883 
887  static symbol_kind_type yytranslate_ (int t);
888 
890  static std::string yytnamerr_ (const char *yystr);
891 
893  static const char* const yytname_[];
894 
895 
896  // Tables.
897  // YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
898  // STATE-NUM.
899  static const short yypact_[];
900 
901  // YYDEFACT[STATE-NUM] -- Default reduction number in state STATE-NUM.
902  // Performed when YYTABLE does not specify something else to do. Zero
903  // means the default is an error.
904  static const unsigned char yydefact_[];
905 
906  // YYPGOTO[NTERM-NUM].
907  static const short yypgoto_[];
908 
909  // YYDEFGOTO[NTERM-NUM].
910  static const short yydefgoto_[];
911 
912  // YYTABLE[YYPACT[STATE-NUM]] -- What to do in state STATE-NUM. If
913  // positive, shift that token. If negative, reduce the rule whose
914  // number is the opposite. If YYTABLE_NINF, syntax error.
915  static const short yytable_[];
916 
917  static const short yycheck_[];
918 
919  // YYSTOS[STATE-NUM] -- The (internal number of the) accessing
920  // symbol of state STATE-NUM.
921  static const unsigned char yystos_[];
922 
923  // YYR1[YYN] -- Symbol number of symbol that rule YYN derives.
924  static const unsigned char yyr1_[];
925 
926  // YYR2[YYN] -- Number of symbols on the right hand side of rule YYN.
927  static const signed char yyr2_[];
928 
929 
930 #if HOAYYDEBUG
931  // YYRLINE[YYN] -- Source line where rule number YYN was defined.
932  static const short yyrline_[];
934  virtual void yy_reduce_print_ (int r) const;
936  virtual void yy_stack_print_ () const;
937 
939  int yydebug_;
941  std::ostream* yycdebug_;
942 
946  template <typename Base>
947  void yy_print_ (std::ostream& yyo, const basic_symbol<Base>& yysym) const;
948 #endif
949 
954  template <typename Base>
955  void yy_destroy_ (const char* yymsg, basic_symbol<Base>& yysym) const;
956 
957  private:
959  struct by_state
960  {
962  by_state () YY_NOEXCEPT;
963 
965  typedef state_type kind_type;
966 
968  by_state (kind_type s) YY_NOEXCEPT;
969 
971  by_state (const by_state& that) YY_NOEXCEPT;
972 
974  void clear () YY_NOEXCEPT;
975 
977  void move (by_state& that);
978 
981  symbol_kind_type kind () const YY_NOEXCEPT;
982 
985  enum { empty_state = 0 };
986 
989  state_type state;
990  };
991 
993  struct stack_symbol_type : basic_symbol<by_state>
994  {
996  typedef basic_symbol<by_state> super_type;
998  stack_symbol_type ();
1000  stack_symbol_type (YY_RVREF (stack_symbol_type) that);
1002  stack_symbol_type (state_type s, YY_MOVE_REF (symbol_type) sym);
1003 #if YY_CPLUSPLUS < 201103L
1006  stack_symbol_type& operator= (stack_symbol_type& that);
1007 
1010  stack_symbol_type& operator= (const stack_symbol_type& that);
1011 #endif
1012  };
1013 
1015  template <typename T, typename S = std::vector<T> >
1016  class stack
1017  {
1018  public:
1019  // Hide our reversed order.
1020  typedef typename S::iterator iterator;
1021  typedef typename S::const_iterator const_iterator;
1022  typedef typename S::size_type size_type;
1023  typedef typename std::ptrdiff_t index_type;
1024 
1025  stack (size_type n = 200)
1026  : seq_ (n)
1027  {}
1028 
1029 #if 201103L <= YY_CPLUSPLUS
1031  stack (const stack&) = delete;
1033  stack& operator= (const stack&) = delete;
1034 #endif
1035 
1039  const T&
1040  operator[] (index_type i) const
1041  {
1042  return seq_[size_type (size () - 1 - i)];
1043  }
1044 
1048  T&
1049  operator[] (index_type i)
1050  {
1051  return seq_[size_type (size () - 1 - i)];
1052  }
1053 
1057  void
1058  push (YY_MOVE_REF (T) t)
1059  {
1060  seq_.push_back (T ());
1061  operator[] (0).move (t);
1062  }
1063 
1065  void
1066  pop (std::ptrdiff_t n = 1) YY_NOEXCEPT
1067  {
1068  for (; 0 < n; --n)
1069  seq_.pop_back ();
1070  }
1071 
1073  void
1074  clear () YY_NOEXCEPT
1075  {
1076  seq_.clear ();
1077  }
1078 
1080  index_type
1081  size () const YY_NOEXCEPT
1082  {
1083  return index_type (seq_.size ());
1084  }
1085 
1087  const_iterator
1088  begin () const YY_NOEXCEPT
1089  {
1090  return seq_.begin ();
1091  }
1092 
1094  const_iterator
1095  end () const YY_NOEXCEPT
1096  {
1097  return seq_.end ();
1098  }
1099 
1101  class slice
1102  {
1103  public:
1104  slice (const stack& stack, index_type range)
1105  : stack_ (stack)
1106  , range_ (range)
1107  {}
1108 
1109  const T&
1110  operator[] (index_type i) const
1111  {
1112  return stack_[range_ - i];
1113  }
1114 
1115  private:
1116  const stack& stack_;
1117  index_type range_;
1118  };
1119 
1120  private:
1121 #if YY_CPLUSPLUS < 201103L
1123  stack (const stack&);
1125  stack& operator= (const stack&);
1126 #endif
1128  S seq_;
1129  };
1130 
1131 
1133  typedef stack<stack_symbol_type> stack_type;
1134 
1136  stack_type yystack_;
1137 
1143  void yypush_ (const char* m, YY_MOVE_REF (stack_symbol_type) sym);
1144 
1151  void yypush_ (const char* m, state_type s, YY_MOVE_REF (symbol_type) sym);
1152 
1154  void yypop_ (int n = 1);
1155 
1157  enum
1158  {
1159  yylast_ = 271,
1160  yynnts_ = 92,
1161  yyfinal_ = 29
1162  };
1163 
1164 
1165  // User arguments.
1166  void* scanner;
1167  result_& res;
1168  spot::location initial_loc;
1169 
1170  };
1171 
1172 
1173 } // hoayy
1174 #line 1175 "parseaut.hh"
1175 
1176 
1177 
1178 
1179 #endif // !YY_HOAYY_PARSEAUT_HH_INCLUDED
Definition: parseaut.hh:832
int expected_tokens(symbol_kind_type yyarg[], int yyargn) const
Present a slice of the top of a stack.
Definition: parseaut.hh:1102
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:479
symbol_kind::symbol_kind_type symbol_kind_type
(Internal) symbol kind.
Definition: parseaut.hh:656
std::ostream & debug_stream() const
The current debugging stream.
token::yytokentype token_kind_type
Token kind, as returned by yylex.
Definition: parseaut.hh:476
spot::location location_type
Symbol locations.
Definition: parseaut.hh:388
virtual int parse()
static std::string symbol_name(symbol_kind_type yysymbol)
int debug_level_type
Type for debugging levels.
Definition: parseaut.hh:810
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:669
Base super_type
Alias to Base.
Definition: parseaut.hh:671
basic_symbol()
Default constructor.
Definition: parseaut.hh:674
symbol_kind_type type_get() const
Backward compatibility (Bison 3.6).
void clear()
Destroy contents, and record that is empty.
Definition: parseaut.hh:706
basic_symbol(const basic_symbol &that)
Copy constructor.
basic_symbol(typename Base::kind_type t, location_type &l)
Constructor for valueless symbols.
basic_symbol(typename Base::kind_type t, const semantic_type &v, const location_type &l)
Constructor for symbols with semantic value.
std::string name() const
The user-facing name of this symbol.
Definition: parseaut.hh:712
~basic_symbol()
Destroy the symbol.
Definition: parseaut.hh:700
Type access provider for token (enum) based symbols.
Definition: parseaut.hh:741
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:754
Symbol kinds.
Definition: parseaut.hh:483
symbol_kind_type
Definition: parseaut.hh:485
"External" symbols: returned by the scanner.
Definition: parseaut.hh:782
Syntax errors thrown from user actions.
Definition: parseaut.hh:392
Token kinds.
Definition: parseaut.hh:410
token_kind_type yytokentype
Backward compatibility alias (Bison 3.6).
Definition: parseaut.hh:472
Definition: parseaut.hh:142
Definition: parseaut.hh:102
Definition: parseaut.hh:100
An acceptance formula.
Definition: acc.hh:479
An acceptance mark.
Definition: acc.hh:85
Definition: public.hh:100
Symbol semantic values.
Definition: parseaut.hh:369

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