spot  2.10.3.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  struct prop_info
140  {
141  spot::location loc;
142  bool val;
143  operator bool() const
144  {
145  return val;
146  };
147  };
148  std::unordered_map<std::string, prop_info> props;
149  spot::location states_loc;
150  spot::location ap_loc;
151  spot::location state_label_loc;
152  spot::location accset_loc;
153  spot::acc_cond::mark_t acc_state;
154  spot::acc_cond::mark_t neg_acc_sets = {};
155  spot::acc_cond::mark_t pos_acc_sets = {};
156  int plus;
157  int minus;
158  std::vector<std::string>* state_names = nullptr;
159  std::map<unsigned, unsigned>* highlight_edges = nullptr;
160  std::map<unsigned, unsigned>* highlight_states = nullptr;
161  std::map<unsigned, unsigned> states_map;
162  std::vector<bool>* state_player = nullptr;
163  spot::location state_player_loc;
164  std::set<int> ap_set;
165  unsigned cur_state;
166  int states = -1;
167  int ap_count = -1;
168  int accset = -1;
169  bdd state_label;
170  bdd cur_label;
171  bool has_state_label = false;
172  bool ignore_more_ap = false; // Set to true after the first "AP:"
173  // line has been read.
174  bool ignore_acc = false; // Set to true in case of missing
175  // Acceptance: lines.
176  bool ignore_acc_silent = false;
177  bool ignore_more_acc = false; // Set to true after the first
178  // "Acceptance:" line has been read.
179 
180  label_style_t label_style = Mixed_Labels;
181  acc_style_t acc_style = Mixed_Acc;
182 
183  bool accept_all_needed = false;
184  bool accept_all_seen = false;
185  bool aliased_states = false;
186 
187  spot::trival universal = spot::trival::maybe();
188  spot::trival existential = spot::trival::maybe();
189  spot::trival complete = spot::trival::maybe();
190  bool trans_acc_seen = false;
191 
192  std::map<std::string, spot::location> labels;
193 
194  prop_info prop_is_true(const std::string& p)
195  {
196  auto i = props.find(p);
197  if (i == props.end())
198  return prop_info{spot::location(), false};
199  return i->second;
200  }
201 
202  prop_info prop_is_false(const std::string& p)
203  {
204  auto i = props.find(p);
205  if (i == props.end())
206  return prop_info{spot::location(), false};
207  return prop_info{i->second.loc, !i->second.val};
208  }
209 
210  ~result_()
211  {
212  delete namer;
213  delete acc_mapper;
214  }
215  };
216  }
217 
218 #line 219 "parseaut.hh"
219 
220 
221 # include <cstdlib> // std::abort
222 # include <iostream>
223 # include <stdexcept>
224 # include <string>
225 # include <vector>
226 
227 #if defined __cplusplus
228 # define YY_CPLUSPLUS __cplusplus
229 #else
230 # define YY_CPLUSPLUS 199711L
231 #endif
232 
233 // Support move semantics when possible.
234 #if 201103L <= YY_CPLUSPLUS
235 # define YY_MOVE std::move
236 # define YY_MOVE_OR_COPY move
237 # define YY_MOVE_REF(Type) Type&&
238 # define YY_RVREF(Type) Type&&
239 # define YY_COPY(Type) Type
240 #else
241 # define YY_MOVE
242 # define YY_MOVE_OR_COPY copy
243 # define YY_MOVE_REF(Type) Type&
244 # define YY_RVREF(Type) const Type&
245 # define YY_COPY(Type) const Type&
246 #endif
247 
248 // Support noexcept when possible.
249 #if 201103L <= YY_CPLUSPLUS
250 # define YY_NOEXCEPT noexcept
251 # define YY_NOTHROW
252 #else
253 # define YY_NOEXCEPT
254 # define YY_NOTHROW throw ()
255 #endif
256 
257 // Support constexpr when possible.
258 #if 201703 <= YY_CPLUSPLUS
259 # define YY_CONSTEXPR constexpr
260 #else
261 # define YY_CONSTEXPR
262 #endif
263 
264 
265 
266 #ifndef YY_ATTRIBUTE_PURE
267 # if defined __GNUC__ && 2 < __GNUC__ + (96 <= __GNUC_MINOR__)
268 # define YY_ATTRIBUTE_PURE __attribute__ ((__pure__))
269 # else
270 # define YY_ATTRIBUTE_PURE
271 # endif
272 #endif
273 
274 #ifndef YY_ATTRIBUTE_UNUSED
275 # if defined __GNUC__ && 2 < __GNUC__ + (7 <= __GNUC_MINOR__)
276 # define YY_ATTRIBUTE_UNUSED __attribute__ ((__unused__))
277 # else
278 # define YY_ATTRIBUTE_UNUSED
279 # endif
280 #endif
281 
282 /* Suppress unused-variable warnings by "using" E. */
283 #if ! defined lint || defined __GNUC__
284 # define YY_USE(E) ((void) (E))
285 #else
286 # define YY_USE(E) /* empty */
287 #endif
288 
289 /* Suppress an incorrect diagnostic about yylval being uninitialized. */
290 #if defined __GNUC__ && ! defined __ICC && 406 <= __GNUC__ * 100 + __GNUC_MINOR__
291 # if __GNUC__ * 100 + __GNUC_MINOR__ < 407
292 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
293  _Pragma ("GCC diagnostic push") \
294  _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"")
295 # else
296 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \
297  _Pragma ("GCC diagnostic push") \
298  _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"") \
299  _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"")
300 # endif
301 # define YY_IGNORE_MAYBE_UNINITIALIZED_END \
302  _Pragma ("GCC diagnostic pop")
303 #else
304 # define YY_INITIAL_VALUE(Value) Value
305 #endif
306 #ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
307 # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN
308 # define YY_IGNORE_MAYBE_UNINITIALIZED_END
309 #endif
310 #ifndef YY_INITIAL_VALUE
311 # define YY_INITIAL_VALUE(Value) /* Nothing. */
312 #endif
313 
314 #if defined __cplusplus && defined __GNUC__ && ! defined __ICC && 6 <= __GNUC__
315 # define YY_IGNORE_USELESS_CAST_BEGIN \
316  _Pragma ("GCC diagnostic push") \
317  _Pragma ("GCC diagnostic ignored \"-Wuseless-cast\"")
318 # define YY_IGNORE_USELESS_CAST_END \
319  _Pragma ("GCC diagnostic pop")
320 #endif
321 #ifndef YY_IGNORE_USELESS_CAST_BEGIN
322 # define YY_IGNORE_USELESS_CAST_BEGIN
323 # define YY_IGNORE_USELESS_CAST_END
324 #endif
325 
326 # ifndef YY_CAST
327 # ifdef __cplusplus
328 # define YY_CAST(Type, Val) static_cast<Type> (Val)
329 # define YY_REINTERPRET_CAST(Type, Val) reinterpret_cast<Type> (Val)
330 # else
331 # define YY_CAST(Type, Val) ((Type) (Val))
332 # define YY_REINTERPRET_CAST(Type, Val) ((Type) (Val))
333 # endif
334 # endif
335 # ifndef YY_NULLPTR
336 # if defined __cplusplus
337 # if 201103L <= __cplusplus
338 # define YY_NULLPTR nullptr
339 # else
340 # define YY_NULLPTR 0
341 # endif
342 # else
343 # define YY_NULLPTR ((void*)0)
344 # endif
345 # endif
346 
347 /* Debug traces. */
348 #ifndef HOAYYDEBUG
349 # if defined YYDEBUG
350 #if YYDEBUG
351 # define HOAYYDEBUG 1
352 # else
353 # define HOAYYDEBUG 0
354 # endif
355 # else /* ! defined YYDEBUG */
356 # define HOAYYDEBUG 1
357 # endif /* ! defined YYDEBUG */
358 #endif /* ! defined HOAYYDEBUG */
359 
360 namespace hoayy {
361 #line 362 "parseaut.hh"
362 
363 
364 
365 
367  class parser
368  {
369  public:
370 #ifdef HOAYYSTYPE
371 # ifdef __GNUC__
372 # pragma GCC message "bison: do not #define HOAYYSTYPE in C++, use %define api.value.type"
373 # endif
374  typedef HOAYYSTYPE value_type;
375 #else
378  {
379 #line 209 "parseaut.yy"
380 
381  std::string* str;
382  unsigned int num;
383  int b;
385  pair* p;
386  std::list<pair>* list;
388  std::vector<unsigned>* states;
389 
390 #line 391 "parseaut.hh"
391 
392  };
393 #endif
396 
398  typedef spot::location location_type;
399 
401  struct syntax_error : std::runtime_error
402  {
403  syntax_error (const location_type& l, const std::string& m)
404  : std::runtime_error (m)
405  , location (l)
406  {}
407 
408  syntax_error (const syntax_error& s)
409  : std::runtime_error (s.what ())
410  , location (s.location)
411  {}
412 
413  ~syntax_error () YY_NOEXCEPT YY_NOTHROW;
414 
415  location_type location;
416  };
417 
419  struct token
420  {
421  enum token_kind_type
422  {
423  HOAYYEMPTY = -2,
424  ENDOFFILE = 0, // "end of file"
425  HOAYYerror = 256, // error
426  HOAYYUNDEF = 257, // "invalid token"
427  HOA = 258, // "HOA:"
428  STATES = 259, // "States:"
429  START = 260, // "Start:"
430  AP = 261, // "AP:"
431  ALIAS = 262, // "Alias:"
432  ACCEPTANCE = 263, // "Acceptance:"
433  ACCNAME = 264, // "acc-name:"
434  CONTROLLABLE_AP = 265, // "controllable-AP:"
435  TOOL = 266, // "tool:"
436  NAME = 267, // "name:"
437  PROPERTIES = 268, // "properties:"
438  BODY = 269, // "--BODY--"
439  END = 270, // "--END--"
440  STATE = 271, // "State:"
441  SPOT_HIGHLIGHT_EDGES = 272, // "spot.highlight.edges:"
442  SPOT_HIGHLIGHT_STATES = 273, // "spot.highlight.states:"
443  SPOT_STATE_PLAYER = 274, // "spot.state-player:"
444  IDENTIFIER = 275, // "identifier"
445  HEADERNAME = 276, // "header name"
446  ANAME = 277, // "alias name"
447  STRING = 278, // "string"
448  INT = 279, // "integer"
449  DRA = 280, // "DRA"
450  DSA = 281, // "DSA"
451  V2 = 282, // "v2"
452  EXPLICIT = 283, // "explicit"
453  ACCPAIRS = 284, // "Acceptance-Pairs:"
454  ACCSIG = 285, // "Acc-Sig:"
455  ENDOFHEADER = 286, // "---"
456  LINEDIRECTIVE = 287, // "#line"
457  BDD = 288, // BDD
458  NEVER = 289, // "never"
459  SKIP = 290, // "skip"
460  IF = 291, // "if"
461  FI = 292, // "fi"
462  DO = 293, // "do"
463  OD = 294, // "od"
464  ARROW = 295, // "->"
465  GOTO = 296, // "goto"
466  FALSE = 297, // "false"
467  ATOMIC = 298, // "atomic"
468  ASSERT = 299, // "assert"
469  FORMULA = 300, // "boolean formula"
470  ENDAUT = 301, // "-1"
471  ENDDSTAR = 302, // "end of DSTAR automaton"
472  LBTT = 303, // "LBTT header"
473  INT_S = 304, // "state acceptance"
474  LBTT_EMPTY = 305, // "acceptance sets for empty automaton"
475  ACC = 306, // "acceptance set"
476  STATE_NUM = 307, // "state number"
477  DEST_NUM = 308 // "destination number"
478  };
480  typedef token_kind_type yytokentype;
481  };
482 
484  typedef token::token_kind_type token_kind_type;
485 
487  typedef token_kind_type token_type;
488 
490  struct symbol_kind
491  {
493  {
494  YYNTOKENS = 69,
495  S_YYEMPTY = -2,
496  S_YYEOF = 0, // "end of file"
497  S_YYerror = 1, // error
498  S_YYUNDEF = 2, // "invalid token"
499  S_HOA = 3, // "HOA:"
500  S_STATES = 4, // "States:"
501  S_START = 5, // "Start:"
502  S_AP = 6, // "AP:"
503  S_ALIAS = 7, // "Alias:"
504  S_ACCEPTANCE = 8, // "Acceptance:"
505  S_ACCNAME = 9, // "acc-name:"
506  S_CONTROLLABLE_AP = 10, // "controllable-AP:"
507  S_TOOL = 11, // "tool:"
508  S_NAME = 12, // "name:"
509  S_PROPERTIES = 13, // "properties:"
510  S_BODY = 14, // "--BODY--"
511  S_END = 15, // "--END--"
512  S_STATE = 16, // "State:"
513  S_SPOT_HIGHLIGHT_EDGES = 17, // "spot.highlight.edges:"
514  S_SPOT_HIGHLIGHT_STATES = 18, // "spot.highlight.states:"
515  S_SPOT_STATE_PLAYER = 19, // "spot.state-player:"
516  S_IDENTIFIER = 20, // "identifier"
517  S_HEADERNAME = 21, // "header name"
518  S_ANAME = 22, // "alias name"
519  S_STRING = 23, // "string"
520  S_INT = 24, // "integer"
521  S_25_ = 25, // '['
522  S_DRA = 26, // "DRA"
523  S_DSA = 27, // "DSA"
524  S_V2 = 28, // "v2"
525  S_EXPLICIT = 29, // "explicit"
526  S_ACCPAIRS = 30, // "Acceptance-Pairs:"
527  S_ACCSIG = 31, // "Acc-Sig:"
528  S_ENDOFHEADER = 32, // "---"
529  S_LINEDIRECTIVE = 33, // "#line"
530  S_BDD = 34, // BDD
531  S_35_ = 35, // '|'
532  S_36_ = 36, // '&'
533  S_37_ = 37, // '!'
534  S_NEVER = 38, // "never"
535  S_SKIP = 39, // "skip"
536  S_IF = 40, // "if"
537  S_FI = 41, // "fi"
538  S_DO = 42, // "do"
539  S_OD = 43, // "od"
540  S_ARROW = 44, // "->"
541  S_GOTO = 45, // "goto"
542  S_FALSE = 46, // "false"
543  S_ATOMIC = 47, // "atomic"
544  S_ASSERT = 48, // "assert"
545  S_FORMULA = 49, // "boolean formula"
546  S_ENDAUT = 50, // "-1"
547  S_ENDDSTAR = 51, // "end of DSTAR automaton"
548  S_LBTT = 52, // "LBTT header"
549  S_INT_S = 53, // "state acceptance"
550  S_LBTT_EMPTY = 54, // "acceptance sets for empty automaton"
551  S_ACC = 55, // "acceptance set"
552  S_STATE_NUM = 56, // "state number"
553  S_DEST_NUM = 57, // "destination number"
554  S_58_t_ = 58, // 't'
555  S_59_f_ = 59, // 'f'
556  S_60_ = 60, // '('
557  S_61_ = 61, // ')'
558  S_62_ = 62, // ']'
559  S_63_ = 63, // '{'
560  S_64_ = 64, // '}'
561  S_65_ = 65, // '+'
562  S_66_ = 66, // '-'
563  S_67_ = 67, // ';'
564  S_68_ = 68, // ':'
565  S_YYACCEPT = 69, // $accept
566  S_aut = 70, // aut
567  S_71_1 = 71, // $@1
568  S_72_aut_1 = 72, // aut-1
569  S_hoa = 73, // hoa
570  S_string_opt = 74, // string_opt
571  S_BOOLEAN = 75, // BOOLEAN
572  S_header = 76, // header
573  S_version = 77, // version
574  S_78_format_version = 78, // format-version
575  S_79_2 = 79, // $@2
576  S_80_controllable_aps = 80, // controllable-aps
577  S_aps = 81, // aps
578  S_82_3 = 82, // $@3
579  S_83_header_items = 83, // header-items
580  S_84_header_item = 84, // header-item
581  S_85_4 = 85, // $@4
582  S_86_5 = 86, // $@5
583  S_87_6 = 87, // $@6
584  S_88_7 = 88, // $@7
585  S_89_8 = 89, // $@8
586  S_90_ap_names = 90, // ap-names
587  S_91_ap_name = 91, // ap-name
588  S_92_acc_spec = 92, // acc-spec
589  S_properties = 93, // properties
590  S_94_highlight_edges = 94, // highlight-edges
591  S_95_highlight_states = 95, // highlight-states
592  S_96_state_player = 96, // state-player
593  S_97_header_spec = 97, // header-spec
594  S_98_state_conj_2 = 98, // state-conj-2
595  S_99_init_state_conj_2 = 99, // init-state-conj-2
596  S_100_label_expr = 100, // label-expr
597  S_101_acc_set = 101, // acc-set
598  S_102_acceptance_cond = 102, // acceptance-cond
599  S_body = 103, // body
600  S_104_state_num = 104, // state-num
601  S_105_checked_state_num = 105, // checked-state-num
602  S_states = 106, // states
603  S_state = 107, // state
604  S_108_state_name = 108, // state-name
605  S_label = 109, // label
606  S_110_state_label_opt = 110, // state-label_opt
607  S_111_trans_label = 111, // trans-label
608  S_112_acc_sig = 112, // acc-sig
609  S_113_acc_sets = 113, // acc-sets
610  S_114_state_acc_opt = 114, // state-acc_opt
611  S_115_trans_acc_opt = 115, // trans-acc_opt
612  S_116_labeled_edges = 116, // labeled-edges
613  S_117_some_labeled_edges = 117, // some-labeled-edges
614  S_118_incorrectly_unlabeled_edge = 118, // incorrectly-unlabeled-edge
615  S_119_labeled_edge = 119, // labeled-edge
616  S_120_state_conj_checked = 120, // state-conj-checked
617  S_121_unlabeled_edges = 121, // unlabeled-edges
618  S_122_unlabeled_edge = 122, // unlabeled-edge
619  S_123_incorrectly_labeled_edge = 123, // incorrectly-labeled-edge
620  S_dstar = 124, // dstar
621  S_dstar_type = 125, // dstar_type
622  S_dstar_header = 126, // dstar_header
623  S_dstar_sizes = 127, // dstar_sizes
624  S_dstar_state_id = 128, // dstar_state_id
625  S_sign = 129, // sign
626  S_dstar_accsigs = 130, // dstar_accsigs
627  S_dstar_state_accsig = 131, // dstar_state_accsig
628  S_dstar_transitions = 132, // dstar_transitions
629  S_dstar_states = 133, // dstar_states
630  S_never = 134, // never
631  S_135_9 = 135, // $@9
632  S_136_nc_states = 136, // nc-states
633  S_137_nc_one_ident = 137, // nc-one-ident
634  S_138_nc_ident_list = 138, // nc-ident-list
635  S_139_nc_transition_block = 139, // nc-transition-block
636  S_140_nc_state = 140, // nc-state
637  S_141_nc_transitions = 141, // nc-transitions
638  S_142_nc_formula_or_ident = 142, // nc-formula-or-ident
639  S_143_nc_formula = 143, // nc-formula
640  S_144_nc_opt_dest = 144, // nc-opt-dest
641  S_145_nc_src_dest = 145, // nc-src-dest
642  S_146_nc_transition = 146, // nc-transition
643  S_lbtt = 147, // lbtt
644  S_148_lbtt_header_states = 148, // lbtt-header-states
645  S_149_lbtt_header = 149, // lbtt-header
646  S_150_lbtt_body = 150, // lbtt-body
647  S_151_lbtt_states = 151, // lbtt-states
648  S_152_lbtt_state = 152, // lbtt-state
649  S_153_lbtt_acc = 153, // lbtt-acc
650  S_154_lbtt_guard = 154, // lbtt-guard
651  S_155_lbtt_transitions = 155 // 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 
674  basic_symbol () YY_NOEXCEPT
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 (value_type) v,
697  YY_RVREF (location_type) l);
698 
701  {
702  clear ();
703  }
704 
705 
706 
708  void clear () YY_NOEXCEPT
709  {
710  Base::clear ();
711  }
712 
714  std::string name () const YY_NOEXCEPT
715  {
716  return parser::symbol_name (this->kind ());
717  }
718 
720  symbol_kind_type type_get () const YY_NOEXCEPT;
721 
723  bool empty () const YY_NOEXCEPT;
724 
726  void move (basic_symbol& s);
727 
729  value_type value;
730 
732  location_type location;
733 
734  private:
735 #if YY_CPLUSPLUS < 201103L
737  basic_symbol& operator= (const basic_symbol& that);
738 #endif
739  };
740 
742  struct by_kind
743  {
745  typedef token_kind_type kind_type;
746 
748  by_kind () YY_NOEXCEPT;
749 
750 #if 201103L <= YY_CPLUSPLUS
752  by_kind (by_kind&& that) YY_NOEXCEPT;
753 #endif
754 
756  by_kind (const by_kind& that) YY_NOEXCEPT;
757 
759  by_kind (kind_type t) YY_NOEXCEPT;
760 
761 
762 
764  void clear () YY_NOEXCEPT;
765 
767  void move (by_kind& that);
768 
771  symbol_kind_type kind () const YY_NOEXCEPT;
772 
774  symbol_kind_type type_get () const YY_NOEXCEPT;
775 
779  };
780 
782  typedef by_kind by_type;
783 
786  {};
787 
789  parser (void* scanner_yyarg, result_& res_yyarg, spot::location initial_loc_yyarg);
790  virtual ~parser ();
791 
792 #if 201103L <= YY_CPLUSPLUS
794  parser (const parser&) = delete;
796  parser& operator= (const parser&) = delete;
797 #endif
798 
801  int operator() ();
802 
805  virtual int parse ();
806 
807 #if HOAYYDEBUG
809  std::ostream& debug_stream () const YY_ATTRIBUTE_PURE;
811  void set_debug_stream (std::ostream &);
812 
814  typedef int debug_level_type;
816  debug_level_type debug_level () const YY_ATTRIBUTE_PURE;
818  void set_debug_level (debug_level_type l);
819 #endif
820 
824  virtual void error (const location_type& loc, const std::string& msg);
825 
827  void error (const syntax_error& err);
828 
831  static std::string symbol_name (symbol_kind_type yysymbol);
832 
833 
834 
835  class context
836  {
837  public:
838  context (const parser& yyparser, const symbol_type& yyla);
839  const symbol_type& lookahead () const YY_NOEXCEPT { return yyla_; }
840  symbol_kind_type token () const YY_NOEXCEPT { return yyla_.kind (); }
841  const location_type& location () const YY_NOEXCEPT { return yyla_.location; }
842 
846  int expected_tokens (symbol_kind_type yyarg[], int yyargn) const;
847 
848  private:
849  const parser& yyparser_;
850  const symbol_type& yyla_;
851  };
852 
853  private:
854 #if YY_CPLUSPLUS < 201103L
856  parser (const parser&);
858  parser& operator= (const parser&);
859 #endif
860 
861 
863  typedef short state_type;
864 
866  int yy_syntax_error_arguments_ (const context& yyctx,
867  symbol_kind_type yyarg[], int yyargn) const;
868 
871  virtual std::string yysyntax_error_ (const context& yyctx) const;
875  static state_type yy_lr_goto_state_ (state_type yystate, int yysym);
876 
879  static bool yy_pact_value_is_default_ (int yyvalue) YY_NOEXCEPT;
880 
883  static bool yy_table_value_is_error_ (int yyvalue) YY_NOEXCEPT;
884 
885  static const short yypact_ninf_;
886  static const short yytable_ninf_;
887 
891  static symbol_kind_type yytranslate_ (int t) YY_NOEXCEPT;
892 
894  static std::string yytnamerr_ (const char *yystr);
895 
897  static const char* const yytname_[];
898 
899 
900  // Tables.
901  // YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
902  // STATE-NUM.
903  static const short yypact_[];
904 
905  // YYDEFACT[STATE-NUM] -- Default reduction number in state STATE-NUM.
906  // Performed when YYTABLE does not specify something else to do. Zero
907  // means the default is an error.
908  static const unsigned char yydefact_[];
909 
910  // YYPGOTO[NTERM-NUM].
911  static const short yypgoto_[];
912 
913  // YYDEFGOTO[NTERM-NUM].
914  static const short yydefgoto_[];
915 
916  // YYTABLE[YYPACT[STATE-NUM]] -- What to do in state STATE-NUM. If
917  // positive, shift that token. If negative, reduce the rule whose
918  // number is the opposite. If YYTABLE_NINF, syntax error.
919  static const short yytable_[];
920 
921  static const short yycheck_[];
922 
923  // YYSTOS[STATE-NUM] -- The symbol kind of the accessing symbol of
924  // state STATE-NUM.
925  static const unsigned char yystos_[];
926 
927  // YYR1[RULE-NUM] -- Symbol kind of the left-hand side of rule RULE-NUM.
928  static const unsigned char yyr1_[];
929 
930  // YYR2[RULE-NUM] -- Number of symbols on the right-hand side of rule RULE-NUM.
931  static const signed char yyr2_[];
932 
933 
934 #if HOAYYDEBUG
935  // YYRLINE[YYN] -- Source line where rule number YYN was defined.
936  static const short yyrline_[];
938  virtual void yy_reduce_print_ (int r) const;
940  virtual void yy_stack_print_ () const;
941 
943  int yydebug_;
945  std::ostream* yycdebug_;
946 
950  template <typename Base>
951  void yy_print_ (std::ostream& yyo, const basic_symbol<Base>& yysym) const;
952 #endif
953 
958  template <typename Base>
959  void yy_destroy_ (const char* yymsg, basic_symbol<Base>& yysym) const;
960 
961  private:
963  struct by_state
964  {
966  by_state () YY_NOEXCEPT;
967 
969  typedef state_type kind_type;
970 
972  by_state (kind_type s) YY_NOEXCEPT;
973 
975  by_state (const by_state& that) YY_NOEXCEPT;
976 
978  void clear () YY_NOEXCEPT;
979 
981  void move (by_state& that);
982 
985  symbol_kind_type kind () const YY_NOEXCEPT;
986 
989  enum { empty_state = 0 };
990 
993  state_type state;
994  };
995 
997  struct stack_symbol_type : basic_symbol<by_state>
998  {
1000  typedef basic_symbol<by_state> super_type;
1002  stack_symbol_type ();
1004  stack_symbol_type (YY_RVREF (stack_symbol_type) that);
1006  stack_symbol_type (state_type s, YY_MOVE_REF (symbol_type) sym);
1007 #if YY_CPLUSPLUS < 201103L
1010  stack_symbol_type& operator= (stack_symbol_type& that);
1011 
1014  stack_symbol_type& operator= (const stack_symbol_type& that);
1015 #endif
1016  };
1017 
1019  template <typename T, typename S = std::vector<T> >
1020  class stack
1021  {
1022  public:
1023  // Hide our reversed order.
1024  typedef typename S::iterator iterator;
1025  typedef typename S::const_iterator const_iterator;
1026  typedef typename S::size_type size_type;
1027  typedef typename std::ptrdiff_t index_type;
1028 
1029  stack (size_type n = 200) YY_NOEXCEPT
1030  : seq_ (n)
1031  {}
1032 
1033 #if 201103L <= YY_CPLUSPLUS
1035  stack (const stack&) = delete;
1037  stack& operator= (const stack&) = delete;
1038 #endif
1039 
1043  const T&
1044  operator[] (index_type i) const
1045  {
1046  return seq_[size_type (size () - 1 - i)];
1047  }
1048 
1052  T&
1053  operator[] (index_type i)
1054  {
1055  return seq_[size_type (size () - 1 - i)];
1056  }
1057 
1061  void
1062  push (YY_MOVE_REF (T) t)
1063  {
1064  seq_.push_back (T ());
1065  operator[] (0).move (t);
1066  }
1067 
1069  void
1070  pop (std::ptrdiff_t n = 1) YY_NOEXCEPT
1071  {
1072  for (; 0 < n; --n)
1073  seq_.pop_back ();
1074  }
1075 
1077  void
1078  clear () YY_NOEXCEPT
1079  {
1080  seq_.clear ();
1081  }
1082 
1084  index_type
1085  size () const YY_NOEXCEPT
1086  {
1087  return index_type (seq_.size ());
1088  }
1089 
1091  const_iterator
1092  begin () const YY_NOEXCEPT
1093  {
1094  return seq_.begin ();
1095  }
1096 
1098  const_iterator
1099  end () const YY_NOEXCEPT
1100  {
1101  return seq_.end ();
1102  }
1103 
1105  class slice
1106  {
1107  public:
1108  slice (const stack& stack, index_type range) YY_NOEXCEPT
1109  : stack_ (stack)
1110  , range_ (range)
1111  {}
1112 
1113  const T&
1114  operator[] (index_type i) const
1115  {
1116  return stack_[range_ - i];
1117  }
1118 
1119  private:
1120  const stack& stack_;
1121  index_type range_;
1122  };
1123 
1124  private:
1125 #if YY_CPLUSPLUS < 201103L
1127  stack (const stack&);
1129  stack& operator= (const stack&);
1130 #endif
1132  S seq_;
1133  };
1134 
1135 
1137  typedef stack<stack_symbol_type> stack_type;
1138 
1140  stack_type yystack_;
1141 
1147  void yypush_ (const char* m, YY_MOVE_REF (stack_symbol_type) sym);
1148 
1155  void yypush_ (const char* m, state_type s, YY_MOVE_REF (symbol_type) sym);
1156 
1158  void yypop_ (int n = 1) YY_NOEXCEPT;
1159 
1161  enum
1162  {
1163  yylast_ = 248,
1164  yynnts_ = 87,
1165  yyfinal_ = 26
1166  };
1167 
1168 
1169  // User arguments.
1170  void* scanner;
1171  result_& res;
1172  spot::location initial_loc;
1173 
1174  };
1175 
1176 
1177 } // hoayy
1178 #line 1179 "parseaut.hh"
1179 
1180 
1181 
1182 
1183 #endif // !YY_HOAYY_PARSEAUT_HH_INCLUDED
Definition: parseaut.hh:836
int expected_tokens(symbol_kind_type yyarg[], int yyargn) const
Present a slice of the top of a stack.
Definition: parseaut.hh:1106
A Bison parser.
Definition: parseaut.hh:368
void error(const syntax_error &err)
Report a syntax error.
token_kind_type token_type
Backward compatibility alias (Bison 3.6).
Definition: parseaut.hh:487
symbol_kind::symbol_kind_type symbol_kind_type
(Internal) symbol kind.
Definition: parseaut.hh:656
token::token_kind_type token_kind_type
Token kind, as returned by yylex.
Definition: parseaut.hh:484
std::ostream & debug_stream() const
The current debugging stream.
spot::location location_type
Symbol locations.
Definition: parseaut.hh:398
virtual int parse()
static std::string symbol_name(symbol_kind_type yysymbol)
int debug_level_type
Type for debugging levels.
Definition: parseaut.hh:814
value_type semantic_type
Backward compatibility (Bison 3.8).
Definition: parseaut.hh:395
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:708
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:714
~basic_symbol()
Destroy the symbol.
Definition: parseaut.hh:700
Type access provider for token (enum) based symbols.
Definition: parseaut.hh:743
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:745
Symbol kinds.
Definition: parseaut.hh:491
symbol_kind_type
Definition: parseaut.hh:493
"External" symbols: returned by the scanner.
Definition: parseaut.hh:786
Syntax errors thrown from user actions.
Definition: parseaut.hh:402
Token kinds.
Definition: parseaut.hh:420
token_kind_type yytokentype
Backward compatibility alias (Bison 3.6).
Definition: parseaut.hh:480
Definition: parseaut.hh:140
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:378

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