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

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.4