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

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